integrate polysat into bv solver

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

src/math/polysat/boolean.cpp

@@ -78,13 +78,13 @@ namespace polysat {
         SASSERT(is_propagation(lit));
     }
 
-    void bool_var_manager::asserted(sat::literal lit, unsigned lvl, unsigned dep) {
+    void bool_var_manager::asserted(sat::literal lit, unsigned lvl, dep_t dep) {
         LOG("Asserted " << lit << " @ " << lvl);
         assign(kind_t::decision, lit, lvl, nullptr, dep);
         SASSERT(is_decision(lit));
     }
 
-    void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, unsigned dep) {
+    void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dep_t dep) {
         SASSERT(!is_assigned(lit));
         SASSERT(k != kind_t::unassigned);
         m_value[lit.index()] = l_true;

src/math/polysat/boolean.h

@@ -29,7 +29,7 @@ namespace polysat {
         svector<sat::bool_var>  m_unused;   // previously deleted variables that can be reused by new_var();
         svector<lbool>          m_value;    // current value (indexed by literal)
         unsigned_vector         m_level;    // level of assignment (indexed by variable)
-        unsigned_vector         m_deps;     // dependencies of external asserts
+        svector<dep_t>          m_deps;     // dependencies of external asserts
         unsigned_vector         m_activity; //
         svector<kind_t>         m_kind;     // decision or propagation?
         // Clause associated with the assignment (indexed by variable):
@@ -40,7 +40,7 @@ namespace polysat {
         var_queue                   m_free_vars;  // free Boolean variables
         vector<ptr_vector<clause>>  m_watch;      // watch list for literals into clauses
 
-        void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, unsigned dep = null_dependency);
+        void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dep_t dep = null_dependency);
 
     public:
 
@@ -66,7 +66,7 @@ namespace polysat {
         unsigned level(sat::literal lit) const { return level(lit.var()); }
         clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_propagation(var) ? m_clause[var] : nullptr; }
         clause* reason(sat::literal lit) const { return reason(lit.var()); }
-        unsigned dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; }
+        dep_t dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; }
 
         clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_clause[var]; }
        
