elaborate on narrow

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/polysat/op_constraint.cpp

@@ -9,6 +9,15 @@ Author:
 
     Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
 
+Notes:
+
+Additional possible functionality on constraints:
+
+- activate - when operation is first activated. It may be created and only activated later.
+- bit-wise assignments - narrow based on bit assignment, not entire word assignment.
+- integration with congruence tables
+- integration with conflict resolution
+
 --*/
 
 #include "math/polysat/op_constraint.h"
@@ -52,6 +61,18 @@ namespace polysat {
         }
     }
 
+    bool op_constraint::is_always_false(bool is_positive) const {
+        return is_always_false(is_positive, p(), q(), r());
+    }
+
+    bool op_constraint::is_currently_false(assignment_t const& a, bool is_positive) const {
+        return is_always_false(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a));
+    }
+
+    bool op_constraint::is_currently_true(assignment_t const& a, bool is_positive) const {
+        return is_always_true(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a));
+    }
+
     std::ostream& op_constraint::display(std::ostream& out, lbool status) const {
         switch (status) {
         case l_true: return display(out);
@@ -60,7 +81,7 @@ namespace polysat {
         }
     }
 
-    std::ostream& operator<<(std::ostream & out, op_constraint::code c) {
+    std::ostream& operator<<(std::ostream& out, op_constraint::code c) {
         switch (c) {
         case op_constraint::code::ashr_op:
             return out << ">>a";
@@ -75,29 +96,31 @@ namespace polysat {
         case op_constraint::code::xor_op:
             return out << "^";
         default:
-            return out << "?";
+            UNREACHABLE();
+            return out;
         }
         return out;
     }
 
     std::ostream& op_constraint::display(std::ostream& out) const {
-        return out << r() << " " << m_op << " " << p() << " << " << q();                
+        if (m_op == code::not_op)
+            return out << r() << " == ~" << p();
+        else
+            return out << r() << " == " << p() << " " << m_op << " " << q();
     }
 
-    bool op_constraint::is_always_false(bool is_positive) const {
+    /**
-        return is_always_false(is_positive, p(), q(), r());
+    * Propagate consequences or detect conflicts based on partial assignments.
-    }
+    * 
-
+    * We can assume that op_constraint is only asserted positive.
-    bool op_constraint::is_currently_false(assignment_t const& a, bool is_positive) const {
+    */
-        return is_always_false(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a));
-    }
-
-    bool op_constraint::is_currently_true(assignment_t const& a, bool is_positive) const {
-        return is_always_true(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a));
-    }
 
     void op_constraint::narrow(solver& s, bool is_positive) {
         SASSERT(is_positive);
+
+        if (is_currently_true(s.assignment(), is_positive))
+            return;
+
         switch (m_op) {
         case code::lshr_op:
             narrow_lshr(s);
@@ -106,6 +129,10 @@ namespace polysat {
             NOT_IMPLEMENTED_YET();
             break;
         }
+        if (!s.is_conflict() && is_currently_false(s.assignment(), is_positive)) {
+            s.set_conflict(signed_constraint(this, is_positive));
+            return;
+        }
     }
 
     unsigned op_constraint::hash() const {
@@ -120,38 +147,61 @@ namespace polysat {
     }
 
     /**
-     * Enforce basic axioms, such as:
+     * Enforce basic axioms for r == p >> q, such as:
      *
-     * r = p >> q & q >= k -> r[i] = 0 for i > K - k
+     * q >= k -> r[i] = 0 for i > K - k
-     * r = p >> q & q >= K -> r = 0
+     * q >= K -> r = 0
-     * r = p >> q & q = k -> r[i] = p[i+k] for k + i < K
+     * q = k -> r[i] = p[i+k] for k + i < K
-     * r = p >> q & q >= k -> r <= 2^{K-k-1}
+     * q >= k -> r <= 2^{K-k-1}
-     * r = p >> q => r <= p
+     * r <= p
-     * r = p >> q & q != 0 => r < p
+     * q != 0 => r <= p
-     * r = p >> q & q = 0 => r = p
+     * q = 0 => r = p
      *
      * when q is a constant, several axioms can be enforced at activation time.
      *
      * Enforce also inferences and bounds
      *
-     * We can assume that op_constraint is only asserted positive.
      */
     void op_constraint::narrow_lshr(solver& s) {
+        auto pv = p().subst_val(s.assignment());
+        auto qv = q().subst_val(s.assignment());
+        auto rv = r().subst_val(s.assignment());
+        unsigned K = p().manager().power_of_2();
+        signed_constraint lshl(this, true);
+        // r <= p
+        if (pv.is_val() && rv.is_val() && rv.val() > pv.val()) {
+            s.add_clause(~lshl, s.ule(r(), p()), true);
+            return;
+        }
+        // q >= K -> r = 0
+        if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero()) {
+            s.add_clause(~lshl, ~s.ule(K, q()), s.eq(r()), true);
+            return;
+        }
+        // q = 0 => r = p
+        if (qv.is_zero() && pv.is_val() && rv.is_val() && pv != rv) {
+            s.add_clause(~lshl, ~s.eq(q()), s.eq(p(), r()), true);
+            return;
+        }
+        // q != 0 & p > 0 => r < p
+        if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && pv <= rv) {
+            s.add_clause(~lshl, s.eq(q()), s.ule(p, 0), s.ult(r(), p()), true);
+            return;
+        }
         NOT_IMPLEMENTED_YET();
     }
 
     lbool op_constraint::eval_lshr(pdd const& p, pdd const& q, pdd const& r) const {
-        if (q.is_val() && r.is_val()) {
+        auto& m = p.manager();
-            auto& m = p.manager();
+
-            if (q.val() >= m.power_of_2())
+        if (p.is_val() && q.is_val() && r.is_val())
-                return r.is_zero() ? l_true : l_false;
+            return r == p * m.mk_val(rational::power_of_two(q.val().get_unsigned())) ? l_true : l_false;
-            if (p.is_val()) {
+            
-                pdd rr = p * m.mk_val(rational::power_of_two(q.val().get_unsigned()));
+        if (q.is_val() && q.val() >= m.power_of_2() && r.is_val())
-                return rr == r ? l_true : l_false;
+            return r.is_zero() ? l_true : l_false;
-            }
+        
-            // other cases when we know lower 
+        // other cases when we know lower 
-            // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant.
+        // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant.
-        }
         return l_undef;
     }
 }

