refactor polysat core / solver interface

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

src/sat/smt/polysat/core.cpp

@@ -69,19 +69,29 @@ namespace polysat {
         void undo() override {            
             auto& [sc, lit, val] = c.m_constraint_index.back();
             auto& vars = sc.vars();
+            auto idx = c.m_constraint_index.size() - 1;
             IF_VERBOSE(10, 
             verbose_stream() << "undo add watch " << sc << " ";
-            if (vars.size() > 0) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[0]] << ") ";
+            if (vars.size() > 0) verbose_stream() << "(" << idx << ": " << c.m_watch[vars[0]] << ") ";
-            if (vars.size() > 1) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[1]] << ") ";
+            if (vars.size() > 1) verbose_stream() << "(" << idx<< ": " << c.m_watch[vars[1]] << ") ";
             verbose_stream() << "\n");
             unsigned n = sc.num_watch();
             SASSERT(n <= vars.size());
-            SASSERT(n <= 0 || c.m_watch[vars[0]].back() == c.m_constraint_index.size() - 1);
+            auto del_watch = [&](unsigned i) {
-            SASSERT(n <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1);
+                auto& w = c.m_watch[vars[i]];
-            if (n > 0)
+                for (unsigned j = w.size(); j-- > 0;) {
-                c.m_watch[vars[0]].pop_back();
+                    if (w[j] == idx) {
+                        std::swap(w[w.size() - 1], w[j]);
+                        w.pop_back();
+                        return;
+                    }
+                }
+                UNREACHABLE();
+            };
+            if (n > 0) 
+                del_watch(0);
             if (n > 1)
-                c.m_watch[vars[1]].pop_back();
+                del_watch(1);
             c.m_constraint_index.pop_back();
         }
     };
@@ -132,7 +142,7 @@ namespace polysat {
         m_var_queue.del_var_eh(v);
     }
 
