diff --git a/src/sat/smt/polysat_constraints.h b/src/sat/smt/polysat_constraints.h index 156776517..b8068c68a 100644 --- a/src/sat/smt/polysat_constraints.h +++ b/src/sat/smt/polysat_constraints.h @@ -73,8 +73,6 @@ namespace polysat { bool is_eq(pvar& v, rational& val) { throw default_exception("nyi"); } }; - using dependent_constraint = std::pair; - class constraints { trail_stack& m_trail; public: diff --git a/src/sat/smt/polysat_core.cpp b/src/sat/smt/polysat_core.cpp index b7ff2e740..f3950adf2 100644 --- a/src/sat/smt/polysat_core.cpp +++ b/src/sat/smt/polysat_core.cpp @@ -40,7 +40,7 @@ namespace polysat { public: mk_assign_var(pvar v, core& c) : m_var(v), c(c) {} void undo() { - c.m_justification[m_var] = nullptr; + c.m_justification[m_var] = dependency::null_dependency(); c.m_assignment.pop(); } }; @@ -84,7 +84,6 @@ namespace polysat { m_viable(*this), m_constraints(s.get_trail_stack()), m_assignment(*this), - m_dep(s.get_region()), m_var_queue(m_activity) {} @@ -107,7 +106,7 @@ namespace polysat { unsigned v = m_vars.size(); m_vars.push_back(sz2pdd(sz).mk_var(v)); m_activity.push_back({ sz, 0 }); - m_justification.push_back(nullptr); + m_justification.push_back(dependency::null_dependency()); m_watch.push_back({}); m_var_queue.mk_var_eh(v); s.ctx.push(mk_add_var(*this)); @@ -123,9 +122,9 @@ namespace polysat { m_var_queue.del_var_eh(v); } - unsigned core::register_constraint(signed_constraint& sc, solver_assertion as) { + unsigned core::register_constraint(signed_constraint& sc, dependency d) { unsigned idx = m_constraint_trail.size(); - m_constraint_trail.push_back({ sc, as }); + m_constraint_trail.push_back({ sc, d }); auto& vars = sc.vars(); unsigned i = 0, j = 0, sz = vars.size(); for (; i < sz && j < 2; ++i) @@ -172,15 +171,24 @@ namespace polysat { return false; s.ctx.push(value_trail(m_qhead)); for (; m_qhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_qhead) - propagate_constraint(m_prop_queue[m_qhead]); + propagate_assignment(m_prop_queue[m_qhead]); s.ctx.push(value_trail(m_vqhead)); for (; m_vqhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_vqhead) propagate_value(m_prop_queue[m_vqhead]); return true; } - void core::propagate_constraint(prop_item& dc) { - auto [idx, sc, dep] = dc; + signed_constraint core::get_constraint(unsigned idx, bool sign) { + auto sc = m_constraint_trail[idx].sc; + if (sign) + sc = ~sc; + return sc; + } + + + void core::propagate_assignment(prop_item& dc) { + auto [idx, sign, dep] = dc; + auto sc = get_constraint(idx, sign); if (sc.is_eq(m_var, m_value)) propagate_assignment(m_var, m_value, dep); } @@ -189,7 +197,7 @@ namespace polysat { m_watch[var].push_back(idx); } - void core::propagate_assignment(pvar v, rational const& value, stacked_dependency* dep) { + void core::propagate_assignment(pvar v, rational const& value, dependency dep) { if (is_assigned(v)) return; if (m_var_queue.contains(v)) { @@ -238,13 +246,15 @@ namespace polysat { } void core::propagate_value(prop_item const& dc) { - auto [idx, sc, dep] = dc; + auto [idx, sign, dep] = dc; + auto sc = get_constraint(idx, sign); // check if sc evaluates to false switch (eval(sc)) { case l_true: - return; + break; case l_false: - m_unsat_core = explain_eval({ sc, dep }); + m_unsat_core = explain_eval(sc); + m_unsat_core.push_back(dep); propagate_unsat_core(); return; default: @@ -253,15 +263,13 @@ namespace polysat { // 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 idx : m_watch[m_var]) { - auto [sc, as] = m_constraint_trail[idx]; + auto [sc, d] = m_constraint_trail[idx]; switch (eval(sc)) { case l_false: - m_unsat_core = explain_eval({ sc, nullptr }); - s.propagate(as, true, m_unsat_core); + s.propagate(d, true, explain_eval(sc)); break; case l_true: - m_unsat_core = explain_eval({ sc, nullptr }); - s.propagate(as, false, m_unsat_core); + s.propagate(d, false, explain_eval(sc)); break; default: break; @@ -272,12 +280,13 @@ namespace polysat { void core::propagate_unsat_core() { // default is to use unsat core: - s.set_conflict(m_unsat_core); // if core is based on viable, use s.set_lemma(); + + s.set_conflict(m_unsat_core); } - void core::assign_eh(unsigned index, signed_constraint const& sc, dependency const& dep) { - m_prop_queue.push_back({ index, sc, m_dep.mk_leaf(dep) }); + void core::assign_eh(unsigned index, bool sign, dependency const& dep) { + m_prop_queue.push_back({ index, sign, dep }); s.ctx.push(push_back_vector(m_prop_queue)); } diff --git a/src/sat/smt/polysat_core.h b/src/sat/smt/polysat_core.h index b3e7dead5..802108ffc 100644 --- a/src/sat/smt/polysat_core.h +++ b/src/sat/smt/polysat_core.h @@ -30,45 +30,36 @@ namespace polysat { class core; class solver; - struct solver_assertion { - unsigned m_var1; - unsigned m_var2 = 0; - public: - solver_assertion(sat::literal lit) : m_var1(2*lit.index()) {} - solver_assertion(unsigned v1, unsigned v2) : m_var1(1 + 2*v1), m_var2(v2) {} - bool is_literal() const { return m_var1 % 2 == 0; } - sat::literal get_literal() const { SASSERT(is_literal()); return sat::to_literal(m_var1 / 2); } - unsigned var1() const { SASSERT(!is_literal()); return (m_var1 - 1) / 2; } - unsigned var2() const { SASSERT(!is_literal()); return m_var2; } - }; - class core { class mk_add_var; class mk_dqueue_var; class mk_assign_var; class mk_add_watch; typedef svector> activity; - typedef std::tuple prop_item; + typedef std::tuple prop_item; friend class viable; friend class constraints; friend class assignment; + struct constraint_info { + signed_constraint sc; + dependency d; + }; solver& s; viable m_viable; constraints m_constraints; assignment m_assignment; unsigned m_qhead = 0, m_vqhead = 0; svector m_prop_queue; - svector> m_constraint_trail; // - stacked_dependency_manager m_dep; + svector m_constraint_trail; // index of constraints mutable scoped_ptr_vector m_pdd; dependency_vector m_unsat_core; // attributes associated with variables - vector m_vars; // for each variable a pdd - vector m_values; // current value of assigned variable - ptr_vector m_justification; // justification for assignment + vector m_vars; // for each variable a pdd + vector m_values; // current value of assigned variable + svector m_justification; // justification for assignment activity m_activity; // activity of variables var_queue m_var_queue; // priority queue of variables to assign vector m_watch; // watch lists for variables for constraints on m_prop_queue where they occur @@ -82,25 +73,27 @@ namespace polysat { unsigned size(pvar v) const { return var2pdd(v).power_of_2(); } void del_var(); - bool is_assigned(pvar v) { return nullptr != m_justification[v]; } - void propagate_constraint(prop_item& dc); + bool is_assigned(pvar v) { return !m_justification[v].is_null(); } void propagate_value(prop_item const& dc); - void propagate_assignment(pvar v, rational const& value, stacked_dependency* dep); + void propagate_assignment(prop_item& dc); + void propagate_assignment(pvar v, rational const& value, dependency dep); void propagate_unsat_core(); void add_watch(unsigned idx, unsigned var); + signed_constraint get_constraint(unsigned idx, bool sign); + lbool eval(signed_constraint sc) { throw default_exception("nyi"); } - dependency_vector explain_eval(dependent_constraint const& dc) { throw default_exception("nyi"); } + dependency_vector explain_eval(signed_constraint const& dc) { throw default_exception("nyi"); } public: core(solver& s); sat::check_result check(); - unsigned register_constraint(signed_constraint& sc, solver_assertion sa); + unsigned register_constraint(signed_constraint& sc, dependency d); bool propagate(); - void assign_eh(unsigned idx, signed_constraint const& sc, dependency const& dep); + void assign_eh(unsigned idx, bool sign, dependency const& d); pdd value(rational const& v, unsigned sz); diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index af53750fc..95979348d 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -163,23 +163,18 @@ namespace polysat { public: mk_atom_trail(sat::bool_var v, solver& th) : th(th), m_var(v) {} void undo() override { - solver::atom* a = th.get_bv2a(m_var); - a->~atom(); th.erase_bv2a(m_var); } }; - solver::atom* solver::mk_atom(sat::literal lit, signed_constraint& sc) { - auto bv = lit.var(); - atom* a = get_bv2a(bv); - if (a) - return a; - a = new (get_region()) atom(bv); + void solver::mk_atom(sat::bool_var bv, signed_constraint& sc) { + if (get_bv2a(bv)) + return; + sat::literal lit(bv, false); + auto index = m_core.register_constraint(sc, dependency(lit, 0)); + auto a = new (get_region()) atom(bv, index); insert_bv2a(bv, a); - a->m_sc = sc; - a->m_index = m_core.register_constraint(sc, lit); ctx.push(mk_atom_trail(bv, *this)); - return a; } void solver::internalize_binaryc(app* e, std::function const& fn) { @@ -187,7 +182,9 @@ namespace polysat { auto q = expr2pdd(e->get_arg(1)); auto sc = ~fn(p, q); sat::literal lit = expr2literal(e); - auto* a = mk_atom(lit, sc); + if (lit.sign()) + sc = ~sc; + mk_atom(lit.var(), sc); } void solver::internalize_div_rem_i(app* e, bool is_div) { @@ -290,12 +287,9 @@ namespace polysat { sc = ~sc; sat::literal lit = expr2literal(e); - atom* a = mk_atom(lit, sc); - } - - void solver::internalize_bit2bool(atom* a, expr* e, unsigned idx) { - pdd p = expr2pdd(e); - a->m_sc = m_core.bit(p, idx); + if (lit.sign()) + sc = ~sc; + mk_atom(lit.var(), sc); } dd::pdd solver::expr2pdd(expr* e) { diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index 84e06636e..65183578d 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -58,15 +58,12 @@ namespace polysat { } void solver::asserted(literal l) { - atom* a = get_bv2a(l.var()); TRACE("bv", tout << "asserted: " << l << "\n";); + atom* a = get_bv2a(l.var()); if (!a) return; force_push(); - auto sc = a->m_sc; - if (l.sign()) - sc = ~sc; - m_core.assign_eh(a->m_index, sc, dependency(l, s().lvl(l))); + m_core.assign_eh(a->m_index, l.sign(), dependency(l, s().lvl(l))); } void solver::set_conflict(dependency_vector const& core) { @@ -150,10 +147,11 @@ namespace polysat { pdd p = var2pdd(v1); pdd q = var2pdd(v2); auto sc = m_core.eq(p, q); - m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2)); + m_var_eqs.setx(m_var_eqs_head, {v1, v2}, {v1, v2}); ctx.push(value_trail(m_var_eqs_head)); - unsigned index = m_core.register_constraint(sc, solver_assertion(v1, v2)); - m_core.assign_eh(index, sc, dependency(m_var_eqs_head, s().scope_lvl())); + auto d = dependency(m_var_eqs_head, s().scope_lvl()); + unsigned index = m_core.register_constraint(sc, d); + m_core.assign_eh(index, false, d); m_var_eqs_head++; } @@ -163,9 +161,10 @@ namespace polysat { pdd q = var2pdd(v2); auto sc = ~m_core.eq(p, q); sat::literal neq = ~expr2literal(ne.eq()); - auto index = m_core.register_constraint(sc, neq); + auto d = dependency(neq, s().lvl(neq)); + auto index = m_core.register_constraint(sc, d); TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n"); - m_core.assign_eh(index, sc, dependency(neq, s().lvl(neq))); + m_core.assign_eh(index, false, d); } // Core uses the propagate callback to add unit propagations to the trail. @@ -178,19 +177,22 @@ namespace polysat { ctx.propagate(lit, ex); } - void solver::propagate(solver_assertion as, bool sign, dependency_vector const& deps) { + void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps) { auto [core, eqs] = explain_deps(deps); - if (as.is_literal()) { - auto lit = as.get_literal(); + if (d.is_literal()) { + auto lit = d.literal(); if (sign) lit.neg(); + if (s().value(lit) == l_true) + return; auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr); ctx.propagate(lit, ex); } - else if (sign) { + else if (sign) { + auto const [v1, v2] = m_var_eqs[d.index()]; // equalities are always asserted so a negative propagation is a conflict. - auto n1 = var2enode(as.var1()); - auto n2 = var2enode(as.var2()); + auto n1 = var2enode(v1); + auto n2 = var2enode(v2); eqs.push_back({ n1, n2 }); auto ex = euf::th_explain::conflict(*this, core, eqs, nullptr); ctx.set_conflict(ex); @@ -223,6 +225,7 @@ namespace polysat { } case ckind_t::smul_fl_t: case ckind_t::op_t: + NOT_IMPLEMENTED_YET(); break; } throw default_exception("nyi"); diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index 6f8e7a640..408d0756c 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -42,9 +42,8 @@ namespace polysat { struct atom { bool_var m_bv; - unsigned m_index = 0; - signed_constraint m_sc; - atom(bool_var b) :m_bv(b) {} + unsigned m_index; + atom(bool_var b, unsigned index) :m_bv(b), m_index(index) {} ~atom() { } }; @@ -92,7 +91,7 @@ namespace polysat { void erase_bv2a(bool_var bv) { m_bool_var2atom[bv] = nullptr; } atom* get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, nullptr); } class mk_atom_trail; - atom* mk_atom(sat::literal lit, signed_constraint& sc); + void mk_atom(sat::bool_var bv, signed_constraint& sc); void set_bit_eh(theory_var v, literal l, unsigned idx); void init_bits(expr* e, expr_ref_vector const & bits); void mk_bits(theory_var v); @@ -122,7 +121,6 @@ namespace polysat { void internalize_polysat(app* a); void assert_bv2int_axiom(app * n); void assert_int2bv_axiom(app* n); - void internalize_bit2bool(atom* a, expr* e, unsigned idx); pdd expr2pdd(expr* e); pdd var2pdd(euf::theory_var v); @@ -134,7 +132,7 @@ namespace polysat { void set_conflict(dependency_vector const& core); void set_lemma(vector const& lemma, unsigned level, dependency_vector const& core); void propagate(signed_constraint sc, dependency_vector const& deps); - void propagate(solver_assertion as, bool sign, dependency_vector const& deps); + void propagate(dependency const& d, bool sign, dependency_vector const& deps); void add_lemma(vector const& lemma); diff --git a/src/sat/smt/polysat_types.h b/src/sat/smt/polysat_types.h index 4296a8247..42f283cc7 100644 --- a/src/sat/smt/polysat_types.h +++ b/src/sat/smt/polysat_types.h @@ -11,28 +11,26 @@ Author: #include "math/dd/dd_pdd.h" #include "util/sat_literal.h" -#include "util/dependency.h" namespace polysat { using pdd = dd::pdd; using pvar = unsigned; - class dependency { unsigned m_index; unsigned m_level; public: dependency(sat::literal lit, unsigned level) : m_index(2 * lit.index()), m_level(level) {} dependency(unsigned var_idx, unsigned level) : m_index(1 + 2 * var_idx), m_level(level) {} + static dependency null_dependency() { return dependency(0, UINT_MAX); } + bool is_null() const { return m_level == UINT_MAX; } bool is_literal() const { return m_index % 2 == 0; } sat::literal literal() const { SASSERT(is_literal()); return sat::to_literal(m_index / 2); } unsigned index() const { SASSERT(!is_literal()); return (m_index - 1) / 2; } unsigned level() const { return m_level; } }; - using stacked_dependency = stacked_dependency_manager::dependency; - inline std::ostream& operator<<(std::ostream& out, dependency d) { if (d.is_literal()) return out << d.literal() << "@" << d.level();