@@ -83,7 +83,7 @@ namespace polysat {
         void propagate(sat::literal lit, unsigned lvl, clause& reason);
         void decide(sat::literal lit, unsigned lvl, clause& lemma);
         void eval(sat::literal lit, unsigned lvl);
-        void asserted(sat::literal lit, unsigned lvl, unsigned dep);
+        void asserted(sat::literal lit, unsigned lvl, dep_t dep);
         void unassign(sat::literal lit);
 
         std::ostream& display(std::ostream& out) const;

src/math/polysat/solver.cpp

@@ -83,6 +83,12 @@ namespace polysat {
         return l_undef;
     }
 
+    lbool solver::unit_propagate() {
+        flet<uint64_t> _max_d(m_max_decisions, m_stats.m_num_decisions + 1);
+        return check_sat();
+    }
+
+
     dd::pdd_manager& solver::sz2pdd(unsigned sz) const {
         m_pdd.reserve(sz + 1);
         if (!m_pdd[sz])
@@ -164,7 +170,7 @@ namespace polysat {
     }
 
 
-    void solver::assign_eh(signed_constraint c, unsigned dep) {
+    void solver::assign_eh(signed_constraint c, dep_t dep) {
         SASSERT(at_base_level());
         SASSERT(c);
         if (is_conflict())
@@ -195,6 +201,7 @@ namespace polysat {
         m_linear_solver.new_constraint(*c.get());
 #endif
     }
+    
 
     bool solver::can_propagate() {
         return m_qhead < m_search.size() && !is_conflict();
@@ -592,7 +599,7 @@ namespace polysat {
         SASSERT(!m_conflict.empty());
     }
 
-    void solver::unsat_core(unsigned_vector& deps) {
+    void solver::unsat_core(svector<dep_t>& deps) {
         deps.reset();
         for (auto c : m_conflict) {
             auto d = m_bvars.dep(c.blit());

src/math/polysat/solver.h

@@ -192,8 +192,6 @@ namespace polysat {
         void narrow(pvar v);
         void linear_propagate();
 
-        /// Evaluate term under the current assignment.
-        bool try_eval(pdd const& p, rational& out_value) const;
 
         bool is_conflict() const { return !m_conflict.empty(); }
         bool at_base_level() const;
@@ -231,6 +229,9 @@ namespace polysat {
         bool wlist_invariant();
         bool assignment_invariant();
         bool verify_sat();
+        
+        bool can_propagate();
+        void propagate();
 
     public:
 
@@ -255,7 +256,7 @@ namespace polysat {
         /**
          * retrieve unsat core dependencies
          */
-        void unsat_core(unsigned_vector& deps);
+        void unsat_core(svector<dep_t>& deps);
         
         /**
          * Add variable with bit-size. 
@@ -302,6 +303,11 @@ namespace polysat {
         unsigned get_level(pvar v) const { SASSERT(is_assigned(v)); return m_justification[v].level(); }
 
 
+        /**
+         * Evaluate term under the current assignment.
+         */
+        bool try_eval(pdd const& p, rational& out_value) const;
+
         /** Create constraints */
         signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }
         signed_constraint diseq(pdd const& p) { return ~m_constraints.eq(p); }
@@ -325,39 +331,38 @@ namespace polysat {
         signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
 
         /** Create and activate polynomial constraints. */
-        void add_eq(pdd const& p, unsigned dep = null_dependency)                { assign_eh(eq(p), dep); }
-        void add_diseq(pdd const& p, unsigned dep = null_dependency)             { assign_eh(diseq(p), dep); }
-        void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(ule(p, q), dep); }
-        void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(ult(p, q), dep); }
-        void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(sle(p, q), dep); }
-        void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(slt(p, q), dep); }
-        void add_noovfl(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); }
-        void add_ovfl(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); }
+        void add_eq(pdd const& p, dep_t dep = null_dependency)                { assign_eh(eq(p), dep); }
+        void add_diseq(pdd const& p, dep_t dep = null_dependency)             { assign_eh(diseq(p), dep); }
+        void add_ule(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(ule(p, q), dep); }
+        void add_ult(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(ult(p, q), dep); }
+        void add_sle(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(sle(p, q), dep); }
+        void add_slt(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(slt(p, q), dep); }
+        void add_noovfl(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); }
+        void add_ovfl(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); }
 
-        void add_ule(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); }
-        void add_ule(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); }
-        void add_ule(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_ule(p, rational(q), dep); }
-        void add_ule(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_ule(rational(p), q, dep); }
-        void add_ult(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_ult(p, p.manager().mk_val(q), dep); }
-        void add_ult(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); }
-        void add_ult(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_ult(p, rational(q), dep); }
-        void add_ult(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_ult(rational(p), q, dep); }
-        void add_noovfl(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); }
-        void add_noovfl(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, dep); }
-        void add_noovfl(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_noovfl(p, rational(q), dep); }
-        void add_noovfl(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, dep); }
+        void add_ule(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); }
+        void add_ule(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); }
+        void add_ule(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_ule(p, rational(q), dep); }
+        void add_ule(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_ule(rational(p), q, dep); }
+        void add_ult(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_ult(p, p.manager().mk_val(q), dep); }
+        void add_ult(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); }
+        void add_ult(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_ult(p, rational(q), dep); }
+        void add_ult(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_ult(rational(p), q, dep); }
+        void add_noovfl(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); }
+        void add_noovfl(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_noovfl(q, p, dep); }
+        void add_noovfl(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_noovfl(p, rational(q), dep); }
+        void add_noovfl(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_noovfl(q, p, dep); }
 
         /**
          * Activate the constraint corresponding to the given boolean variable.
          * Note: to deactivate, use push/pop.
          */
-        void assign_eh(signed_constraint c, unsigned dep);
+        void assign_eh(signed_constraint c, dep_t dep);
 
         /**
-         * main state transitions.
+         * Unit propagation accessible over API.
          */
