diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp index 5dd8140e8..b8eb757e4 100644 --- a/src/math/polysat/conflict_core.cpp +++ b/src/math/polysat/conflict_core.cpp @@ -57,4 +57,29 @@ namespace polysat { m_needs_model = true; } + void conflict_core::resolve(sat::bool_var var, clause const& cl) { + // TODO: fix the implementation: should resolve the given clause with the current conflict core. +#if 0 + DEBUG_CODE({ + bool this_has_pos = std::count(begin(), end(), sat::literal(var)) > 0; + bool this_has_neg = std::count(begin(), end(), ~sat::literal(var)) > 0; + bool other_has_pos = std::count(other.begin(), other.end(), sat::literal(var)) > 0; + bool other_has_neg = std::count(other.begin(), other.end(), ~sat::literal(var)) > 0; + SASSERT(!this_has_pos || !this_has_neg); // otherwise this is tautology + SASSERT(!other_has_pos || !other_has_neg); // otherwise other is tautology + SASSERT((this_has_pos && other_has_neg) || (this_has_neg && other_has_pos)); + }); + // The resolved var should not be one of the new constraints + int j = 0; + for (auto lit : m_literals) + if (lit.var() != var) + m_literals[j++] = lit; + m_literals.shrink(j); + for (sat::literal lit : other) + if (lit.var() != var) + m_literals.push_back(lit); + return true; +#endif + } + } diff --git a/src/math/polysat/conflict_core.h b/src/math/polysat/conflict_core.h index 8692c4b37..f9d5521e9 100644 --- a/src/math/polysat/conflict_core.h +++ b/src/math/polysat/conflict_core.h @@ -21,6 +21,7 @@ namespace polysat { vector m_constraints; /** Storage for new constraints that may not yet have a boolean variable yet */ + // TODO: not necessary anymore, if we keep constraint_manager::gc() ptr_vector m_storage; // If this is not null_var, the conflict was due to empty viable set for this variable. @@ -67,6 +68,11 @@ namespace polysat { m_storage.reset(); } + /** Perform boolean resolution with the clause upon variable 'var'. + * Precondition: core/clause contain complementary 'var'-literals. + */ + void resolve(sat::bool_var var, clause const& cl); + std::ostream& display(std::ostream& out) const; }; diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 10a160d31..0abd66507 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -27,18 +27,14 @@ namespace polysat { void constraint_manager::assign_bv2c(sat::bool_var bv, constraint* c) { SASSERT_EQ(get_bv2c(bv), nullptr); SASSERT(!c->has_bvar()); - SASSERT(!m_constraint_table.contains(c)); c->m_bvar = bv; m_bv2constraint.setx(bv, c, nullptr); - m_constraint_table.insert(c); } void constraint_manager::erase_bv2c(constraint* c) { SASSERT(c->has_bvar()); SASSERT_EQ(get_bv2c(c->bvar()), c); - SASSERT(m_constraint_table.contains(c)); m_bv2constraint[c->bvar()] = nullptr; - m_constraint_table.remove(c); c->m_bvar = sat::null_bool_var; } @@ -46,14 +42,42 @@ namespace polysat { return m_bv2constraint.get(bv, nullptr); } - constraint* constraint_manager::store(scoped_constraint_ptr scoped_c) { - constraint* c = scoped_c.detach(); - LOG_V("Store constraint: " << show_deref(c)); + void constraint_manager::assign_bvar(constraint* c) { assign_bv2c(m_bvars.new_var(), c); + } + + void constraint_manager::erase_bvar(constraint* c) { + erase_bv2c(c); + } + + /** Add constraint to per-level storage */ + void constraint_manager::store(constraint* c) { + LOG_V("Store constraint: " << show_deref(c)); while (m_constraints.size() <= c->level()) m_constraints.push_back({}); m_constraints[c->level()].push_back(c); - return c; + } + + /** Remove the given constraint from the per-level storage (without deallocating it) */ + void constraint_manager::erase(constraint* c) { + LOG_V("Erase constraint: " << show_deref(c)); + auto& vec = m_constraints[c->level()]; + for (unsigned i = vec.size(); i-- > 0; ) + if (vec[i] == c) { + vec.swap(i, vec.size() - 1); + constraint* c0 = vec.detach_back(); + SASSERT(c0 == c); + vec.pop_back(); + return; + } + UNREACHABLE(); + } + + /** Change level of the given constraint, adjusting its storage position */ + void constraint_manager::set_level(constraint* c, unsigned new_lvl) { + erase(c); + c->m_level = new_lvl; + store(c); } clause* constraint_manager::store(clause_ref cl_ref) { @@ -84,6 +108,7 @@ namespace polysat { SASSERT(m_external_constraints.contains(dep)); m_external_constraints.remove(dep); } + m_constraint_table.erase(c); erase_bv2c(c); } m_constraints[l].reset(); @@ -112,45 +137,52 @@ namespace polysat { /** Look up constraint among stored constraints. */ constraint* constraint_manager::dedup(constraint* c1) { - auto it = m_constraint_table.find(c1); - if (it == m_constraint_table.end()) - return c1; - constraint* c0 = *it; - // TODO: can this assertion be violated? - // Yes, e.g.: constraint c was asserted at level 1, the conflict resolution derived ~c from c1,c2 at level 0... - // In that case we have to adjust c0's level in the storage. - // What about the level of the boolean variable? That depends on its position in the assignment stack and should probably stay where it is. - // Will be updated separately when we patch the assignment stack. - - // NB code review: currently you separate dedup from insertion into the constraint table. - // It seems more convenient to also ensure that the new constraint is inserted into the table at this point. - // You also erase c from the constraint table in erase_bv2c. - // again association with m_constraint_table seems to be only for deduplication purposes. - // - // the store function is used separately from solver::new_constraint - // shouldn't it be combined with deduplication? - // in this way we can fix the level if a new duplicate constraint is created at a lower level -#if 0 auto it = m_constraint_table.find(c1); if (it == m_constraint_table.end()) { store(c1); m_constraint_table.insert(c1); + // Assuming c is a temporary constraint, we need to: + // 1. erase(c); + // 2. m_constraint_table.remove(c); + // before we dealloc it. + // But even if we don't do this, there is not a real memory leak because the constraint will be deallocated properly when the level is popped. + // So maybe the best way is to just do periodic GC passes where we throw out constraints that do not have a boolean variable, + // instead of precise lifetime tracking for temprorary constraints. + // It should be safe to do a GC pass outside of conflict resolution. + // TODO: if this is the path we take, then we can drop the scoped_signed_constraint and the scoped_constraint_ptr classes. + // TODO: we could maintain a counter of temporary constraints (#constraints - #bvars) to decide when to do a GC, or just do it after every conflict resolution return c1; } constraint* c0 = *it; - if (c1->level() < c0->level()) { - m_constraints[c0->level()].erase(c0); - m_constraints[c1->level()].push_back(c0); - c0->m_level = c1->level(); - } + if (c1->level() < c0->level()) + set_level(c0, c1->level()); dealloc(c1); return c0; + } -#endif - - SASSERT(c0->level() <= c1->level()); - dealloc(c1); - return c0; + void constraint_manager::gc() { + for (auto& vec : m_constraints) + for (int i = vec.size(); i-- > 0; ) { + constraint* c = vec[i]; + if (!c->has_bvar()) { + LOG_V("Destroying constraint: " << show_deref(c)); + m_constraint_table.erase(c); + vec.swap(i, vec.size() - 1); + vec.pop_back(); + } + } + DEBUG_CODE({ + for (auto const& vec : m_constraints) + for (auto* c : vec) { + SASSERT(c->has_bvar()); + SASSERT(m_constraint_table.contains(c)); + } + }); + } + + bool constraint_manager::should_gc() { + // TODO: maybe replace this by a better heuristic + return true; } scoped_signed_constraint constraint_manager::eq(unsigned lvl, pdd const& p) { @@ -271,35 +303,6 @@ namespace polysat { }); } -#if 0 - // NB code review: - // resolve is done elsewhere or should be done elsewhere. - // by not having it as a method on clauses we can work with fixed literal arrays - // instead of dynamically expandable vectors. - - bool clause::resolve(sat::bool_var var, clause const& other) { - DEBUG_CODE({ - bool this_has_pos = std::count(begin(), end(), sat::literal(var)) > 0; - bool this_has_neg = std::count(begin(), end(), ~sat::literal(var)) > 0; - bool other_has_pos = std::count(other.begin(), other.end(), sat::literal(var)) > 0; - bool other_has_neg = std::count(other.begin(), other.end(), ~sat::literal(var)) > 0; - SASSERT(!this_has_pos || !this_has_neg); // otherwise this is tautology - SASSERT(!other_has_pos || !other_has_neg); // otherwise other is tautology - SASSERT((this_has_pos && other_has_neg) || (this_has_neg && other_has_pos)); - }); - // The resolved var should not be one of the new constraints - int j = 0; - for (auto lit : m_literals) - if (lit.var() != var) - m_literals[j++] = lit; - m_literals.shrink(j); - for (sat::literal lit : other) - if (lit.var() != var) - m_literals.push_back(lit); - return true; - } -#endif - std::ostream& clause::display(std::ostream& out) const { bool first = true; for (auto lit : *this) { diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 8ae4919af..252636a41 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -57,7 +57,7 @@ namespace polysat { vector> m_constraints; vector> m_clauses; - + // Association to external dependency values (i.e., external names for constraints) u_map m_external_constraints; @@ -66,17 +66,19 @@ namespace polysat { void erase_bv2c(constraint* c); constraint* get_bv2c(sat::bool_var bv) const; + void store(constraint* c); + void erase(constraint* c); + void set_level(constraint* c, unsigned new_lvl); + constraint* dedup(constraint* c); public: constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {} ~constraint_manager(); - /** Start managing the lifetime of the given constraint - * - Keeps the constraint until the corresponding level is popped - * - Allocates a boolean variable for the constraint - */ - constraint* store(scoped_constraint_ptr c); + void assign_bvar(constraint* c); + void erase_bvar(constraint* c); + sat::literal get_or_assign_blit(signed_constraint& c); clause* store(clause_ref cl); @@ -86,6 +88,10 @@ namespace polysat { /// Release constraints at the given level and above. void release_level(unsigned lvl); + /// Garbage-collect temporary constraints (i.e., those that do not have a boolean variable). + void gc(); + bool should_gc(); + constraint* lookup(sat::bool_var var) const; signed_constraint lookup(sat::literal lit) const; constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); } @@ -119,7 +125,7 @@ namespace polysat { // constraint_manager* m_manager; clause* m_unit_clause = nullptr; ///< If this constraint was asserted by a unit clause, we store that clause here. - unsigned m_storage_level; ///< Controls lifetime of the constraint object. Always a base level. + unsigned m_level; ///< Controls lifetime of the constraint object. Always a base level. ckind_t m_kind; unsigned_vector m_vars; /** The boolean variable associated to this constraint, if any. @@ -131,7 +137,7 @@ namespace polysat { sat::bool_var m_bvar = sat::null_bool_var; constraint(constraint_manager& m, unsigned lvl, ckind_t k): - /*m_manager(&m),*/ m_storage_level(lvl), m_kind(k) {} + /*m_manager(&m),*/ m_level(lvl), m_kind(k) {} protected: std::ostream& display_extra(std::ostream& out, lbool status) const; @@ -162,7 +168,7 @@ namespace polysat { unsigned_vector& vars() { return m_vars; } unsigned_vector const& vars() const { return m_vars; } unsigned var(unsigned idx) const { return m_vars[idx]; } - unsigned level() const { return m_storage_level; } + unsigned level() const { return m_level; } bool has_bvar() const { return m_bvar != sat::null_bool_var; } sat::bool_var bvar() const { return m_bvar; } @@ -347,9 +353,6 @@ namespace polysat { static clause_ref from_unit(signed_constraint c, p_dependency_ref d); static clause_ref from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals); - // Resolve with 'other' upon 'var'. - // bool resolve(sat::bool_var var, clause const& other); - p_dependency* dep() const { return m_dep; } unsigned level() const { return m_level; } diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 0149d2189..5332a1c26 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -17,7 +17,28 @@ Author: namespace polysat { - conflict_explainer::conflict_explainer(solver& s): m_solver(s) {} + bool inf_polynomial_superposition:: perform(conflict_explainer& ce) { + // TODO + return false; + } + + conflict_explainer::conflict_explainer(solver& s): m_solver(s) { + inference_engines.push_back(alloc(inf_polynomial_superposition)); + } + + bool conflict_explainer::saturate() { + for (auto* engine : inference_engines) + if (engine->perform(*this)) + return true; + return false; + } + + + + + + + // clause_ref conflict_explainer::resolve(pvar v, ptr_vector const& cjust) { // LOG_H3("Attempting to explain conflict for v" << v); diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h index 5c4144b2e..714d2c579 100644 --- a/src/math/polysat/explain.h +++ b/src/math/polysat/explain.h @@ -21,28 +21,41 @@ namespace polysat { class solver; + class inference_engine { + public: + virtual ~inference_engine() {} + /** Try to apply an inference rule. Returns true if a new constraint was added to the core. */ + virtual bool perform(conflict_explainer& ce) = 0; + }; + + class inf_polynomial_superposition : public inference_engine { + public: + bool perform(conflict_explainer& ce) override; + }; + + // TODO: other rules + // clause_ref by_ugt_x(); + // clause_ref by_ugt_y(); + // clause_ref by_ugt_z(); + // clause_ref y_ule_ax_and_x_ule_z(); + class conflict_explainer { solver& m_solver; - pvar m_var = null_var; - ptr_vector m_cjust_v; + conflict_core m_conflict; - // TODO: instead of listing methods, create an abstract class for explanation methods, register them in a vector and call them in turn - /* Conflict explanation methods */ - clause_ref by_polynomial_superposition(); - clause_ref by_ugt_x(); - clause_ref by_ugt_y(); - clause_ref by_ugt_z(); - clause_ref y_ule_ax_and_x_ule_z(); + scoped_ptr_vector inference_engines; - p_dependency_ref null_dep(); - // p_dependency_ref null_dep() const { return m_solver.mk_dep_ref(null_dependency); } bool push_omega_mul(clause_builder& clause, unsigned level, unsigned p, pdd const& x, pdd const& y); - public: /** Create empty conflict */ conflict_explainer(solver& s); + /** Perform one step of core saturation, if possible. + * Core saturation derives new constraints according applicable inference rules. + */ + bool saturate(); + /** resolve conflict state against assignment to v */ void resolve(pvar v, ptr_vector const& cjust_v); void resolve(sat::literal lit); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 9d2c04a93..cfcab64eb 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -66,6 +66,9 @@ namespace polysat { if (!m_conflict.empty()) LOG("Conflict: " << m_conflict); IF_LOGGING(m_viable.log()); + if (!is_conflict() && m_constraints.should_gc()) + m_constraints.gc(); + if (pending_disjunctive_lemma()) { LOG_H2("UNDEF (handle lemma externally)"); return l_undef; } else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; } else if (is_conflict()) resolve_conflict(); @@ -140,7 +143,7 @@ namespace polysat { SASSERT(sc); SASSERT(activate || dep != null_dependency); // if we don't activate the constraint, we need the dependency to access it again later. signed_constraint c = sc.get_signed(); - m_constraints.store(sc.detach()); + sc.detach(); clause* unit = m_constraints.store(clause::from_unit(c, mk_dep_ref(dep))); c->set_unit_clause(unit); if (dep != null_dependency) diff --git a/src/util/scoped_ptr_vector.h b/src/util/scoped_ptr_vector.h index 38e96810f..04d29a9f2 100644 --- a/src/util/scoped_ptr_vector.h +++ b/src/util/scoped_ptr_vector.h @@ -81,6 +81,12 @@ public: m_vector[m_vector.size()-1] = tmp; } + T* detach_back() { + SASSERT(!empty()); + T* tmp = m_vector.back(); + m_vector.back() = nullptr; + return tmp; + } ptr_vector detach() { ptr_vector tmp(std::move(m_vector));