Allow creation of op_constraint lemmas without adding them

src/math/polysat/constraint.h

@@ -84,6 +84,12 @@ namespace polysat {
         bool is_currently_false(solver const& s, bool is_positive) const { return is_currently_true(s, !is_positive); }
 
         virtual void narrow(solver& s, bool is_positive, bool first) = 0;
+        /**
+         * If possible, produce a lemma that contradicts the given assignment.
+         * This method should not modify the solver's search state.
+         * TODO: don't pass the solver, but an interface that only allows creation of constraints
+         */
+        virtual clause_ref produce_lemma(solver& s, assignment const& a, bool is_positive) { return {}; }
 
         ule_constraint& to_ule();
         ule_constraint const& to_ule() const;
@@ -153,6 +159,7 @@ namespace polysat {
         bool is_currently_true(solver const& s) const { return get()->is_currently_true(s, is_positive()); }
         lbool bvalue(solver& s) const;
         void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }
+        clause_ref produce_lemma(solver& s, assignment const& a) { return get()->produce_lemma(s, a, is_positive()); }
 
         void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep) const { get()->add_to_univariate_solver(s, us, dep, is_positive()); }
 

src/math/polysat/op_constraint.cpp

@@ -109,34 +109,51 @@ namespace polysat {
     }
 
     /**
-    * Propagate consequences or detect conflicts based on partial assignments.
+     * Propagate consequences or detect conflicts based on partial assignments.
-    *
+     *
-    * We can assume that op_constraint is only asserted positive.
+     * We can assume that op_constraint is only asserted positive.
-    */
+     */
     void op_constraint::narrow(solver& s, bool is_positive, bool first) {
         SASSERT(is_positive);
 
         if (is_currently_true(s, is_positive))
             return;
 
-        switch (m_op) {
+        if (clause_ref lemma = produce_lemma(s, s.assignment()))
-        case code::lshr_op:
+            s.add_clause(*lemma);
-            narrow_lshr(s);
+
-            break;
-        case code::shl_op:
-            narrow_shl(s);
-            break;
-        case code::and_op:
-            narrow_and(s);
-            break;
-        default:
-            NOT_IMPLEMENTED_YET();
-            break;
-        }
         if (!s.is_conflict() && is_currently_false(s, is_positive))
             s.set_conflict(signed_constraint(this, is_positive));
     }
 
+    /**
+     * Produce lemmas that contradict the given assignment.
+     *
+     * We can assume that op_constraint is only asserted positive.
+     */
+    clause_ref op_constraint::produce_lemma(solver& s, assignment const& a, bool is_positive) {
+        SASSERT(is_positive);
+
+        if (is_currently_true(a, is_positive))
+            return {};
+
+        return produce_lemma(s, a);
+    }
+
+    clause_ref op_constraint::produce_lemma(solver& s, assignment const& a) {
+        switch (m_op) {
+        case code::lshr_op:
+            return lemma_lshr(s, a);
+        case code::shl_op:
+            return lemma_shl(s, a);
+        case code::and_op:
+            return lemma_and(s, a);
+        default:
+            NOT_IMPLEMENTED_YET();
+            return {};
+        }
+    }
+
     unsigned op_constraint::hash() const {
         return mk_mix(p().hash(), q().hash(), r().hash());
     }
@@ -169,47 +186,46 @@ namespace polysat {
      * s.m_viable.max_viable()
      * when r, q are variables.
      */
-    void op_constraint::narrow_lshr(solver& s) {
+    clause_ref op_constraint::lemma_lshr(solver& s, assignment const& a) {
-        auto const pv = s.subst(p());
+        auto const pv = a.apply_to(p());
-        auto const qv = s.subst(q());
+        auto const qv = a.apply_to(q());
-        auto const rv = s.subst(r());
+        auto const rv = a.apply_to(r());
         unsigned const K = p().manager().power_of_2();
 
         signed_constraint const lshr(this, true);
 
         if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
             // r <= p
-            s.add_clause(~lshr, s.ule(r(), p()), true);
+            return s.mk_clause(~lshr, s.ule(r(), p()), true);
         else if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero())
             // q >= K -> r = 0
-            s.add_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true);
+            return s.mk_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true);
         else if (qv.is_zero() && pv.is_val() && rv.is_val() && pv != rv)
             // q = 0 -> p = r
-            s.add_clause(~lshr, ~s.eq(q()), s.eq(p(), r()), true);
+            return s.mk_clause(~lshr, ~s.eq(q()), s.eq(p(), r()), true);
         else if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && !pv.is_zero() && rv.val() >= pv.val())
             // q != 0 & p > 0 -> r < p