-        bool can_propagate();
-        void propagate();
+        lbool unit_propagate();
 
         /**
          * External context managment.

src/math/polysat/types.h

@@ -29,8 +29,8 @@ namespace polysat {
     typedef dd::bdd bdd;
     typedef dd::bddv bddv;
     typedef unsigned pvar;
-
-    const unsigned null_dependency = UINT_MAX;
+    typedef unsigned dep_t;
+    const dep_t null_dependency = std::numeric_limits<unsigned>::max();;
     const pvar null_var = UINT_MAX;
 
 }

src/sat/smt/CMakeLists.txt

@@ -14,6 +14,7 @@ z3_add_component(sat_smt
     bv_delay_internalize.cpp
     bv_internalize.cpp
     bv_invariant.cpp
+    bv_polysat.cpp
     bv_solver.cpp
     dt_solver.cpp
     euf_ackerman.cpp
@@ -46,5 +47,6 @@ z3_add_component(sat_smt
     euf
     mbp
     smt_params
+    polysat
 )
 

src/sat/smt/bv_delay_internalize.cpp

@@ -357,28 +357,12 @@ namespace bv {
     }
 
     solver::internalize_mode solver::get_internalize_mode(expr* e) {
-        if (!bv.is_bv(e))
-            return internalize_mode::no_delay_i;
         if (!reflect())
             return internalize_mode::no_delay_i;
-        if (get_config().m_bv_polysat) {
-            switch (to_app(e)->get_decl_kind()) {
-            case OP_BMUL: 
-            case OP_BUMUL_NO_OVFL:
-            case OP_BSMOD_I:
-            case OP_BUREM_I:
-            case OP_BUDIV_I:
-            case OP_BADD:
-                return internalize_mode::polysat_i;
-            case OP_BSMUL_NO_OVFL:
-            case OP_BSMUL_NO_UDFL:
-            case OP_BSDIV_I: 
-            case OP_BSREM_I:
-            default:
-                return internalize_mode::no_delay_i;
-            }
-        }
-
+        if (get_config().m_bv_polysat)
+            return internalize_mode::polysat_i;
+        if (!bv.is_bv(e))
+            return internalize_mode::no_delay_i;
         if (!get_config().m_bv_delay)
             return internalize_mode::no_delay_i;
         internalize_mode mode;

src/sat/smt/bv_internalize.cpp

@@ -96,6 +96,8 @@ namespace bv {
 
     void solver::apply_sort_cnstr(euf::enode * n, sort * s) {
         force_push();
+        if (polysat_sort_cnstr(n))
+            return;
         get_var(n);
     }
 
@@ -149,7 +151,7 @@ namespace bv {
             internalize_circuit(a);
             break;
         case internalize_mode::polysat_i:
-            NOT_IMPLEMENTED_YET();
+            internalize_polysat(a);
             break;
         default:
             mk_bits(n->get_th_var(get_id()));
@@ -351,8 +353,8 @@ namespace bv {
             for (expr* bit : bits) {
                 sat::literal lit = ctx.internalize(bit, false, false, m_is_redundant);
                 TRACE("bv", tout << "set " << m_bits[v][i] << " == " << lit << "\n";);
-                add_clause(~lit, m_bits[v][i]);
-                add_clause(lit, ~m_bits[v][i]);
+                add_equiv(lit, m_bits[v][i]);
+                ctx.add_aux_equiv(lit, m_bits[v][i]);
                 ++i;
             }
             return;
@@ -545,8 +547,8 @@ namespace bv {
 	    unsigned sz = bv.get_bv_size(n);
 	    expr_ref zero(bv.mk_numeral(0, sz), m);
 	    sat::literal eqZ = eq_internalize(arg2, zero);
-	    sat::literal eqU = mk_literal(iun(arg1));
-	    sat::literal eqI = mk_literal(ibin(arg1, arg2));
+	    sat::literal eqU = eq_internalize(n, iun(arg1));
+	    sat::literal eqI = eq_internalize(n, ibin(arg1, arg2));
 	    add_clause(~eqZ, eqU);
 	    add_clause(eqZ, eqI);
 	    ctx.add_aux(~eqZ, eqU);
@@ -676,12 +678,13 @@ namespace bv {
             TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";);
             atom* a = new (get_region()) atom(lit.var());
             a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
+            polysat_bit2bool(a, arg, idx);
             insert_bv2a(lit.var(), a);
             ctx.push(mk_atom_trail(lit.var(), *this));
         }
         else if (lit != lit0) {
-            add_clause(lit0, ~lit);
-            add_clause(~lit0, lit);
+            add_equiv(lit0, lit);
+            ctx.add_aux_equiv(lit0, lit);
         }
 
         // validate_atoms();

src/sat/smt/bv_polysat.cpp

@@ -0,0 +1,324 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    bv_polysat.cpp
+
+Abstract:
+
+    PolySAT interface to bit-vector
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-01-26
+
+Notes:
+- equality propagation from polysat?
+- reuse bit propagation from bv-solver?
+- finish other bit-vector operations
+- introduce gradual bit-blasting?
+
+--*/
+
+#include "params/bv_rewriter_params.hpp"
+#include "sat/smt/bv_solver.h"
+#include "sat/smt/euf_solver.h"
+#include "math/polysat/solver.h"
+
+namespace bv {
+
+    typedef polysat::pdd pdd;
+
+    void solver::internalize_polysat(app* a) {
+
+        std::function<polysat::pdd(polysat::pdd, polysat::pdd)> bin;
+
+#define mk_binary(a, fn) bin = fn; polysat_binary(a, bin);
+
+        switch (to_app(a)->get_decl_kind()) {
+        case OP_BMUL:             mk_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break;
+        case OP_BADD:             mk_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break;
+        case OP_BSUB:             mk_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break;
+        case OP_BLSHR:            mk_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.lshr(p, q); }); break;
+        case OP_BAND:             mk_binary(a, [&](pdd const& p, pdd const& q) { return m_polysat.band(p, q); }); break;
+
+        case OP_BNEG:             polysat_neg(a); break;            
+        case OP_MKBV:             polysat_mkbv(a); break;
+        case OP_BV_NUM:           polysat_num(a); break;
+            
+        case OP_ULEQ:             polysat_le<false, false, false>(a); break;
+        case OP_SLEQ:             polysat_le<true,  false, false>(a); break;
+        case OP_UGEQ:             polysat_le<false, true,  false>(a); break;
+        case OP_SGEQ:             polysat_le<true,  true,  false>(a); break;
+        case OP_ULT:              polysat_le<false, true,  true>(a); break;
+        case OP_SLT:              polysat_le<true,  true,  true>(a); break;
+        case OP_UGT:              polysat_le<false, false, true>(a); break;
+        case OP_SGT:              polysat_le<true,  false, true>(a); break;
+
+        case OP_BUMUL_NO_OVFL:    polysat_umul_noovfl(a); break;
+        case OP_BUDIV_I:          polysat_div_rem_i(a, true); break;       
+        case OP_BUREM_I:          polysat_div_rem_i(a, false); break;
+
+        case OP_BUDIV:            polysat_div_rem(a, true); break;            
+        case OP_BUREM:            polysat_div_rem(a, false); break;
+        case OP_BSDIV0:           break;
+        case OP_BUDIV0:           break;
+        case OP_BSREM0:           break;
+        case OP_BUREM0:           break;
+        case OP_BSMOD0:           break;
+
+            // polysat::solver should also support at least:
+        case OP_BREDAND: // x == 2^K - 1
+        case OP_BREDOR:  // x > 0
+        case OP_BSDIV:            
+        case OP_BSREM:            
+        case OP_BSMOD:                        
+        case OP_BSMUL_NO_OVFL:    
+        case OP_BSMUL_NO_UDFL:    
+        case OP_BSDIV_I:            
+        case OP_BSREM_I:                        
+        case OP_BSMOD_I:
+        case OP_BSHL:            
+        case OP_BASHR:
+        case OP_BOR:
+        case OP_BXOR:
+        case OP_BNAND:
+        case OP_BNOR:
+        case OP_BNOT:
+        case OP_BCOMP:
+        case OP_SIGN_EXT:
+        case OP_ZERO_EXT:
+        case OP_CONCAT:
+        case OP_EXTRACT:
+            std::cout << mk_pp(a, m) << "\n";
+            NOT_IMPLEMENTED_YET();
+            return;
+        default:
+            std::cout << "fall back to circuit " << mk_pp(a, m) << "\n";
+            internalize_circuit(a);
+            break;            
+        }
+    }
+
+    void solver::polysat_umul_noovfl(app* e) {
+        auto p = expr2pdd(e->get_arg(0));
+        auto q = expr2pdd(e->get_arg(1));
+        auto sc = ~m_polysat.mul_ovfl(p, q);
+        sat::literal lit = expr2literal(e);
+        atom* a = mk_atom(lit.var());
+        a->m_sc = sc;
+    }
+
+    void solver::polysat_div_rem_i(app* e, bool is_div) {
+        auto p = expr2pdd(e->get_arg(0));
+        auto q = expr2pdd(e->get_arg(1));
+        auto [quot, rem] = m_polysat.quot_rem(p, q);
+        polysat_set(e, is_div ? quot : rem);        
+    }
+
+    void solver::polysat_div_rem(app* e, bool is_div) {
+        bv_rewriter_params p(s().params());
+        if (p.hi_div0()) {
+            polysat_div_rem_i(e, is_div);
+            return;
+        }        
+        expr* arg1 = e->get_arg(0);
+        expr* arg2 = e->get_arg(1);
+        unsigned sz = bv.get_bv_size(e);
+        expr_ref zero(bv.mk_numeral(0, sz), m);
+        sat::literal eqZ = eq_internalize(arg2, zero);
+        sat::literal eqU = eq_internalize(e, is_div ? bv.mk_bv_udiv0(arg1) : bv.mk_bv_urem0(arg1));
+        sat::literal eqI = eq_internalize(e, is_div ? bv.mk_bv_udiv_i(arg1, arg2) : bv.mk_bv_urem_i(arg1, arg2));
+        add_clause(~eqZ, eqU);
+        add_clause(eqZ, eqI);
+        ctx.add_aux(~eqZ, eqU);
+        ctx.add_aux(eqZ, eqI);        
+    }
+
+    void solver::polysat_neg(app* e) {
+        SASSERT(e->get_num_args() == 1);
+        auto p = expr2pdd(e->get_arg(0));
+        polysat_set(e, -p);
+    }
+
+    void solver::polysat_num(app* a) {
+        numeral val;
+        unsigned sz = 0;
+        VERIFY(bv.is_numeral(a, val, sz));
+        auto p = m_polysat.value(val, sz);
+        polysat_set(a, p);
+    }
+
+    // TODO - test that internalize works with recursive call on bit2bool
+    void solver::polysat_mkbv(app* a) {
+        unsigned i = 0;
+        for (expr* arg : *a) {
+            expr_ref b2b(m);
+            b2b = bv.mk_bit2bool(a, i);            
+            sat::literal bit_i = ctx.internalize(b2b, false, false, m_is_redundant);
+            sat::literal lit = expr2literal(arg);
+            add_equiv(lit, bit_i);
+            ctx.add_aux_equiv(lit, bit_i);
+            ++i;
+        }
+    }
+
+    void solver::polysat_binary(app* e, std::function<polysat::pdd(polysat::pdd, polysat::pdd)>& fn) {
+        SASSERT(e->get_num_args() >= 1);
+        auto p = expr2pdd(e->get_arg(0));
+        for (unsigned i = 1; i < e->get_num_args(); ++i) 
+            p = fn(p, expr2pdd(e->get_arg(i)));
+        polysat_set(e, p);
+    }
+
+    template<bool Signed, bool Rev, bool Negated>
+    void solver::polysat_le(app* e) {
+        auto p = expr2pdd(e->get_arg(0));
+        auto q = expr2pdd(e->get_arg(1));
+        if (Rev)
+            std::swap(p, q);
+        
+        auto sc = Signed ? m_polysat.sle(p, q) : m_polysat.ule(p, q);
+        if (Negated)
+            sc = ~sc;
+        
+        sat::literal lit = expr2literal(e);
+        atom* a = mk_atom(lit.var());
+        a->m_sc = sc;
+    }
+
+    void solver::polysat_bit2bool(atom* a, expr* e, unsigned idx) {
+        if (!use_polysat())
+            return;
+        pdd p = expr2pdd(e);
+        a->m_sc = m_polysat.bit(p, idx);
+    }
+
+    void solver::polysat_assign(atom* a) {
+        polysat::signed_constraint sc = a->m_sc;
+        if (!sc)
+            return;
+        SASSERT(s().value(a->m_bv) != l_undef);
+        bool sign = l_false == s().value(a->m_bv);
+        sat::literal lit(a->m_bv, sign);
+        if (sign)
+            sc = ~sc;
+        m_polysat.assign_eh(sc, 1 + 2*lit.index());
+    }
+
+    bool solver::polysat_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
+        if (!use_polysat())
+            return false;
+        pdd p = var2pdd(r1);
+        pdd q = var2pdd(r2);
+        auto sc = m_polysat.eq(p, q);
+        m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2));
+        ctx.push(value_trail<unsigned>(m_var_eqs_head));        
+        m_polysat.assign_eh(sc, 2 * m_var_eqs_head); 
+        m_var_eqs_head++;
+        return true;
+    }
+
+    bool solver::polysat_diseq_eh(euf::th_eq const& ne) {
+        euf::theory_var v1 = ne.v1(), v2 = ne.v2();
+        pdd p = var2pdd(v1);
+        pdd q = var2pdd(v2);
+        auto sc = ~m_polysat.eq(p, q);
+        sat::literal neq = ~expr2literal(ne.eq());
+        m_polysat.assign_eh(sc, 1 + 2 * neq.index());
+        return true;
+    }
+
+    void solver::polysat_propagate() {
+        if (!use_polysat())
+            return;
+        lbool r = m_polysat.unit_propagate();
+        if (r == l_false)
+            polysat_core();
+    }
+
+    lbool solver::polysat_final() {
+        if (!use_polysat())
+            return l_true;
+        lbool r = m_polysat.check_sat();
+        if (r == l_false) 
+            polysat_core();
+        return r;
+    }
+
+    void solver::polysat_core() {
+        svector<polysat::dep_t> deps;
+        sat::literal_vector core;
+        euf::enode_pair_vector eqs;
+        m_polysat.unsat_core(deps);
+        for (auto n : deps) {
+            if (0 != (n & 1))
+                core.push_back(sat::to_literal(n / 2));
+            else {
+                auto [v1, v2] = m_var_eqs[n / 2];
+                eqs.push_back(euf::enode_pair(var2enode(v1), var2enode(v2)));
+            }
+        }
+        auto* ex = euf::th_explain::conflict(*this, core, eqs);
+        ctx.set_conflict(ex);
+    }
+
+    polysat::pdd solver::expr2pdd(expr* e) {
+        return var2pdd(get_th_var(e));
+    }
+
+    polysat::pdd solver::var2pdd(euf::theory_var v) {
+        if (!m_var2pdd_valid.get(v, false)) {
+            unsigned bv_size = get_bv_size(v);
+            polysat::pvar pv = m_polysat.add_var(bv_size);
+            m_pddvar2var.setx(pv, v, UINT_MAX);
+            pdd p = m_polysat.var(pv);
+            polysat_set(v, p);
+            return p;
+        }
+        return m_var2pdd[v];
+    }
+
+    bool solver::polysat_sort_cnstr(euf::enode* n) {
+        if (!use_polysat())
+            return false;
+        if (!bv.is_bv(n->get_expr()))
+            return false;
+        theory_var v = n->get_th_var(get_id());
+        if (v == euf::null_theory_var) 
+            v = mk_var(n);
+        var2pdd(v);
+        return true;
+    }
+
+    void solver::polysat_set(expr* e, pdd const& p) {
+        polysat_set(get_th_var(e), p);
+    }
+
+    void solver::polysat_set(euf::theory_var v, pdd const& p) {
+        m_var2pdd.reserve(get_num_vars(), p);
+        m_var2pdd_valid.reserve(get_num_vars(), false);
+        ctx.push(set_bitvector_trail(m_var2pdd_valid, v));
+        m_var2pdd[v] = p;        
+    }
+
+    void solver::polysat_pop(unsigned n) {
+        if (!use_polysat())
+            return;
+        m_polysat.pop(n);
+    }
+
+    void solver::polysat_push() {
+        if (!use_polysat())
+            return;
+        m_polysat.push();
+    }
+
+    void solver::polysat_add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
+        auto p = expr2pdd(n->get_expr());
+        rational val;
+        VERIFY(m_polysat.try_eval(p, val));
+        values[n->get_root_id()] = bv.mk_numeral(val, get_bv_size(n));        
+    }   
+}

