From cecaf25c6f64c9bbcd037d34349cae57fb30acd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2023 10:40:02 -0800 Subject: [PATCH] refactor polysat core / solver interface Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/core.cpp | 85 ++++++++++++-------- src/sat/smt/polysat/core.h | 14 ++-- src/sat/smt/polysat/types.h | 3 + src/sat/smt/polysat/umul_ovfl_constraint.cpp | 2 +- src/sat/smt/polysat_solver.cpp | 27 ++++--- src/sat/smt/polysat_solver.h | 4 +- 6 files changed, 76 insertions(+), 59 deletions(-) diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index b3f8474b7..0607f530d 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/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() > 1) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[1]] << ") "; + if (vars.size() > 0) verbose_stream() << "(" << idx << ": " << c.m_watch[vars[0]] << ") "; + 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); - SASSERT(n <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1); - if (n > 0) - c.m_watch[vars[0]].pop_back(); + auto del_watch = [&](unsigned i) { + auto& w = c.m_watch[vars[i]]; + for (unsigned j = w.size(); j-- > 0;) { + 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) { - auto [idx, sign, dep] = dc; - auto sc = get_constraint(idx, sign); + void core::propagate_assignment(constraint_id idx) { + auto [sc, dep, value] = m_constraint_index[idx.id]; + 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) { - auto [idx, sign, dep] = dc; - 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; - } + void core::propagate_value(constraint_id idx) { + auto [sc, d, value] = m_constraint_index[idx.id]; // 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_constraint_index[index].value = to_lbool(!sign); - s.trail().push(unassign(*this, index)); + m_prop_queue.push_back(index); + m_constraint_index[index.id].value = to_lbool(!sign); + 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) { diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index 6297e567e..fb0875ec8 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -37,7 +37,6 @@ namespace polysat { class mk_assign_var; class mk_add_watch; typedef svector> activity; - typedef std::tuple 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 m_prop_queue; + svector m_prop_queue; svector 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_assignment(prop_item& dc); + void propagate_value(constraint_id idx); + 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& 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&); diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index d0b5f7bca..d9008392c 100644 --- a/src/sat/smt/polysat/types.h +++ b/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(&m_data); } std::pair eq() const { SASSERT(!is_literal()); return *std::get_if>(&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); diff --git a/src/sat/smt/polysat/umul_ovfl_constraint.cpp b/src/sat/smt/polysat/umul_ovfl_constraint.cpp index 445169c2f..596a94340 100644 --- a/src/sat/smt/polysat/umul_ovfl_constraint.cpp +++ b/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(); diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 0fa4ab8e6..75dd09075 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/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(m_var_eqs_head)); auto d = dependency(v1, v2, s().scope_lvl()); - unsigned index = m_core.register_constraint(sc, d); - m_core.assign_eh(index, false, d); + constraint_id id = m_core.register_constraint(sc, 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. diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index d7032046d..0ecc8941b 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -43,8 +43,8 @@ namespace polysat { struct atom { bool_var m_bv; - unsigned m_index; - atom(bool_var b, unsigned index) :m_bv(b), m_index(index) {} + constraint_id m_index; + atom(bool_var b, constraint_id index) :m_bv(b), m_index(index) {} ~atom() { } };