-    unsigned core::register_constraint(signed_constraint& sc, dependency d) {
+    constraint_id core::register_constraint(signed_constraint& sc, dependency d) {
         unsigned idx = m_constraint_index.size();
         m_constraint_index.push_back({ sc, d, l_undef });
         auto& vars = sc.vars();
@@ -150,7 +160,7 @@ namespace polysat {
                     if (j > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") ";
                     verbose_stream() << "\n");
         s.trail().push(mk_add_watch(*this));
-        return idx;
+        return { idx };
     }
 
     // case split on unassigned variables until all are assigned values.
@@ -202,9 +212,11 @@ namespace polysat {
         return sc;
     }
 
-    void core::propagate_assignment(prop_item& dc) { 
+    void core::propagate_assignment(constraint_id idx) { 
-        auto [idx, sign, dep] = dc;
+        auto [sc, dep, value] = m_constraint_index[idx.id];
-        auto sc = get_constraint(idx, sign);
+        SASSERT(value != l_undef);
+        if (value == l_false)
+            sc = ~sc;
         if (sc.is_eq(m_var, m_value))
             propagate_assignment(m_var, m_value, dep);
         else 
@@ -252,7 +264,9 @@ namespace polysat {
             // this can create fresh literals and update m_watch, but
             // will not update m_watch[v] (other than copy constructor for m_watch)
             // because v has been assigned a value.
-            sc.propagate(*this, value, dep);
+            propagate(sc, value, dep);
+            if (s.inconsistent())
+                return;
            
             SASSERT(!swapped || vars.size() <= 1 || (!is_assigned(vars[0]) && !is_assigned(vars[1])));
             if (swapped)
@@ -272,30 +286,17 @@ namespace polysat {
         verbose_stream() << "new watch " << v << ": " << m_watch[v] << "\n";
     }
 
-    void core::propagate_value(prop_item const& dc) {
+    void core::propagate_value(constraint_id idx) {
-        auto [idx, sign, dep] = dc;
+        auto [sc, d, value] = m_constraint_index[idx.id];
-        auto sc = get_constraint(idx, sign);
-        // check if sc evaluates to false
-        switch (eval(sc)) {
-        case l_true:
-            break;
-        case l_false:
-            m_unsat_core = explain_eval(sc);
-            m_unsat_core.push_back(dep);
-            propagate_unsat_core();
-            return;
-        default:
-            break;
-        }
         // propagate current assignment for sc
-        sc.propagate(*this, to_lbool(!sign), dep);
+        propagate(sc, value, d);
         if (s.inconsistent())
             return;
 
         // if sc is v == value, then check the watch list for v to propagate truth assignments
         if (sc.is_eq(m_var, m_value)) {
             for (auto idx1 : m_watch[m_var]) {
-                if (idx == idx1)
+                if (idx.id == idx1)
                     continue;
                 auto [sc, d, value] = m_constraint_index[idx1];
                 switch (eval(sc)) {
@@ -312,6 +313,19 @@ namespace polysat {
         }       
     }
 
+    void core::propagate(signed_constraint& sc, lbool value, dependency const& d) {
+        lbool eval_value = eval(sc);
+        if (eval_value == l_undef)
+            sc.propagate(*this, value, d);
+        else if (value == l_undef)
+            s.propagate(d, eval_value != l_true, explain_eval(sc));
+        else if (value != eval_value) {
+            m_unsat_core = explain_eval(sc);
+            m_unsat_core.push_back(value == l_false ? ~d : d);
+            propagate_unsat_core();
+        }                   
+    }
+
     void core::get_bitvector_prefixes(pvar v, pvar_vector& out) {
         s.get_bitvector_prefixes(v, out);
     }
@@ -331,7 +345,7 @@ namespace polysat {
         s.set_conflict(m_unsat_core);       
     }
 
-    void core::assign_eh(unsigned index, bool sign, dependency const& dep) { 
+    void core::assign_eh(constraint_id index, bool sign, unsigned level) { 
         struct unassign : public trail {
             core& c;
             unsigned m_index;
@@ -341,9 +355,10 @@ namespace polysat {
                 c.m_prop_queue.pop_back();
             }
         };
-        m_prop_queue.push_back({ index, sign, dep });
+        m_prop_queue.push_back(index);
-        m_constraint_index[index].value = to_lbool(!sign);
+        m_constraint_index[index.id].value = to_lbool(!sign);
-        s.trail().push(unassign(*this, index));
+        m_constraint_index[index.id].d.set_level(level);
+        s.trail().push(unassign(*this, index.id));
     }
 
     dependency_vector core::explain_eval(signed_constraint const& sc) { 
@@ -392,7 +407,7 @@ namespace polysat {
 
     void core::add_axiom(signed_constraint sc) {
         auto idx = register_constraint(sc, dependency::axiom());
-        assign_eh(idx, false, dependency::axiom());
+        assign_eh(idx, false, 0);
     }
 
     void core::add_clause(char const* name, core_vector const& cs, bool is_redundant) {

src/sat/smt/polysat/core.h

@@ -37,7 +37,6 @@ namespace polysat {
         class mk_assign_var;
         class mk_add_watch;
         typedef svector<std::pair<unsigned, unsigned>> activity;
-        typedef std::tuple<unsigned, bool, dependency> prop_item;
         friend class viable;
         friend class constraints;
         friend class assignment;
@@ -53,7 +52,7 @@ namespace polysat {
         constraints m_constraints;
         assignment m_assignment;
         unsigned m_qhead = 0, m_vqhead = 0;
-        svector<prop_item> m_prop_queue;
+        svector<constraint_id> m_prop_queue;
         svector<constraint_info> m_constraint_index;  // index of constraints
         dependency_vector m_unsat_core;
 
@@ -76,17 +75,16 @@ namespace polysat {
         void del_var();
 
         bool is_assigned(pvar v) { return !m_justification[v].is_null(); }
-        void propagate_value(prop_item const& dc);
+        void propagate_value(constraint_id idx);
-        void propagate_assignment(prop_item& dc);
+        void propagate_assignment(constraint_id idx);
         void propagate_assignment(pvar v, rational const& value, dependency dep);
         void propagate_unsat_core();
+        void propagate(signed_constraint& sc, lbool value, dependency const& d);
 
         void get_bitvector_prefixes(pvar v, pvar_vector& out);
         void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits);
         bool inconsistent() const;
 
-
-
         void add_watch(unsigned idx, unsigned var);
 
         signed_constraint get_constraint(unsigned idx, bool sign);
@@ -100,9 +98,9 @@ namespace polysat {
         core(solver_interface& s);
 
         sat::check_result check();        
-        unsigned register_constraint(signed_constraint& sc, dependency d);
+        constraint_id register_constraint(signed_constraint& sc, dependency d);
         bool propagate();
-        void assign_eh(unsigned idx, bool sign, dependency const& d);
+        void assign_eh(constraint_id idx, bool sign, unsigned level);
 
         pdd value(rational const& v, unsigned sz);
         pdd subst(pdd const&);

src/sat/smt/polysat/types.h

@@ -22,6 +22,7 @@ namespace polysat {
     using pdd = dd::pdd;
     using pvar = unsigned;
     using theory_var = unsigned;
+    struct constraint_id { unsigned id; };
 
     using pvar_vector = unsigned_vector;
     inline const pvar null_var = UINT_MAX;
@@ -44,6 +45,8 @@ namespace polysat {
         sat::literal literal() const { SASSERT(is_literal()); return *std::get_if<sat::literal>(&m_data); }
         std::pair<theory_var, theory_var> eq() const { SASSERT(!is_literal()); return *std::get_if<std::pair<theory_var, theory_var>>(&m_data); }
         unsigned level() const { return m_level; }
+        void set_level(unsigned level) { m_level = level; }
+        dependency operator~() const { SASSERT(is_literal()); return dependency(~literal(), level()); }
     };
 
     inline const dependency null_dependency = dependency(sat::null_literal, UINT_MAX);

src/sat/smt/polysat/umul_ovfl_constraint.cpp

@@ -97,7 +97,7 @@ namespace polysat {
 
         if (!p.is_val())
             return false;
-        VERIFY(!p.is_zero() && !p.is_one());  // evaluation should catch this case
+        SASSERT(!p.is_zero() && !p.is_one());  // evaluation should catch this case
 
         rational const& M = p.manager().two_to_N();
         auto& C = c.cs();

src/sat/smt/polysat_solver.cpp

@@ -91,7 +91,7 @@ namespace polysat {
         if (!a)
             return;
         force_push();
-        m_core.assign_eh(a->m_index, l.sign(), dependency(l, s().lvl(l)));
+        m_core.assign_eh(a->m_index, l.sign(), s().lvl(l));
     }
 
     void solver::set_conflict(dependency_vector const& core) {
@@ -115,17 +115,18 @@ namespace polysat {
                 eqs.push_back(euf::enode_pair(n1, n2));
             }
         }
-        DEBUG_CODE({
-            for (auto lit : core)
-                VERIFY(s().value(lit) == l_true);
-            for (auto const& [n1, n2] : eqs)
-                VERIFY(n1->get_root() == n2->get_root());
-            });
         IF_VERBOSE(10,
             for (auto lit : core)
-                verbose_stream() << "    " << lit << ":  " << mk_ismt2_pp(literal2expr(lit), m) << "\n";
+                verbose_stream() << "    " << lit << ":  " << mk_ismt2_pp(literal2expr(lit), m) << " " << s().value(lit) << "\n";
+        for (auto const& [n1, n2] : eqs)
+            verbose_stream() << "    " << ctx.bpp(n1) << "  ==  " << ctx.bpp(n2) << "\n";);
+        DEBUG_CODE({
+            for (auto lit : core)
+                SASSERT(s().value(lit) == l_true);
             for (auto const& [n1, n2] : eqs)
-                verbose_stream() << "    " << ctx.bpp(n1) << "  ==  " << ctx.bpp(n2) << "\n";);
+                SASSERT(n1->get_root() == n2->get_root());
+            });
+
 
         return { core, eqs };
     }
@@ -203,8 +204,8 @@ namespace polysat {
         m_var_eqs.setx(m_var_eqs_head, {v1, v2}, {v1, v2});
         ctx.push(value_trail<unsigned>(m_var_eqs_head));    
         auto d = dependency(v1, v2, s().scope_lvl());
-        unsigned index = m_core.register_constraint(sc, d);
+        constraint_id id = m_core.register_constraint(sc, d);
-        m_core.assign_eh(index, false, d); 
+        m_core.assign_eh(id, false, s().scope_lvl()); 
         m_var_eqs_head++;
     }
 
@@ -218,9 +219,9 @@ namespace polysat {
         auto sc = ~m_core.eq(p, q);
         sat::literal neq = ~expr2literal(ne.eq());
         auto d = dependency(neq, s().lvl(neq));
-        auto index = m_core.register_constraint(sc, d);
+        auto id = m_core.register_constraint(sc, d);
         TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n");
-        m_core.assign_eh(index, false, d);
+        m_core.assign_eh(id, false, s().lvl(neq));
     }
 
     // Core uses the propagate callback to add unit propagations to the trail.

src/sat/smt/polysat_solver.h

@@ -43,8 +43,8 @@ namespace polysat {
 
         struct atom {
             bool_var                m_bv;
-            unsigned                m_index;
+            constraint_id           m_index;
-            atom(bool_var b, unsigned index) :m_bv(b), m_index(index) {}
+            atom(bool_var b, constraint_id index) :m_bv(b), m_index(index) {}
             ~atom() { }
         };