-            s.add_clause(~lshr, s.eq(q()), s.ule(p(), 0), s.ult(r(), p()), true);
+            return s.mk_clause(~lshr, s.eq(q()), s.ule(p(), 0), s.ult(r(), p()), true);
         else if (qv.is_val() && !qv.is_zero() && qv.val() < K && rv.is_val() &&
             rv.val() > rational::power_of_two(K - qv.val().get_unsigned()) - 1)
             // q >= k -> r <= 2^{K-k} - 1
-            s.add_clause(~lshr, ~s.ule(qv.val(), q()), s.ule(r(), rational::power_of_two(K - qv.val().get_unsigned()) - 1), true);
+            return s.mk_clause(~lshr, ~s.ule(qv.val(), q()), s.ule(r(), rational::power_of_two(K - qv.val().get_unsigned()) - 1), true);
         else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) {
             unsigned const k = qv.val().get_unsigned();
             // q = k  ->  r[i] = p[i+k] for 0 <= i < K - k
             for (unsigned i = 0; i < K - k; ++i) {
                 if (rv.val().get_bit(i) && !pv.val().get_bit(i + k)) {
-                    s.add_clause(~lshr, ~s.eq(q(), k), ~s.bit(r(), i), s.bit(p(), i + k), true);
+                    return s.mk_clause(~lshr, ~s.eq(q(), k), ~s.bit(r(), i), s.bit(p(), i + k), true);
-                    return;
                 }
                 if (!rv.val().get_bit(i) && pv.val().get_bit(i + k)) {
-                    s.add_clause(~lshr, ~s.eq(q(), k), s.bit(r(), i), ~s.bit(p(), i + k), true);
+                    return s.mk_clause(~lshr, ~s.eq(q(), k), s.bit(r(), i), ~s.bit(p(), i + k), true);
-                    return;
                 }
             }
         }
         else {
             SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
         }
+        return {};
     }
 
     /** Evaluate constraint: r == p >> q */
