From 5098d5bbfebc2bfcfddf00550cc5f4bcce604684 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2023 16:28:59 -0800 Subject: [PATCH] refactor for handling cores Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/core.cpp | 44 +++++++++++++++++++++------------- src/sat/smt/polysat/core.h | 13 ++++++---- src/sat/smt/polysat/types.h | 7 ++++-- src/sat/smt/polysat/viable.cpp | 6 ++--- src/sat/smt/polysat/viable.h | 2 +- 5 files changed, 44 insertions(+), 28 deletions(-) diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 7c6977299..6cf1db764 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -38,7 +38,7 @@ namespace polysat { public: mk_assign_var(pvar v, core& c) : m_var(v), c(c) {} void undo() { - c.m_justification[m_var] = null_dependency; + c.m_justification[m_var] = constraint_id::null(); c.m_assignment.pop(); } }; @@ -123,7 +123,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(null_dependency); + m_justification.push_back(constraint_id::null()); m_watch.push_back({}); m_var_queue.mk_var_eh(v); m_viable.ensure_var(v); @@ -174,11 +174,11 @@ namespace polysat { s.trail().push(mk_dqueue_var(m_var, *this)); switch (m_viable.find_viable(m_var, m_value)) { case find_t::empty: - s.set_lemma(m_viable.get_core(), m_viable.explain()); + s.set_lemma(m_viable.get_core(), get_dependencies(m_viable.explain())); // propagate_unsat_core(); return sat::check_result::CR_CONTINUE; case find_t::singleton: - s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain()); + s.propagate(m_constraints.eq(var2pdd(m_var), m_value), get_dependencies(m_viable.explain())); return sat::check_result::CR_CONTINUE; case find_t::multiple: s.add_eq_literal(m_var, m_value); @@ -210,7 +210,7 @@ namespace polysat { if (value == l_false) sc = ~sc; if (sc.is_eq(m_var, m_value)) - propagate_assignment(m_var, m_value, dep); + propagate_assignment(m_var, m_value, idx); else sc.activate(*this, dep); } @@ -219,7 +219,7 @@ namespace polysat { m_watch[var].push_back(idx); } - void core::propagate_assignment(pvar v, rational const& value, dependency dep) { + void core::propagate_assignment(pvar v, rational const& value, constraint_id dep) { if (is_assigned(v)) return; if (m_var_queue.contains(v)) { @@ -255,7 +255,7 @@ 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. - propagate(sc, value, dep); + propagate({ idx }, sc, value, dep); if (s.inconsistent()) return; @@ -280,7 +280,7 @@ namespace polysat { void core::propagate_value(constraint_id idx) { auto [sc, d, value] = m_constraint_index[idx.id]; // propagate current assignment for sc - propagate(sc, value, d); + propagate(idx, sc, value, d); if (s.inconsistent()) return; @@ -292,10 +292,10 @@ namespace polysat { auto [sc, d, value] = m_constraint_index[idx1]; switch (eval(sc)) { case l_false: - s.propagate(d, true, explain_eval(sc)); + s.propagate(d, true, get_dependencies(explain_eval(sc))); break; case l_true: - s.propagate(d, false, explain_eval(sc)); + s.propagate(d, false, get_dependencies(explain_eval(sc))); break; default: break; @@ -304,15 +304,25 @@ namespace polysat { } } - void core::propagate(signed_constraint& sc, lbool value, dependency const& d) { + dependency_vector core::get_dependencies(constraint_id_vector const& cc) { + dependency_vector result; + for (auto idx : cc) { + auto [sc, d, value] = m_constraint_index[idx.id]; + SASSERT(value != l_undef); + result.push_back(value == l_false ? ~d : d); + } + return result; + } + + void core::propagate(constraint_id id, 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)); + s.propagate(d, eval_value != l_true, get_dependencies(explain_eval(sc))); else if (value != eval_value) { m_unsat_core = explain_eval(sc); - m_unsat_core.push_back(value == l_false ? ~d : d); + m_unsat_core.push_back(id); propagate_unsat_core(); } } @@ -333,7 +343,7 @@ namespace polysat { // default is to use unsat core: // if core is based on viable, use s.set_lemma(); - s.set_conflict(m_unsat_core); + s.set_conflict(get_dependencies(m_unsat_core)); } void core::assign_eh(constraint_id index, bool sign, unsigned level) { @@ -352,8 +362,8 @@ namespace polysat { s.trail().push(unassign(*this, index.id)); } - dependency_vector core::explain_eval(signed_constraint const& sc) { - dependency_vector deps; + constraint_id_vector core::explain_eval(signed_constraint const& sc) { + constraint_id_vector deps; for (auto v : sc.vars()) if (is_assigned(v)) deps.push_back(m_justification[v]); @@ -379,7 +389,7 @@ namespace polysat { for (auto const& [sc, d, value] : m_constraint_index) out << sc << " " << d << " := " << value << "\n"; for (unsigned i = 0; i < m_vars.size(); ++i) - out << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n"; + out << m_vars[i] << " := " << m_values[i] << " " << m_constraint_index[m_justification[i].id].d << "\n"; m_var_queue.display(out << "vars ") << "\n"; return out; } diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index cfc6c1d82..109f0ac0e 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -31,6 +31,8 @@ namespace polysat { class core; class solver_interface; + + class core { class mk_add_var; class mk_dqueue_var; @@ -54,13 +56,13 @@ namespace polysat { unsigned m_qhead = 0, m_vqhead = 0; svector m_prop_queue; svector m_constraint_index; // index of constraints - dependency_vector m_unsat_core; + constraint_id_vector m_unsat_core; // attributes associated with variables vector m_vars; // for each variable a pdd vector m_values; // current value of assigned variable - svector m_justification; // justification for assignment + 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 @@ -77,9 +79,9 @@ namespace polysat { bool is_assigned(pvar v) { return !m_justification[v].is_null(); } void propagate_value(constraint_id idx); void propagate_assignment(constraint_id idx); - void propagate_assignment(pvar v, rational const& value, dependency dep); + void propagate_assignment(pvar v, rational const& value, constraint_id dep); void propagate_unsat_core(); - void propagate(signed_constraint& sc, lbool value, dependency const& d); + void propagate(constraint_id id, 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); @@ -88,7 +90,8 @@ namespace polysat { void add_watch(unsigned idx, unsigned var); lbool eval(signed_constraint const& sc); - dependency_vector explain_eval(signed_constraint const& sc); + constraint_id_vector explain_eval(signed_constraint const& sc); + dependency_vector get_dependencies(constraint_id_vector const& cc); void add_axiom(signed_constraint sc); diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index d9008392c..e0aefb6a9 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -22,7 +22,10 @@ namespace polysat { using pdd = dd::pdd; using pvar = unsigned; using theory_var = unsigned; - struct constraint_id { unsigned id; }; + struct constraint_id { + unsigned id; bool is_null() const { return id == UINT_MAX; } + static constraint_id null() { return constraint_id{ UINT_MAX }; } + }; using pvar_vector = unsigned_vector; inline const pvar null_var = UINT_MAX; @@ -80,7 +83,7 @@ namespace polysat { using dependency_vector = vector; using core_vector = std::initializer_list>; - + using constraint_id_vector = svector; // diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 20a31b730..3f217d1ce 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -809,12 +809,12 @@ namespace polysat { /* * Explain why the current variable is not viable or signleton. */ - dependency_vector viable::explain() { - dependency_vector result; + constraint_id_vector viable::explain() { + constraint_id_vector result; for (auto e : m_explain) { auto index = e->constraint_index; auto const& [sc, d, value] = c.m_constraint_index[index]; - result.push_back(d); + result.push_back({ index }); result.append(c.explain_eval(sc)); } // TODO: explaination for fixed bits diff --git a/src/sat/smt/polysat/viable.h b/src/sat/smt/polysat/viable.h index 64a8d3194..03f94e698 100644 --- a/src/sat/smt/polysat/viable.h +++ b/src/sat/smt/polysat/viable.h @@ -253,7 +253,7 @@ namespace polysat { /* * Explain why the current variable is not viable or signleton. */ - dependency_vector explain(); + constraint_id_vector explain(); /* * flag whether there is a forbidden interval core