adding band

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

src/sat/smt/intblast_solver.cpp

@@ -23,7 +23,10 @@ Author:
 namespace intblast {
 
     solver::solver(euf::solver& ctx) :
+<<<<<<< HEAD
         th_euf_solver(ctx, symbol("intblast"), ctx.get_manager().get_family_id("bv")),
+=======
+>>>>>>> 17c480f83 (adding band)
         ctx(ctx),
         s(ctx.s()),
         m(ctx.get_manager()),
@@ -34,6 +37,7 @@ namespace intblast {
         m_pinned(m)
     {}
 
+<<<<<<< HEAD
     euf::theory_var solver::mk_var(euf::enode* n) {
         auto r = euf::th_euf_solver::mk_var(n);
         ctx.attach_th_var(n, this, r);
@@ -184,6 +188,9 @@ namespace intblast {
     }
 
     lbool solver::check_solver_state() {
+=======
+    lbool solver::check() {
+>>>>>>> 17c480f83 (adding band)
         sat::literal_vector literals;
         uint_set selected;
         for (auto const& clause : s.clauses()) {
@@ -253,8 +260,8 @@ namespace intblast {
         }
 
         IF_VERBOSE(10, verbose_stream() << "check\n";
-            m_solver->display(verbose_stream());
+        m_solver->display(verbose_stream());
-            verbose_stream() << es << "\n");
+        verbose_stream() << es << "\n");
 
         lbool r = m_solver->check_sat(es);
 

src/sat/smt/polysat/CMakeLists.txt

@@ -5,6 +5,7 @@ z3_add_component(polysat
     core.cpp
     fixed_bits.cpp
     forbidden_intervals.cpp
+    op_constraint.cpp
     ule_constraint.cpp
     umul_ovfl_constraint.cpp
     viable.cpp

src/sat/smt/polysat/constraints.cpp

@@ -17,6 +17,7 @@ Author:
 #include "sat/smt/polysat/constraints.h"
 #include "sat/smt/polysat/ule_constraint.h"
 #include "sat/smt/polysat/umul_ovfl_constraint.h"
+#include "sat/smt/polysat/op_constraint.h"
 
 namespace polysat {
 
@@ -36,6 +37,30 @@ namespace polysat {
         return signed_constraint(ckind_t::umul_ovfl_t, cnstr);
     }
 
+    signed_constraint constraints::lshr(pdd const& a, pdd const& b, pdd const& r) {
+        auto* cnstr = alloc(op_constraint, op_constraint::code::lshr_op, a, b, r);
+        c.trail().push(new_obj_trail(cnstr));
+        return signed_constraint(ckind_t::op_t, cnstr);
+    }
+
+    signed_constraint constraints::ashr(pdd const& a, pdd const& b, pdd const& r) {
+        auto* cnstr = alloc(op_constraint, op_constraint::code::ashr_op, a, b, r);
+        c.trail().push(new_obj_trail(cnstr));
+        return signed_constraint(ckind_t::op_t, cnstr);
+    }
+
+    signed_constraint constraints::shl(pdd const& a, pdd const& b, pdd const& r) {
+        auto* cnstr = alloc(op_constraint, op_constraint::code::shl_op, a, b, r);
+        c.trail().push(new_obj_trail(cnstr));
+        return signed_constraint(ckind_t::op_t, cnstr);
+    }
+
+    signed_constraint constraints::band(pdd const& a, pdd const& b, pdd const& r) {
+        auto* cnstr = alloc(op_constraint, op_constraint::code::and_op, a, b, r);
+        c.trail().push(new_obj_trail(cnstr));
+        return signed_constraint(ckind_t::op_t, cnstr);
+    }
+
     bool signed_constraint::is_eq(pvar& v, rational& val) {
         if (m_sign)
             return false;
@@ -64,10 +89,4 @@ namespace polysat {
         return out << *m_constraint;        
     }
 
-    bool signed_constraint::is_always_true() const {
-        return m_sign ? m_constraint->is_always_false() : m_constraint->is_always_true();
-    }
-    bool signed_constraint::is_always_false() const {
-        return m_sign ? m_constraint->is_always_true() : m_constraint->is_always_false();
-    }
 }

src/sat/smt/polysat/constraints.h

@@ -41,8 +41,6 @@ namespace polysat {
         virtual std::ostream& display(std::ostream& out) const = 0;
         virtual lbool eval() const = 0;
         virtual lbool eval(assignment const& a) const = 0;
-        virtual bool is_always_true() const = 0;
-        virtual bool is_always_false() const = 0;
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
@@ -63,9 +61,10 @@ namespace polysat {
         unsigned_vector const& vars() const { return m_constraint->vars(); }
         unsigned var(unsigned idx) const { return m_constraint->var(idx); }
         bool contains_var(pvar v) const { return m_constraint->contains_var(v); }
-        bool is_always_true() const;
+        bool is_always_true() const { return eval() == l_true; }
-        bool is_always_false() const;
+        bool is_always_false() const { return eval() == l_false; }
         lbool eval(assignment& a) const;
+        lbool eval() const { return m_sign ? ~m_constraint->eval() : m_constraint->eval();}
         ckind_t op() const { return m_op; }
         bool is_ule() const { return m_op == ule_t; }
         bool is_umul_ovfl() const { return m_op == umul_ovfl_t; }
@@ -138,6 +137,10 @@ namespace polysat {
         signed_constraint umul_ovfl(int             p, pdd const& q) { return umul_ovfl(rational(p), q); }
         signed_constraint umul_ovfl(unsigned        p, pdd const& q) { return umul_ovfl(rational(p), q); }
 
+        signed_constraint lshr(pdd const& a, pdd const& b, pdd const& r);
+        signed_constraint ashr(pdd const& a, pdd const& b, pdd const& r);
+        signed_constraint shl(pdd const& a, pdd const& b, pdd const& r);
+        signed_constraint band(pdd const& a, pdd const& b, pdd const& r);
 
         //signed_constraint even(pdd const& p) { return parity_at_least(p, 1); }
         //signed_constraint odd(pdd const& p) { return ~even(p); }

src/sat/smt/polysat/core.h

@@ -115,10 +115,10 @@ namespace polysat {
         signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
 
 
-        void lshr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("lshr nyi"); }
+        signed_constraint lshr(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.lshr(a, b, r); }
-        void ashr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("ashr nyi"); }
+        signed_constraint ashr(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.ashr(a, b, r); }
-        void shl(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("shlh nyi"); }
+        signed_constraint shl(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.shl(a, b, r); }
-        void band(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET();  throw default_exception("band nyi"); }
+        signed_constraint band(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.band(a, b, r); }
 
         pdd bnot(pdd p) { return -p - 1; }
 

src/sat/smt/polysat/ule_constraint.cpp

@@ -343,22 +343,4 @@ namespace polysat {
         return eval(a.apply_to(lhs()), a.apply_to(rhs()));
     }
 
-    bool ule_constraint::is_always_true() const {
-        if (lhs().is_zero())
-            return true;      // 0 <= p
-        if (rhs().is_max())
-            return true;      // p <= -1
-        if (lhs().is_val() && rhs().is_val())
-            return lhs().val() <= rhs().val();
-        return false;
-    }
-
-    bool ule_constraint::is_always_false() const {
-        if (lhs().is_never_zero() && rhs().is_zero())
-            return true;      // p > 0, q = 0
-        if (lhs().is_val() && rhs().is_val())
-            return lhs().val() > rhs().val();
-        return false;
-    }
-
 }

src/sat/smt/polysat/ule_constraint.h

@@ -35,8 +35,6 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         lbool eval() const override;
         lbool eval(assignment const& a) const override;
-        bool is_always_true() const override;
-        bool is_always_false() const override;
         bool is_eq() const { return m_rhs.is_zero(); }
         unsigned power_of_2() const { return m_lhs.power_of_2(); }
 

src/sat/smt/polysat/umul_ovfl_constraint.h

@@ -34,8 +34,6 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         lbool eval() const override;
         lbool eval(assignment const& a) const override;
-        bool is_always_true() const override { return false; } // todo port
-        bool is_always_false() const override { return false; }
     };
 
 }

src/sat/smt/polysat_internalize.cpp

@@ -234,7 +234,9 @@ namespace polysat {
         if (n->get_num_args() == 2) {
             expr* x, * y;
             VERIFY(bv.is_bv_and(n, x, y));
-            m_core.band(expr2pdd(n), expr2pdd(x), expr2pdd(y));
+            auto sc = m_core.band(expr2pdd(x), expr2pdd(y), expr2pdd(n));
+            // auto index = m_core.register_constraint(sc, dependency::axiom());
+            // 
         }
         else {
             expr_ref z(n->get_arg(0), m);
@@ -249,13 +251,13 @@ namespace polysat {
     void solver::internalize_lshr(app* n) {
         expr* x, * y;
         VERIFY(bv.is_bv_lshr(n, x, y));
-        m_core.lshr(expr2pdd(n), expr2pdd(x), expr2pdd(y));
+        auto sc = m_core.lshr(expr2pdd(x), expr2pdd(y), expr2pdd(n));
     }
 
     void solver::internalize_shl(app* n) {
         expr* x, * y;
         VERIFY(bv.is_bv_shl(n, x, y));
-        m_core.shl(expr2pdd(n), expr2pdd(x), expr2pdd(y));
+        auto sc = m_core.shl(expr2pdd(x), expr2pdd(y), expr2pdd(n));
     }  
 
     void solver::internalize_urem_i(app* rem) {