src/math/polysat/op_constraint.h

@@ -6,11 +6,11 @@ Module Name:
     Op constraint.
 
     lshr: r == p >> q
-    ashr: r == p >> q
+    ashr: r == p >>a q
     lshl: r == p << q
     and:  r == p & q
     or:   r == p | q
-    neg:  r == ~p
+    not:  r == ~p
     xor:  r == p ^ q
     
 Author:

src/math/polysat/solver.cpp

@@ -793,6 +793,34 @@ namespace polysat {
         add_clause(*clause);
     }
 
+    void solver::add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant) {
+        clause_builder cb(*this);
+        if (!c1.is_always_false())
+            cb.push(c1);
+        if (!c2.is_always_false())
+            cb.push(c2);
+        if (!c3.is_always_false())
+            cb.push(c3);
+        clause_ref clause = cb.build();
+        clause->set_redundant(is_redundant);
+        add_clause(*clause);
+    }
+
+    void solver::add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant) {
+        clause_builder cb(*this);
+        if (!c1.is_always_false())
+            cb.push(c1);
+        if (!c2.is_always_false())
+            cb.push(c2);
+        if (!c3.is_always_false())
+            cb.push(c3);
+        if (!c4.is_always_false())
+            cb.push(c4);
+        clause_ref clause = cb.build();
+        clause->set_redundant(is_redundant);
+        add_clause(*clause);
+    }
+
     void solver::insert_constraint(signed_constraints& cs, signed_constraint c) {
         SASSERT(c);
         LOG_V("INSERTING: " << c);

src/math/polysat/solver.h

@@ -56,6 +56,7 @@ namespace polysat {
         friend class constraint;
         friend class ule_constraint;
         friend class mul_ovfl_constraint;
+        friend class op_constraint;
         friend class signed_constraint;
         friend class clause;
         friend class clause_builder;
@@ -207,6 +208,8 @@ namespace polysat {
         void backjump(unsigned new_level);
         void add_clause(clause& lemma);
         void add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant);
+        void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant);
+        void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant);
 
 
         signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }