Add some clause names

src/math/polysat/constraint_manager.cpp

@@ -397,12 +397,12 @@ namespace polysat {
         //      b = 0  ==>  q = -1
         // TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
         //       Maybe we need something like an op_constraint for better propagation.
-        s.add_clause(eq(b * q + r - a), false);
-        s.add_clause(~umul_ovfl(b, q), false);
+        s.add_clause("[axiom] quot_rem 1", { eq(b * q + r - a) }, false);
+        s.add_clause("[axiom] quot_rem 2", { ~umul_ovfl(b, q)  }, false);
         // r <= b*q+r
         //  { apply equivalence:  p <= q  <=>  q-p <= -p-1 }
         // b*q <= -r-1
-        s.add_clause(ule(b*q, -r-1), false);
+        s.add_clause("[axiom] quot_rem 3", { ule(b*q, -r-1)    }, false);
 #if 0
         // b*q <= b*q+r
         //  { apply equivalence:  p <= q  <=>  q-p <= -p-1 }
@@ -411,8 +411,8 @@ namespace polysat {
 #endif
 
         auto c_eq = eq(b);
-        s.add_clause(c_eq, ult(r, b), false);
-        s.add_clause(~c_eq, eq(q + 1), false);
+        s.add_clause("[axiom] quot_rem 4", {  c_eq, ult(r, b)  }, false);
+        s.add_clause("[axiom] quot_rem 5", { ~c_eq, eq(q + 1)  }, false);
 
         return {std::move(q), std::move(r)};
     }

src/math/polysat/op_constraint.cpp

@@ -45,6 +45,7 @@ namespace polysat {
         default:
             break;
         }
+        VERIFY(r.is_var());
     }
 
     lbool op_constraint::eval() const {
@@ -342,12 +343,12 @@ namespace polysat {
                 rational const& q_val = qv.val();
                 if (q_val >= N)
                     // q >= N ==> r = 0
-                    return s.mk_clause(~shl, ~s.ule(N, q()), s.eq(r()), true);
+                    return s.mk_clause("shl forward 1", {~shl, ~s.ule(N, q()), s.eq(r())}, true);
                 if (pv.is_val()) {
                     SASSERT(q_val.is_unsigned());
                     // p = p_val & q = q_val ==> r = p_val * 2^q_val
                     rational const r_val = pv.val() * rational::power_of_two(q_val.get_unsigned());
-                    return s.mk_clause(~shl, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), r_val), true);
+                    return s.mk_clause("shl forward 2", {~shl, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), r_val)}, true);
                 }
             }
         }

src/math/polysat/op_constraint.h

@@ -27,21 +27,21 @@ namespace polysat {
     class op_constraint final : public constraint {
     public:
         enum class code {
-            /// r is the logical right shift of p by q
+            /// r is the logical right shift of p by q.
             lshr_op,
-            /// r is the arithmetic right shift of p by q
+            /// r is the arithmetic right shift of p by q.
             ashr_op,
-            /// r is the left shift of p by q
+            /// r is the left shift of p by q.
             shl_op,
-            /// r is the bit-wise 'and' of p and q
+            /// r is the bit-wise 'and' of p and q.
             and_op,
             /// r is the smallest multiplicative pseudo-inverse of p;
             /// by definition we set r == 0 when p == 0.
             /// Note that in general, there are 2^parity(p) many pseudo-inverses of p.
             inv_op,
-            // r is the quotient of dividing p by q 
+            // r is the quotient of unsigned division of p by q.
             udiv_op,
-            // r is the remainder of dividing p by q
+            // r is the remainder of unsigned division of p by q.
             urem_op,
         };
     protected:

src/math/polysat/solver.cpp

@@ -1395,12 +1395,20 @@ namespace polysat {
             enqueue_pwatch(lit2cnstr(lit).get());
     }
 
-    void solver::add_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
-        clause_ref clause = mk_clause(n, cs, is_redundant);
+    void solver::add_clause(char const* name, unsigned n, signed_constraint const* cs, bool is_redundant) {
+        clause_ref clause = mk_clause(name, n, cs, is_redundant);
         if (clause)
             add_clause(*clause);
     }
 
+    void solver::add_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant) {
+        add_clause(name, static_cast<unsigned>(cs.size()), std::data(cs), is_redundant);
+    }
+
+    void solver::add_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
+        add_clause("", n, cs, is_redundant);
+    }
+
     void solver::add_clause(std::initializer_list<signed_constraint> cs, bool is_redundant) {
         add_clause(static_cast<unsigned>(cs.size()), std::data(cs), is_redundant);
     }

src/math/polysat/solver.h

@@ -327,6 +327,8 @@ namespace polysat {
         void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant);
         void add_clause(std::initializer_list<signed_constraint> cs, bool is_redundant);
         void add_clause(unsigned n, signed_constraint const* cs, bool is_redundant);
+        void add_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant);
+        void add_clause(char const* name, unsigned n, signed_constraint const* cs, bool is_redundant);
 
         // Create a clause without adding it to the solver.
         clause_ref mk_clause(signed_constraint c1, bool is_redundant);