From ebaea2159e6e7527ca66f2ae3ae2c3d62de3dfff Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 18 Aug 2021 20:02:46 +0200 Subject: [PATCH] Polysat: use constraint_literal and begin move to core-based conflict representation (#5489) * Rename solver_scope for fixplex tests (otherwise the wrong constructor is called for polysat's solver_scope) * Update conflict_core * simplify * Be clearer about constraint_literal lifetime * remove old comment * Remove status (positive/negative) from constraint * Use constraint_literal in the solver * Fix build (constraint -> get_constraint) --- src/math/polysat/clause_builder.cpp | 6 +- src/math/polysat/clause_builder.h | 2 +- src/math/polysat/conflict_core.cpp | 35 +- src/math/polysat/conflict_core.h | 47 +- src/math/polysat/constraint.cpp | 78 +- src/math/polysat/constraint.h | 243 +++--- src/math/polysat/eq_constraint.cpp | 70 +- src/math/polysat/eq_constraint.h | 14 +- src/math/polysat/explain.cpp | 983 ++++++++++++----------- src/math/polysat/explain.h | 32 +- src/math/polysat/forbidden_intervals.cpp | 32 +- src/math/polysat/forbidden_intervals.h | 2 +- src/math/polysat/linear_solver.cpp | 2 - src/math/polysat/log_helper.h | 15 - src/math/polysat/solver.cpp | 234 +++--- src/math/polysat/solver.h | 62 +- src/math/polysat/ule_constraint.cpp | 59 +- src/math/polysat/ule_constraint.h | 16 +- src/test/fixplex.cpp | 5 +- 19 files changed, 933 insertions(+), 1004 deletions(-) diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp index 792da5ce3..2135e82a7 100644 --- a/src/math/polysat/clause_builder.cpp +++ b/src/math/polysat/clause_builder.cpp @@ -52,12 +52,10 @@ namespace polysat { m_literals.push_back(lit); } - void clause_builder::push_new_constraint(constraint_literal c) { + void clause_builder::push_new_constraint(constraint_literal_ref 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()) + if (c.get().is_always_false()) return; m_level = std::max(m_level, c->level()); m_literals.push_back(c.literal()); diff --git a/src/math/polysat/clause_builder.h b/src/math/polysat/clause_builder.h index c01af485e..dfa65a21d 100644 --- a/src/math/polysat/clause_builder.h +++ b/src/math/polysat/clause_builder.h @@ -46,7 +46,7 @@ namespace polysat { 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); + void push_new_constraint(constraint_literal_ref c); }; } diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp index 7306e381f..37ceff69e 100644 --- a/src/math/polysat/conflict_core.cpp +++ b/src/math/polysat/conflict_core.cpp @@ -20,9 +20,40 @@ Author: namespace polysat { std::ostream& conflict_core::display(std::ostream& out) const { - out << "TODO: display conflict_core"; - // depending on sign: A /\ B /\ C or ¬A \/ ¬B \/ ¬C + bool first = true; + for (auto c : m_constraints) { + if (first) + first = false; + else + out << " ; "; + out << c; + } + if (m_needs_model) + out << " ; + current model"; return out; } + void conflict_core::set(std::nullptr_t) { + SASSERT(empty()); + m_constraints.push_back({}); + m_needs_model = false; + } + + void conflict_core::set(constraint_literal c) { + LOG("Conflict: " << c); + SASSERT(empty()); + m_constraints.push_back(std::move(c)); + m_needs_model = true; + } + + void conflict_core::set(pvar v, vector const& cjust_v) { + LOG("Conflict for v" << v << ": " << cjust_v); + SASSERT(empty()); + NOT_IMPLEMENTED_YET(); + m_constraints.append(cjust_v); + if (cjust_v.empty()) + m_constraints.push_back({}); + m_needs_model = true; + } + } diff --git a/src/math/polysat/conflict_core.h b/src/math/polysat/conflict_core.h index c44723e78..4b081297b 100644 --- a/src/math/polysat/conflict_core.h +++ b/src/math/polysat/conflict_core.h @@ -16,47 +16,38 @@ Author: namespace polysat { - /// Represents a conflict as core (~negation of clause). - /// - /// TODO: can probably move some clause_builder functionality into this class. + /** Conflict state, represented as core (~negation of clause). */ class conflict_core { - // constraint_ref_vector m_constraints; + // TODO: core needs to own the constraint literals... vector m_constraints; - bool m_needs_model = true; ///< True iff the conflict depends on the current variable assignment. (If so, additional constraints must be added to the final learned clause.) + + /** True iff the conflict depends on the current variable assignment. (If so, additional constraints must be added to the final learned clause.) */ + bool m_needs_model = false; + // NOTE: for now we keep this simple implementation. + // The drawback is that we may get weaker lemmas in some cases (but they are still correct). + // For example: if we have 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core. public: - vector const& constraints() const { - return m_constraints; - } + + vector const& constraints() const { return m_constraints; } + bool needs_model() const { return m_needs_model; } bool empty() const { - return m_constraints.empty(); + return m_constraints.empty() && !m_needs_model; } void reset() { m_constraints.reset(); - m_needs_model = true; - } - - // for bailing out with a conflict at the base level - void set(std::nullptr_t) { - SASSERT(empty()); - m_constraints.push_back({}); m_needs_model = false; + SASSERT(empty()); } - // void set( - - // TODO: set core from conflicting units - // TODO: set clause - - // TODO: use iterator instead (this method is needed for marking so duplicates don't necessarily have to be skipped) - unsigned_vector vars(constraint_manager const& cm) const { - unsigned_vector vars; - for (auto const& c : m_constraints) - vars.append(c->vars()); - return vars; - } + /** for bailing out with a conflict at the base level */ + void set(std::nullptr_t); + /** conflict because the constraint c is false under current variable assignment */ + void set(constraint_literal c); + /** conflict because there is no viable value for the variable v */ + void set(pvar v, vector const& cjust_v); std::ostream& display(std::ostream& out) const; }; diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index ebb86ff4c..0a6b668bd 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -93,6 +93,10 @@ namespace polysat { return get_bv2c(var); } + constraint_literal constraint_manager::lookup(sat::literal lit) const { + return {lit, lookup(lit.var())}; + } + eq_constraint& constraint::to_eq() { return *dynamic_cast(this); } @@ -109,16 +113,16 @@ namespace polysat { return *dynamic_cast(this); } - constraint_literal constraint_manager::eq(unsigned lvl, pdd const& p) { - return constraint_literal{alloc(eq_constraint, *this, lvl, p)}; + constraint_literal_ref constraint_manager::eq(unsigned lvl, pdd const& p) { + return constraint_literal_ref{alloc(eq_constraint, *this, lvl, p)}; } - constraint_literal constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) { - return constraint_literal{alloc(ule_constraint, *this, lvl, a, b)}; + constraint_literal_ref constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) { + return constraint_literal_ref{alloc(ule_constraint, *this, lvl, a, b)}; } - constraint_literal constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) { + constraint_literal_ref constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) { // a < b <=> !(b <= a) return ~ule(lvl, b, a); } @@ -139,25 +143,26 @@ namespace polysat { // // Argument: flipping the msb swaps the negative and non-negative blocks // - constraint_literal constraint_manager::sle(unsigned lvl, pdd const& a, pdd const& b) { + constraint_literal_ref 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, a + shift, b + shift); } - constraint_literal constraint_manager::slt(unsigned lvl, pdd const& a, pdd const& b) { + constraint_literal_ref 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, a + shift, b + shift); } - std::ostream& constraint::display_extra(std::ostream& out) const { + std::ostream& constraint::display_extra(std::ostream& out, lbool status) const { out << " @" << level() << " (b" << bvar() << ")"; - if (is_positive()) out << " [pos]"; - if (is_negative()) out << " [neg]"; - if (is_undef()) out << " [inactive]"; + (void)status; + // if (is_positive()) out << " [pos]"; + // if (is_negative()) out << " [neg]"; + // if (is_undef()) out << " [inactive]"; // TODO: not sure if we still need/want this... decide later return out; } - bool constraint::propagate(solver& s, pvar v) { + bool constraint::propagate(solver& s, bool is_positive, pvar v) { LOG_H3("Propagate " << s.m_vars[v] << " in " << *this); SASSERT(!vars().empty()); unsigned idx = 0; @@ -168,24 +173,35 @@ namespace polysat { for (unsigned i = vars().size(); i-- > 2; ) { unsigned other_v = vars()[i]; if (!s.is_assigned(other_v)) { - s.add_watch(*this, other_v); + s.add_watch({this, is_positive}, other_v); std::swap(vars()[idx], vars()[i]); return true; } } // at most one variable remains unassigned. unsigned other_v = vars()[idx]; - propagate_core(s, v, other_v); + propagate_core(s, is_positive, v, other_v); return false; } - void constraint::propagate_core(solver& s, pvar v, pvar other_v) { + void constraint::propagate_core(solver& s, bool is_positive, pvar v, pvar other_v) { (void)v; (void)other_v; - narrow(s); + narrow(s, is_positive); } - clause_ref clause::from_unit(constraint_literal c, p_dependency_ref d) { + std::ostream &constraint_literal::display(std::ostream &out) const { + if (*this) + return out << m_literal << "{ " << *m_constraint << " }"; + else + return out << ""; + } + + std::ostream &constraint_literal_ref::display(std::ostream &out) const { + return out << get(); + } + + clause_ref clause::from_unit(constraint_literal_ref c, p_dependency_ref d) { SASSERT(c); unsigned const lvl = c->level(); sat::literal_vector lits; @@ -201,17 +217,15 @@ namespace polysat { bool clause::is_always_false(solver& s) const { return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) { - constraint *c = s.m_constraints.lookup(lit.var()); - tmp_assign _t(c, lit); - return c->is_always_false(); + constraint_literal c = s.m_constraints.lookup(lit); + return c.is_always_false(); }); } bool clause::is_currently_false(solver& s) const { return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) { - constraint *c = s.m_constraints.lookup(lit.var()); - tmp_assign _t(c, lit); - return c->is_currently_false(s); + constraint_literal c = s.m_constraints.lookup(lit); + return c.is_currently_false(s); }); } @@ -251,22 +265,4 @@ namespace polysat { return out; } - std::ostream& constraints_and_clauses::display(std::ostream& out) const { - bool first = true; - for (auto c : units()) { - if (first) - first = false; - else - out << " ; "; - out << show_deref(c); - } - for (auto cl : clauses()) { - if (first) - first = false; - else - out << " ; "; - out << show_deref(cl); - } - return out; - } } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index bbdf5e595..34c58701f 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -26,6 +26,7 @@ namespace polysat { enum csign_t : bool { neg_t = false, pos_t = true }; class constraint_literal; + class constraint_literal_ref; class constraint; class constraint_manager; class clause; @@ -34,6 +35,7 @@ namespace polysat { class ule_constraint; using constraint_ref = ref; using constraint_ref_vector = sref_vector; + using constraint_literal_ref_vector = vector; using clause_ref = ref; using clause_ref_vector = sref_vector; @@ -49,7 +51,7 @@ namespace polysat { void erase_bv2c(sat::bool_var bv) { m_bv2constraint[bv] = nullptr; } constraint* get_bv2c(sat::bool_var bv) const { return m_bv2constraint.get(bv, nullptr); } - // Constraint storage per level; should be destructed before m_bv2constraint + // Constraint storage per level; should be destructed before m_bv2constraint because constraint's destructor calls erase_bv2c vector> m_constraints; vector> m_clauses; @@ -74,13 +76,14 @@ namespace polysat { void release_level(unsigned lvl); constraint* lookup(sat::bool_var var) const; + constraint_literal lookup(sat::literal lit) const; constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); } - 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); + constraint_literal_ref eq(unsigned lvl, pdd const& p); + constraint_literal_ref ule(unsigned lvl, pdd const& a, pdd const& b); + constraint_literal_ref ult(unsigned lvl, pdd const& a, pdd const& b); + constraint_literal_ref sle(unsigned lvl, pdd const& a, pdd const& b); + constraint_literal_ref slt(unsigned lvl, pdd const& a, pdd const& b); // p_dependency_ref null_dep() const { return {nullptr, m_dm}; } }; @@ -109,12 +112,10 @@ 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_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, ckind_t k): m_manager(&m), m_storage_level(lvl), m_kind(k), m_bvar(m_manager->m_bvars.new_var()) { @@ -123,7 +124,7 @@ namespace polysat { } protected: - std::ostream& display_extra(std::ostream& out) const; + std::ostream& display_extra(std::ostream& out, lbool status) const; public: void inc_ref() { m_ref_count++; } @@ -140,14 +141,16 @@ namespace polysat { bool is_eq() const { return m_kind == ckind_t::eq_t; } bool is_ule() const { return m_kind == ckind_t::ule_t; } ckind_t kind() const { return m_kind; } - virtual std::ostream& display(std::ostream& out) const = 0; - bool propagate(solver& s, pvar v); - virtual void propagate_core(solver& s, pvar v, pvar other_v); - virtual bool is_always_false() = 0; - virtual bool is_currently_false(solver& s) = 0; - virtual bool is_currently_true(solver& s) = 0; - virtual void narrow(solver& s) = 0; - virtual inequality as_inequality() const = 0; + virtual std::ostream& display(std::ostream& out, lbool status = l_undef) const = 0; + + bool propagate(solver& s, bool is_positive, pvar v); + virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v); + virtual bool is_always_false(bool is_positive) = 0; + virtual bool is_currently_false(solver& s, bool is_positive) = 0; + virtual bool is_currently_true(solver& s, bool is_positive) = 0; + virtual void narrow(solver& s, bool is_positive) = 0; + virtual inequality as_inequality(bool is_positive) const = 0; + eq_constraint& to_eq(); eq_constraint const& to_eq() const; ule_constraint& to_ule(); @@ -155,27 +158,8 @@ namespace polysat { unsigned_vector& vars() { return m_vars; } unsigned_vector const& vars() const { return m_vars; } unsigned level() const { return m_storage_level; } - // unsigned active_level() const { - // SASSERT(!is_undef()); - // return m_manager->m_bvars.level(bvar()); - // } - // unsigned active_at_base_level(solver& s) const { - // return !is_undef() && active_level() <= s.base_level(); - // } sat::bool_var bvar() const { return m_bvar; } - 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_status == l_undef || m_status == to_lbool(is_true)); - // 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; } - 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; } - clause* unit_clause() const { return m_unit_clause; } void set_unit_clause(clause* cl) { SASSERT(cl); SASSERT(!m_unit_clause || m_unit_clause == cl); m_unit_clause = cl; } p_dependency* unit_dep() const; @@ -186,43 +170,111 @@ 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_literal& out_neg_cond) { return false; } + // TODO: we can probably remove this and unify the implementations for both cases by relying on as_inequality(). + virtual bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, constraint_literal_ref& out_neg_cond) { return false; } }; inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); } - /// Literal together with the constraint it represents. - /// (or: constraint with polarity) + /// Literal together with the constraint it represents (i.e., constraint with polarity). + /// Non-owning version. class constraint_literal { + sat::literal m_literal = sat::null_literal; + constraint* m_constraint = nullptr; + + public: + constraint_literal() {} + constraint_literal(sat::literal lit, constraint* c): + m_literal(lit), m_constraint(c) { + SASSERT(get_constraint()); + SASSERT(literal().var() == get_constraint()->bvar()); + } + constraint_literal(constraint* c, bool is_positive): constraint_literal(sat::literal(c->bvar(), !is_positive), c) {} + + constraint_literal operator~() const { + return {~m_literal, m_constraint}; + } + + void negate() { + m_literal = ~m_literal; + } + + bool is_positive() const { return !m_literal.sign(); } + bool is_negative() const { return m_literal.sign(); } + + bool propagate(solver& s, pvar v) { return get_constraint()->propagate(s, !literal().sign(), v); } + void propagate_core(solver& s, pvar v, pvar other_v) { get_constraint()->propagate_core(s, !literal().sign(), v, other_v); } + bool is_always_false() { return get_constraint()->is_always_false(!literal().sign()); } + bool is_currently_false(solver& s) { return get_constraint()->is_currently_false(s, !literal().sign()); } + bool is_currently_true(solver& s) { return get_constraint()->is_currently_true(s, !literal().sign()); } + void narrow(solver& s) { get_constraint()->narrow(s, !literal().sign()); } + inequality as_inequality() const { return get_constraint()->as_inequality(!literal().sign()); } + + sat::literal literal() const { return m_literal; } + constraint* get_constraint() const { return m_constraint; } + + explicit operator bool() const { return !!m_constraint; } + bool operator!() const { return !m_constraint; } + constraint* operator->() const { return m_constraint; } + constraint const& operator*() const { return *m_constraint; } + + constraint_literal& operator=(std::nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; } + + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, constraint_literal const& c) { return c.display(out); } + + inline bool operator==(constraint_literal const& lhs, constraint_literal const& rhs) { + if (lhs.literal() == rhs.literal()) + SASSERT(lhs.get_constraint() == rhs.get_constraint()); + return lhs.literal() == rhs.literal(); + } + + + /// Version of constraint_literal that owns the constraint. + class constraint_literal_ref { sat::literal m_literal = sat::null_literal; constraint_ref m_constraint = nullptr; public: - constraint_literal() {} - constraint_literal(sat::literal lit, constraint_ref c): + constraint_literal_ref() {} + constraint_literal_ref(sat::literal lit, constraint_ref c): m_literal(lit), m_constraint(std::move(c)) { - SASSERT(get()); - SASSERT(literal().var() == get()->bvar()); + SASSERT(get_constraint()); + SASSERT(literal().var() == get_constraint()->bvar()); } - constraint_literal operator~() const&& { + constraint_literal_ref(constraint_literal cl): constraint_literal_ref(cl.literal(), cl.get_constraint()) {} + + constraint_literal_ref operator~() const&& { return {~m_literal, std::move(m_constraint)}; } + + void negate() { + m_literal = ~m_literal; + } + sat::literal literal() const { return m_literal; } - constraint* get() const { return m_constraint.get(); } + constraint* get_constraint() const { return m_constraint.get(); } + constraint_literal get() const { return {literal(), get_constraint()}; } 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; } - constraint* operator->() const { return m_constraint.get(); } + constraint* operator->() const { return m_constraint.operator->(); } constraint const& operator*() const { return *m_constraint; } - constraint_literal& operator=(std::nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; } + constraint_literal_ref& operator=(std::nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; } + + std::ostream& display(std::ostream& out) const; private: friend class constraint_manager; - explicit constraint_literal(constraint* c): constraint_literal(sat::literal(c->bvar()), c) {} + explicit constraint_literal_ref(constraint* c): constraint_literal_ref(sat::literal(c->bvar()), c) {} }; + inline std::ostream& operator<<(std::ostream& out, constraint_literal_ref const& c) { return c.display(out); } + /// Disjunction of constraints represented by boolean literals class clause { @@ -254,7 +306,7 @@ 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_literal c, p_dependency_ref d); + static clause_ref from_unit(constraint_literal_ref 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'. @@ -286,98 +338,5 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); } - - // Container for unit constraints and clauses. - class constraints_and_clauses { - constraint_ref_vector m_units; - clause_ref_vector m_clauses; - - public: - constraint_ref_vector const& units() const { return m_units; } - constraint_ref_vector& units() { return m_units; } - - clause_ref_vector const& clauses() const { return m_clauses; } - clause_ref_vector& clauses() { return m_clauses; } - - bool is_unit() const { return units().size() == 1 && clauses().empty(); } - constraint* get_unit() const { SASSERT(is_unit()); return units()[0]; } - - bool is_clause() const { return units().empty() && clauses().size() == 1; } - clause* get_clause() const { SASSERT(is_clause()); return clauses()[0]; } - - unsigned size() const { - return m_units.size() + m_clauses.size(); - } - - bool empty() const { - return m_units.empty() && m_clauses.empty(); - } - - void reset() { - m_units.reset(); - m_clauses.reset(); - } - - void append(ptr_vector const& cs) { - for (constraint* c : cs) - m_units.push_back(c); - } - - void push_back(std::nullptr_t) { m_units.push_back(nullptr); } - void push_back(constraint_ref c) { m_units.push_back(std::move(c)); } - void push_back(clause_ref cl) { m_clauses.push_back(std::move(cl)); } - - // TODO: use iterator instead - unsigned_vector vars(constraint_manager const& cm) const { - unsigned_vector vars; - for (auto const& c : m_units) - vars.append(c->vars()); - for (auto const& cl : m_clauses) - for (auto lit : *cl) { - constraint* c = cm.lookup(lit.var()); - if (c) - vars.append(c->vars()); - } - return vars; - } - - std::ostream& display(std::ostream& out) const; - }; - - inline std::ostream& operator<<(std::ostream& out, constraints_and_clauses const& c) { return c.display(out); } - - - /// Temporarily assign a constraint according to the sign of the given literal. - class tmp_assign final { - constraint* m_constraint; - bool m_should_unassign = false; - public: - /// c must live longer than tmp_assign. - tmp_assign(constraint* c, sat::literal lit): - m_constraint(c) { - SASSERT(c); - SASSERT_EQ(c->bvar(), lit.var()); - if (c->is_undef()) { - c->assign(!lit.sign()); - m_should_unassign = true; - } - else - SASSERT_EQ(c->blit(), lit); - } - void revert() { - if (m_should_unassign) { - m_constraint->unassign(); - m_should_unassign = false; - } - } - ~tmp_assign() { - revert(); - } - tmp_assign(tmp_assign&) = delete; - tmp_assign(tmp_assign&&) = delete; - tmp_assign& operator=(tmp_assign&) = delete; - 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 d7cf64bd5..27f5ff1d0 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/src/math/polysat/eq_constraint.cpp @@ -18,82 +18,73 @@ Author: namespace polysat { - std::ostream& eq_constraint::display(std::ostream& out) const { - out << p() << " == 0"; - return display_extra(out); + std::ostream& eq_constraint::display(std::ostream& out, lbool status) const { + out << p(); + if (status == l_true) out << " == 0"; + else if (status == l_false) out << " != 0"; + else out << " ==/!= 0"; + return display_extra(out, status); } - void eq_constraint::narrow(solver& s) { - SASSERT(!is_undef()); + void eq_constraint::narrow(solver& s, bool is_positive) { LOG("Assignment: " << assignments_pp(s)); auto q = p().subst_val(s.assignment()); LOG("Substituted: " << p() << " := " << q); if (q.is_zero()) { - if (is_positive()) - return; - if (is_negative()) { + if (!is_positive) { LOG("Conflict (zero under current assignment)"); - s.set_conflict(*this); - return; + s.set_conflict({this, is_positive}); } + return; } if (q.is_never_zero()) { - if (is_positive()) { + if (is_positive) { LOG("Conflict (never zero under current assignment)"); - s.set_conflict(*this); - return; + s.set_conflict({this, is_positive}); } - if (is_negative()) - return; + return; } if (q.is_unilinear()) { // a*x + b == 0 pvar v = q.var(); - s.push_cjust(v, this); + s.push_cjust(v, {this, is_positive}); rational a = q.hi().val(); rational b = q.lo().val(); - s.m_viable.intersect_eq(a, v, b, is_positive()); + s.m_viable.intersect_eq(a, v, b, is_positive); rational val; if (s.m_viable.find_viable(v, val) == dd::find_t::singleton) - s.propagate(v, val, *this); + s.propagate(v, val, {this, is_positive}); return; } - // TODO: what other constraints can be extracted cheaply? } - bool eq_constraint::is_always_false() { - if (is_positive()) + bool eq_constraint::is_always_false(bool is_positive) { + if (is_positive) return p().is_never_zero(); - if (is_negative()) + else return p().is_zero(); - UNREACHABLE(); - return false; } - bool eq_constraint::is_currently_false(solver& s) { + bool eq_constraint::is_currently_false(solver& s, bool is_positive) { pdd r = p().subst_val(s.assignment()); - if (is_positive()) + if (is_positive) return r.is_never_zero(); - if (is_negative()) + else return r.is_zero(); - UNREACHABLE(); - return false; } - bool eq_constraint::is_currently_true(solver& s) { + bool eq_constraint::is_currently_true(solver& s, bool is_positive) { pdd r = p().subst_val(s.assignment()); - if (is_positive()) + if (is_positive) return r.is_zero(); - if (is_negative()) + else return r.is_never_zero(); - UNREACHABLE(); - return false; } @@ -130,10 +121,8 @@ namespace polysat { /// 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_literal& out_neg_cond) + bool eq_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, constraint_literal_ref& out_neg_cond) { - SASSERT(!is_undef()); - // Current only works when degree(v) is at most one unsigned const deg = p().degree(v); if (deg > 1) @@ -182,7 +171,7 @@ namespace polysat { rational lo_val = (1 - e1s).val(); pdd hi = -e1; rational hi_val = (-e1s).val(); - if (is_negative()) { + if (!is_positive) { swap(lo, hi); lo_val.swap(hi_val); } @@ -191,10 +180,9 @@ namespace polysat { return true; } - inequality eq_constraint::as_inequality() const { - SASSERT(!is_undef()); + inequality eq_constraint::as_inequality(bool is_positive) const { pdd zero = p() - p(); - if (is_positive()) + if (is_positive) // p <= 0 return inequality(p(), zero, false, this); else diff --git a/src/math/polysat/eq_constraint.h b/src/math/polysat/eq_constraint.h index 4974c730e..bd6597ab7 100644 --- a/src/math/polysat/eq_constraint.h +++ b/src/math/polysat/eq_constraint.h @@ -26,13 +26,13 @@ namespace polysat { } ~eq_constraint() override {} pdd const & p() const { return m_poly; } - std::ostream& display(std::ostream& out) const 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_literal& out_neg_cond) override; - inequality as_inequality() const override; + std::ostream& display(std::ostream& out, lbool status) const override; + bool is_always_false(bool is_positive) override; + bool is_currently_false(solver& s, bool is_positive) override; + bool is_currently_true(solver& s, bool is_positive) override; + void narrow(solver& s, bool is_positive) override; + bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, constraint_literal_ref& out_neg_cond) override; + inequality as_inequality(bool is_positive) const override; unsigned hash() const override; bool operator==(constraint const& other) const override; }; diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 681bb7461..f358211d3 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -13,551 +13,552 @@ Author: --*/ #include "math/polysat/explain.h" #include "math/polysat/log.h" +#include "math/polysat/solver.h" namespace polysat { - conflict_explainer::conflict_explainer(solver& s, constraints_and_clauses const& conflict): - m_solver(s), m_conflict(conflict) {} + conflict_explainer::conflict_explainer(solver& s): m_solver(s) {} - clause_ref conflict_explainer::resolve(pvar v, ptr_vector const& cjust) { - LOG_H3("Attempting to explain conflict for v" << v); - m_var = v; - m_cjust_v = cjust; +// clause_ref conflict_explainer::resolve(pvar v, ptr_vector const& cjust) { +// LOG_H3("Attempting to explain conflict for v" << v); +// m_var = v; +// m_cjust_v = cjust; - for (auto* c : cjust) - m_conflict.push_back(c); +// for (auto* c : cjust) +// m_conflict.push_back(c); - for (auto* c : m_conflict.units()) - LOG("Constraint: " << show_deref(c)); - for (auto* c : m_conflict.clauses()) - LOG("Clause: " << show_deref(c)); +// for (auto* c : m_conflict.units()) +// LOG("Constraint: " << show_deref(c)); +// 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: 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); - // Collect unit constraints - // - // TODO: the distinction between units and unit clauses is a bit awkward; maybe it should be removed. - // We could then also remove the hybrid container 'constraints_and_clauses' by a clause_ref_vector - SASSERT(m_conflict_units.empty()); - for (constraint* c : m_conflict.units()) - // if (c->is_eq()) - m_conflict_units.push_back(c); - for (auto clause : m_conflict.clauses()) { - if (clause->size() == 1) { - sat::literal lit = (*clause)[0]; - constraint* c = m_solver.m_constraints.lookup(lit.var()); - LOG("unit clause: " << show_deref(c)); - // Morally, a derived unit clause is always asserted at the base level. - // (Even if we don't want to keep this one around. But maybe we should? Do we want to reconstruct proofs?) - c->set_unit_clause(clause); - c->assign(!lit.sign()); - // this clause is really a unit. - // if (c->is_eq()) { - m_conflict_units.push_back(c); - // } - } - } +// // Collect unit constraints +// // +// // TODO: the distinction between units and unit clauses is a bit awkward; maybe it should be removed. +// // We could then also remove the hybrid container 'constraints_and_clauses' by a clause_ref_vector +// SASSERT(m_conflict_units.empty()); +// for (constraint* c : m_conflict.units()) +// // if (c->is_eq()) +// m_conflict_units.push_back(c); +// for (auto clause : m_conflict.clauses()) { +// if (clause->size() == 1) { +// sat::literal lit = (*clause)[0]; +// constraint* c = m_solver.m_constraints.lookup(lit.var()); +// LOG("unit clause: " << show_deref(c)); +// // Morally, a derived unit clause is always asserted at the base level. +// // (Even if we don't want to keep this one around. But maybe we should? Do we want to reconstruct proofs?) +// c->set_unit_clause(clause); +// c->assign(!lit.sign()); +// // this clause is really a unit. +// // if (c->is_eq()) { +// m_conflict_units.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(); - if (!lemma) lemma = by_ugt_x(); - if (!lemma) lemma = by_ugt_y(); - if (!lemma) lemma = by_ugt_z(); - if (!lemma) lemma = y_ule_ax_and_x_ule_z(); +// // TODO: we should share work done for examining constraints between different resolution methods +// clause_ref lemma; +// if (!lemma) lemma = by_polynomial_superposition(); +// if (!lemma) lemma = by_ugt_x(); +// if (!lemma) lemma = by_ugt_y(); +// if (!lemma) lemma = by_ugt_z(); +// if (!lemma) lemma = y_ule_ax_and_x_ule_z(); - 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) == l_false) - continue; - SASSERT(m_solver.m_bvars.value(lit) != 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"); - } - }); +// 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) == l_false) +// continue; +// SASSERT(m_solver.m_bvars.value(lit) != 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"); +// } +// }); - m_var = null_var; - m_cjust_v.reset(); - return lemma; - } +// m_var = null_var; +// m_cjust_v.reset(); +// return lemma; +// } - /** - * Polynomial superposition. - * So far between two equalities. - * TODO: Also handle =, != superposition here? - * TODO: handle case when m_conflict.units().size() > 2 - * TODO: handle super-position into a clause? - */ - clause_ref conflict_explainer::by_polynomial_superposition() { - LOG_H3("units-size: " << m_conflict.units().size() << " conflict-clauses " << m_conflict.clauses().size()); +// /** +// * Polynomial superposition. +// * So far between two equalities. +// * TODO: Also handle =, != superposition here? +// * TODO: handle case when m_conflict.units().size() > 2 +// * TODO: handle super-position into a clause? +// */ +// clause_ref conflict_explainer::by_polynomial_superposition() { +// LOG_H3("units-size: " << m_conflict.units().size() << " conflict-clauses " << m_conflict.clauses().size()); -#if 0 - constraint* c1 = nullptr, *c2 = nullptr; +// #if 0 +// constraint* c1 = nullptr, *c2 = nullptr; - if (m_conflict.units().size() == 2 && m_conflict.clauses().size() == 0) { - c1 = m_conflict.units()[0]; - c2 = m_conflict.units()[1]; - } - else { - // other combinations? +// if (m_conflict.units().size() == 2 && m_conflict.clauses().size() == 0) { +// c1 = m_conflict.units()[0]; +// c2 = m_conflict.units()[1]; +// } +// else { +// // other combinations? -#if 1 - // A clause can also be a unit. - // Even if a clause is not a unit, we could still resolve a propagation - // into some literal in the current conflict clause. - // Selecting resolvents should not be specific to superposition. +// #if 1 +// // A clause can also be a unit. +// // Even if a clause is not a unit, we could still resolve a propagation +// // into some literal in the current conflict clause. +// // Selecting resolvents should not be specific to superposition. - for (auto clause : m_conflict.clauses()) { - LOG("clause " << *clause << " size " << clause->size()); - if (clause->size() == 1) { - sat::literal lit = (*clause)[0]; - // if (lit.sign()) - // continue; - constraint* c = m_solver.m_constraints.lookup(lit.var()); - // Morally, a derived unit clause is always asserted at the base level. - // (Even if we don't want to keep this one around. But maybe we should? Do we want to reconstruct proofs?) - c->set_unit_clause(clause); - c->assign(!lit.sign()); - // this clause is really a unit. - LOG("unit clause: " << *c); - if (c->is_eq()) { // && c->is_positive()) { - c1 = c; - break; - } - } - } - if (!c1) - return nullptr; +// for (auto clause : m_conflict.clauses()) { +// LOG("clause " << *clause << " size " << clause->size()); +// if (clause->size() == 1) { +// sat::literal lit = (*clause)[0]; +// // if (lit.sign()) +// // continue; +// constraint* c = m_solver.m_constraints.lookup(lit.var()); +// // Morally, a derived unit clause is always asserted at the base level. +// // (Even if we don't want to keep this one around. But maybe we should? Do we want to reconstruct proofs?) +// c->set_unit_clause(clause); +// c->assign(!lit.sign()); +// // this clause is really a unit. +// LOG("unit clause: " << *c); +// if (c->is_eq()) { // && c->is_positive()) { +// c1 = c; +// break; +// } +// } +// } +// if (!c1) +// return nullptr; - for (constraint* c : m_conflict.units()) { - if (c->is_eq() && c->is_positive()) { - c2 = c; - break; - } - } -#endif - } - if (!c1 || !c2 || c1 == c2) - return nullptr; - LOG("c1: " << show_deref(c1)); - LOG("c2: " << show_deref(c2)); - if (c1->is_eq() && c2->is_eq() && c1->is_positive() && c2->is_positive()) { - pdd a = c1->to_eq().p(); - pdd b = c2->to_eq().p(); - pdd r = a; - if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r)) - return nullptr; - 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(); - } - if (c1->is_eq() && c2->is_eq() && c1->is_negative() && c2->is_positive()) { - pdd a = c1->to_eq().p(); - pdd b = c2->to_eq().p(); - pdd r = a; - // TODO: only holds if the factor for 'a' is non-zero - if (!a.resolve(m_var, b, r)) - return nullptr; - 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)); - SASSERT(false); // TODO "breakpoint" for debugging - return clause.build(); - } +// for (constraint* c : m_conflict.units()) { +// if (c->is_eq() && c->is_positive()) { +// c2 = c; +// break; +// } +// } +// #endif +// } +// if (!c1 || !c2 || c1 == c2) +// return nullptr; +// LOG("c1: " << show_deref(c1)); +// LOG("c2: " << show_deref(c2)); +// if (c1->is_eq() && c2->is_eq() && c1->is_positive() && c2->is_positive()) { +// pdd a = c1->to_eq().p(); +// pdd b = c2->to_eq().p(); +// pdd r = a; +// if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r)) +// return nullptr; +// 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(); +// } +// if (c1->is_eq() && c2->is_eq() && c1->is_negative() && c2->is_positive()) { +// pdd a = c1->to_eq().p(); +// pdd b = c2->to_eq().p(); +// pdd r = a; +// // TODO: only holds if the factor for 'a' is non-zero +// if (!a.resolve(m_var, b, r)) +// return nullptr; +// 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)); +// SASSERT(false); // TODO "breakpoint" for debugging +// return clause.build(); +// } -#else - for (constraint* c1 : m_conflict_units) { - if (!c1->is_eq()) - continue; - for (constraint* c2 : m_conflict_units) { // TODO: can start iteration at index(c1)+1 - if (c1 == c2) - continue; - if (!c2->is_eq()) - continue; - if (c1->is_negative() && c2->is_negative()) - continue; - LOG("c1: " << show_deref(c1)); - LOG("c2: " << show_deref(c2)); - if (c1->is_positive() && c2->is_negative()) { - std::swap(c1, c2); - } - pdd a = c1->to_eq().p(); - pdd b = c2->to_eq().p(); - pdd r = a; - unsigned const lvl = std::max(c1->level(), c2->level()); - if (c1->is_positive() && c2->is_positive()) { - if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r)) - continue; - 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)); - auto cl = clause.build(); - LOG("r: " << show_deref(cl->new_constraints()[0])); - LOG("result: " << show_deref(cl)); - // SASSERT(false); // NOTE: this is a simple "breakpoint" for debugging - return cl; - } - if (c1->is_negative() && c2->is_positive()) { - // TODO: only holds if the factor for 'a' is non-zero - if (!a.resolve(m_var, b, r)) - continue; - 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)); - auto cl = clause.build(); - LOG("r: " << show_deref(cl->new_constraints()[0])); - LOG("result: " << show_deref(cl)); - // SASSERT(false); // NOTE: this is a simple "breakpoint" for debugging - return cl; - } - } - } -#endif - return nullptr; - } +// #else +// for (constraint* c1 : m_conflict_units) { +// if (!c1->is_eq()) +// continue; +// for (constraint* c2 : m_conflict_units) { // TODO: can start iteration at index(c1)+1 +// if (c1 == c2) +// continue; +// if (!c2->is_eq()) +// continue; +// if (c1->is_negative() && c2->is_negative()) +// continue; +// LOG("c1: " << show_deref(c1)); +// LOG("c2: " << show_deref(c2)); +// if (c1->is_positive() && c2->is_negative()) { +// std::swap(c1, c2); +// } +// pdd a = c1->to_eq().p(); +// pdd b = c2->to_eq().p(); +// pdd r = a; +// unsigned const lvl = std::max(c1->level(), c2->level()); +// if (c1->is_positive() && c2->is_positive()) { +// if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r)) +// continue; +// 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)); +// auto cl = clause.build(); +// LOG("r: " << show_deref(cl->new_constraints()[0])); +// LOG("result: " << show_deref(cl)); +// // SASSERT(false); // NOTE: this is a simple "breakpoint" for debugging +// return cl; +// } +// if (c1->is_negative() && c2->is_positive()) { +// // TODO: only holds if the factor for 'a' is non-zero +// if (!a.resolve(m_var, b, r)) +// continue; +// 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)); +// auto cl = clause.build(); +// LOG("r: " << show_deref(cl->new_constraints()[0])); +// LOG("result: " << show_deref(cl)); +// // SASSERT(false); // NOTE: this is a simple "breakpoint" for debugging +// return cl; +// } +// } +// } +// #endif +// return nullptr; +// } - /// [x] zx > yx ==> Ω*(x,y) \/ z > y - /// [x] yx <= zx ==> Ω*(x,y) \/ y <= z - clause_ref conflict_explainer::by_ugt_x() { - LOG_H3("Try zx > yx where x := v" << m_var); +// /// [x] zx > yx ==> Ω*(x,y) \/ z > y +// /// [x] yx <= zx ==> Ω*(x,y) \/ y <= z +// clause_ref conflict_explainer::by_ugt_x() { +// LOG_H3("Try zx > yx where x := v" << m_var); - pdd const x = m_solver.var(m_var); - unsigned const sz = m_solver.size(m_var); - pdd const zero = m_solver.sz2pdd(sz).zero(); +// pdd const x = m_solver.var(m_var); +// unsigned const sz = m_solver.size(m_var); +// pdd const zero = m_solver.sz2pdd(sz).zero(); - // Find constraint of shape: yx <= zx - for (auto* c1 : m_conflict.units()) { - auto c = c1->as_inequality(); - if (c.lhs.degree(m_var) != 1) - continue; - if (c.rhs.degree(m_var) != 1) - continue; - pdd y = zero; - pdd rest = zero; - c.lhs.factor(m_var, 1, y, rest); - if (!rest.is_zero()) - continue; - pdd z = zero; - c.rhs.factor(m_var, 1, z, rest); - if (!rest.is_zero()) - continue; +// // Find constraint of shape: yx <= zx +// for (auto* c1 : m_conflict.units()) { +// auto c = c1->as_inequality(); +// if (c.lhs.degree(m_var) != 1) +// continue; +// if (c.rhs.degree(m_var) != 1) +// continue; +// pdd y = zero; +// pdd rest = zero; +// c.lhs.factor(m_var, 1, y, rest); +// if (!rest.is_zero()) +// continue; +// pdd z = zero; +// c.rhs.factor(m_var, 1, z, rest); +// if (!rest.is_zero()) +// continue; - unsigned const lvl = c.src->level(); +// 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_literal y_le_z; - if (c.is_strict) - y_le_z = m_solver.m_constraints.ult(lvl, y, z); - else - 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)); +// 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_literal y_le_z; +// if (c.is_strict) +// y_le_z = m_solver.m_constraints.ult(lvl, y, z); +// else +// 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)); - return clause.build(); - } - return nullptr; - } +// return clause.build(); +// } +// return nullptr; +// } - /// [y] z' <= y /\ zx > yx ==> Ω*(x,y) \/ zx > z'x - /// [y] z' <= y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx - clause_ref conflict_explainer::by_ugt_y() { - LOG_H3("Try z' <= y && zx > yx where y := v" << m_var); +// /// [y] z' <= y /\ zx > yx ==> Ω*(x,y) \/ zx > z'x +// /// [y] z' <= y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx +// clause_ref conflict_explainer::by_ugt_y() { +// LOG_H3("Try z' <= y && zx > yx where y := v" << m_var); - pdd const y = m_solver.var(m_var); - unsigned const sz = m_solver.size(m_var); - pdd const zero = m_solver.sz2pdd(sz).zero(); +// pdd const y = m_solver.var(m_var); +// unsigned const sz = m_solver.size(m_var); +// pdd const zero = m_solver.sz2pdd(sz).zero(); - // Collect constraints of shape "_ <= y" - vector ds; - for (auto* d1 : m_conflict.units()) { - auto d = d1->as_inequality(); - // TODO: a*y where 'a' divides 'x' should also be easy to handle (assuming for now they're numbers) - // TODO: also z' < y should follow the same pattern. - if (d.rhs != y) - continue; - LOG("z' <= y candidate: " << show_deref(d.src)); - ds.push_back(std::move(d)); - } - if (ds.empty()) - return nullptr; +// // Collect constraints of shape "_ <= y" +// vector ds; +// for (auto* d1 : m_conflict.units()) { +// auto d = d1->as_inequality(); +// // TODO: a*y where 'a' divides 'x' should also be easy to handle (assuming for now they're numbers) +// // TODO: also z' < y should follow the same pattern. +// if (d.rhs != y) +// continue; +// LOG("z' <= y candidate: " << show_deref(d.src)); +// ds.push_back(std::move(d)); +// } +// if (ds.empty()) +// return nullptr; - // Find constraint of shape: yx <= zx - for (auto* c1 : m_conflict.units()) { - auto c = c1->as_inequality(); - if (c.lhs.degree(m_var) != 1) - continue; - pdd x = zero; - pdd rest = zero; - c.lhs.factor(m_var, 1, x, rest); - if (!rest.is_zero()) - continue; - // TODO: in principle, 'x' could be any polynomial. However, we need to divide the lhs by x, and we don't have general polynomial division yet. - // so for now we just allow the form 'value*variable'. - // (extension to arbitrary monomials for 'x' should be fairly easy too) - if (!x.is_unary()) - continue; - unsigned x_var = x.var(); - rational x_coeff = x.hi().val(); - pdd xz = zero; - if (!c.rhs.try_div(x_coeff, xz)) - continue; - pdd z = zero; - xz.factor(x_var, 1, z, rest); - if (!rest.is_zero()) - continue; +// // Find constraint of shape: yx <= zx +// for (auto* c1 : m_conflict.units()) { +// auto c = c1->as_inequality(); +// if (c.lhs.degree(m_var) != 1) +// continue; +// pdd x = zero; +// pdd rest = zero; +// c.lhs.factor(m_var, 1, x, rest); +// if (!rest.is_zero()) +// continue; +// // TODO: in principle, 'x' could be any polynomial. However, we need to divide the lhs by x, and we don't have general polynomial division yet. +// // so for now we just allow the form 'value*variable'. +// // (extension to arbitrary monomials for 'x' should be fairly easy too) +// if (!x.is_unary()) +// continue; +// unsigned x_var = x.var(); +// rational x_coeff = x.hi().val(); +// pdd xz = zero; +// if (!c.rhs.try_div(x_coeff, xz)) +// continue; +// pdd z = zero; +// xz.factor(x_var, 1, z, rest); +// if (!rest.is_zero()) +// continue; - LOG("zx > yx: " << show_deref(c.src)); +// LOG("zx > yx: " << show_deref(c.src)); - // TODO: for now, we just try all ds - for (auto const& d : ds) { - unsigned const lvl = std::max(c.src->level(), d.src->level()); - pdd const& z_prime = d.lhs; +// // TODO: for now, we just try all ds +// for (auto const& d : ds) { +// unsigned const lvl = std::max(c.src->level(), d.src->level()); +// 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_literal zpx_le_zx; - if (c.is_strict || d.is_strict) - zpx_le_zx = m_solver.m_constraints.ult(lvl, z_prime*x, z*x); - else - 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)); +// 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_literal zpx_le_zx; +// if (c.is_strict || d.is_strict) +// zpx_le_zx = m_solver.m_constraints.ult(lvl, z_prime*x, z*x); +// else +// 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)); - return clause.build(); - } - } - return nullptr; - } +// return clause.build(); +// } +// } +// return nullptr; +// } - /// [z] z <= y' /\ zx > yx ==> Ω*(x,y') \/ y'x > yx - /// [z] z <= y' /\ yx <= zx ==> Ω*(x,y') \/ yx <= y'x - clause_ref conflict_explainer::by_ugt_z() { - LOG_H3("Try z <= y' && zx > yx where z := v" << m_var); +// /// [z] z <= y' /\ zx > yx ==> Ω*(x,y') \/ y'x > yx +// /// [z] z <= y' /\ yx <= zx ==> Ω*(x,y') \/ yx <= y'x +// clause_ref conflict_explainer::by_ugt_z() { +// LOG_H3("Try z <= y' && zx > yx where z := v" << m_var); - pdd const z = m_solver.var(m_var); - unsigned const sz = m_solver.size(m_var); - pdd const zero = m_solver.sz2pdd(sz).zero(); +// pdd const z = m_solver.var(m_var); +// unsigned const sz = m_solver.size(m_var); +// pdd const zero = m_solver.sz2pdd(sz).zero(); - // Collect constraints of shape "z <= _" - vector ds; - for (auto* d1 : m_conflict.units()) { - auto d = d1->as_inequality(); - // TODO: a*y where 'a' divides 'x' should also be easy to handle (assuming for now they're numbers) - // TODO: also z < y' should follow the same pattern. - if (d.lhs != z) - continue; - LOG("z <= y' candidate: " << show_deref(d.src)); - ds.push_back(std::move(d)); - } - if (ds.empty()) - return nullptr; +// // Collect constraints of shape "z <= _" +// vector ds; +// for (auto* d1 : m_conflict.units()) { +// auto d = d1->as_inequality(); +// // TODO: a*y where 'a' divides 'x' should also be easy to handle (assuming for now they're numbers) +// // TODO: also z < y' should follow the same pattern. +// if (d.lhs != z) +// continue; +// LOG("z <= y' candidate: " << show_deref(d.src)); +// ds.push_back(std::move(d)); +// } +// if (ds.empty()) +// return nullptr; - // Find constraint of shape: yx <= zx - for (auto* c1 : m_conflict.units()) { - auto c = c1->as_inequality(); - if (c.rhs.degree(m_var) != 1) - continue; - pdd x = zero; - pdd rest = zero; - c.rhs.factor(m_var, 1, x, rest); - if (!rest.is_zero()) - continue; - // TODO: in principle, 'x' could be any polynomial. However, we need to divide the lhs by x, and we don't have general polynomial division yet. - // so for now we just allow the form 'value*variable'. - // (extension to arbitrary monomials for 'x' should be fairly easy too) - if (!x.is_unary()) - continue; - unsigned x_var = x.var(); - rational x_coeff = x.hi().val(); - pdd xy = zero; - if (!c.lhs.try_div(x_coeff, xy)) - continue; - pdd y = zero; - xy.factor(x_var, 1, y, rest); - if (!rest.is_zero()) - continue; +// // Find constraint of shape: yx <= zx +// for (auto* c1 : m_conflict.units()) { +// auto c = c1->as_inequality(); +// if (c.rhs.degree(m_var) != 1) +// continue; +// pdd x = zero; +// pdd rest = zero; +// c.rhs.factor(m_var, 1, x, rest); +// if (!rest.is_zero()) +// continue; +// // TODO: in principle, 'x' could be any polynomial. However, we need to divide the lhs by x, and we don't have general polynomial division yet. +// // so for now we just allow the form 'value*variable'. +// // (extension to arbitrary monomials for 'x' should be fairly easy too) +// if (!x.is_unary()) +// continue; +// unsigned x_var = x.var(); +// rational x_coeff = x.hi().val(); +// pdd xy = zero; +// if (!c.lhs.try_div(x_coeff, xy)) +// continue; +// pdd y = zero; +// xy.factor(x_var, 1, y, rest); +// if (!rest.is_zero()) +// continue; - LOG("zx > yx: " << show_deref(c.src)); +// LOG("zx > yx: " << show_deref(c.src)); - // TODO: for now, we just try all ds - for (auto const& d : ds) { - unsigned const lvl = std::max(c.src->level(), d.src->level()); - pdd const& y_prime = d.rhs; +// // TODO: for now, we just try all ds +// for (auto const& d : ds) { +// unsigned const lvl = std::max(c.src->level(), d.src->level()); +// 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_literal yx_le_ypx; - if (c.is_strict || d.is_strict) - yx_le_ypx = m_solver.m_constraints.ult(lvl, y*x, y_prime*x); - else - 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)); +// 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_literal yx_le_ypx; +// if (c.is_strict || d.is_strict) +// yx_le_ypx = m_solver.m_constraints.ult(lvl, y*x, y_prime*x); +// else +// 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)); - return clause.build(); - } - } - return nullptr; - } +// return clause.build(); +// } +// } +// return nullptr; +// } - /// [x] y <= ax /\ x <= z (non-overflow case) - /// ==> Ω*(a, z) \/ y <= az - clause_ref conflict_explainer::y_ule_ax_and_x_ule_z() { - LOG_H3("Try y <= ax && x <= z where x := v" << m_var); +// /// [x] y <= ax /\ x <= z (non-overflow case) +// /// ==> Ω*(a, z) \/ y <= az +// clause_ref conflict_explainer::y_ule_ax_and_x_ule_z() { +// LOG_H3("Try y <= ax && x <= z where x := v" << m_var); - pdd const x = m_solver.var(m_var); - unsigned const sz = m_solver.size(m_var); - pdd const zero = m_solver.sz2pdd(sz).zero(); +// pdd const x = m_solver.var(m_var); +// unsigned const sz = m_solver.size(m_var); +// pdd const zero = m_solver.sz2pdd(sz).zero(); - // Collect constraints of shape "x <= _" - vector ds; - for (auto* d1 : m_conflict.units()) { - inequality d = d1->as_inequality(); - if (d.lhs != x) - continue; - LOG("x <= z' candidate: " << show_deref(d.src)); - ds.push_back(std::move(d)); - } - if (ds.empty()) - return nullptr; +// // Collect constraints of shape "x <= _" +// vector ds; +// for (auto* d1 : m_conflict.units()) { +// inequality d = d1->as_inequality(); +// if (d.lhs != x) +// continue; +// LOG("x <= z' candidate: " << show_deref(d.src)); +// ds.push_back(std::move(d)); +// } +// if (ds.empty()) +// return nullptr; - // Find constraint of shape: y <= ax - for (auto* c1 : m_conflict.units()) { - inequality c = c1->as_inequality(); - if (c.rhs.degree(m_var) != 1) - continue; - pdd a = zero; - pdd rest = zero; - c.rhs.factor(m_var, 1, a, rest); - if (!rest.is_zero()) - continue; - pdd const& y = c.lhs; +// // Find constraint of shape: y <= ax +// for (auto* c1 : m_conflict.units()) { +// inequality c = c1->as_inequality(); +// if (c.rhs.degree(m_var) != 1) +// continue; +// pdd a = zero; +// pdd rest = zero; +// c.rhs.factor(m_var, 1, a, rest); +// if (!rest.is_zero()) +// continue; +// pdd const& y = c.lhs; - LOG("y <= ax: " << show_deref(c1)); +// LOG("y <= ax: " << show_deref(c1)); - // TODO: for now, we just try all of the other constraints in order - for (auto const& d : ds) { - unsigned const lvl = std::max(c1->level(), d.src->level()); - pdd const& z = d.rhs; +// // TODO: for now, we just try all of the other constraints in order +// for (auto const& d : ds) { +// unsigned const lvl = std::max(c1->level(), d.src->level()); +// 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_literal y_ule_az; - if (c.is_strict || d.is_strict) - y_ule_az = m_solver.m_constraints.ult(lvl, y, a*z); - else - 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)); +// 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_literal y_ule_az; +// if (c.is_strict || d.is_strict) +// y_ule_az = m_solver.m_constraints.ult(lvl, y, a*z); +// else +// 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)); - return clause.build(); - } - } - return nullptr; - } +// return clause.build(); +// } +// } +// return nullptr; +// } - /// Add Ω*(x, y) to the clause. - /// - /// @param[in] p bit width - bool conflict_explainer::push_omega_mul(clause_builder& clause, unsigned level, unsigned p, pdd const& x, pdd const& y) { - LOG_H3("Omega^*(x, y)"); - LOG("x = " << x); - LOG("y = " << y); - auto& pddm = m_solver.sz2pdd(p); - unsigned min_k = 0; - unsigned max_k = p - 1; - unsigned k = p/2; +// /// Add Ω*(x, y) to the clause. +// /// +// /// @param[in] p bit width +// bool conflict_explainer::push_omega_mul(clause_builder& clause, unsigned level, unsigned p, pdd const& x, pdd const& y) { +// LOG_H3("Omega^*(x, y)"); +// LOG("x = " << x); +// LOG("y = " << y); +// auto& pddm = m_solver.sz2pdd(p); +// unsigned min_k = 0; +// unsigned max_k = p - 1; +// unsigned k = p/2; - rational x_val; - if (m_solver.try_eval(x, x_val)) { - unsigned x_bits = x_val.bitsize(); - LOG("eval x: " << x << " := " << x_val << " (x_bits: " << x_bits << ")"); - SASSERT(x_val < rational::power_of_two(x_bits)); - min_k = x_bits; - } +// rational x_val; +// if (m_solver.try_eval(x, x_val)) { +// unsigned x_bits = x_val.bitsize(); +// LOG("eval x: " << x << " := " << x_val << " (x_bits: " << x_bits << ")"); +// SASSERT(x_val < rational::power_of_two(x_bits)); +// min_k = x_bits; +// } - rational y_val; - if (m_solver.try_eval(y, y_val)) { - unsigned y_bits = y_val.bitsize(); - LOG("eval y: " << y << " := " << y_val << " (y_bits: " << y_bits << ")"); - SASSERT(y_val < rational::power_of_two(y_bits)); - max_k = p - y_bits; - } +// rational y_val; +// if (m_solver.try_eval(y, y_val)) { +// unsigned y_bits = y_val.bitsize(); +// LOG("eval y: " << y << " := " << y_val << " (y_bits: " << y_bits << ")"); +// SASSERT(y_val < rational::power_of_two(y_bits)); +// max_k = p - y_bits; +// } - if (min_k > max_k) { - // In this case, we cannot choose k such that both literals are false. - // This means x*y overflows in the current model and the chosen rule is not applicable. - // (or maybe we are in the case where we need the msb-encoding for overflow). - return false; - } +// if (min_k > max_k) { +// // In this case, we cannot choose k such that both literals are false. +// // This means x*y overflows in the current model and the chosen rule is not applicable. +// // (or maybe we are in the case where we need the msb-encoding for overflow). +// return false; +// } - SASSERT(min_k <= max_k); // if this assertion fails, we cannot choose k s.t. both literals are false +// SASSERT(min_k <= max_k); // if this assertion fails, we cannot choose k s.t. both literals are false - // TODO: could also choose other value for k (but between the bounds) - if (min_k == 0) - k = max_k; - else - k = min_k; +// // TODO: could also choose other value for k (but between the bounds) +// if (min_k == 0) +// k = max_k; +// else +// k = min_k; - LOG("k = " << k << "; min_k = " << min_k << "; max_k = " << max_k << "; p = " << p); - SASSERT(min_k <= k && k <= max_k); +// LOG("k = " << k << "; min_k = " << min_k << "; max_k = " << max_k << "; p = " << p); +// SASSERT(min_k <= k && k <= max_k); + +// // x >= 2^k +// auto c1 = m_solver.m_constraints.ule(level, pddm.mk_val(rational::power_of_two(k)), x); +// // y > 2^{p-k} +// 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; +// } - // x >= 2^k - auto c1 = m_solver.m_constraints.ule(level, pddm.mk_val(rational::power_of_two(k)), x); - // y > 2^{p-k} - 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 daac9fef7..48fe0faad 100644 --- a/src/math/polysat/explain.h +++ b/src/math/polysat/explain.h @@ -3,7 +3,7 @@ Copyright (c) 2021 Microsoft Corporation Module Name: - Conflict explanation / resolution + Conflict explanation Author: @@ -15,33 +15,41 @@ Author: #include "math/polysat/constraint.h" #include "math/polysat/clause_builder.h" #include "math/polysat/interval.h" -#include "math/polysat/solver.h" namespace polysat { - // TODO: later, we probably want to update this class incrementally (adding/removing constraints as we go back through the trail) - // TODO: indexing of constraints/clauses? + class solver; + class conflict_explainer { solver& m_solver; - constraints_and_clauses m_conflict; - ptr_vector m_conflict_units; + pvar m_var = null_var; ptr_vector m_cjust_v; - + // 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(); - p_dependency_ref null_dep() const { return m_solver.mk_dep_ref(null_dependency); } + 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: - conflict_explainer(solver& s, constraints_and_clauses const& conflict); + public: + /** Create empty conflict */ + conflict_explainer(solver& s); + + /** resolve conflict state against assignment to v */ clause_ref resolve(pvar v, ptr_vector const& cjust_v); + + // TODO: move conflict resolution from solver into this class. + // we have a single public method as entry point to conflict resolution. + // what do we need to return? + + /** conflict resolution */ + void resolve(); }; } diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 0aa466fc7..fb3068002 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -22,8 +22,8 @@ namespace polysat { struct fi_record { eval_interval interval; - constraint_literal neg_cond; // could be multiple constraints later - constraint* src; + constraint_literal_ref neg_cond; // could be multiple constraints later + constraint_literal src; }; /** @@ -64,24 +64,20 @@ namespace polysat { return true; } - bool forbidden_intervals::explain(solver& s, constraint_ref_vector const& conflict, pvar v, clause_ref& out_lemma) { + bool forbidden_intervals::explain(solver& s, vector const& conflict, pvar v, clause_ref& out_lemma) { // Extract forbidden intervals from conflicting constraints vector records; bool has_full = false; rational longest_len; unsigned longest_i = UINT_MAX; - for (constraint* c : conflict) { - LOG_H3("Computing forbidden interval for: " << *c); - if (c->is_undef()) { - LOG("TODO: undef constraint in conflict... what does this mean???"); - continue; - } + for (constraint_literal c : conflict) { + LOG_H3("Computing forbidden interval for: " << c); eval_interval interval = eval_interval::full(); - constraint_literal neg_cond; - if (c->forbidden_interval(s, v, interval, neg_cond)) { + constraint_literal_ref neg_cond; + if (c->forbidden_interval(s, c.is_positive(), v, interval, neg_cond)) { LOG("interval: " << interval); - LOG("neg_cond: " << show_deref(neg_cond)); + LOG("neg_cond: " << neg_cond); if (interval.is_currently_empty()) continue; if (interval.is_full()) @@ -106,7 +102,7 @@ namespace polysat { auto& full_record = records.back(); SASSERT(full_record.interval.is_full()); clause_builder clause(s); - clause.push_literal(~full_record.src->blit()); + clause.push_literal(~full_record.src.literal()); if (full_record.neg_cond) clause.push_new_constraint(std::move(full_record.neg_cond)); out_lemma = clause.build(); @@ -134,7 +130,7 @@ namespace polysat { unsigned lemma_lvl = 0; for (unsigned i : seq) { - constraint* c = records[i].src; + constraint_literal const& c = records[i].src; lemma_lvl = std::max(lemma_lvl, c->level()); } @@ -149,7 +145,7 @@ namespace polysat { clause_builder clause(s); // Add negation of src constraints as antecedents (may be resolved during backtracking) for (unsigned const i : seq) { - sat::literal src_lit = records[i].src->blit(); + sat::literal src_lit = records[i].src.literal(); clause.push_literal(~src_lit); } // Add side conditions and interval constraints @@ -163,12 +159,12 @@ 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_literal c = ~s.m_constraints.ult(lemma_lvl, lhs, rhs); - LOG("constraint: " << *c); + constraint_literal_ref 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_literal& neg_cond = records[i].neg_cond; + constraint_literal_ref& neg_cond = records[i].neg_cond; if (neg_cond) clause.push_new_constraint(std::move(neg_cond)); } diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index f36e90452..e47ed340d 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -22,7 +22,7 @@ namespace polysat { class forbidden_intervals { public: - static bool explain(solver& s, constraint_ref_vector const& conflict, pvar v, clause_ref& out_lemma); + static bool explain(solver& s, vector const& conflict, pvar v, clause_ref& out_lemma); }; } diff --git a/src/math/polysat/linear_solver.cpp b/src/math/polysat/linear_solver.cpp index fbd61999e..822e0bd60 100644 --- a/src/math/polysat/linear_solver.cpp +++ b/src/math/polysat/linear_solver.cpp @@ -134,7 +134,6 @@ namespace polysat { if (!fp) return; rational z(0), o(1); - SASSERT(!c.is_undef()); if (is_positive) fp->set_bounds(v, z, z, c_dep); else @@ -211,7 +210,6 @@ namespace polysat { void linear_solver::activate_constraint(bool is_positive, constraint& c) { m_active.push_back(&c); m_trail.push_back(trail_i::set_active_i); - SASSERT(!c.is_undef()); switch (c.kind()) { case ckind_t::eq_t: assert_eq(is_positive, c.to_eq()); diff --git a/src/math/polysat/log_helper.h b/src/math/polysat/log_helper.h index 76ad7b99a..10408bb6c 100644 --- a/src/math/polysat/log_helper.h +++ b/src/math/polysat/log_helper.h @@ -40,21 +40,6 @@ show_deref_t show_deref(T* ptr) { return show_deref_t{ptr}; } -// template -// show_deref_t show_deref(ref const& ptr) { -// return show_deref_t{ptr.get()}; -// } - -// template -// show_deref_t show_deref(scoped_ptr const& ptr) { -// return show_deref_t{ptr.get()}; -// } - -// template ())> -// show_deref_t show_deref(Ptr const& ptr) { -// return show_deref_t{&*ptr}; -// } - template ().get())>::type> show_deref_t show_deref(Ptr const& ptr) { return show_deref_t{ptr.get()}; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index e5c6a31eb..7a08f7327 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -26,7 +26,6 @@ Author: namespace polysat { - dd::pdd_manager& solver::sz2pdd(unsigned sz) { m_pdd.reserve(sz + 1); if (!m_pdd[sz]) @@ -83,8 +82,8 @@ namespace polysat { m_value.push_back(rational::zero()); m_justification.push_back(justification::unassigned()); m_viable.push(sz); - m_cjust.push_back(constraints()); - m_watch.push_back(ptr_vector()); + m_cjust.push_back({}); + m_watch.push_back({}); m_activity.push_back(0); m_vars.push_back(sz2pdd(sz).mk_var(v)); m_size.push_back(sz); @@ -112,51 +111,52 @@ namespace polysat { m_free_vars.del_var_eh(v); } - constraint_literal solver::mk_eq(pdd const& p) { + constraint_literal_ref solver::mk_eq(pdd const& p) { return m_constraints.eq(m_level, p); } - constraint_literal solver::mk_diseq(pdd const& p) { + constraint_literal_ref solver::mk_diseq(pdd const& p) { return ~m_constraints.eq(m_level, p); } - constraint_literal solver::mk_ule(pdd const& p, pdd const& q) { + constraint_literal_ref solver::mk_ule(pdd const& p, pdd const& q) { return m_constraints.ule(m_level, p, q); } - constraint_literal solver::mk_ult(pdd const& p, pdd const& q) { + constraint_literal_ref solver::mk_ult(pdd const& p, pdd const& q) { return m_constraints.ult(m_level, p, q); } - constraint_literal solver::mk_sle(pdd const& p, pdd const& q) { + constraint_literal_ref solver::mk_sle(pdd const& p, pdd const& q) { return m_constraints.sle(m_level, p, q); } - constraint_literal solver::mk_slt(pdd const& p, pdd const& q) { + constraint_literal_ref solver::mk_slt(pdd const& p, pdd const& q) { return m_constraints.slt(m_level, p, q); } - void solver::new_constraint(constraint_literal cl, unsigned dep, bool activate) { + void solver::new_constraint(constraint_literal_ref cl, unsigned dep, bool activate) { VERIFY(at_base_level()); 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(); + constraint_literal 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_constraints.register_external(c.get_constraint()); + LOG("New constraint: " << c); m_original.push_back(c); #if ENABLE_LINEAR_SOLVER - m_linear_solver.new_constraint(*c); + m_linear_solver.new_constraint(*c.constraint()); #endif if (activate && !is_conflict()) - activate_constraint_base(c, !lit.sign()); + activate_constraint_base(c); } void solver::assign_eh(unsigned dep, bool is_true) { VERIFY(at_base_level()); + NOT_IMPLEMENTED_YET(); + /* constraint* c = m_constraints.lookup_external(dep); if (!c) { LOG("WARN: there is no constraint for dependency " << dep); @@ -164,7 +164,10 @@ namespace polysat { } if (is_conflict()) return; - activate_constraint_base(c, is_true); + // TODO: this is wrong. (e.g., if the external constraint was negative) we need to store constraint_literals + constraint_literal cl{c, is_true}; + activate_constraint_base(cl); + */ } @@ -199,10 +202,9 @@ namespace polysat { void solver::propagate(sat::literal lit) { LOG_H2("Propagate boolean literal " << lit); - constraint* c = m_constraints.lookup(lit.var()); + constraint_literal c = m_constraints.lookup(lit); (void)c; SASSERT(c); - SASSERT(!c->is_undef()); // c->narrow(*this); } @@ -211,14 +213,14 @@ namespace polysat { auto& wlist = m_watch[v]; unsigned i = 0, j = 0, sz = wlist.size(); for (; i < sz && !is_conflict(); ++i) - if (!wlist[i]->propagate(*this, v)) + if (!wlist[i].propagate(*this, v)) wlist[j++] = wlist[i]; for (; i < sz; ++i) wlist[j++] = wlist[i]; wlist.shrink(j); } - void solver::propagate(pvar v, rational const& val, constraint& c) { + void solver::propagate(pvar v, rational const& val, constraint_literal c) { LOG("Propagation: " << assignment_pp(*this, v, val) << ", due to " << c); if (m_viable.is_viable(v, val)) { m_free_vars.del_var_eh(v); @@ -274,8 +276,8 @@ namespace polysat { case trail_instr_t::assign_bool_i: { sat::literal lit = m_search.back().lit(); LOG_V("Undo assign_bool_i: " << lit); - constraint* c = m_constraints.lookup(lit.var()); - deactivate_constraint(*c); + constraint_literal c = m_constraints.lookup(lit); + deactivate_constraint(c); m_bvars.unassign(lit); m_search.pop(); break; @@ -298,42 +300,44 @@ namespace polysat { SASSERT(m_level == target_level); } - void solver::pop_constraints(ptr_vector& cs) { + void solver::pop_constraints(constraint_literals& cs) { VERIFY(invariant(cs)); while (!cs.empty() && cs.back()->level() > m_level) { - deactivate_constraint(*cs.back()); + deactivate_constraint(cs.back()); cs.pop_back(); } } - void solver::add_watch(constraint& c) { - auto const& vars = c.vars(); + void solver::add_watch(constraint_literal c) { + SASSERT(c); + auto const& vars = c.get_constraint()->vars(); if (vars.size() > 0) add_watch(c, vars[0]); if (vars.size() > 1) add_watch(c, vars[1]); } - void solver::add_watch(constraint &c, pvar v) { + void solver::add_watch(constraint_literal c, pvar v) { + SASSERT(c); LOG("Watching v" << v << " in constraint " << c); - m_watch[v].push_back(&c); + m_watch[v].push_back(c); } - void solver::erase_watch(constraint& c) { - auto const& vars = c.vars(); + void solver::erase_watch(constraint_literal c) { + auto const& vars = c.get_constraint()->vars(); if (vars.size() > 0) erase_watch(vars[0], c); if (vars.size() > 1) erase_watch(vars[1], c); } - void solver::erase_watch(pvar v, constraint& c) { + void solver::erase_watch(pvar v, constraint_literal c) { if (v == null_var) return; auto& wlist = m_watch[v]; unsigned sz = wlist.size(); for (unsigned i = 0; i < sz; ++i) { - if (&c == wlist[i]) { + if (c == wlist[i]) { wlist[i] = wlist.back(); wlist.pop_back(); return; @@ -388,49 +392,27 @@ namespace polysat { #endif } - void solver::set_conflict(constraint& c) { - LOG("Conflict: " << c); - LOG("\n" << *this); - SASSERT(!is_conflict()); - m_conflict.push_back(&c); - } - - void solver::set_conflict(clause& cl) { - LOG("Conflict: " << cl); - SASSERT(!is_conflict()); - m_conflict.push_back(&cl); + void solver::set_conflict(constraint_literal c) { + m_conflict.set(c); } void solver::set_conflict(pvar v) { - SASSERT(!is_conflict()); - m_conflict.append(m_cjust[v]); - if (m_cjust[v].empty()) - m_conflict.push_back(nullptr); - LOG("Conflict for v" << v << ": " << m_conflict); + m_conflict.set(v, m_cjust[v]); + } + + void solver::set_marks(conflict_core const& cc) { + for (auto c : cc.constraints()) + if (c) + set_marks(*c); } void solver::set_marks(constraint const& c) { - LOG_V("Marking in: " << c); if (c.bvar() != sat::null_bool_var) m_bvars.set_mark(c.bvar()); for (auto v : c.vars()) set_mark(v); } - void solver::set_marks(clause const& cl) { - LOG_V("Marking in: " << cl); - for (auto lit : cl) - set_marks(*m_constraints.lookup(lit.var())); - } - - void solver::set_marks(constraints_and_clauses const& cc) { - for (auto c : cc.units()) - if (c) - set_marks(*c); - for (auto cl : cc.clauses()) - set_marks(*cl); - } - /** * Conflict resolution. * - m_conflict are constraints that are infeasible in the current assignment. @@ -456,6 +438,9 @@ namespace polysat { SASSERT(is_conflict()); + NOT_IMPLEMENTED_YET(); // TODO: needs to be refactored to use conflict_core, will be moved to conflict_explainer + + /* if (m_conflict.units().size() == 1 && !m_conflict.units()[0]) { report_unsat(); return; @@ -595,9 +580,12 @@ namespace polysat { } } report_unsat(); + */ } clause_ref solver::resolve_bool(sat::literal lit) { + NOT_IMPLEMENTED_YET(); return nullptr; + /* if (m_conflict.size() != 1) return nullptr; if (m_conflict.clauses().size() != 1) @@ -623,9 +611,12 @@ namespace polysat { } return lemma; // currently modified in-place + */ } void solver::backtrack(unsigned i, clause_ref lemma) { + NOT_IMPLEMENTED_YET(); + /* do { auto const& item = m_search[i]; if (item.is_assignment()) { @@ -676,6 +667,7 @@ namespace polysat { while (i-- > 0); add_lemma(lemma); // TODO: this lemma is stored but otherwise "lost" because it will not be activated / not added to any watch data structures report_unsat(); + */ } void solver::report_unsat() { @@ -684,6 +676,8 @@ namespace polysat { } void solver::unsat_core(unsigned_vector& deps) { + NOT_IMPLEMENTED_YET(); // TODO: needs to be fixed to work with conflict_core + /* deps.reset(); p_dependency_ref conflict_dep(m_dm); for (auto& c : m_conflict.units()) @@ -692,6 +686,7 @@ namespace polysat { for (auto& c : m_conflict.clauses()) conflict_dep = m_dm.mk_join(c->dep(), conflict_dep); m_dm.linearize(conflict_dep, deps); + */ } void solver::learn_lemma(pvar v, clause_ref lemma) { @@ -704,15 +699,15 @@ namespace polysat { add_lemma(std::move(lemma)); if (cl->size() == 1) { sat::literal lit = cl->literals()[0]; - constraint* c = m_constraints.lookup(lit.var()); + constraint_literal c = m_constraints.lookup(lit); c->set_unit_clause(cl); push_cjust(v, c); - activate_constraint_base(c, !lit.sign()); + activate_constraint_base(c); } else { sat::literal lit = decide_bool(*cl); SASSERT(lit != sat::null_literal); - constraint* c = m_constraints.lookup(lit.var()); + constraint_literal c = m_constraints.lookup(lit); push_cjust(v, c); } } @@ -729,10 +724,9 @@ namespace polysat { if (m_bvars.value(lit) == l_false) // already assigned => cannot decide on this (comes from either lemma LHS or previously decided literals that are now changed to propagation) return false; 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); + constraint_literal c = m_constraints.lookup(lit); + SASSERT(!c.is_currently_true(*this)); // should not happen in a valid lemma + return !c.is_currently_false(*this); }; sat::literal choice = sat::null_literal; @@ -747,11 +741,12 @@ namespace polysat { } LOG_V("num_choices: " << num_choices); - if (num_choices == 0) + if (num_choices == 0) { // This case may happen when all undefined literals are false under the current variable assignment. // TODO: The question is whether such lemmas should be generated? Check test_monot() for such a case. - set_conflict(lemma); - else if (num_choices == 1) + // set_conflict(lemma); + NOT_IMPLEMENTED_YET(); + } else if (num_choices == 1) propagate_bool(choice, &lemma); else decide_bool(choice, lemma); @@ -772,6 +767,8 @@ namespace polysat { void solver::revert_decision(pvar v, clause_ref reason) { rational val = m_value[v]; LOG_H3("Reverting decision: pvar " << v << " := " << val); + NOT_IMPLEMENTED_YET(); + /* SASSERT(m_justification[v].is_decision()); backjump(m_justification[v].level()-1); @@ -816,6 +813,7 @@ namespace polysat { m_free_vars.del_var_eh(v); decide(v); } + */ } void solver::revert_bool_decision(sat::literal lit, clause_ref reason) { @@ -823,6 +821,9 @@ namespace polysat { LOG_H3("Reverting boolean decision: " << lit); SASSERT(m_bvars.is_decision(var)); + NOT_IMPLEMENTED_YET(); + /* + if (reason) { LOG("Reason: " << show_deref(reason)); bool contains_var = std::any_of(reason->begin(), reason->end(), [var](sat::literal reason_lit) { return reason_lit.var() == var; }); @@ -890,6 +891,7 @@ namespace polysat { } decide_bool(*lemma); + */ } void solver::decide_bool(sat::literal lit, clause& lemma) { @@ -903,9 +905,9 @@ namespace polysat { SASSERT(reason); if (reason->literals().size() == 1) { SASSERT(reason->literals()[0] == lit); - constraint* c = m_constraints.lookup(lit.var()); + constraint_literal c = m_constraints.lookup(lit); // m_redundant.push_back(c); - activate_constraint_base(c, !lit.sign()); + activate_constraint_base(c); } else assign_bool_backtrackable(lit, reason, nullptr); @@ -919,22 +921,19 @@ namespace polysat { m_trail.push_back(trail_instr_t::assign_bool_i); m_search.push_boolean(lit); - constraint* c = m_constraints.lookup(lit.var()); - SASSERT(c); - bool is_true = !lit.sign(); - activate_constraint(*c, is_true); + constraint_literal c = m_constraints.lookup(lit); + activate_constraint(c); } /// Activate a constraint at the base level. /// Used for external unit constraints and unit consequences. - void solver::activate_constraint_base(constraint* c, bool is_true) { + void solver::activate_constraint_base(constraint_literal c) { SASSERT(c); LOG("\n" << *this); // 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_bool_core(c.literal(), nullptr, nullptr); + activate_constraint(c); } /// Assign a boolean literal @@ -949,22 +948,21 @@ namespace polysat { * constraints activated within the linear solver are de-activated when the linear * solver is popped. */ - void solver::activate_constraint(constraint& c, bool is_true) { - LOG("Activating constraint: " << c << " ; is_true = " << is_true); - SASSERT(m_bvars.value(c.bvar()) == to_lbool(is_true)); - c.assign(is_true); + void solver::activate_constraint(constraint_literal c) { + SASSERT(c); + LOG("Activating constraint: " << c); + SASSERT(m_bvars.value(c.literal()) == l_true); add_watch(c); c.narrow(*this); #if ENABLE_LINEAR_SOLVER - m_linear_solver.activate_constraint(c.is_positive(), c); + m_linear_solver.activate_constraint(c.is_positive(), c.constraint()); // TODO: linear solver should probably take a constraint_literal #endif } /// Deactivate constraint - void solver::deactivate_constraint(constraint& c) { + void solver::deactivate_constraint(constraint_literal c) { LOG("Deactivating constraint: " << c); erase_watch(c); - c.unassign(); } void solver::backjump(unsigned new_level) { @@ -973,23 +971,6 @@ namespace polysat { if (num_levels > 0) pop_levels(num_levels); } - - /** - * Return residue of superposing p and q with respect to v. - */ - clause_ref solver::resolve(pvar v) { - LOG_H3("Resolve v" << v); - SASSERT(!m_cjust[v].empty()); - SASSERT(m_justification[v].is_propagation()); - LOG("Conflict: " << m_conflict); - LOG("cjust[v" << v << "]: " << m_cjust[v]); - - 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; - } /** * placeholder for factoring/gcd common factors @@ -1007,18 +988,18 @@ namespace polysat { clause* cl = m_constraints.store(std::move(lemma)); m_redundant_clauses.push_back(cl); if (cl->size() == 1) { - constraint* c = m_constraints.lookup(cl->literals()[0].var()); + constraint_literal c = m_constraints.lookup(cl->literals()[0]); insert_constraint(m_redundant, c); } } - void solver::insert_constraint(ptr_vector& cs, constraint* c) { + void solver::insert_constraint(constraint_literals& cs, constraint_literal c) { SASSERT(c); - LOG_V("INSERTING: " << *c); + LOG_V("INSERTING: " << c); cs.push_back(c); for (unsigned i = cs.size() - 1; i-- > 0; ) { - auto* c1 = cs[i + 1]; - auto* c2 = cs[i]; + auto c1 = cs[i + 1]; + auto c2 = cs[i]; if (c1->level() >= c2->level()) break; std::swap(cs[i], cs[i+1]); @@ -1088,11 +1069,11 @@ namespace polysat { } out << "Boolean assignment:\n\t" << m_bvars << "\n"; out << "Original:\n"; - for (auto* c : m_original) - out << "\t" << *c << "\n"; + for (auto c : m_original) + out << "\t" << c << "\n"; out << "Redundant:\n"; - for (auto* c : m_redundant) - out << "\t" << *c << "\n"; + for (auto c : m_redundant) + out << "\t" << c << "\n"; out << "Redundant clauses:\n"; for (auto* cl : m_redundant_clauses) { out << "\t" << *cl << "\n"; @@ -1136,7 +1117,7 @@ namespace polysat { /** * constraints are sorted by levels so they can be removed when levels are popped. */ - bool solver::invariant(ptr_vector const& cs) { + bool solver::invariant(constraint_literals const& cs) { unsigned sz = cs.size(); for (unsigned i = 0; i + 1 < sz; ++i) VERIFY(cs[i]->level() <= cs[i + 1]->level()); @@ -1147,12 +1128,10 @@ namespace polysat { * Check that two variables of each constraint are watched. */ bool solver::wlist_invariant() { - constraints cs; + constraint_literals cs; cs.append(m_original.size(), m_original.data()); cs.append(m_redundant.size(), m_redundant.data()); - for (auto* c : cs) { - if (c->is_undef()) - continue; + for (auto c : cs) { int64_t num_watches = 0; for (auto const& wlist : m_watch) { auto n = std::count(wlist.begin(), wlist.end(), c); @@ -1172,12 +1151,13 @@ namespace polysat { bool solver::verify_sat() { LOG_H1("Checking current model..."); LOG("Assignment: " << assignments_pp(*this)); - for (auto* c : m_original) { - bool ok = c->is_currently_true(*this); - LOG((ok ? "PASS" : "FAIL") << ": " << show_deref(c)); - if (!ok) return false; + bool all_ok = true; + for (auto c : m_original) { + bool ok = c.is_currently_true(*this); + LOG((ok ? "PASS" : "FAIL") << ": " << c); + all_ok = all_ok && ok; } - LOG("All good!"); + if (all_ok) LOG("All good!"); return true; } } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 671848357..56d63ee7b 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -21,9 +21,11 @@ Author: #include "util/statistics.h" #include "util/params.h" #include "math/polysat/boolean.h" +#include "math/polysat/conflict_core.h" #include "math/polysat/constraint.h" #include "math/polysat/clause_builder.h" #include "math/polysat/eq_constraint.h" +#include "math/polysat/explain.h" #include "math/polysat/ule_constraint.h" #include "math/polysat/justification.h" #include "math/polysat/linear_solver.h" @@ -59,6 +61,7 @@ namespace polysat { friend class assignments_pp; typedef ptr_vector constraints; + typedef vector constraint_literals; reslimit& m_lim; params_ref m_params; @@ -68,7 +71,7 @@ namespace polysat { small_object_allocator m_alloc; poly_dep_manager m_dm; linear_solver m_linear_solver; - constraints_and_clauses m_conflict; + conflict_core m_conflict; // constraints m_stash_just; var_queue m_free_vars; stats m_stats; @@ -81,8 +84,8 @@ namespace polysat { // Per constraint state constraint_manager m_constraints; - ptr_vector m_original; - ptr_vector m_redundant; + constraint_literals m_original; + constraint_literals m_redundant; ptr_vector m_redundant_clauses; svector m_disjunctive_lemma; @@ -90,8 +93,8 @@ namespace polysat { // Per variable information vector m_value; // assigned value vector m_justification; // justification for variable assignment - vector m_cjust; // constraints justifying variable range. - vector m_watch; // watch list datastructure into constraints. + vector m_cjust; // constraints justifying variable range. + vector m_watch; // watch list datastructure into constraints. unsigned_vector m_activity; vector m_vars; unsigned_vector m_size; // store size of variables. @@ -125,12 +128,12 @@ namespace polysat { m_qhead_trail.pop_back(); } - void push_cjust(pvar v, constraint* c) { + void push_cjust(pvar v, constraint_literal c) { if (m_cjust[v].contains(c)) // TODO: better check (flag on constraint?) return; - LOG_V("cjust[v" << v << "] += " << show_deref(c)); + LOG_V("cjust[v" << v << "] += " << c); SASSERT(c); - m_cjust[v].push_back(c); + m_cjust[v].push_back(c); m_trail.push_back(trail_instr_t::just_i); m_cjust_trail.push_back(v); } @@ -148,14 +151,14 @@ namespace polysat { void push_level(); void pop_levels(unsigned num_levels); - void pop_constraints(ptr_vector& cs); + void pop_constraints(constraint_literals& cs); void assign_bool_backtrackable(sat::literal lit, clause* reason, clause* lemma); - void activate_constraint_base(constraint* c, bool is_true); + void activate_constraint_base(constraint_literal c); 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); - void deactivate_constraint(constraint& c); + void activate_constraint(constraint_literal c); + void deactivate_constraint(constraint_literal c); sat::literal decide_bool(clause& lemma); void decide_bool(sat::literal lit, clause& lemma); void propagate_bool(sat::literal lit, clause* reason); @@ -168,14 +171,13 @@ namespace polysat { void propagate(sat::literal lit); void propagate(pvar v); - void propagate(pvar v, rational const& val, constraint& c); - void erase_watch(pvar v, constraint& c); - void erase_watch(constraint& c); - void add_watch(constraint& c); - void add_watch(constraint& c, pvar v); + void propagate(pvar v, rational const& val, constraint_literal c); + void erase_watch(pvar v, constraint_literal c); + void erase_watch(constraint_literal c); + void add_watch(constraint_literal c); + void add_watch(constraint_literal c, pvar v); - void set_conflict(constraint& c); - void set_conflict(clause& cl); + void set_conflict(constraint_literal c); void set_conflict(pvar v); unsigned_vector m_marks; @@ -184,13 +186,11 @@ namespace polysat { bool is_marked(pvar v) const { return m_clock == m_marks[v]; } void set_mark(pvar v) { LOG_V("Marking: v" << v); m_marks[v] = m_clock; } - void set_marks(constraints_and_clauses const& cc); + void set_marks(conflict_core const& cc); void set_marks(constraint const& c); - void set_marks(clause const& cl); unsigned m_conflict_level { 0 }; - clause_ref resolve(pvar v); clause_ref resolve_bool(sat::literal lit); bool can_decide() const { return !m_free_vars.empty(); } @@ -219,17 +219,17 @@ namespace polysat { void backjump(unsigned new_level); void add_lemma(clause_ref lemma); - 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); + constraint_literal_ref mk_eq(pdd const& p); + constraint_literal_ref mk_diseq(pdd const& p); + constraint_literal_ref mk_ule(pdd const& p, pdd const& q); + constraint_literal_ref mk_ult(pdd const& p, pdd const& q); + constraint_literal_ref mk_sle(pdd const& p, pdd const& q); + constraint_literal_ref mk_slt(pdd const& p, pdd const& q); + void new_constraint(constraint_literal_ref c, unsigned dep, bool activate); + static void insert_constraint(constraint_literals& cs, constraint_literal c); bool invariant(); - static bool invariant(ptr_vector const& cs); + static bool invariant(constraint_literals const& cs); bool wlist_invariant(); bool verify_sat(); diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index a3b0c7930..ac0121432 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -18,12 +18,16 @@ Author: namespace polysat { - std::ostream& ule_constraint::display(std::ostream& out) const { - out << m_lhs << " <= " << m_rhs; - return display_extra(out); + std::ostream& ule_constraint::display(std::ostream& out, lbool status) const { + out << m_lhs; + if (status == l_true) out << " <= "; + else if (status == l_false) out << " > "; + else out << " <=/> "; + out << m_rhs; + return display_extra(out, status); } - void ule_constraint::narrow(solver& s) { + void ule_constraint::narrow(solver& s, bool is_positive) { LOG_H3("Narrowing " << *this); LOG("Assignment: " << assignments_pp(s)); auto p = lhs().subst_val(s.assignment()); @@ -31,15 +35,13 @@ namespace polysat { auto q = rhs().subst_val(s.assignment()); LOG("Substituted RHS: " << rhs() << " := " << q); - SASSERT(!is_undef()); - - if (is_always_false(p, q)) { - s.set_conflict(*this); + if (is_always_false(is_positive, p, q)) { + s.set_conflict({this, is_positive}); return; } if (p.is_val() && q.is_val()) { - SASSERT(!is_positive() || p.val() <= q.val()); - SASSERT(!is_negative() || p.val() > q.val()); + SASSERT(!is_positive || p.val() <= q.val()); + SASSERT(is_positive || p.val() > q.val()); return; } @@ -70,13 +72,13 @@ namespace polysat { d = q.lo().val(); } if (v != null_var) { - s.push_cjust(v, this); + s.push_cjust(v, {this, is_positive}); - s.m_viable.intersect_ule(v, a, b, c, d, is_positive()); + s.m_viable.intersect_ule(v, a, b, c, d, is_positive); rational val; if (s.m_viable.find_viable(v, val) == dd::find_t::singleton) - s.propagate(v, val, *this); + s.propagate(v, val, {this, is_positive}); return; } @@ -84,39 +86,35 @@ namespace polysat { // TODO: other cheap constraints possible? } - bool ule_constraint::is_always_false(pdd const& lhs, pdd const& rhs) { + bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) { // TODO: other conditions (e.g. when forbidden interval would be full) - VERIFY(!is_undef()); - if (is_positive()) + if (is_positive) return lhs.is_val() && rhs.is_val() && lhs.val() > rhs.val(); else return (lhs.is_val() && rhs.is_val() && lhs.val() <= rhs.val()) || (lhs == rhs); } - bool ule_constraint::is_always_false() { - return is_always_false(lhs(), rhs()); + bool ule_constraint::is_always_false(bool is_positive) { + return is_always_false(is_positive, lhs(), rhs()); } - bool ule_constraint::is_currently_false(solver& s) { + bool ule_constraint::is_currently_false(solver& s, bool is_positive) { auto p = lhs().subst_val(s.assignment()); auto q = rhs().subst_val(s.assignment()); - return is_always_false(p, q); + return is_always_false(is_positive, p, q); } - bool ule_constraint::is_currently_true(solver& s) { + bool ule_constraint::is_currently_true(solver& s, bool is_positive) { auto p = lhs().subst_val(s.assignment()); auto q = rhs().subst_val(s.assignment()); - VERIFY(!is_undef()); - if (is_positive()) + if (is_positive) return p.is_val() && q.is_val() && p.val() <= q.val(); else 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_literal& out_neg_cond) + bool ule_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, constraint_literal_ref& out_neg_cond) { - SASSERT(!is_undef()); - // Current only works when degree(v) is at most one on both sides unsigned const deg1 = lhs().degree(v); unsigned const deg2 = rhs().degree(v); @@ -249,7 +247,7 @@ namespace polysat { out_neg_cond = s.m_constraints.eq(level(), condition_body); if (is_trivial) { - if (is_positive()) + if (is_positive) // TODO: we cannot use empty intervals for interpolation. So we // can remove the empty case (make it represent 'full' instead), // and return 'false' here. Then we do not need the proper/full @@ -276,7 +274,7 @@ namespace polysat { else SASSERT(y_coeff.is_one()); - if (is_negative()) { + if (!is_positive) { swap(lo, hi); lo_val.swap(hi_val); } @@ -286,9 +284,8 @@ namespace polysat { return true; } - inequality ule_constraint::as_inequality() const { - SASSERT(!is_undef()); - if (is_positive()) + inequality ule_constraint::as_inequality(bool is_positive) const { + if (is_positive) return inequality(lhs(), rhs(), false, this); else return inequality(rhs(), lhs(), true, this); diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index cc148a811..c70461d7d 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -31,14 +31,14 @@ namespace polysat { ~ule_constraint() override {} pdd const& lhs() const { return m_lhs; } pdd const& rhs() const { return m_rhs; } - std::ostream& display(std::ostream& out) const 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_literal& out_neg_cond) override; - inequality as_inequality() const override; + std::ostream& display(std::ostream& out, lbool status) const override; + bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs); + bool is_always_false(bool is_positive) override; + bool is_currently_false(solver& s, bool is_positive) override; + bool is_currently_true(solver& s, bool is_positive) override; + void narrow(solver& s, bool is_positive) override; + bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, constraint_literal_ref& out_neg_cond) override; + inequality as_inequality(bool is_positive) const override; unsigned hash() const override; bool operator==(constraint const& other) const override; }; diff --git a/src/test/fixplex.cpp b/src/test/fixplex.cpp index 9dc526917..a8b765b7f 100644 --- a/src/test/fixplex.cpp +++ b/src/test/fixplex.cpp @@ -11,11 +11,12 @@ namespace polysat { typedef uint64_ext::numeral numeral; - struct solver_scope { + struct fp_scope { params_ref p; reslimit lim; }; - struct scoped_fp : public solver_scope, public fixplex { + + struct scoped_fp : public fp_scope, public fixplex { scoped_fp(): fixplex(p, lim) {}