From 3436b52c4a8fdf46830dd7127679b39e13f43653 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 25 Jun 2021 20:04:25 +0200 Subject: [PATCH] Polysat: refactor constraints (#5372) * Refactor: remove sign and dep from constraint * fix some bugs * improve log messages * Add missing premises to lemma * Rename getter in an attempt to fix linux build --- src/math/polysat/CMakeLists.txt | 1 + src/math/polysat/clause_builder.cpp | 68 +++++++++++ src/math/polysat/clause_builder.h | 49 ++++++++ src/math/polysat/constraint.cpp | 104 ++++++---------- src/math/polysat/constraint.h | 147 ++++++++++++----------- src/math/polysat/eq_constraint.cpp | 76 +++++------- src/math/polysat/eq_constraint.h | 11 +- src/math/polysat/explain.cpp | 100 +++++++++------ src/math/polysat/explain.h | 1 + src/math/polysat/forbidden_intervals.cpp | 19 ++- src/math/polysat/forbidden_intervals.h | 1 - src/math/polysat/solver.cpp | 110 ++++++++++------- src/math/polysat/solver.h | 50 ++++---- src/math/polysat/ule_constraint.cpp | 12 +- src/math/polysat/ule_constraint.h | 7 +- src/test/polysat.cpp | 4 +- 16 files changed, 435 insertions(+), 325 deletions(-) create mode 100644 src/math/polysat/clause_builder.cpp create mode 100644 src/math/polysat/clause_builder.h diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index 56e2eb57e..2648fe70e 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(polysat SOURCES boolean.cpp + clause_builder.cpp constraint.cpp eq_constraint.cpp explain.cpp diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp new file mode 100644 index 000000000..5bfdfa805 --- /dev/null +++ b/src/math/polysat/clause_builder.cpp @@ -0,0 +1,68 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat clause builder + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ + +#include "math/polysat/clause_builder.h" +#include "math/polysat/solver.h" +#include "math/polysat/log.h" + +namespace polysat { + + clause_builder::clause_builder(solver& s): + m_solver(s), m_dep(nullptr, s.m_dm) + {} + + void clause_builder::reset() { + m_literals.reset(); + m_new_constraints.reset(); + m_level = 0; + m_dep = nullptr; + SASSERT(empty()); + } + + clause_ref clause_builder::build() { + // TODO: here we could set all the levels of the new constraints. so we do not have to compute the max at every use site. + clause_ref cl = clause::from_literals(m_level, std::move(m_dep), std::move(m_literals), std::move(m_new_constraints)); + m_level = 0; + SASSERT(empty()); + return cl; + } + + void clause_builder::add_dependency(p_dependency* d) { + m_dep = m_solver.m_dm.mk_join(m_dep, d); + } + + void clause_builder::push_literal(sat::literal lit) { + constraint* c = m_solver.m_constraints.lookup(lit.var()); + SASSERT(c); + if (c->unit_clause()) { + add_dependency(c->unit_clause()->dep()); + return; + } + m_level = std::max(m_level, c->level()); + m_literals.push_back(lit); + } + + void clause_builder::push_new_constraint(constraint_literal c) { + // TODO: assert that constraint is new (not 'inserted' into manager yet) + SASSERT(c); + SASSERT(c->is_undef()); + tmp_assign _t(c.get(), c.literal()); + if (c->is_always_false()) + return; + m_level = std::max(m_level, c->level()); + m_literals.push_back(c.literal()); + m_new_constraints.push_back(c.detach()); + } + +} diff --git a/src/math/polysat/clause_builder.h b/src/math/polysat/clause_builder.h new file mode 100644 index 000000000..26be8ffc2 --- /dev/null +++ b/src/math/polysat/clause_builder.h @@ -0,0 +1,49 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat clause builder + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once +#include "math/polysat/constraint.h" +#include "math/polysat/types.h" + +namespace polysat { + + /// Builds a clause from literals and constraints. + /// Takes care to + /// - resolve with unit clauses and accumulate their dependencies, + /// - skip trivial new constraints such as "4 <= 1". + class clause_builder { + solver& m_solver; + sat::literal_vector m_literals; + constraint_ref_vector m_new_constraints; + p_dependency_ref m_dep; + unsigned m_level = 0; + + public: + clause_builder(solver& s); + + bool empty() const { return m_literals.empty() && m_new_constraints.empty() && m_dep == nullptr && m_level == 0; } + void reset(); + + /// Build the clause. This will reset the clause builder so it can be reused. + clause_ref build(); + + void add_dependency(p_dependency* d); + + /// Add a literal to the clause. + /// Intended to be used for literals representing a constraint that already exists. + void push_literal(sat::literal lit); + /// Add a constraint to the clause that does not yet exist in the solver so far. + void push_new_constraint(constraint_literal c); + }; + +} diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 9689ee1a8..da9f12928 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -21,17 +21,11 @@ Author: namespace polysat { - constraint* constraint_manager::insert(constraint_ref c) { - LOG_V("Inserting constraint: " << show_deref(c)); + constraint* constraint_manager::store(constraint_ref c) { + LOG_V("Store constraint: " << show_deref(c)); SASSERT(c); SASSERT(c->bvar() != sat::null_bool_var); SASSERT(get_bv2c(c->bvar()) == c.get()); - // TODO: use explicit insert_external(constraint* c, unsigned dep) for that. - if (c->dep() && c->dep()->is_leaf()) { - unsigned dep = c->dep()->leaf_value(); - SASSERT(!m_external_constraints.contains(dep)); - m_external_constraints.insert(dep, c.get()); - } while (m_constraints.size() <= c->level()) m_constraints.push_back({}); constraint* pc = c.get(); @@ -39,12 +33,12 @@ namespace polysat { return pc; } - clause* constraint_manager::insert(clause_ref cl) { + clause* constraint_manager::store(clause_ref cl) { + LOG_V("Store clause: " << show_deref(cl)); SASSERT(cl); // Insert new constraints for (constraint* c : cl->m_new_constraints) - // TODO: if (!inserted) ? - insert(c); + store(c); cl->m_new_constraints = {}; // free vector memory // Insert clause while (m_clauses.size() <= cl->level()) @@ -54,14 +48,17 @@ namespace polysat { return pcl; } + void constraint_manager::register_external(constraint* c) { + SASSERT(c); + SASSERT(c->unit_dep()); + SASSERT(c->unit_dep()->is_leaf()); + unsigned const dep = c->unit_dep()->leaf_value(); + SASSERT(!m_external_constraints.contains(dep)); + m_external_constraints.insert(dep, c); + } + // Release constraints at the given level and above. void constraint_manager::release_level(unsigned lvl) { - for (unsigned l = m_clauses.size(); l-- > lvl; ) { - for (auto const& cl : m_clauses[l]) { - SASSERT_EQ(cl->m_ref_count, 1); // otherwise there is a leftover reference somewhere - } - m_clauses[l].reset(); - } for (unsigned l = m_constraints.size(); l-- > lvl; ) { for (auto const& c : m_constraints[l]) { LOG_V("Removing constraint: " << show_deref(c)); @@ -69,14 +66,21 @@ namespace polysat { // NOTE: ref count could be two if the constraint was added twice (once as part of clause, and later as unit constraint) LOG_H1("Expected ref_count 1 or 2, got " << c->m_ref_count << " for " << *c); } - if (c->dep() && c->dep()->is_leaf()) { - unsigned dep = c->dep()->leaf_value(); + auto* d = c->unit_dep(); + if (d && d->is_leaf()) { + unsigned const dep = d->leaf_value(); SASSERT(m_external_constraints.contains(dep)); m_external_constraints.remove(dep); } } m_constraints[l].reset(); } + for (unsigned l = m_clauses.size(); l-- > lvl; ) { + for (auto const& cl : m_clauses[l]) { + SASSERT_EQ(cl->m_ref_count, 1); // otherwise there is a leftover reference somewhere + } + m_clauses[l].reset(); + } } constraint_manager::~constraint_manager() { @@ -105,18 +109,18 @@ namespace polysat { return *dynamic_cast(this); } - constraint_ref constraint_manager::eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d) { - return alloc(eq_constraint, *this, lvl, sign, p, d); + constraint_literal constraint_manager::eq(unsigned lvl, pdd const& p) { + return constraint_literal{alloc(eq_constraint, *this, lvl, p)}; } - constraint_ref constraint_manager::ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { - return alloc(ule_constraint, *this, lvl, sign, a, b, d); + constraint_literal constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) { + return constraint_literal{alloc(ule_constraint, *this, lvl, a, b)}; } - constraint_ref constraint_manager::ult(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { + constraint_literal constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) { // a < b <=> !(b <= a) - return ule(lvl, static_cast(!sign), b, a, d); + return ~ule(lvl, b, a); } // To do signed comparison of bitvectors, flip the msb and do unsigned comparison: @@ -135,14 +139,14 @@ namespace polysat { // // Argument: flipping the msb swaps the negative and non-negative blocks // - constraint_ref constraint_manager::sle(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { + constraint_literal constraint_manager::sle(unsigned lvl, pdd const& a, pdd const& b) { auto shift = rational::power_of_two(a.power_of_2() - 1); - return ule(lvl, sign, a + shift, b + shift, d); + return ule(lvl, a + shift, b + shift); } - constraint_ref constraint_manager::slt(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { + constraint_literal constraint_manager::slt(unsigned lvl, pdd const& a, pdd const& b) { auto shift = rational::power_of_two(a.power_of_2() - 1); - return ult(lvl, sign, a + shift, b + shift, d); + return ult(lvl, a + shift, b + shift); } std::ostream& constraint::display_extra(std::ostream& out) const { @@ -180,19 +184,18 @@ namespace polysat { narrow(s); } - clause_ref clause::from_unit(constraint_ref c) { + clause_ref clause::from_unit(constraint_literal c, p_dependency_ref d) { SASSERT(c); unsigned const lvl = c->level(); - auto const& dep = c->m_dep; sat::literal_vector lits; - lits.push_back(sat::literal(c->bvar())); + lits.push_back(c.literal()); constraint_ref_vector cs; - cs.push_back(std::move(c)); - return clause::from_literals(lvl, dep, std::move(lits), std::move(cs)); + cs.push_back(c.detach()); + return clause::from_literals(lvl, std::move(d), std::move(lits), std::move(cs)); } - clause_ref clause::from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector constraints) { - return alloc(clause, lvl, d, std::move(literals), std::move(constraints)); + clause_ref clause::from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals, constraint_ref_vector constraints) { + return alloc(clause, lvl, std::move(d), std::move(literals), std::move(constraints)); } bool clause::is_always_false(solver& s) const { @@ -247,35 +250,6 @@ namespace polysat { return out; } - void clause_builder::reset() { - m_literals.reset(); - m_new_constraints.reset(); - SASSERT(empty()); - } - - clause_ref clause_builder::build(unsigned lvl, p_dependency_ref const& d) { - clause_ref cl = clause::from_literals(lvl, d, std::move(m_literals), std::move(m_new_constraints)); - SASSERT(empty()); - return cl; - } - - void clause_builder::push_literal(sat::literal lit) { - if (m_solver.active_at_base_level(lit)) - return; - m_literals.push_back(lit); - } - - void clause_builder::push_new_constraint(constraint_ref c) { - SASSERT(c); - SASSERT(c->is_undef()); - sat::literal lit{c->bvar()}; - tmp_assign _t(c, lit); - if (c->is_always_false()) - return; - m_literals.push_back(lit); - m_new_constraints.push_back(std::move(c)); - } - std::ostream& constraints_and_clauses::display(std::ostream& out) const { bool first = true; for (auto c : units()) { diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index b56983b9b..966f225e6 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -25,6 +25,7 @@ namespace polysat { enum ckind_t { eq_t, ule_t }; enum csign_t : bool { neg_t = false, pos_t = true }; + class constraint_literal; class constraint; class constraint_manager; class clause; @@ -41,6 +42,7 @@ namespace polysat { friend class constraint; bool_var_manager& m_bvars; + // poly_dep_manager& m_dm; // Association to boolean variables ptr_vector m_bv2constraint; @@ -59,24 +61,29 @@ namespace polysat { public: constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {} + // constraint_manager(bool_var_manager& bvars, poly_dep_manager& dm): m_bvars(bvars), m_dm(dm) {} ~constraint_manager(); // Start managing lifetime of the given constraint - // TODO: rename to "store", or "keep"... because the bvar->constraint mapping is already inserted at creation. - constraint* insert(constraint_ref c); - clause* insert(clause_ref cl); + constraint* store(constraint_ref c); + clause* store(clause_ref cl); - // Release constraints at the given level and above. + /// Register a unit clause with an external dependency. + void register_external(constraint* c); + + /// Release constraints at the given level and above. void release_level(unsigned lvl); constraint* lookup(sat::bool_var var) const; constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); } - constraint_ref eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d); - constraint_ref ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); - constraint_ref ult(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); - constraint_ref sle(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); - constraint_ref slt(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); + constraint_literal eq(unsigned lvl, pdd const& p); + constraint_literal ule(unsigned lvl, pdd const& a, pdd const& b); + constraint_literal ult(unsigned lvl, pdd const& a, pdd const& b); + constraint_literal sle(unsigned lvl, pdd const& a, pdd const& b); + constraint_literal slt(unsigned lvl, pdd const& a, pdd const& b); + + // p_dependency_ref null_dep() const { return {nullptr, m_dm}; } }; @@ -101,20 +108,17 @@ namespace polysat { friend class ule_constraint; constraint_manager* m_manager; - unsigned m_ref_count = 0; - // bool m_stored = false; ///< Whether it has been inserted into the constraint_manager to be tracked by level - unsigned m_storage_level; ///< Controls lifetime of the constraint object. Always a base level (for external dependencies the level at which it was created, and for others the maximum storage level of its external dependencies). - // unsigned m_active_level = UINT_MAX; ///< Level at which the constraint was activated. Possibly different from m_storage_level because constraints in lemmas may become activated only at a higher level. NOTE: this is actually the level of the corresponding bool_var. - ckind_t m_kind; - p_dependency_ref m_dep; - unsigned_vector m_vars; - sat::bool_var m_bvar; ///< boolean variable associated to this constraint; convention: a constraint itself always represents the positive sat::literal - csign_t m_sign; ///< sign/polarity - lbool m_status = l_undef; ///< current constraint status, computed from value of m_lit and m_sign - lbool m_bvalue = l_undef; ///< TODO: remove m_sign and m_bvalue, use m_status as current value. the constraint itself is always the positive literal. use unit clauses for unit/external constraints; negation may come in through there. + clause* m_unit_clause = nullptr; ///< If this constraint was asserted by a unit clause, we store that clause here. + unsigned m_ref_count = 0; + // TODO: we could remove the level on constraints and instead store constraint_refs for all literals inside the clause? (clauses will then be 4 times larger though...) + unsigned m_storage_level; ///< Controls lifetime of the constraint object. Always a base level. + ckind_t m_kind; + unsigned_vector m_vars; + sat::bool_var m_bvar; ///< boolean variable associated to this constraint; convention: a constraint itself always represents the positive sat::literal + lbool m_status = l_undef; ///< current constraint status; intended to be the same as m_manager->m_bvars.value(bvar()) if that value is set. - constraint(constraint_manager& m, unsigned lvl, csign_t sign, p_dependency_ref const& dep, ckind_t k): - m_manager(&m), m_storage_level(lvl), m_kind(k), m_dep(dep), m_bvar(m_manager->m_bvars.new_var()), m_sign(sign) { + constraint(constraint_manager& m, unsigned lvl, ckind_t k): + m_manager(&m), m_storage_level(lvl), m_kind(k), m_bvar(m_manager->m_bvars.new_var()) { SASSERT_EQ(m_manager->get_bv2c(bvar()), nullptr); m_manager->insert_bv2c(bvar(), this); } @@ -146,7 +150,6 @@ namespace polysat { eq_constraint const& to_eq() const; ule_constraint& to_ule(); ule_constraint const& to_ule() const; - p_dependency* dep() const { return m_dep; } unsigned_vector& vars() { return m_vars; } unsigned_vector const& vars() const { return m_vars; } unsigned level() const { return m_storage_level; } @@ -158,22 +161,21 @@ namespace polysat { // return !is_undef() && active_level() <= s.base_level(); // } sat::bool_var bvar() const { return m_bvar; } - sat::literal blit() const { SASSERT(m_bvalue != l_undef); return m_bvalue == l_true ? sat::literal(m_bvar) : ~sat::literal(m_bvar); } - bool sign() const { return m_sign; } + + sat::literal blit() const { SASSERT(!is_undef()); return m_status == l_true ? sat::literal(m_bvar) : ~sat::literal(m_bvar); } void assign(bool is_true) { - SASSERT(m_bvalue == l_undef || m_bvalue == to_lbool(is_true)); - m_bvalue = to_lbool(is_true); - lbool new_status = (is_true ^ !m_sign) ? l_true : l_false; - SASSERT(is_undef() || new_status == m_status); - m_status = new_status; + SASSERT(m_status == l_undef /* || m_status == to_lbool(is_true) */); + m_status = to_lbool(is_true); + // SASSERT(m_manager->m_bvars.value(bvar()) == l_undef || m_manager->m_bvars.value(bvar()) == m_status); // TODO: is this always true? maybe we sometimes want to check the opposite phase temporarily. } - void unassign() { m_status = l_undef; m_bvalue = l_undef; } + void unassign() { m_status = l_undef; } bool is_undef() const { return m_status == l_undef; } bool is_positive() const { return m_status == l_true; } bool is_negative() const { return m_status == l_false; } - // TODO: must return a 'clause_ref' instead. If we resolve with a non-base constraint, we need to keep it in the clause (or should we track those as dependencies? the level needs to be higher then.) - virtual constraint_ref resolve(solver& s, pvar v) = 0; + clause* unit_clause() const { return m_unit_clause; } + void set_unit_clause(clause* cl) { SASSERT(cl); SASSERT(!m_unit_clause); m_unit_clause = cl; } + p_dependency* unit_dep() const; /** Precondition: all variables other than v are assigned. * @@ -181,18 +183,50 @@ namespace polysat { * \param[out] out_neg_cond Negation of the side condition (the side condition is true when the forbidden interval is trivial). May be NULL if the condition is constant. * \returns True iff a forbidden interval exists and the output parameters were set. */ - virtual bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_ref& out_neg_cond) { return false; } + virtual bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) { return false; } }; inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); } - // Disjunction of constraints represented by boolean literals + + /// Literal together with the constraint it represents. + /// (or: constraint with polarity) + class constraint_literal { + sat::literal m_literal = sat::null_literal; + constraint_ref m_constraint = nullptr; + + public: + constraint_literal() {} + constraint_literal(sat::literal lit, constraint_ref c): + m_literal(lit), m_constraint(std::move(c)) { + SASSERT(get()); + SASSERT(literal().var() == get()->bvar()); + } + constraint_literal operator~() const&& { + return {~m_literal, std::move(m_constraint)}; + } + sat::literal literal() const { return m_literal; } + constraint* get() const { return m_constraint.get(); } + constraint_ref detach() { m_literal = sat::null_literal; return std::move(m_constraint); } + + explicit operator bool() const { return !!m_constraint; } + bool operator!() const { return !m_constraint; } + polysat::constraint* operator->() const { return m_constraint.get(); } + polysat::constraint const& operator*() const { return *m_constraint; } + + constraint_literal& operator=(nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; } + private: + friend class constraint_manager; + explicit constraint_literal(polysat::constraint* c): constraint_literal(sat::literal(c->bvar()), c) {} + }; + + + /// Disjunction of constraints represented by boolean literals class clause { friend class constraint_manager; unsigned m_ref_count = 0; - unsigned m_level; // TODO: this is "storage" level, rename accordingly - // unsigned m_next_guess = UINT_MAX; // next guess for enumerative backtracking + unsigned m_level; unsigned m_next_guess = 0; // next guess for enumerative backtracking p_dependency_ref m_dep; sat::literal_vector m_literals; @@ -207,8 +241,8 @@ namespace polysat { } */ - clause(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector new_constraints): - m_level(lvl), m_dep(d), m_literals(std::move(literals)), m_new_constraints(std::move(new_constraints)) + clause(unsigned lvl, p_dependency_ref d, sat::literal_vector literals, constraint_ref_vector new_constraints): + m_level(lvl), m_dep(std::move(d)), m_literals(std::move(literals)), m_new_constraints(std::move(new_constraints)) { SASSERT(std::count(m_literals.begin(), m_literals.end(), sat::null_literal) == 0); } @@ -217,8 +251,8 @@ namespace polysat { void inc_ref() { m_ref_count++; } void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); } - static clause_ref from_unit(constraint_ref c); - static clause_ref from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector new_constraints); + static clause_ref from_unit(constraint_literal c, p_dependency_ref d); + static clause_ref from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals, constraint_ref_vector new_constraints); // Resolve with 'other' upon 'var'. bool resolve(sat::bool_var var, clause const& other); @@ -249,32 +283,6 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); } - /// Builds a clause from literals and constraints. - /// Takes care to - /// - skip literals that are active at the base level, - /// - skip trivial new constraints such as "4 <= 1". - class clause_builder { - solver& m_solver; - sat::literal_vector m_literals; - constraint_ref_vector m_new_constraints; - - public: - clause_builder(solver& s): m_solver(s) {} - - bool empty() const { return m_literals.empty() && m_new_constraints.empty(); } - void reset(); - - /// Build the clause. This will reset the clause builder so it can be reused. - clause_ref build(unsigned lvl, p_dependency_ref const& d); - - /// Add a literal to the clause. - /// Intended to be used for literals representing a constraint that already exists. - void push_literal(sat::literal lit); - /// Add a constraint to the clause that does not yet exist in the solver so far. - /// By convention, this will add the positive literal for this constraint. - /// (TODO: we might need to change this later; but then we will add a second argument for the literal or the sign.) - void push_new_constraint(constraint_ref c); - }; // Container for unit constraints and clauses. class constraints_and_clauses { @@ -344,13 +352,13 @@ namespace polysat { tmp_assign(constraint* c, sat::literal lit): m_constraint(c) { SASSERT(c); - SASSERT(c->bvar() == lit.var()); + SASSERT_EQ(c->bvar(), lit.var()); if (c->is_undef()) { c->assign(!lit.sign()); m_should_unassign = true; } else - SASSERT(c->blit() == lit); + SASSERT_EQ(c->blit(), lit); } tmp_assign(constraint_ref const& c, sat::literal lit): tmp_assign(c.get(), lit) {} void revert() { @@ -368,4 +376,5 @@ namespace polysat { tmp_assign& operator=(tmp_assign&&) = delete; }; + inline p_dependency* constraint::unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; } } diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp index f1d96672c..18b7cc81c 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/src/math/polysat/eq_constraint.cpp @@ -19,19 +19,10 @@ Author: namespace polysat { std::ostream& eq_constraint::display(std::ostream& out) const { - out << p() << (sign() == pos_t ? " == 0" : " != 0"); + out << p() << " == 0 "; return display_extra(out); } - constraint_ref eq_constraint::resolve(solver& s, pvar v) { - if (is_positive()) - return eq_resolve(s, v); - if (is_negative()) - return diseq_resolve(s, v); - UNREACHABLE(); - return nullptr; - } - void eq_constraint::narrow(solver& s) { SASSERT(!is_undef()); LOG("Assignment: " << assignments_pp(s)); @@ -110,47 +101,36 @@ namespace polysat { * Equality constraints */ - constraint_ref eq_constraint::eq_resolve(solver& s, pvar v) { - LOG("Resolve " << *this << " upon v" << v); - if (s.m_conflict.size() != 1) - return nullptr; - if (!s.m_conflict.clauses().empty()) - return nullptr; - constraint* c = s.m_conflict.units()[0]; - SASSERT(c->is_currently_false(s)); - // 'c == this' can happen if propagation was from decide() with only one value left - // (e.g., if there's an unsatisfiable clause and we try all values). - // Resolution would give us '0 == 0' in this case, which is useless. - if (c == this) - return nullptr; - SASSERT(is_currently_true(s)); // TODO: might not always hold (due to similar case as in comment above?) - if (c->is_eq() && c->is_positive()) { - pdd a = c->to_eq().p(); - pdd b = p(); - pdd r = a; - if (!a.resolve(v, b, r)) - return nullptr; - p_dependency_ref d(s.m_dm.mk_join(c->dep(), dep()), s.m_dm); - unsigned lvl = std::max(c->level(), level()); - return s.m_constraints.eq(lvl, pos_t, r, d); - } - return nullptr; - } - - - /** - * Disequality constraints - */ - - constraint_ref eq_constraint::diseq_resolve(solver& s, pvar v) { - NOT_IMPLEMENTED_YET(); - return nullptr; - } - + // constraint_ref eq_constraint::eq_resolve(solver& s, pvar v) { + // LOG("Resolve " << *this << " upon v" << v); + // if (s.m_conflict.size() != 1) + // return nullptr; + // if (!s.m_conflict.clauses().empty()) + // return nullptr; + // constraint* c = s.m_conflict.units()[0]; + // SASSERT(c->is_currently_false(s)); + // // 'c == this' can happen if propagation was from decide() with only one value left + // // (e.g., if there's an unsatisfiable clause and we try all values). + // // Resolution would give us '0 == 0' in this case, which is useless. + // if (c == this) + // return nullptr; + // SASSERT(is_currently_true(s)); // TODO: might not always hold (due to similar case as in comment above?) + // if (c->is_eq() && c->is_positive()) { + // pdd a = c->to_eq().p(); + // pdd b = p(); + // pdd r = a; + // if (!a.resolve(v, b, r)) + // return nullptr; + // p_dependency_ref d(s.m_dm.mk_join(c->dep(), dep()), s.m_dm); + // unsigned lvl = std::max(c->level(), level()); + // return s.m_constraints.eq(lvl, pos_t, r, d); + // } + // return nullptr; + // } /// Compute forbidden interval for equality constraint by considering it as p <=u 0 (or p >u 0 for disequality) - bool eq_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_ref& out_neg_cond) + bool eq_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) { SASSERT(!is_undef()); diff --git a/src/math/polysat/eq_constraint.h b/src/math/polysat/eq_constraint.h index 83f56b30f..b1790303b 100644 --- a/src/math/polysat/eq_constraint.h +++ b/src/math/polysat/eq_constraint.h @@ -20,24 +20,19 @@ namespace polysat { class eq_constraint : public constraint { pdd m_poly; public: - eq_constraint(constraint_manager& m, unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& dep): - constraint(m, lvl, sign, dep, ckind_t::eq_t), m_poly(p) { + eq_constraint(constraint_manager& m, unsigned lvl, pdd const& p): + constraint(m, lvl, ckind_t::eq_t), m_poly(p) { m_vars.append(p.free_vars()); } ~eq_constraint() override {} pdd const & p() const { return m_poly; } std::ostream& display(std::ostream& out) const override; - constraint_ref resolve(solver& s, pvar v) override; bool is_always_false() override; bool is_currently_false(solver& s) override; bool is_currently_true(solver& s) override; void narrow(solver& s) override; - bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_ref& out_neg_cond) override; + bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) override; inequality as_inequality() const override; - - private: - constraint_ref eq_resolve(solver& s, pvar v); - constraint_ref diseq_resolve(solver& s, pvar v); }; } diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 0509a099b..bf33d4f55 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -32,6 +32,15 @@ namespace polysat { for (auto* c : m_conflict.clauses()) LOG("Clause: " << show_deref(c)); + // TODO: this is a temporary workaround! we should not get any undef constraints at this point + constraints_and_clauses confl = std::move(m_conflict); + SASSERT(m_conflict.empty()); + for (auto* c : confl.units()) + if (!c->is_undef()) + m_conflict.push_back(c); + for (auto* c : confl.clauses()) + m_conflict.push_back(c); + // TODO: we should share work done for examining constraints between different resolution methods clause_ref lemma; if (!lemma) lemma = by_polynomial_superposition(); @@ -40,15 +49,32 @@ namespace polysat { if (!lemma) lemma = by_ugt_z(); if (!lemma) lemma = y_ule_ax_and_x_ule_z(); - if (lemma) { - LOG("New lemma: " << *lemma); - for (auto* c : lemma->new_constraints()) { - LOG("New constraint: " << show_deref(c)); + DEBUG_CODE({ + if (lemma) { + LOG("New lemma: " << *lemma); + for (auto* c : lemma->new_constraints()) { + LOG("New constraint: " << show_deref(c)); + } + // All constraints in the lemma must be false in the conflict state + for (auto lit : lemma->literals()) { + if (m_solver.m_bvars.value(lit.var()) == l_false) + continue; + SASSERT(m_solver.m_bvars.value(lit.var()) != l_true); + constraint* c = m_solver.m_constraints.lookup(lit.var()); + SASSERT(c); + tmp_assign _t(c, lit); + // if (c->is_currently_true(m_solver)) { + // LOG("ERROR: constraint is true: " << show_deref(c)); + // SASSERT(false); + // } + // SASSERT(!c->is_currently_true(m_solver)); + // SASSERT(c->is_currently_false(m_solver)); // TODO: pvar v may not have a value at this point... + } } - } - else { - LOG("No lemma"); - } + else { + LOG("No lemma"); + } + }); m_var = null_var; m_cjust_v.reset(); @@ -70,11 +96,12 @@ namespace polysat { pdd r = a; if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r)) return nullptr; - p_dependency_ref d(m_solver.m_dm.mk_join(c1->dep(), c2->dep()), m_solver.m_dm); - unsigned lvl = std::max(c1->level(), c2->level()); - constraint_ref c = m_solver.m_constraints.eq(lvl, pos_t, r, d); - c->assign(true); - return clause::from_unit(c); + unsigned const lvl = std::max(c1->level(), c2->level()); + clause_builder clause(m_solver); + clause.push_literal(~c1->blit()); + clause.push_literal(~c2->blit()); + clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r)); + return clause.build(); } return nullptr; } @@ -108,19 +135,19 @@ namespace polysat { unsigned const lvl = c.src->level(); clause_builder clause(m_solver); + clause.push_literal(~c.src->blit()); // Omega^*(x, y) if (!push_omega_mul(clause, lvl, sz, x, y)) continue; - constraint_ref y_le_z; + constraint_literal y_le_z; if (c.is_strict) - y_le_z = m_solver.m_constraints.ult(lvl, pos_t, y, z, null_dep()); + y_le_z = m_solver.m_constraints.ult(lvl, y, z); else - y_le_z = m_solver.m_constraints.ule(lvl, pos_t, y, z, null_dep()); + y_le_z = m_solver.m_constraints.ule(lvl, y, z); LOG("z>y: " << show_deref(y_le_z)); clause.push_new_constraint(std::move(y_le_z)); - p_dependency_ref dep(c.src->dep(), m_solver.m_dm); - return clause.build(lvl, dep); + return clause.build(); } return nullptr; } @@ -181,20 +208,21 @@ namespace polysat { pdd const& z_prime = d.lhs; clause_builder clause(m_solver); + clause.push_literal(~c.src->blit()); + clause.push_literal(~d.src->blit()); // Omega^*(x, y) if (!push_omega_mul(clause, lvl, sz, x, y)) continue; // z'x <= zx - constraint_ref zpx_le_zx; + constraint_literal zpx_le_zx; if (c.is_strict || d.is_strict) - zpx_le_zx = m_solver.m_constraints.ult(lvl, pos_t, z_prime*x, z*x, null_dep()); + zpx_le_zx = m_solver.m_constraints.ult(lvl, z_prime*x, z*x); else - zpx_le_zx = m_solver.m_constraints.ule(lvl, pos_t, z_prime*x, z*x, null_dep()); + zpx_le_zx = m_solver.m_constraints.ule(lvl, z_prime*x, z*x); LOG("zx>z'x: " << show_deref(zpx_le_zx)); clause.push_new_constraint(std::move(zpx_le_zx)); - p_dependency_ref dep(m_solver.m_dm.mk_join(c.src->dep(), d.src->dep()), m_solver.m_dm); - return clause.build(lvl, dep); + return clause.build(); } } return nullptr; @@ -256,20 +284,21 @@ namespace polysat { pdd const& y_prime = d.rhs; clause_builder clause(m_solver); + clause.push_literal(~c.src->blit()); + clause.push_literal(~d.src->blit()); // Omega^*(x, y') if (!push_omega_mul(clause, lvl, sz, x, y_prime)) continue; // yx <= y'x - constraint_ref yx_le_ypx; + constraint_literal yx_le_ypx; if (c.is_strict || d.is_strict) - yx_le_ypx = m_solver.m_constraints.ult(lvl, pos_t, y*x, y_prime*x, null_dep()); + yx_le_ypx = m_solver.m_constraints.ult(lvl, y*x, y_prime*x); else - yx_le_ypx = m_solver.m_constraints.ule(lvl, pos_t, y*x, y_prime*x, null_dep()); + yx_le_ypx = m_solver.m_constraints.ule(lvl, y*x, y_prime*x); LOG("y'x>yx: " << show_deref(yx_le_ypx)); clause.push_new_constraint(std::move(yx_le_ypx)); - p_dependency_ref dep(m_solver.m_dm.mk_join(c.src->dep(), d.src->dep()), m_solver.m_dm); - return clause.build(lvl, dep); + return clause.build(); } } return nullptr; @@ -316,20 +345,21 @@ namespace polysat { pdd const& z = d.rhs; clause_builder clause(m_solver); + clause.push_literal(~c.src->blit()); + clause.push_literal(~d.src->blit()); // Omega^*(a, z) if (!push_omega_mul(clause, lvl, sz, a, z)) continue; // y'x > yx - constraint_ref y_ule_az; + constraint_literal y_ule_az; if (c.is_strict || d.is_strict) - y_ule_az = m_solver.m_constraints.ult(lvl, pos_t, y, a*z, null_dep()); + y_ule_az = m_solver.m_constraints.ult(lvl, y, a*z); else - y_ule_az = m_solver.m_constraints.ule(lvl, pos_t, y, a*z, null_dep()); + y_ule_az = m_solver.m_constraints.ule(lvl, y, a*z); LOG("y<=az: " << show_deref(y_ule_az)); clause.push_new_constraint(std::move(y_ule_az)); - p_dependency_ref dep(m_solver.m_dm.mk_join(c1->dep(), d.src->dep()), m_solver.m_dm); - return clause.build(lvl, dep); + return clause.build(); } } return nullptr; @@ -382,9 +412,9 @@ namespace polysat { SASSERT(min_k <= k && k <= max_k); // x >= 2^k - constraint_ref c1 = m_solver.m_constraints.ult(level, pos_t, pddm.mk_val(rational::power_of_two(k)), x, null_dep()); + auto c1 = m_solver.m_constraints.ule(level, pddm.mk_val(rational::power_of_two(k)), x); // y > 2^{p-k} - constraint_ref c2 = m_solver.m_constraints.ule(level, pos_t, pddm.mk_val(rational::power_of_two(p-k)), y, null_dep()); + auto c2 = m_solver.m_constraints.ult(level, pddm.mk_val(rational::power_of_two(p-k)), y); clause.push_new_constraint(std::move(c1)); clause.push_new_constraint(std::move(c2)); return true; diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h index 3ce5048d8..062fbe2d6 100644 --- a/src/math/polysat/explain.h +++ b/src/math/polysat/explain.h @@ -13,6 +13,7 @@ Author: --*/ #pragma once #include "math/polysat/constraint.h" +#include "math/polysat/clause_builder.h" #include "math/polysat/interval.h" #include "math/polysat/solver.h" diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index d9e58ee7b..0aa466fc7 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -14,13 +14,15 @@ Author: --*/ #include "math/polysat/forbidden_intervals.h" +#include "math/polysat/clause_builder.h" +#include "math/polysat/interval.h" #include "math/polysat/log.h" namespace polysat { struct fi_record { eval_interval interval; - constraint_ref neg_cond; // could be multiple constraints later + constraint_literal neg_cond; // could be multiple constraints later constraint* src; }; @@ -76,7 +78,7 @@ namespace polysat { continue; } eval_interval interval = eval_interval::full(); - constraint_ref neg_cond; + constraint_literal neg_cond; if (c->forbidden_interval(s, v, interval, neg_cond)) { LOG("interval: " << interval); LOG("neg_cond: " << show_deref(neg_cond)); @@ -107,9 +109,7 @@ namespace polysat { clause.push_literal(~full_record.src->blit()); if (full_record.neg_cond) clause.push_new_constraint(std::move(full_record.neg_cond)); - unsigned lemma_lvl = full_record.src->level(); - p_dependency_ref lemma_dep(full_record.src->dep(), s.m_dm); - out_lemma = clause.build(lemma_lvl, lemma_dep); + out_lemma = clause.build(); return true; } @@ -132,14 +132,11 @@ namespace polysat { LOG("seq: " << seq); SASSERT(seq.size() >= 2); // otherwise has_full should have been true - p_dependency* d = nullptr; unsigned lemma_lvl = 0; for (unsigned i : seq) { constraint* c = records[i].src; - d = s.m_dm.mk_join(d, c->dep()); lemma_lvl = std::max(lemma_lvl, c->level()); } - p_dependency_ref lemma_dep(d, s.m_dm); // Create lemma // Idea: @@ -166,16 +163,16 @@ namespace polysat { auto const& next_hi = records[next_i].interval.hi(); auto const& lhs = hi - next_lo; auto const& rhs = next_hi - next_lo; - constraint_ref c = s.m_constraints.ult(lemma_lvl, neg_t, lhs, rhs, s.mk_dep_ref(null_dependency)); + constraint_literal c = ~s.m_constraints.ult(lemma_lvl, lhs, rhs); LOG("constraint: " << *c); clause.push_new_constraint(std::move(c)); // Side conditions // TODO: check whether the condition is subsumed by c? maybe at the end do a "lemma reduction" step, to try and reduce branching? - constraint_ref& neg_cond = records[i].neg_cond; + constraint_literal& neg_cond = records[i].neg_cond; if (neg_cond) clause.push_new_constraint(std::move(neg_cond)); } - out_lemma = clause.build(lemma_lvl, lemma_dep); + out_lemma = clause.build(); return true; } diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index b36fdcb08..f36e90452 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -15,7 +15,6 @@ Author: --*/ #pragma once #include "math/polysat/constraint.h" -#include "math/polysat/interval.h" #include "math/polysat/solver.h" namespace polysat { diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 3815c876d..e838fbbba 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -61,7 +61,7 @@ namespace polysat { m_disjunctive_lemma.reset(); while (m_lim.inc()) { m_stats.m_num_iterations++; - LOG_H1("Next solving loop iteration"); + LOG_H1("Next solving loop iteration (#" << m_stats.m_num_iterations << ")"); LOG("Free variables: " << m_free_vars); LOG("Assignment: " << assignments_pp(*this)); if (!m_conflict.empty()) LOG("Conflict: " << m_conflict); @@ -112,42 +112,47 @@ namespace polysat { m_free_vars.del_var_eh(v); } - constraint_ref solver::mk_eq(pdd const& p, unsigned dep) { - return m_constraints.eq(m_level, pos_t, p, mk_dep_ref(dep)); + constraint_literal solver::mk_eq(pdd const& p) { + return m_constraints.eq(m_level, p); } - constraint_ref solver::mk_diseq(pdd const& p, unsigned dep) { - return m_constraints.eq(m_level, neg_t, p, mk_dep_ref(dep)); + constraint_literal solver::mk_diseq(pdd const& p) { + return ~m_constraints.eq(m_level, p); } - constraint_ref solver::mk_ule(pdd const& p, pdd const& q, unsigned dep) { - return m_constraints.ule(m_level, pos_t, p, q, mk_dep_ref(dep)); + constraint_literal solver::mk_ule(pdd const& p, pdd const& q) { + return m_constraints.ule(m_level, p, q); } - constraint_ref solver::mk_ult(pdd const& p, pdd const& q, unsigned dep) { - return m_constraints.ult(m_level, pos_t, p, q, mk_dep_ref(dep)); + constraint_literal solver::mk_ult(pdd const& p, pdd const& q) { + return m_constraints.ult(m_level, p, q); } - constraint_ref solver::mk_sle(pdd const& p, pdd const& q, unsigned dep) { - return m_constraints.sle(m_level, pos_t, p, q, mk_dep_ref(dep)); + constraint_literal solver::mk_sle(pdd const& p, pdd const& q) { + return m_constraints.sle(m_level, p, q); } - constraint_ref solver::mk_slt(pdd const& p, pdd const& q, unsigned dep) { - return m_constraints.slt(m_level, pos_t, p, q, mk_dep_ref(dep)); + constraint_literal solver::mk_slt(pdd const& p, pdd const& q) { + return m_constraints.slt(m_level, p, q); } - void solver::new_constraint(constraint_ref cr, bool activate) { + void solver::new_constraint(constraint_literal cl, unsigned dep, bool activate) { VERIFY(at_base_level()); - SASSERT(cr); - SASSERT(activate || cr->dep()); // if we don't activate the constraint, we need the dependency to access it again later. - constraint* c = m_constraints.insert(std::move(cr)); + SASSERT(cl); + SASSERT(activate || dep != null_dependency); // if we don't activate the constraint, we need the dependency to access it again later. + sat::literal lit = cl.literal(); + constraint* c = cl.get(); + clause* unit = m_constraints.store(clause::from_unit(std::move(cl), mk_dep_ref(dep))); + c->set_unit_clause(unit); + if (dep != null_dependency) + m_constraints.register_external(c); LOG("New constraint: " << *c); m_original.push_back(c); #if ENABLE_LINEAR_SOLVER m_linear_solver.new_constraint(*c); #endif if (activate && !is_conflict()) - activate_constraint_base(c); + activate_constraint_base(c, !lit.sign()); } void solver::assign_eh(unsigned dep, bool is_true) { @@ -159,7 +164,7 @@ namespace polysat { } if (is_conflict()) return; - activate_constraint_base(c); + activate_constraint_base(c, is_true); } @@ -382,7 +387,7 @@ namespace polysat { void solver::set_conflict(constraint& c) { LOG("Conflict: " << c); - LOG(*this); + LOG("\n" << *this); SASSERT(!is_conflict()); m_conflict.push_back(&c); } @@ -442,7 +447,7 @@ namespace polysat { void solver::resolve_conflict() { IF_VERBOSE(1, verbose_stream() << "resolve conflict\n"); LOG_H2("Resolve conflict"); - LOG(*this); + LOG("\n" << *this); LOG("search state: " << m_search); ++m_stats.m_num_conflicts; @@ -489,6 +494,7 @@ namespace polysat { conflict_explainer cx(*this, m_conflict); lemma = cx.resolve(conflict_var, {}); LOG("resolved: " << show_deref(lemma)); + // SASSERT(false && "pause on explanation"); } } @@ -678,7 +684,7 @@ namespace polysat { p_dependency_ref conflict_dep(m_dm); for (auto& c : m_conflict.units()) if (c) - conflict_dep = m_dm.mk_join(c->dep(), conflict_dep); + conflict_dep = m_dm.mk_join(c->unit_dep(), conflict_dep); for (auto& c : m_conflict.clauses()) conflict_dep = m_dm.mk_join(c->dep(), conflict_dep); m_dm.linearize(conflict_dep, deps); @@ -706,21 +712,15 @@ namespace polysat { c = m_constraints.lookup(lemma->literals()[0].var()); } SASSERT_EQ(lemma->literals()[0].var(), c->bvar()); - SASSERT(!lemma->literals()[0].sign()); // TODO: that case is handled incorrectly atm - learn_lemma_unit(v, std::move(c)); + SASSERT(c); + add_lemma_unit(c); + push_cjust(v, c.get()); + activate_constraint_base(c.get(), !lemma->literals()[0].sign()); } else learn_lemma_clause(v, std::move(lemma)); } - void solver::learn_lemma_unit(pvar v, constraint_ref lemma) { - SASSERT(lemma); - constraint* c = lemma.get(); - add_lemma_unit(std::move(lemma)); - push_cjust(v, c); - activate_constraint_base(c); - } - void solver::learn_lemma_clause(pvar v, clause_ref lemma) { SASSERT(lemma); sat::literal lit = decide_bool(*lemma); @@ -744,6 +744,7 @@ namespace polysat { SASSERT(m_bvars.value(lit) != l_true); // cannot happen in a valid lemma constraint* c = m_constraints.lookup(lit.var()); tmp_assign _t(c, lit); + SASSERT(!c->is_currently_true(*this)); // should not happen in a valid lemma return !c->is_currently_false(*this); }; @@ -863,19 +864,19 @@ namespace polysat { // * the reason for reverting this decision then needs to be the (negation of the) conflicting literals. Or we give up on resolving this lemma? SASSERT(m_conflict.clauses().empty()); // not sure how to handle otherwise clause_builder clause(*this); - unsigned reason_lvl = m_constraints.lookup(lit.var())->level(); - p_dependency_ref reason_dep(m_constraints.lookup(lit.var())->dep(), m_dm); + // unsigned reason_lvl = m_constraints.lookup(lit.var())->level(); + // p_dependency_ref reason_dep(m_constraints.lookup(lit.var())->dep(), m_dm); clause.push_literal(~lit); // propagated literal for (auto c : m_conflict.units()) { if (c->bvar() == var) continue; if (c->is_undef()) // TODO: see revert_decision for a note on this. continue; - reason_lvl = std::max(reason_lvl, c->level()); - reason_dep = m_dm.mk_join(reason_dep, c->dep()); + // reason_lvl = std::max(reason_lvl, c->level()); + // reason_dep = m_dm.mk_join(reason_dep, c->dep()); clause.push_literal(c->blit()); } - reason = clause.build(reason_lvl, reason_dep); + reason = clause.build(); LOG("Made-up reason: " << show_deref(reason)); } @@ -923,7 +924,7 @@ namespace polysat { SASSERT(reason->literals()[0] == lit); constraint* c = m_constraints.lookup(lit.var()); m_redundant.push_back(c); - activate_constraint_base(c); + activate_constraint_base(c, !lit.sign()); } else assign_bool_backtrackable(lit, reason, nullptr); @@ -945,15 +946,16 @@ namespace polysat { /// Activate a constraint at the base level. /// Used for external unit constraints and unit consequences. - void solver::activate_constraint_base(constraint* c) { + void solver::activate_constraint_base(constraint* c, bool is_true) { SASSERT(c); - assign_bool_core(sat::literal(c->bvar()), nullptr, nullptr); - activate_constraint(*c, true); // c must be in m_original or m_redundant so it can be deactivated properly when popping the base level SASSERT_EQ(std::count(m_original.begin(), m_original.end(), c) + std::count(m_redundant.begin(), m_redundant.end(), c), 1); + sat::literal lit(c->bvar(), !is_true); + assign_bool_core(lit, nullptr, nullptr); + activate_constraint(*c, is_true); } - /// Assign a boolean literal and activate the corresponding constraint + /// Assign a boolean literal void solver::assign_bool_core(sat::literal lit, clause* reason, clause* lemma) { LOG("Assigning boolean literal: " << lit); m_bvars.assign(lit, m_level, reason, lemma); @@ -976,6 +978,9 @@ namespace polysat { LOG("Deactivating constraint: " << c); erase_watch(c); c.unassign(); +#if ENABLE_LINEAR_SOLVER + m_linear_solver.deactivate_constraint(c); // TODO add this method to linear solver? +#endif } void solver::backjump(unsigned new_level) { @@ -998,6 +1003,7 @@ namespace polysat { conflict_explainer cx(*this, m_conflict); clause_ref res = cx.resolve(v, m_cjust[v]); LOG("resolved: " << show_deref(res)); + // SASSERT(false && "pause on explanation"); return res; } @@ -1013,20 +1019,22 @@ namespace polysat { if (!lemma) return; LOG("Lemma: " << show_deref(lemma)); - constraint* c = m_constraints.insert(std::move(lemma)); + constraint* c = m_constraints.store(std::move(lemma)); insert_constraint(m_redundant, c); + // TODO: create unit clause } // Add lemma to storage but do not activate it void solver::add_lemma_clause(clause_ref lemma) { if (!lemma) return; + // TODO: check for unit clauses! LOG("Lemma: " << show_deref(lemma)); if (lemma->size() < 2) { LOG_H1("TODO: this should be treated as unit constraint and asserted at the base level!"); } // SASSERT(lemma->size() > 1); - clause* cl = m_constraints.insert(std::move(lemma)); + clause* cl = m_constraints.store(std::move(lemma)); m_redundant_clauses.push_back(cl); } @@ -1074,7 +1082,15 @@ namespace polysat { } bool solver::active_at_base_level(sat::bool_var bvar) const { - return m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level(); + // NOTE: this active_at_base_level is actually not what we want!!! + // first of all, it might not really be a base level: could be a non-base level between previous base levels. + // in that case, how do we determine the right dependencies??? + // secondly, we are interested in "unit clauses", not as much whether we assigned something on the base level... + // TODO: however, propagating stuff at the base level... need to be careful with dependencies there... might need to turn all base-level propagations into unit clauses... + VERIFY(false); + // bool res = m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level(); + // SASSERT_EQ(res, !!m_constraints.lookup(bvar)->unit_clause()); + // return res; } bool solver::try_eval(pdd const& p, rational& out_value) const { @@ -1085,14 +1101,16 @@ namespace polysat { } std::ostream& solver::display(std::ostream& out) const { + out << "Assignment:\n"; for (auto [v, val] : assignment()) { auto j = m_justification[v]; - out << assignment_pp(*this, v, val) << " @" << j.level(); + out << "\t" << assignment_pp(*this, v, val) << " @" << j.level(); if (j.is_propagation()) out << " " << m_cjust[v]; out << "\n"; // out << m_viable[v] << "\n"; } + out << "Boolean assignment:\n\t" << m_bvars << "\n"; out << "Original:\n"; for (auto* c : m_original) out << "\t" << *c << "\n"; diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index fffda2277..b6a292b38 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -21,6 +21,7 @@ Author: #include "util/statistics.h" #include "math/polysat/boolean.h" #include "math/polysat/constraint.h" +#include "math/polysat/clause_builder.h" #include "math/polysat/eq_constraint.h" #include "math/polysat/ule_constraint.h" #include "math/polysat/justification.h" @@ -96,14 +97,6 @@ namespace polysat { search_state m_search; assignment_t const& assignment() const { return m_search.assignment(); } - // (old, remove later) - // using bool_clauses = ptr_vector; - // vector m_bool_value; // value of boolean literal (indexed by literal) - // vector m_bool_watch; // watch list into clauses (indexed by literal) - // // scoped_ptr_vector m_bool_clauses; // NOTE: as of now, external clauses will only be units! So this is not needed. - // svector m_bool_units; // externally asserted unit clauses, via assign_eh - // scoped_ptr_vector m_bool_redundant; // learned clause storage - unsigned m_qhead { 0 }; // next item to propagate (index into m_search) unsigned m_level { 0 }; @@ -155,7 +148,7 @@ namespace polysat { void pop_constraints(ptr_vector& cs); void assign_bool_backtrackable(sat::literal lit, clause* reason, clause* lemma); - void activate_constraint_base(constraint* c); + void activate_constraint_base(constraint* c, bool is_true); void assign_bool_core(sat::literal lit, clause* reason, clause* lemma); // void assign_bool_base(sat::literal lit); void activate_constraint(constraint& c, bool is_true); @@ -224,19 +217,18 @@ namespace polysat { void revert_decision(pvar v, clause_ref reason); void revert_bool_decision(sat::literal lit, clause_ref reason); void learn_lemma(pvar v, clause_ref lemma); - void learn_lemma_unit(pvar v, constraint_ref lemma); void learn_lemma_clause(pvar v, clause_ref lemma); void backjump(unsigned new_level); void add_lemma_unit(constraint_ref lemma); void add_lemma_clause(clause_ref lemma); - constraint_ref mk_eq(pdd const& p, unsigned dep); - constraint_ref mk_diseq(pdd const& p, unsigned dep); - constraint_ref mk_ule(pdd const& p, pdd const& q, unsigned dep); - constraint_ref mk_ult(pdd const& p, pdd const& q, unsigned dep); - constraint_ref mk_sle(pdd const& p, pdd const& q, unsigned dep); - constraint_ref mk_slt(pdd const& p, pdd const& q, unsigned dep); - void new_constraint(constraint_ref c, bool activate); + constraint_literal mk_eq(pdd const& p); + constraint_literal mk_diseq(pdd const& p); + constraint_literal mk_ule(pdd const& p, pdd const& q); + constraint_literal mk_ult(pdd const& p, pdd const& q); + constraint_literal mk_sle(pdd const& p, pdd const& q); + constraint_literal mk_slt(pdd const& p, pdd const& q); + void new_constraint(constraint_literal c, unsigned dep, bool activate); static void insert_constraint(ptr_vector& cs, constraint* c); bool invariant(); @@ -301,20 +293,20 @@ namespace polysat { * Create polynomial constraints (but do not activate them). * Each constraint is tracked by a dependency. */ - void new_eq(pdd const& p, unsigned dep) { new_constraint(mk_eq(p, dep), false); } - void new_diseq(pdd const& p, unsigned dep) { new_constraint(mk_diseq(p, dep), false); } - void new_ule(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ule(p, q, dep), false); } - void new_ult(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ult(p, q, dep), false); } - void new_sle(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_sle(p, q, dep), false); } - void new_slt(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_slt(p, q, dep), false); } + void new_eq(pdd const& p, unsigned dep) { new_constraint(mk_eq(p), dep, false); } + void new_diseq(pdd const& p, unsigned dep) { new_constraint(mk_diseq(p), dep, false); } + void new_ule(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ule(p, q), dep, false); } + void new_ult(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ult(p, q), dep, false); } + void new_sle(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_sle(p, q), dep, false); } + void new_slt(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_slt(p, q), dep, false); } /** Create and activate polynomial constraints. */ - void add_eq(pdd const& p, unsigned dep = null_dependency) { new_constraint(mk_eq(p, dep), true); } - void add_diseq(pdd const& p, unsigned dep = null_dependency) { new_constraint(mk_diseq(p, dep), true); } - void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ule(p, q, dep), true); } - void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ult(p, q, dep), true); } - void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_sle(p, q, dep), true); } - void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_slt(p, q, dep), true); } + void add_eq(pdd const& p, unsigned dep = null_dependency) { new_constraint(mk_eq(p), dep, true); } + void add_diseq(pdd const& p, unsigned dep = null_dependency) { new_constraint(mk_diseq(p), dep, true); } + void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ule(p, q), dep, true); } + void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ult(p, q), dep, true); } + void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_sle(p, q), dep, true); } + void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_slt(p, q), dep, true); } /** * Activate the constraint corresponding to the given boolean variable. diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index 965383365..e53bb26f4 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -19,14 +19,10 @@ Author: namespace polysat { std::ostream& ule_constraint::display(std::ostream& out) const { - out << m_lhs << (sign() == pos_t ? " <= " : " > ") << m_rhs; + out << m_lhs << " <= " << m_rhs; return display_extra(out); } - constraint_ref ule_constraint::resolve(solver& s, pvar v) { - return nullptr; - } - void ule_constraint::narrow(solver& s) { LOG_H3("Narrowing " << *this); LOG("Assignment: " << assignments_pp(s)); @@ -117,7 +113,7 @@ namespace polysat { return p.is_val() && q.is_val() && p.val() > q.val(); } - bool ule_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_ref& out_neg_cond) + bool ule_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) { SASSERT(!is_undef()); @@ -247,8 +243,10 @@ namespace polysat { SASSERT(is_trivial == condition_body.is_zero()); out_neg_cond = nullptr; } + else if (is_trivial) + out_neg_cond = ~s.m_constraints.eq(level(), condition_body); else - out_neg_cond = s.m_constraints.eq(level(), is_trivial ? neg_t : pos_t, condition_body, s.mk_dep_ref(null_dependency)); + out_neg_cond = s.m_constraints.eq(level(), condition_body); if (is_trivial) { if (is_positive()) diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index 807dfec34..f0e94e5bd 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -21,8 +21,8 @@ namespace polysat { pdd m_lhs; pdd m_rhs; public: - ule_constraint(constraint_manager& m, unsigned lvl, csign_t sign, pdd const& l, pdd const& r, p_dependency_ref const& dep): - constraint(m, lvl, sign, dep, ckind_t::ule_t), m_lhs(l), m_rhs(r) { + ule_constraint(constraint_manager& m, unsigned lvl, pdd const& l, pdd const& r): + constraint(m, lvl, ckind_t::ule_t), m_lhs(l), m_rhs(r) { m_vars.append(l.free_vars()); for (auto v : r.free_vars()) if (!m_vars.contains(v)) @@ -32,13 +32,12 @@ namespace polysat { pdd const& lhs() const { return m_lhs; } pdd const& rhs() const { return m_rhs; } std::ostream& display(std::ostream& out) const override; - constraint_ref resolve(solver& s, pvar v) override; bool is_always_false(pdd const& lhs, pdd const& rhs); bool is_always_false() override; bool is_currently_false(solver& s) override; bool is_currently_true(solver& s) override; void narrow(solver& s) override; - bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_ref& out_neg_cond) override; + bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) override; inequality as_inequality() const override; }; diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index ab0af87ea..b84db711b 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -833,8 +833,8 @@ namespace polysat { void tst_polysat() { - polysat::test_monot_bounds(8); - // polysat::test_monot_bounds_simple(8); + // polysat::test_monot_bounds(8); + polysat::test_monot_bounds_simple(8); return; polysat::test_add_conflicts();