na

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

src/math/polysat/op_constraint.cpp

@@ -30,24 +30,11 @@ namespace polysat {
     lbool op_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
         switch (m_op) {
         case code::lshr_op:
-            if (q.is_val() && r.is_val()) {
-                auto& m = p.manager();
-                if (q.val() >= m.power_of_2())
-                    return r.is_zero() ? 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.
-            }
-            break;
+            return eval_lshr(p, q, r);         
         default:
-            break;
-        }
-
             return l_undef;            
         }       
+    }
     
     bool op_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
         switch (eval(p, q, r)) {
@@ -73,13 +60,28 @@ namespace polysat {
         }
     }
 
-    std::ostream& op_constraint::display(std::ostream& out) const {
-        switch (m_op) {
-        case code::lshr_op:
-            return out << r() << " == " << p() << " << " << q();
+    std::ostream& operator<<(std::ostream & out, op_constraint::code c) {
+        switch (c) {
+        case op_constraint::code::ashr_op:
+            return out << ">>a";
+        case op_constraint::code::lshr_op:
+            return out << ">>";
+        case op_constraint::code::shl_op:
+            return out << "<<";
+        case op_constraint::code::and_op:
+            return out << "&";
+        case op_constraint::code::or_op:
+            return out << "|";
+        case op_constraint::code::xor_op:
+            return out << "^";
         default:
+            return out << "?";
+        }
         return out;
     }
+
+    std::ostream& op_constraint::display(std::ostream& out) const {
+        return out << r() << " " << m_op << " " << p() << " << " << q();                
     }
 
     bool op_constraint::is_always_false(bool is_positive) const {
@@ -94,6 +96,29 @@ namespace polysat {
         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);
+        switch (m_op) {
+        case code::lshr_op:
+            narrow_lshr(s);
+            break;
+        default:
+            NOT_IMPLEMENTED_YET();
+            break;
+        }
+    }
+
+    unsigned op_constraint::hash() const {
+        return mk_mix(p().hash(), q().hash(), r().hash());
+    }
+
+    bool op_constraint::operator==(constraint const& other) const {
+        if (other.kind() != ckind_t::op_t)
+            return false;
+        auto const& o = other.to_op();
+        return m_op == o.m_op && p() == o.p() && q() == o.q() && r() == o.r();
+    }
+
     /**
      * Enforce basic axioms, such as:
      *
@@ -111,20 +136,22 @@ namespace polysat {
      *
      * We can assume that op_constraint is only asserted positive.
      */
-    void op_constraint::narrow(solver& s, bool is_positive) {
-        SASSERT(is_positive);
+    void op_constraint::narrow_lshr(solver& s) {
         NOT_IMPLEMENTED_YET();
     }
 
-    unsigned op_constraint::hash() const {
-        return mk_mix(p().hash(), q().hash(), r().hash());
+    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();
+            if (q.val() >= m.power_of_2())
+                return r.is_zero() ? 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;
             }
-
-    bool op_constraint::operator==(constraint const& other) const {
-        if (other.kind() != ckind_t::op_t)
-            return false;
-        auto const& o = other.to_op();
-        return m_op == o.m_op && p() == o.p() && q() == o.q() && r() == o.r();
+            // other cases when we know lower 
+            // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant.
+        }
+        return l_undef;
     }
-
 }

src/math/polysat/op_constraint.h

@@ -40,6 +40,9 @@ namespace polysat {
         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;
 
+        void narrow_lshr(solver& s);
+        lbool eval_lshr(pdd const& p, pdd const& q, pdd const& r) const;
+
     public:        
         ~op_constraint() override {}
         pdd const& p() const { return m_p; }