rename to op-constraint to give space for other operations

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

src/math/polysat/CMakeLists.txt

@@ -15,7 +15,7 @@ z3_add_component(polysat
     saturation.cpp
     search_state.cpp
     simplify.cpp
-    shr_constraint.cpp
+    op_constraint.cpp
     solver.cpp
     ule_constraint.cpp
     viable.cpp

src/math/polysat/constraint.cpp

@@ -19,7 +19,7 @@ Author:
 #include "math/polysat/log_helper.h"
 #include "math/polysat/ule_constraint.h"
 #include "math/polysat/mul_ovfl_constraint.h"
-#include "math/polysat/shr_constraint.h"
+#include "math/polysat/op_constraint.h"
 
 namespace polysat {
 
@@ -233,11 +233,10 @@ namespace polysat {
         return { dedup(alloc(mul_ovfl_constraint, *this, a, b)), true };
     }
 
-    signed_constraint constraint_manager::shr(pdd const& p, pdd const& q, pdd const& r) {
+    signed_constraint constraint_manager::lshr(pdd const& p, pdd const& q, pdd const& r) {
-        return { dedup(alloc(shr_constraint, *this, p, q, r)), true };
+        return { dedup(alloc(op_constraint, *this, op_constraint::code::lshr_op, p, q, r)), true };
     }
 
-
     // To do signed comparison of bitvectors, flip the msb and do unsigned comparison:
     //
     //      x <=s y    <=>    x + 2^(w-1)  <=u  y + 2^(w-1)
@@ -284,12 +283,12 @@ namespace polysat {
         return *dynamic_cast<mul_ovfl_constraint const*>(this);
     }
 
-    shr_constraint& constraint::to_shr() {
+    op_constraint& constraint::to_op() {
-        return *dynamic_cast<shr_constraint*>(this);
+        return *dynamic_cast<op_constraint*>(this);
     }
 
-    shr_constraint const& constraint::to_shr() const {
+    op_constraint const& constraint::to_op() const {
-        return *dynamic_cast<shr_constraint const*>(this);
+        return *dynamic_cast<op_constraint const*>(this);
     }
 
     std::string constraint::bvar2string() const {

src/math/polysat/constraint.h

@@ -20,12 +20,12 @@ Author:
 
 namespace polysat {
 
-    enum ckind_t { ule_t, mul_ovfl_t, shr_t };
+    enum ckind_t { ule_t, mul_ovfl_t, op_t };
 
     class constraint;
     class ule_constraint;
     class mul_ovfl_constraint;
-    class shr_constraint;
+    class op_constraint;
     class signed_constraint;
 
     using constraint_hash = obj_ptr_hash<constraint>;
@@ -97,7 +97,7 @@ namespace polysat {
         signed_constraint slt(pdd const& a, pdd const& b);
         signed_constraint mul_ovfl(pdd const& p, pdd const& q);
         signed_constraint bit(pdd const& p, unsigned i);
-        signed_constraint shr(pdd const& p, pdd const& q, pdd const& r);
+        signed_constraint lshr(pdd const& p, pdd const& q, pdd const& r);
 
         constraint *const* begin() const { return m_constraints.data(); }
         constraint *const* end() const { return m_constraints.data() + m_constraints.size(); }
@@ -136,7 +136,7 @@ namespace polysat {
         friend class clause;
         friend class ule_constraint;
         friend class mul_ovfl_constraint;
-        friend class shr_constraint;
+        friend class op_constraint;
 
         // constraint_manager* m_manager;
         ckind_t             m_kind;
@@ -165,7 +165,7 @@ namespace polysat {
         virtual bool is_diseq() const { return false; }
         bool is_ule() const { return m_kind == ckind_t::ule_t; }
         bool is_mul_ovfl() const { return m_kind == ckind_t::mul_ovfl_t; }
-        bool is_shr() const { return m_kind == ckind_t::shr_t; }
+        bool is_op() const { return m_kind == ckind_t::op_t; }
         ckind_t kind() const { return m_kind; }
         virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
         virtual std::ostream& display(std::ostream& out) const = 0;
@@ -182,8 +182,8 @@ namespace polysat {
         ule_constraint const& to_ule() const;
         mul_ovfl_constraint& to_mul_ovfl();
         mul_ovfl_constraint const& to_mul_ovfl() const;
-        shr_constraint& to_shr();
+        op_constraint& to_op();
-        shr_constraint const& to_shr() const;
+        op_constraint const& to_op() const;
         unsigned_vector& vars() { return m_vars; }
         unsigned_vector const& vars() const { return m_vars; }
         unsigned var(unsigned idx) const { return m_vars[idx]; }

src/math/polysat/op_constraint.cpp

@@ -11,13 +11,13 @@ Author:
 
 --*/
 
-#include "math/polysat/shr_constraint.h"
+#include "math/polysat/op_constraint.h"
 #include "math/polysat/solver.h"
 
 namespace polysat {
 
-    shr_constraint::shr_constraint(constraint_manager& m, pdd const& p, pdd const& q, pdd const& r):
+    op_constraint::op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r):
-        constraint(m, ckind_t::shr_t), m_p(p), m_q(q), m_r(r) {
+        constraint(m, ckind_t::op_t), m_op(c), m_p(p), m_q(q), m_r(r) {
         m_vars.append(p.free_vars());
         for (auto v : q.free_vars())
             if (!m_vars.contains(v))
@@ -27,22 +27,29 @@ namespace polysat {
                 m_vars.push_back(v);
     }    
 
-    lbool shr_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
+    lbool op_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
-        if (q.is_val() && r.is_val()) {
+        switch (m_op) {
-            auto& m = p.manager();
+        case code::lshr_op:
-            if (q.val() >= m.power_of_2())
+            if (q.is_val() && r.is_val()) {
-                return r.is_zero() ? l_true : l_false;            
+                auto& m = p.manager();
-            if (p.is_val()) {
+                if (q.val() >= m.power_of_2())
-                pdd rr = p * m.mk_val(rational::power_of_two(q.val().get_unsigned()));
+                    return r.is_zero() ? l_true : l_false;
-                return rr == r ? l_true : l_false;
+                if (p.is_val()) {
+                    pdd rr = p * m.mk_val(rational::power_of_two(q.val().get_unsigned()));
+                    return rr == r ? l_true : l_false;
+                }
+                // other cases when we know lower 
+                // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant.
             }
-            // other cases when we know lower 
+            break;
-            // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant.
+        default:
+            break;
         }
+
         return l_undef;
     }
     
-    bool shr_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
+    bool op_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
         switch (eval(p, q, r)) {
         case l_true: return !is_positive;
         case l_false: return is_positive;
@@ -50,7 +57,7 @@ namespace polysat {
         }
     }
 
-    bool shr_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
+    bool op_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
         switch (eval(p, q, r)) {
         case l_true: return is_positive;
         case l_false: return !is_positive;
@@ -58,7 +65,7 @@ namespace polysat {
         }
     }
     
-    std::ostream& shr_constraint::display(std::ostream& out, lbool status) const {
+    std::ostream& op_constraint::display(std::ostream& out, lbool status) const {
         switch (status) {
         case l_true: return display(out);
         case l_false: return display(out << "~");
@@ -66,19 +73,24 @@ namespace polysat {
         }
     }
 
-    std::ostream& shr_constraint::display(std::ostream& out) const {
+    std::ostream& op_constraint::display(std::ostream& out) const {
-        return out << r() << " == " << p() << " << " << q();
+        switch (m_op) {
+        case code::lshr_op:
+            return out << r() << " == " << p() << " << " << q();
+        default:
+            return out;
+        }        
     }
 
-    bool shr_constraint::is_always_false(bool is_positive) const {
+    bool op_constraint::is_always_false(bool is_positive) const {
         return is_always_false(is_positive, p(), q(), r());
     }
 
-    bool shr_constraint::is_currently_false(assignment_t const& a, bool is_positive) const {
+    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 shr_constraint::is_currently_true(assignment_t const& a, bool is_positive) const {
+    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));
     }
 
@@ -97,22 +109,22 @@ namespace polysat {
     * 
     * Enforce also inferences and bounds
     * 
-    * We can assume that shr_constraint is only asserted positive.
+    * We can assume that op_constraint is only asserted positive.
     */
-    void shr_constraint::narrow(solver& s, bool is_positive) {
+    void op_constraint::narrow(solver& s, bool is_positive) {
         SASSERT(is_positive);
         NOT_IMPLEMENTED_YET();
     }
 
-    unsigned shr_constraint::hash() const {
+    unsigned op_constraint::hash() const {
         return mk_mix(p().hash(), q().hash(), r().hash());
     }
 
-    bool shr_constraint::operator==(constraint const& other) const {
+    bool op_constraint::operator==(constraint const& other) const {
-        if (other.kind() != ckind_t::shr_t)
+        if (other.kind() != ckind_t::op_t)
             return false;
-        auto const& o = other.to_shr();
+        auto const& o = other.to_op();
-        return p() == o.p() && q() == o.q() && r() == o.r();
+        return m_op == o.m_op && p() == o.p() && q() == o.q() && r() == o.r();
     }
 
 }

src/math/polysat/op_constraint.h

@@ -3,8 +3,16 @@ Copyright (c) 2021 Microsoft Corporation
 
 Module Name:
 
-    polysat shift right constraint.
+    Op constraint.
 
+    lshr: r == p >> q
+    ashr: r == p >> q
+    lshl: r == p << q
+    and:  r == p & q
+    or:   r == p | q
+    neg:  r == ~p
+    xor:  r == p ^ q
+    
 Author:
 
     Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
@@ -15,21 +23,25 @@ Author:
 
 namespace polysat {
 
-    class shr_constraint final : public constraint {
+    class op_constraint final : public constraint {
+    public:
+        enum class code { lshr_op, ashr_op, shl_op, and_op, or_op, xor_op, not_op };
+    protected:
         friend class constraint_manager;
 
+        code m_op;
         pdd m_p;
         pdd m_q;
         pdd m_r;
 
-        shr_constraint(constraint_manager& m, pdd const& p, pdd const& q, pdd const& r);
+        op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r);
-        void simplify();
+        void simplify() {}
         bool is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const;
         bool is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const;
         lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
 
-    public:
+    public:        
-        ~shr_constraint() override {}
+        ~op_constraint() override {}
         pdd const& p() const { return m_p; }
         pdd const& q() const { return m_q; }
         pdd const& r() const { return m_r; }

src/math/polysat/solver.cpp

@@ -135,11 +135,11 @@ namespace polysat {
         return std::tuple<pdd, pdd>(quot, rem);
     }
 
-    pdd solver::shr(pdd const& p, pdd const& q) {
+    pdd solver::lshr(pdd const& p, pdd const& q) {
         auto& m = p.manager();
         unsigned sz = m.power_of_2();
         pdd r = m.mk_var(add_var(sz));
-        assign_eh(m_constraints.shr(p, q, r), null_dependency);
+        assign_eh(m_constraints.lshr(p, q, r), null_dependency);
         return r;
     }
 

src/math/polysat/solver.h

@@ -270,7 +270,7 @@ namespace polysat {
         /**
         * Create expression for the logical right shift of p by q.
         */
-        pdd shr(pdd const& p, pdd const& q);
+        pdd lshr(pdd const& p, pdd const& q);
 
         /**
          * Create polynomial constant.

src/test/polysat.cpp

@@ -1034,7 +1034,7 @@ namespace polysat {
         else if (bv.is_bv_lshr(e, a, b)) {
             auto pa = to_pdd(m, s, expr2pdd, a);
             auto pb = to_pdd(m, s, expr2pdd, b);
-            r = alloc(pdd, s.shr(pa, pb));
+            r = alloc(pdd, s.lshr(pa, pb));
         }
         else if (bv.is_numeral(e, n, sz)) 
             r = alloc(pdd, s.value(n, sz));