src/sat/smt/bv_solver.cpp

@@ -52,6 +52,7 @@ namespace bv {
         euf::th_euf_solver(ctx, symbol("bv"), id),
         bv(m),
         m_autil(m),
+        m_polysat(m.limit()),
         m_ackerman(*this),
         m_bb(m, get_config()),
         m_find(*this) {
@@ -217,6 +218,8 @@ namespace bv {
             return;
         if (s().is_probing())
             return;
+        if (polysat_diseq_eh(ne))
+            return;
         
         TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";);
         unsigned sz = m_bits[v1].size();
@@ -400,9 +403,8 @@ namespace bv {
         if (a) {
             force_push();
             m_prop_queue.push_back(propagation_item(a));            
-            for (auto p : a->m_bit2occ) {
-                del_eq_occurs(p.first, p.second);
-            }
+            for (auto p : a->m_bit2occ) 
+                del_eq_occurs(p.first, p.second);            
         }
     }
 
@@ -417,11 +419,13 @@ namespace bv {
                 for (auto vp : *p.m_atom)
                     propagate_bits(vp);
                 for (eq_occurs const& eq : p.m_atom->eqs()) 
-                    propagate_eq_occurs(eq);                
+                    propagate_eq_occurs(eq);
+                polysat_assign(p.m_atom);
             }
             else 
                 propagate_bits(p.m_vp);            
         }
+        polysat_propagate();
         // check_missing_propagation();
         return true;
     }
@@ -521,13 +525,19 @@ namespace bv {
         
         if (!ok)
             return sat::check_result::CR_CONTINUE;
-        return sat::check_result::CR_DONE;
+
+        switch (polysat_final()) {
+        case l_true: return sat::check_result::CR_DONE;
+        case l_false: return sat::check_result::CR_CONTINUE;
+        default: return sat::check_result::CR_GIVEUP;
+        }
     }
 
     void solver::push_core() {
         TRACE("bv", tout << "push: " << get_num_vars() << "@" << m_prop_queue_lim.size() << "\n";);
         th_euf_solver::push_core();
         m_prop_queue_lim.push_back(m_prop_queue.size());
+        polysat_push();
     }
 
     void solver::pop_core(unsigned n) {
@@ -540,6 +550,8 @@ namespace bv {
         m_bits.shrink(old_sz);
         m_wpos.shrink(old_sz);
         m_zero_one_bits.shrink(old_sz);
+        polysat_pop(n);
+        
         TRACE("bv", tout << "num vars " << old_sz << "@" << m_prop_queue_lim.size() << "\n";);
     }
 
@@ -605,10 +617,13 @@ namespace bv {
     lbool solver::get_phase(bool_var v) { return l_undef; }
     std::ostream& solver::display(std::ostream& out) const {
         unsigned num_vars = get_num_vars();
-        if (num_vars > 0)
-            out << "bv-solver:\n";
+        if (num_vars == 0)
+            return out;
+        out << "bv-solver:\n";
         for (unsigned v = 0; v < num_vars; v++)
             out << pp(v);
+        if (use_polysat())
+            m_polysat.display(out);
         return out;
     }
 
@@ -662,6 +677,7 @@ namespace bv {
         st.update("bv bit2eq", m_stats.m_num_bit2eq);
         st.update("bv bit2ne", m_stats.m_num_bit2ne);
         st.update("bv ackerman", m_stats.m_ackerman);
+        m_polysat.collect_statistics(st);
     }
 
     sat::extension* solver::copy(sat::solver* s) { UNREACHABLE(); return nullptr; }
@@ -727,6 +743,10 @@ namespace bv {
             return;
         }
         theory_var v = n->get_th_var(get_id());
+        if (m_bits[v].empty() && use_polysat()) {
+            polysat_add_value(n, mdl, values);
+            return;
+        }
         rational val;
         unsigned i = 0;
         for (auto l : m_bits[v]) {
@@ -748,6 +768,9 @@ namespace bv {
 
     void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
 
+        if (polysat_merge_eh(r1, r2, v1, v2))
+            return;
+
         TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";);
 
         if (!merge_zero_one_bits(r1, r2)) {

src/sat/smt/bv_solver.h

@@ -19,6 +19,7 @@ Author:
 #include "sat/smt/sat_th.h"
 #include "sat/smt/bv_ackerman.h"
 #include "ast/rewriter/bit_blaster/bit_blaster.h"
+#include "math/polysat/solver.h"
 
 namespace euf {
     class solver;
@@ -166,6 +167,7 @@ namespace bv {
             svector<std::pair<atom*, eq_occurs*>> m_bit2occ;
             literal    m_var = sat::null_literal;
             literal    m_def = sat::null_literal;
+            polysat::signed_constraint m_sc;
             atom(bool_var b) :m_bv(b), m_eqs(nullptr), m_occs(nullptr) {}
             ~atom() { m_bit2occ.clear(); }
             var_pos_it begin() const { return var_pos_it(m_occs); }
@@ -194,6 +196,7 @@ namespace bv {
 
         bv_util                  bv;
         arith_util               m_autil;
+        polysat::solver          m_polysat;
         stats                    m_stats;
         ackerman                 m_ackerman;
         bit_blaster              m_bb;
@@ -232,7 +235,7 @@ namespace bv {
         void add_bit(theory_var v, sat::literal lit);
         atom* mk_atom(sat::bool_var b);
         void eq_internalized(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, sat::literal eq, euf::enode* n);
-        void del_eq_occurs(atom* a, eq_occurs* occ);
+        void del_eq_occurs(atom* a, eq_occurs* occ);        
 
         void set_bit_eh(theory_var v, literal l, unsigned idx);
         void init_bits(expr* e, expr_ref_vector const & bits);
@@ -263,6 +266,39 @@ namespace bv {
         void assert_ackerman(theory_var v1, theory_var v2);
         bool reflect() const { return get_config().m_bv_reflect; }
 
+        // polysat
+        void internalize_polysat(app* a);
+        void polysat_push();
+        void polysat_pop(unsigned n);
+        void polysat_binary(app* e, std::function<polysat::pdd(polysat::pdd, polysat::pdd)>& fn);
+        polysat::pdd expr2pdd(expr* e);
+        void polysat_set(euf::theory_var v, polysat::pdd const& p);
+        polysat::pdd var2pdd(euf::theory_var v);
+        void polysat_set(expr* e, polysat::pdd const& p);
+        template<bool Signed, bool Reverse, bool Negated>
+        void polysat_le(app* n);
+        void polysat_neg(app* a);
+        void polysat_num(app* a);
+        void polysat_mkbv(app* a);
+        void solver::polysat_umul_noovfl(app* e);
+        void solver::polysat_div_rem_i(app* e, bool is_div);
+        void solver::polysat_div_rem(app* e, bool is_div);
+        void polysat_bit2bool(atom* a, expr* e, unsigned idx);
+        bool polysat_sort_cnstr(euf::enode* n);
+        void polysat_assign(atom* a);
+        void polysat_propagate();
+        void polysat_core();
+        bool polysat_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2);
+        bool polysat_diseq_eh(euf::th_eq const& ne);
+        void polysat_add_value(euf::enode* n, model& mdl, expr_ref_vector& values);
+        lbool polysat_final();
+        bool use_polysat() const { return get_config().m_bv_polysat; }
+        vector<polysat::pdd> m_var2pdd;
+        bool_vector          m_var2pdd_valid;
+        unsigned_vector      m_pddvar2var;
+        svector<std::pair<euf::theory_var, euf::theory_var>> m_var_eqs;
+        unsigned             m_var_eqs_head = 0;
+
         // delay internalize
         enum class internalize_mode {
             delay_i,

src/sat/smt/euf_solver.h

@@ -384,6 +384,7 @@ namespace euf {
         void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); }
         void add_aux(unsigned n, sat::literal const* lits) { m_relevancy.add_def(n, lits); }
         void add_aux(sat::literal a) { sat::literal lits[1] = { a }; add_aux(1, lits); }
+        void add_aux_equiv(sat::literal a, sat::literal b) { add_aux(~a, b); add_aux(a, ~b); }
         void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } 
         void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); }
         void mark_relevant(sat::literal lit) { m_relevancy.mark_relevant(lit); }

src/smt/params/smt_params_helper.pyg

@@ -50,7 +50,7 @@ def_module_params(module_name='smt',
 	                  ('bv.eq_axioms', BOOL, True, 'add dynamic equality axioms'),
                           ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'),
                           ('bv.delay', BOOL, True, 'delay internalize expensive bit-vector operations'),
-			  ('bv.polysat', BOOL, True, 'use polysat bit-vector solver'),
+			  ('bv.polysat', BOOL, False, 'use polysat bit-vector solver'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
                           ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),

src/smt/params/theory_bv_params.h

@@ -36,7 +36,7 @@ struct theory_bv_params {
     bool         m_bv_enable_int2bv2int = true;
     bool         m_bv_watch_diseq = false;
     bool         m_bv_delay = true;
-    bool         m_bv_polysat = true;
+    bool         m_bv_polysat = false;
     theory_bv_params(params_ref const & p = params_ref()) {
         updt_params(p);
     }