Add assertions to ensure valid literal values in semitone methods

Author: riccardodebenedictis

src/la_theory.cpp

@@ -225,7 +225,7 @@ namespace smt
                 if (ub(expr) <= c_right)
                     return; // the constraint is already satisfied..
                 else if (lb(expr) > c_right)
-                    net.add_clause({!p});
+                    return net.add_clause({!p}); // the constraint is conflicting..
 
                 // we add a slack variable to the tableau..
                 auto slack = new_real(std::move(expr));

src/semitone.cpp

@@ -102,10 +102,22 @@ namespace smt
         }
     }
 
-    void semitone::add_lt(const utils::lin &lhs, const utils::lin &rhs, const utils::lit &p) { la.new_lt(lhs, rhs, p, true); }
-    void semitone::add_le(const utils::lin &lhs, const utils::lin &rhs, const utils::lit &p) { la.new_lt(lhs, rhs, p); }
+    void semitone::add_lt(const utils::lin &lhs, const utils::lin &rhs, const utils::lit &p)
+    {
+        assert(value(p) != utils::False);
+        la.new_lt(lhs, rhs, p, true);
+    }
+    void semitone::add_le(const utils::lin &lhs, const utils::lin &rhs, const utils::lit &p)
+    {
+        assert(value(p) != utils::False);
+        la.new_lt(lhs, rhs, p);
+    }
 
-    void semitone::add_distance(utils::var from, utils::var to, const utils::rational &dist, const utils::lit &p) { dl.new_distance(from, to, dist, p); }
+    void semitone::add_distance(utils::var from, utils::var to, const utils::rational &dist, const utils::lit &p)
+    {
+        assert(value(p) != utils::False);
+        dl.new_distance(from, to, dist, p);
+    }
 
     void semitone::assume(const utils::lit &p)
     {