@@ -244,10 +260,10 @@ namespace polysat {
      *      r != 0  ->  r >= p
      *      q = 0   ->  r = p
      */
-    void op_constraint::narrow_shl(solver& s) {
+    clause_ref op_constraint::lemma_shl(solver& s, assignment const& a) {
-        auto const pv = s.subst(p());
+        auto const pv = a.apply_to(p());
-        auto const qv = s.subst(q());
+        auto const qv = a.apply_to(q());
-        auto const rv = s.subst(r());
+        auto const rv = a.apply_to(r());
         unsigned const K = p().manager().power_of_2();
 
         signed_constraint const shl(this, true);
@@ -256,35 +272,34 @@ namespace polysat {
             // r != 0  ->  r >= p
             // r = 0 \/ r >= p      (equivalent)
             // r-1 >= p-1           (equivalent unit constraint to better support narrowing)
-            s.add_clause(~shl, s.ule(p() - 1, r() - 1), true);
+            return s.mk_clause(~shl, s.ule(p() - 1, r() - 1), true);
         else if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero())
             // q >= K  ->  r = 0
-            s.add_clause(~shl, ~s.ule(K, q()), s.eq(r()), true);
+            return s.mk_clause(~shl, ~s.ule(K, q()), s.eq(r()), true);
         else if (qv.is_zero() && pv.is_val() && rv.is_val() && rv != pv)
             // q = 0  ->  r = p
-            s.add_clause(~shl, ~s.eq(q()), s.eq(r(), p()), true);
+            return s.mk_clause(~shl, ~s.eq(q()), s.eq(r(), p()), true);
         else if (qv.is_val() && !qv.is_zero() && qv.val() < K && rv.is_val() &&
             !rv.is_zero() && rv.val() < rational::power_of_two(qv.val().get_unsigned()))
             // q >= k  ->  r = 0  \/  r >= 2^k  (intuitive version)
             // q >= k  ->  r - 1 >= 2^k - 1     (equivalent unit constraint to better support narrowing)
-            s.add_clause(~shl, ~s.ule(qv.val(), q()), s.ule(rational::power_of_two(qv.val().get_unsigned()) - 1, r() - 1), true);
+            return s.mk_clause(~shl, ~s.ule(qv.val(), q()), s.ule(rational::power_of_two(qv.val().get_unsigned()) - 1, r() - 1), true);
         else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) {
             unsigned const k = qv.val().get_unsigned();
             // q = k  ->  r[i+k] = p[i] for 0 <= i < K - k
             for (unsigned i = 0; i < K - k; ++i) {
                 if (rv.val().get_bit(i + k) && !pv.val().get_bit(i)) {
-                    s.add_clause(~shl, ~s.eq(q(), k), ~s.bit(r(), i + k), s.bit(p(), i), true);
+                    return s.mk_clause(~shl, ~s.eq(q(), k), ~s.bit(r(), i + k), s.bit(p(), i), true);
-                    return;
                 }
                 if (!rv.val().get_bit(i + k) && pv.val().get_bit(i)) {
-                    s.add_clause(~shl, ~s.eq(q(), k), s.bit(r(), i + k), ~s.bit(p(), i), true);
+                    return s.mk_clause(~shl, ~s.eq(q(), k), s.bit(r(), i + k), ~s.bit(p(), i), true);
-                    return;
                 }
             }
         }
         else {
             SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
         }
+        return {};
     }
 
     /** Evaluate constraint: r == p << q */
@@ -323,18 +338,19 @@ namespace polysat {
      * p = max_value => q = r
      * q = max_value => p = r
      */
-    void op_constraint::narrow_and(solver& s) {
+    clause_ref op_constraint::lemma_and(solver& s, assignment const& a) {
-        auto pv = s.subst(p());
+        auto pv = a.apply_to(p());
-        auto qv = s.subst(q());
+        auto qv = a.apply_to(q());
-        auto rv = s.subst(r());
+        auto rv = a.apply_to(r());
+
+        signed_constraint const andc(this, true);
 
-        signed_constraint andc(this, true);
         if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
-            s.add_clause(~andc, s.ule(r(), p()), true);
+            return s.mk_clause(~andc, s.ule(r(), p()), true);
         else if (qv.is_val() && rv.is_val() && rv.val() > qv.val())
-            s.add_clause(~andc, s.ule(r(), q()), true);
+            return s.mk_clause(~andc, s.ule(r(), q()), true);
         else if (pv.is_val() && qv.is_val() && rv.is_val() && pv == qv && rv != pv)
-            s.add_clause(~andc, ~s.eq(p(), q()), s.eq(r(), p()), true);
+            return s.mk_clause(~andc, ~s.eq(p(), q()), s.eq(r(), p()), true);
         else if (pv.is_val() && qv.is_val() && rv.is_val()) {
             unsigned K = p().manager().power_of_2();
             for (unsigned i = 0; i < K; ++i) {
@@ -344,16 +360,17 @@ namespace polysat {
                 if (rb == (pb && qb))
                     continue;
                 if (pb && qb && !rb)
-                    s.add_clause(~andc, ~s.bit(p(), i), ~s.bit(q(), i), s.bit(r(), i), true);
+                    return s.mk_clause(~andc, ~s.bit(p(), i), ~s.bit(q(), i), s.bit(r(), i), true);
                 else if (!pb && rb)
-                    s.add_clause(~andc, s.bit(p(), i), ~s.bit(r(), i), true);
+                    return s.mk_clause(~andc, s.bit(p(), i), ~s.bit(r(), i), true);
                 else if (!qb && rb)
-                    s.add_clause(~andc, s.bit(q(), i), ~s.bit(r(), i), true);
+                    return s.mk_clause(~andc, s.bit(q(), i), ~s.bit(r(), i), true);
                 else
                     UNREACHABLE();
-                return;
+                return {};
             }
         }
+        return {};
     }
 
     /** Evaluate constraint: r == p & q */

src/math/polysat/op_constraint.h

@@ -39,14 +39,15 @@ namespace polysat {
 
         op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r);
         lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
+        clause_ref produce_lemma(solver& s, assignment const& a);
 
-        void narrow_lshr(solver& s);
+        clause_ref lemma_lshr(solver& s, assignment const& a);
         static lbool eval_lshr(pdd const& p, pdd const& q, pdd const& r);
 
-        void narrow_shl(solver& s);
+        clause_ref lemma_shl(solver& s, assignment const& a);
         static lbool eval_shl(pdd const& p, pdd const& q, pdd const& r);
 
-        void narrow_and(solver& s);
+        clause_ref lemma_and(solver& s, assignment const& a);
         static lbool eval_and(pdd const& p, pdd const& q, pdd const& r);
 
         std::ostream& display(std::ostream& out, char const* eq) const;
@@ -61,6 +62,7 @@ namespace polysat {
         lbool eval() const override;
         lbool eval(assignment const& a) const override;
         void narrow(solver& s, bool is_positive, bool first) override;
+        virtual clause_ref produce_lemma(solver& s, assignment const& a, bool is_positive) override;
         unsigned hash() const override;
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return false; }