diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index 0b06ae3a4..abff51f65 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -1,11 +1,13 @@ z3_add_component(polysat SOURCES + boolean.cpp constraint.cpp eq_constraint.cpp forbidden_intervals.cpp justification.cpp linear_solver.cpp log.cpp + search_state.cpp solver.cpp ule_constraint.cpp var_constraint.cpp diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp new file mode 100644 index 000000000..bd7e6291d --- /dev/null +++ b/src/math/polysat/boolean.cpp @@ -0,0 +1,78 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat boolean variables + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#include "math/polysat/boolean.h" +#include "math/polysat/log.h" + +namespace polysat { + + sat::bool_var bool_var_manager::new_var() { + if (m_unused.empty()) { + sat::bool_var var = size(); + m_value.push_back(l_undef); + m_value.push_back(l_undef); + m_level.push_back(UINT_MAX); + m_reason.push_back(nullptr); + m_lemma.push_back(nullptr); + return var; + } else { + sat::bool_var var = m_unused.back(); + m_unused.pop_back(); + SASSERT_EQ(m_level[var], UINT_MAX); + return var; + } + } + + void bool_var_manager::del_var(sat::bool_var var) { + SASSERT(std::all_of(m_unused.begin(), m_unused.end(), [var](unsigned unused_var) { return var != unused_var; })); + auto lit = sat::literal(var); + m_value[lit.index()] = l_undef; + m_value[(~lit).index()] = l_undef; + m_level[var] = UINT_MAX; + m_reason[var] = nullptr; + m_lemma[var] = nullptr; + m_unused.push_back(var); + } + + void bool_var_manager::assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma) { + SASSERT(!is_assigned(lit)); + m_value[lit.index()] = l_true; + m_value[(~lit).index()] = l_false; + m_level[lit.var()] = lvl; + m_reason[lit.var()] = reason; + m_lemma[lit.var()] = lemma; + } + + void bool_var_manager::unassign(sat::literal lit) { + SASSERT(is_assigned(lit)); + m_value[lit.index()] = l_undef; + m_value[(~lit).index()] = l_undef; + m_level[lit.var()] = UINT_MAX; + m_reason[lit.var()] = nullptr; + m_lemma[lit.var()] = nullptr; + } + + void bool_var_manager::reset_marks() { + m_marks.reserve(size()); + m_clock++; + if (m_clock != 0) + return; + m_clock++; + m_marks.fill(0); + } + + void bool_var_manager::set_mark(sat::bool_var var) { + SASSERT(var != sat::null_bool_var); + m_marks[var] = m_clock; + } +} diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h new file mode 100644 index 000000000..977dcfc22 --- /dev/null +++ b/src/math/polysat/boolean.h @@ -0,0 +1,63 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat boolean variables + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once +#include "math/polysat/types.h" +#include "util/sat_literal.h" + +namespace polysat { + + class clause; + + class bool_var_manager { + svector m_unused; // previously deleted variables that can be reused by new_var(); + svector m_value; // current value (indexed by literal) + svector m_level; // level of assignment (indexed by variable) + svector m_reason; // propagation reason, NULL for decisions (indexed by variable) + + // For enumerative backtracking we store the lemma we're handling with a certain decision + svector m_lemma; + + unsigned_vector m_marks; + unsigned m_clock { 0 }; + + // allocated size (not the number of active variables) + unsigned size() const { return m_level.size(); } + + public: + sat::bool_var new_var(); + void del_var(sat::bool_var var); + + void reset_marks(); + bool is_marked(sat::bool_var var) const { return m_clock == m_marks[var]; } + void set_mark(sat::bool_var var); + + bool is_assigned(sat::bool_var var) const { return value(var) != l_undef; } + bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; } + bool is_decision(sat::bool_var var) const { return is_assigned(var) && !reason(var); } + // bool is_decision(bool_lit lit) const { return is_decision(lit.var()); } + bool is_propagation(sat::bool_var var) const { return is_assigned(var) && reason(var); } + lbool value(sat::bool_var var) const { return value(sat::literal(var)); } + lbool value(sat::literal lit) const { return m_value[lit.index()]; } + unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; } + // unsigned level(sat::literal lit) const { return level(lit.var()); } + clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_reason[var]; } + + clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_lemma[var]; } + + /// Set the given literal to true + void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma); + void unassign(sat::literal lit); + }; + +} diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 5b08d78ae..2d731b108 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -21,6 +21,45 @@ Author: namespace polysat { + constraint* constraint_manager::insert(scoped_ptr&& sc) { + constraint* c = sc.detach(); + LOG_V("Inserting constraint: " << show_deref(c)); + SASSERT(c); + SASSERT(c->bvar() != sat::null_bool_var); + SASSERT(get_bv2c(c->bvar()) == nullptr); + insert_bv2c(c->bvar(), c); + // TODO: use explicit insert_external(constraint* c, unsigned dep) for that. + if (c->dep() && c->dep()->is_leaf()) { + unsigned dep = c->dep()->leaf_value(); + SASSERT(!m_external_constraints.contains(dep)); + m_external_constraints.insert(dep, c); + } + while (m_constraints.size() <= c->level()) + m_constraints.push_back({}); + m_constraints[c->level()].push_back(c); + return c; + } + + // Release constraints at the given level and above. + void constraint_manager::release_level(unsigned lvl) { + for (unsigned l = m_constraints.size(); l-- > lvl; ) { + for (constraint* c : m_constraints[l]) { + LOG_V("Removing constraint: " << show_deref(c)); + erase_bv2c(c->bvar()); + if (c->dep() && c->dep()->is_leaf()) { + unsigned dep = c->dep()->leaf_value(); + SASSERT(m_external_constraints.contains(dep)); + m_external_constraints.remove(dep); + } + } + m_constraints[l].reset(); + } + } + + constraint* constraint_manager::lookup(sat::bool_var var) const { + return get_bv2c(var); + } + eq_constraint& constraint::to_eq() { return *dynamic_cast(this); } @@ -45,19 +84,22 @@ namespace polysat { return *dynamic_cast(this); } - - constraint* constraint::eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref const& d) { - return alloc(eq_constraint, lvl, bvar, sign, p, d); + scoped_ptr constraint_manager::eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d) { + return alloc(eq_constraint, *this, lvl, sign, p, d); } - constraint* constraint::viable(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d) { - return alloc(var_constraint, lvl, bvar, sign, v, b, d); + scoped_ptr constraint_manager::viable(unsigned lvl, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d) { + return alloc(var_constraint, *this, lvl, sign, v, b, d); } - constraint* constraint::ule(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { - return alloc(ule_constraint, lvl, bvar, sign, a, b, d); + scoped_ptr constraint_manager::ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { + return alloc(ule_constraint, *this, lvl, sign, a, b, d); } + scoped_ptr constraint_manager::ult(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { + // a < b <=> !(b <= a) + return ule(lvl, static_cast(!sign), b, a, d); + } // To do signed comparison of bitvectors, flip the msb and do unsigned comparison: // @@ -75,19 +117,14 @@ namespace polysat { // // Argument: flipping the msb swaps the negative and non-negative blocks // - constraint* constraint::sle(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { + scoped_ptr constraint_manager::sle(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { auto shift = rational::power_of_two(a.power_of_2() - 1); - return ule(lvl, bvar, sign, a + shift, b + shift, d); + return ule(lvl, sign, a + shift, b + shift, d); } - constraint* constraint::slt(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { + scoped_ptr constraint_manager::slt(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { auto shift = rational::power_of_two(a.power_of_2() - 1); - return ult(lvl, bvar, sign, a + shift, b + shift, d); - } - - constraint* constraint::ult(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { - // a < b <=> !(b <= a) - return ule(lvl, bvar, static_cast(!sign), b, a, d); + return ult(lvl, sign, a + shift, b + shift, d); } bool constraint::propagate(solver& s, pvar v) { @@ -118,4 +155,66 @@ namespace polysat { narrow(s); } + clause* clause::from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector const& literals) { + return alloc(clause, lvl, d, literals); + } + + 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()); + 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()); + return c->is_currently_false(s); + }); + } + std::ostream& clause::display(std::ostream& out) const { + bool first = true; + for (auto lit : literals()) { + if (first) + first = false; + else + out << " \\/ "; + out << lit; + } + return out; + } + + scoped_clause::scoped_clause(scoped_ptr&& c) { + SASSERT(c); + sat::literal_vector lits; + lits.push_back(sat::literal(c->bvar())); + m_clause = clause::from_literals(c->level(), c->m_dep, lits); + m_owned.push_back(c.detach()); + } + + std::ostream& scoped_clause::display(std::ostream& out) const { + if (m_clause) + return out << *m_clause; + else + 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 3465a6778..e5b88e6fc 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -12,46 +12,91 @@ Author: --*/ #pragma once +#include "math/polysat/boolean.h" #include "math/polysat/types.h" #include "math/polysat/interval.h" +#include "util/map.h" namespace polysat { enum ckind_t { eq_t, ule_t, bit_t }; enum csign_t : bool { neg_t = false, pos_t = true }; + class constraint; + class clause; + class scoped_clause; class eq_constraint; class var_constraint; class ule_constraint; + // Manage constraint lifetime, deduplication, and connection to boolean variables/literals. + class constraint_manager { + friend class constraint; + + bool_var_manager& m_bvars; + + // Constraint storage per level + vector> m_constraints; + + // Association to boolean variables + ptr_vector m_bv2constraint; + void insert_bv2c(sat::bool_var bv, constraint* c) { m_bv2constraint.setx(bv, c, nullptr); } + 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); } + + // Association to external dependency values (i.e., external names for constraints) + u_map m_external_constraints; + + // TODO: some hashmaps to look up whether constraint (or its negation) already exists + + public: + constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {} + + // Start managing lifetime of the given constraint + constraint* insert(scoped_ptr&& c); + + // Release constraints at the given level and above. + void release_level(unsigned lvl); + + constraint* lookup(sat::bool_var var) const; + constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); } + + scoped_ptr eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d); + scoped_ptr viable(unsigned lvl, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d); + scoped_ptr ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); + scoped_ptr ult(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); + scoped_ptr sle(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); + scoped_ptr slt(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); + }; + class constraint { + friend class constraint_manager; + friend class clause; + friend class scoped_clause; friend class var_constraint; friend class eq_constraint; friend class ule_constraint; - unsigned m_level; + constraint_manager* m_manager; + unsigned m_storage_level; ///< Controls lifetime of the constraint object. Always a base level (for external dependencies the level at which it was created, and for others the maximum storage level of its external dependencies). + unsigned m_active_level; ///< Level at which the constraint was activated. Possibly different from m_storage_level because constraints in lemmas may become activated only at a higher level. ckind_t m_kind; p_dependency_ref m_dep; unsigned_vector m_vars; - bool_var m_bool_var; + sat::bool_var m_bvar; ///< boolean variable associated to this constraint; convention: a constraint itself always represents the positive sat::literal csign_t m_sign; ///< sign/polarity - lbool m_status = l_undef; ///< current constraint status, computed from value of m_bool_var and m_sign - constraint(unsigned lvl, bool_var bvar, csign_t sign, p_dependency_ref const& dep, ckind_t k): - m_level(lvl), m_kind(k), m_dep(dep), m_bool_var(bvar), m_sign(sign) {} + lbool m_status = l_undef; ///< current constraint status, computed from value of m_lit and m_sign + constraint(constraint_manager& m, unsigned lvl, csign_t sign, p_dependency_ref const& dep, ckind_t k): + m_manager(&m), m_storage_level(lvl), m_kind(k), m_dep(dep), m_bvar(m_manager->m_bvars.new_var()), m_sign(sign) {} public: - static constraint* eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref const& d); - static constraint* viable(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d); - static constraint* ule(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); - static constraint* ult(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); - static constraint* sle(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); - static constraint* slt(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); - virtual ~constraint() {} + virtual ~constraint() { m_manager->m_bvars.del_var(m_bvar); } bool is_eq() const { return m_kind == ckind_t::eq_t; } bool is_ule() const { return m_kind == ckind_t::ule_t; } + bool is_bit() const { return m_kind == ckind_t::bit_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 constraint* resolve(solver& s, pvar v) = 0; + virtual scoped_ptr resolve(solver& s, pvar v) = 0; virtual bool is_always_false() = 0; virtual bool is_currently_false(solver& s) = 0; virtual bool is_currently_true(solver& s) = 0; @@ -64,14 +109,19 @@ namespace polysat { var_constraint const& to_bit() const; p_dependency* dep() const { return m_dep; } unsigned_vector& vars() { return m_vars; } - unsigned level() const { return m_level; } - bool_var bvar() const { return m_bool_var; } + unsigned_vector const& vars() const { return m_vars; } + unsigned level() const { return m_storage_level; } + sat::bool_var bvar() const { return m_bvar; } bool sign() const { return m_sign; } - void assign_eh(bool is_true) { m_status = (is_true ^ !m_sign) ? l_true : l_false; } - void unassign_eh() { m_status = l_undef; } + void assign(bool is_true) { + lbool new_status = (is_true ^ !m_sign) ? l_true : l_false; + SASSERT(is_undef() || new_status == m_status); + m_status = new_status; + } + 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; } - bool is_undef() const { return m_status == l_undef; } /** Precondition: all variables other than v are assigned. * @@ -84,30 +134,154 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); } + // Disjunction of constraints represented by boolean literals class clause { - scoped_ptr_vector m_literals; + unsigned m_level; + unsigned m_next_guess = UINT_MAX; // next guess for enumerative backtracking + p_dependency_ref m_dep; + sat::literal_vector m_literals; + + /* TODO: embed literals to save an indirection? + unsigned m_num_literals; + constraint* m_literals[0]; + + static size_t object_size(unsigned m_num_literals) { + return sizeof(clause) + m_num_literals * sizeof(constraint*); + } + */ + + clause(unsigned lvl, p_dependency_ref const& d, sat::literal_vector const& literals): + m_level(lvl), m_dep(d), m_literals(literals) + { + SASSERT(std::all_of(m_literals.begin(), m_literals.end(), [this](sat::literal l) { return l != sat::null_literal; })); + } + public: - clause() {} - clause(scoped_ptr&& c) { - SASSERT(c); - m_literals.push_back(c.detach()); - } - clause(scoped_ptr_vector&& literals): m_literals(std::move(literals)) { - SASSERT(std::all_of(m_literals.begin(), m_literals.end(), [](constraint* c) { return c != nullptr; })); - SASSERT(empty() || std::all_of(m_literals.begin(), m_literals.end(), [this](constraint* c) { return c->level() == level(); })); - } + // static clause* unit(constraint* c); + static clause* from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector const& literals); + + // Resolve with 'other' upon 'var'. + bool resolve(sat::bool_var var, clause const* other); + + sat::literal_vector const& literals() const { return m_literals; } + p_dependency* dep() const { return m_dep; } + unsigned level() const { return m_level; } bool empty() const { return m_literals.empty(); } unsigned size() const { return m_literals.size(); } - constraint* operator[](unsigned idx) const { return m_literals[idx]; } + sat::literal operator[](unsigned idx) const { return m_literals[idx]; } - using const_iterator = typename scoped_ptr_vector::const_iterator; + using const_iterator = typename sat::literal_vector::const_iterator; const_iterator begin() const { return m_literals.begin(); } const_iterator end() const { return m_literals.end(); } - ptr_vector detach() { return m_literals.detach(); } + bool is_always_false(solver& s) const; + bool is_currently_false(solver& s) const; - unsigned level() const { SASSERT(!empty()); return m_literals[0]->level(); } + unsigned next_guess() { + SASSERT(m_next_guess < m_literals.size()); + return m_next_guess++; + } + + std::ostream& display(std::ostream& out) const; }; + inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); } + + // A clause that owns (some of) the constraints represented by its literals. + class scoped_clause { + scoped_ptr m_clause; + scoped_ptr_vector m_owned; + + public: + scoped_clause() {} + scoped_clause(std::nullptr_t) {} + + scoped_clause(scoped_ptr&& c); + + scoped_clause(scoped_ptr&& clause, scoped_ptr_vector&& owned_literals): + m_clause(std::move(clause)), m_owned(std::move(owned_literals)) {} + + operator bool() const { return m_clause; } + + bool is_owned_unit() const { return m_clause && m_clause->size() == 1 && m_owned.size() == 1; } + + bool empty() const { SASSERT(m_clause); return m_clause->empty(); } + unsigned size() const { SASSERT(m_clause); return m_clause->size(); } + sat::literal operator[](unsigned idx) const { SASSERT(m_clause); return (*m_clause)[idx]; } + + bool is_always_false(solver& s) const { return m_clause->is_always_false(s); } + bool is_currently_false(solver& s) const { return m_clause->is_currently_false(s); } + + clause* get() { return m_clause.get(); } + clause* detach() { SASSERT(m_owned.empty()); return m_clause.detach(); } + ptr_vector detach_constraints() { return m_owned.detach(); } + + using const_iterator = typename clause::const_iterator; + const_iterator begin() const { SASSERT(m_clause); return m_clause->begin(); } + const_iterator end() const { SASSERT(m_clause); return m_clause->end(); } + + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, scoped_clause const& c) { return c.display(out); } + + // Container for unit constraints and clauses. + class constraints_and_clauses { + ptr_vector m_units; + ptr_vector m_clauses; + + public: + ptr_vector const& units() const { return m_units; } + ptr_vector& units() { return m_units; } + + ptr_vector const& clauses() const { return m_clauses; } + ptr_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) { + m_units.append(cs); + } + + void push_back(std::nullptr_t) { m_units.push_back(nullptr); } + void push_back(constraint* c) { m_units.push_back(c); } + void push_back(clause* cl) { m_clauses.push_back(cl); } + + // TODO: use iterator instead + unsigned_vector vars(constraint_manager const& cm) const { + unsigned_vector vars; + for (constraint* c : m_units) + vars.append(c->vars()); + for (clause* 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); } + } diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp index a039ff123..45122d0b5 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/src/math/polysat/eq_constraint.cpp @@ -19,10 +19,13 @@ Author: namespace polysat { std::ostream& eq_constraint::display(std::ostream& out) const { - return out << p() << (sign() == pos_t ? " == 0" : " != 0") << " [" << m_status << "]"; + out << p() << (sign() == pos_t ? " == 0" : " != 0") << " @" << level(); + if (is_undef()) + out << " [inactive]"; + return out; } - constraint* eq_constraint::resolve(solver& s, pvar v) { + scoped_ptr eq_constraint::resolve(solver& s, pvar v) { if (is_positive()) return eq_resolve(s, v); if (is_negative()) @@ -33,8 +36,8 @@ namespace polysat { void eq_constraint::narrow(solver& s) { SASSERT(!is_undef()); - LOG("Assignment: " << s.m_search); - auto q = p().subst_val(s.m_search); + LOG("Assignment: " << s.assignment()); + auto q = p().subst_val(s.assignment()); LOG("Substituted: " << p() << " := " << q); if (q.is_zero()) { if (is_positive()) @@ -88,7 +91,7 @@ namespace polysat { } bool eq_constraint::is_currently_false(solver& s) { - pdd r = p().subst_val(s.m_search); + pdd r = p().subst_val(s.assignment()); if (is_positive()) return r.is_never_zero(); if (is_negative()) @@ -98,7 +101,7 @@ namespace polysat { } bool eq_constraint::is_currently_true(solver& s) { - pdd r = p().subst_val(s.m_search); + pdd r = p().subst_val(s.assignment()); if (is_positive()) return r.is_zero(); if (is_negative()) @@ -112,11 +115,13 @@ namespace polysat { * Equality constraints */ - constraint* eq_constraint::eq_resolve(solver& s, pvar v) { + scoped_ptr eq_constraint::eq_resolve(solver& s, pvar v) { LOG("Resolve " << *this << " upon v" << v); if (s.m_conflict.size() != 1) return nullptr; - constraint* c = s.m_conflict[0]; + if (!s.m_conflict.clauses().empty()) + return nullptr; + constraint* c = s.m_conflict.units()[0]; SASSERT(c->is_currently_false(s)); // 'c == this' can happen if propagation was from decide() with only one value left // (e.g., if there's an unsatisfiable clause and we try all values). @@ -124,7 +129,7 @@ namespace polysat { if (c == this) return nullptr; SASSERT(is_currently_true(s)); // TODO: might not always hold (due to similar case as in comment above?) - if (c->is_eq()) { + if (c->is_eq() && c->is_positive()) { pdd a = c->to_eq().p(); pdd b = p(); pdd r = a; @@ -132,9 +137,7 @@ namespace polysat { return nullptr; p_dependency_ref d(s.m_dm.mk_join(c->dep(), dep()), s.m_dm); unsigned lvl = std::max(c->level(), level()); - constraint* lemma = constraint::eq(lvl, s.m_next_bvar++, pos_t, r, d); - lemma->assign_eh(true); - return lemma; + return s.m_constraints.eq(lvl, pos_t, r, d); } return nullptr; } @@ -144,7 +147,7 @@ namespace polysat { * Disequality constraints */ - constraint* eq_constraint::diseq_resolve(solver& s, pvar v) { + scoped_ptr eq_constraint::diseq_resolve(solver& s, pvar v) { NOT_IMPLEMENTED_YET(); return nullptr; } @@ -162,6 +165,7 @@ namespace polysat { return false; if (deg == 0) { + return false; UNREACHABLE(); // this case is not useful for conflict resolution (but it could be handled in principle) // i is empty or full, condition would be this constraint itself? return true; @@ -191,7 +195,7 @@ namespace polysat { */ // Concrete values of evaluable terms - auto e1s = e1.subst_val(s.m_search); + auto e1s = e1.subst_val(s.assignment()); auto e2s = m.zero(); SASSERT(e1s.is_val()); SASSERT(e2s.is_val()); diff --git a/src/math/polysat/eq_constraint.h b/src/math/polysat/eq_constraint.h index d7878a535..953aa330e 100644 --- a/src/math/polysat/eq_constraint.h +++ b/src/math/polysat/eq_constraint.h @@ -20,14 +20,14 @@ namespace polysat { class eq_constraint : public constraint { pdd m_poly; public: - eq_constraint(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref const& dep): - constraint(lvl, bvar, sign, dep, ckind_t::eq_t), m_poly(p) { + eq_constraint(constraint_manager& m, unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& dep): + constraint(m, lvl, sign, dep, ckind_t::eq_t), m_poly(p) { m_vars.append(p.free_vars()); } ~eq_constraint() override {} pdd const & p() const { return m_poly; } std::ostream& display(std::ostream& out) const override; - constraint* resolve(solver& s, pvar v) override; + scoped_ptr resolve(solver& s, pvar v) override; bool is_always_false() override; bool is_currently_false(solver& s) override; bool is_currently_true(solver& s) override; @@ -35,8 +35,8 @@ namespace polysat { bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, scoped_ptr& out_neg_cond) override; private: - constraint* eq_resolve(solver& s, pvar v); - constraint* diseq_resolve(solver& s, pvar v); + scoped_ptr eq_resolve(solver& s, pvar v); + scoped_ptr diseq_resolve(solver& s, pvar v); }; } diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index b35673d50..d171eb001 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -62,7 +62,7 @@ namespace polysat { return true; } - bool forbidden_intervals::explain(solver& s, ptr_vector const& conflict, pvar v, clause& out_lemma) { + bool forbidden_intervals::explain(solver& s, ptr_vector const& conflict, pvar v, scoped_clause& out_lemma) { // Extract forbidden intervals from conflicting constraints vector records; @@ -99,7 +99,16 @@ namespace polysat { // => the side conditions of that interval are enough to produce a conflict auto& full_record = records.back(); SASSERT(full_record.interval.is_full()); - out_lemma = std::move(full_record.neg_cond); + sat::literal_vector literals; + scoped_ptr_vector new_constraints; + literals.push_back(~sat::literal(full_record.src->bvar())); // TODO: only do this if it's not a base-level constraint! (from unit clauses, e.g., external constraints) + if (full_record.neg_cond) { + literals.push_back(sat::literal(full_record.neg_cond.get()->bvar())); + new_constraints.push_back(full_record.neg_cond.detach()); + } + unsigned lemma_lvl = full_record.src->level(); + p_dependency_ref lemma_dep(full_record.src->dep(), s.m_dm); + out_lemma = scoped_clause(clause::from_literals(lemma_lvl, lemma_dep, literals), std::move(new_constraints)); return true; } @@ -130,11 +139,22 @@ namespace polysat { // Create lemma // Idea: - // - If the side conditions hold, and + // - If the src constraints hold, and + // - if the side conditions hold, and // - the upper bound of each interval is contained in the next interval, // then the forbidden intervals cover the whole domain and we have a conflict. // We learn the negation of this conjunction. - scoped_ptr_vector literals; + + sat::literal_vector literals; + scoped_ptr_vector new_constraints; + // Add negation of src constraints as antecedents (may be resolved during backtracking) + for (unsigned const i : seq) { + // TODO: don't add base-level constraints! (from unit clauses, e.g., external constraints) + // (maybe extract that into a helper function on 'clause'... it could sort out base-level and other constraints; add the first to lemma_dep and the other to antecedents) + sat::literal src_lit{records[i].src->bvar()}; + literals.push_back(~src_lit); + } + // Add side conditions and interval constraints for (unsigned seq_i = seq.size(); seq_i-- > 0; ) { unsigned const i = seq[seq_i]; unsigned const next_i = seq[(seq_i+1) % seq.size()]; @@ -145,17 +165,20 @@ 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* c = constraint::ult(lemma_lvl, s.m_next_bvar++, neg_t, lhs, rhs, lemma_dep); + scoped_ptr c = s.m_constraints.ult(lemma_lvl, neg_t, lhs, rhs, s.mk_dep_ref(null_dependency)); LOG("constraint: " << *c); - literals.push_back(c); + literals.push_back(sat::literal(c->bvar())); + new_constraints.push_back(c.detach()); // 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? scoped_ptr& neg_cond = records[i].neg_cond; - if (neg_cond) - literals.push_back(neg_cond.detach()); + if (neg_cond) { + literals.push_back(sat::literal(neg_cond->bvar())); + new_constraints.push_back(neg_cond.detach()); + } } - - out_lemma = std::move(literals); + scoped_ptr cl = clause::from_literals(lemma_lvl, lemma_dep, literals); + out_lemma = scoped_clause(std::move(cl), std::move(new_constraints)); return true; } diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 7ccd72c63..6e733b47f 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -23,7 +23,7 @@ namespace polysat { class forbidden_intervals { public: - static bool explain(solver& s, ptr_vector const& conflict, pvar v, clause& out_lemma); + static bool explain(solver& s, ptr_vector const& conflict, pvar v, scoped_clause& out_lemma); }; } diff --git a/src/math/polysat/linear_solver.cpp b/src/math/polysat/linear_solver.cpp index b01ee45ba..024f1e64b 100644 --- a/src/math/polysat/linear_solver.cpp +++ b/src/math/polysat/linear_solver.cpp @@ -114,6 +114,7 @@ namespace polysat { m_trail.push_back(trail_i::set_bound_i); m_rows.push_back(std::make_pair(v, sz)); rational z(0), o(1); + SASSERT(!c.is_undef()); if (c.is_positive()) fp.set_bounds(v, z, z); else @@ -168,6 +169,7 @@ namespace polysat { } void linear_solver::activate_constraint(constraint& c) { + SASSERT(!c.is_undef()); switch (c.kind()) { case ckind_t::eq_t: assert_eq(c.to_eq()); @@ -199,7 +201,7 @@ namespace polysat { if (m_mono2var.find(m, m1)) return m1.var; m.vars = static_cast(m_alloc.allocate(var.size()*sizeof(unsigned))); - for (unsigned i = 0; i < var.size(); var.data()) + for (unsigned i = 0; i < var.size(); ++i) m.vars[i] = var[i]; m.var = fresh_var(sz); m_mono2var.insert(m); diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp new file mode 100644 index 000000000..551d35c52 --- /dev/null +++ b/src/math/polysat/search_state.cpp @@ -0,0 +1,47 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat search state + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ + +#include "math/polysat/search_state.h" + +namespace polysat { + + std::ostream& search_item::display(std::ostream& out) const { + switch (kind()) { + case search_item_k::assignment: + return out << "assignment(v" << var() << ")"; + case search_item_k::boolean: + return out << "boolean(" << lit() << ")"; + } + UNREACHABLE(); + return out; + } + + void search_state::push_assignment(pvar p, rational const& r) { + m_items.push_back(search_item::assignment(p)); + m_assignment.push_back({p, r}); + } + + void search_state::push_boolean(sat::literal lit) { + m_items.push_back(search_item::boolean(lit)); + } + + void search_state::pop() { + auto const& item = m_items.back(); + if (item.is_assignment()) { + m_assignment.pop_back(); + } + m_items.pop_back(); + } + +} diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h new file mode 100644 index 000000000..08bee4b22 --- /dev/null +++ b/src/math/polysat/search_state.h @@ -0,0 +1,73 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat search state + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once +#include "math/polysat/boolean.h" +#include "math/polysat/types.h" + +namespace polysat { + + typedef std::pair assignment_item_t; + typedef vector assignment_t; + + enum class search_item_k + { + assignment, + boolean, + }; + + class search_item { + search_item_k m_kind; + union { + pvar m_var; + sat::literal m_lit; + }; + + search_item(pvar var): m_kind(search_item_k::assignment), m_var(var) {} + search_item(sat::literal lit): m_kind(search_item_k::boolean), m_lit(lit) {} + public: + static search_item assignment(pvar var) { return search_item(var); } + static search_item boolean(sat::literal lit) { return search_item(lit); } + bool is_assignment() const { return m_kind == search_item_k::assignment; } + bool is_boolean() const { return m_kind == search_item_k::boolean; } + search_item_k kind() const { return m_kind; } + pvar var() const { SASSERT(is_assignment()); return m_var; } + sat::literal lit() const { SASSERT(is_boolean()); return m_lit; } + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, search_item const& s) { return s.display(out); } + + + class search_state { + + vector m_items; + assignment_t m_assignment; // First-order part of the search state + + public: + unsigned size() const { return m_items.size(); } + search_item const& back() const { return m_items.back(); } + search_item const& operator[](unsigned i) const { return m_items[i]; } + + assignment_t const& assignment() const { return m_assignment; } + + void push_assignment(pvar p, rational const& r); + void push_boolean(sat::literal lit); + void pop(); + + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, search_state const& s) { return s.display(out); } + +} diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index d0a36dcd1..eb6630ac7 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -71,7 +71,9 @@ namespace polysat { m_linear_solver(*this), m_bdd(1000), m_dm(m_value_manager, m_alloc), - m_free_vars(m_activity) { + m_free_vars(m_activity), + m_bvars(), + m_constraints(m_bvars) { } solver::~solver() {} @@ -105,7 +107,7 @@ namespace polysat { while (m_lim.inc()) { LOG_H1("Next solving loop iteration"); LOG("Free variables: " << m_free_vars); - LOG("Assignments: " << m_search); + LOG("Assignments: " << assignment()); LOG("Conflict: " << m_conflict); IF_LOGGING({ for (pvar v = 0; v < m_viable.size(); ++v) { @@ -153,82 +155,76 @@ namespace polysat { m_free_vars.del_var_eh(v); } - bool_var solver::new_constraint(constraint* c) { - SASSERT(c); - LOG("New constraint: " << *c); - m_linear_solver.new_constraint(*c); - m_constraints.push_back(c); - SASSERT(!get_bv2c(c->bvar())); - insert_bv2c(c->bvar(), c); - return c->bvar(); + scoped_ptr solver::mk_eq(pdd const& p, unsigned dep) { + return m_constraints.eq(m_level, pos_t, p, mk_dep_ref(dep)); } - bool_var solver::new_eq(pdd const& p, unsigned dep) { - p_dependency_ref d(mk_dep(dep), m_dm); - constraint* c = constraint::eq(m_level, m_next_bvar++, pos_t, p, d); - new_constraint(c); - return c->bvar(); - } - - bool_var solver::new_diseq(pdd const& p, unsigned dep) { - // if (p.is_val()) { - // if (!p.is_zero()) - // return; - // // set conflict. - // NOT_IMPLEMENTED_YET(); // TODO: not here, only when activated - // return; - // } + scoped_ptr solver::mk_diseq(pdd const& p, unsigned dep) { + if (p.is_val()) { + // if (!p.is_zero()) + // return nullptr; // TODO: probably better to create a dummy always-true constraint? + // // Use 0 != 0 for a constraint that is always false + // Use p != 0 as evaluable dummy constraint + return m_constraints.eq(m_level, neg_t, p, mk_dep_ref(dep)); + } unsigned sz = size(p.var()); auto slack = add_var(sz); auto q = p + var(slack); - add_eq(q, dep); + add_eq(q, dep); // TODO: 'dep' now refers to two constraints; this is not yet supported auto non_zero = sz2bits(sz).non_zero(); - p_dependency_ref d(mk_dep(dep), m_dm); - constraint* c = constraint::viable(m_level, m_next_bvar++, pos_t, slack, non_zero, d); - return new_constraint(c); + return m_constraints.viable(m_level, pos_t, slack, non_zero, mk_dep_ref(dep)); } - bool_var solver::new_ule(pdd const& p, pdd const& q, unsigned dep, csign_t sign) { - p_dependency_ref d(mk_dep(dep), m_dm); - return new_constraint(constraint::ule(m_level, m_next_bvar++, sign, p, q, d)); + scoped_ptr solver::mk_ule(pdd const& p, pdd const& q, unsigned dep) { + return m_constraints.ule(m_level, pos_t, p, q, mk_dep_ref(dep)); } - bool_var solver::new_sle(pdd const& p, pdd const& q, unsigned dep, csign_t sign) { - p_dependency_ref d(mk_dep(dep), m_dm); - return new_constraint(constraint::sle(m_level, m_next_bvar++, sign, p, q, d)); + scoped_ptr solver::mk_ult(pdd const& p, pdd const& q, unsigned dep) { + return m_constraints.ult(m_level, pos_t, p, q, mk_dep_ref(dep)); } - bool_var solver::new_ult(pdd const& p, pdd const& q, unsigned dep) { - return new_ule(q, p, dep, neg_t); + scoped_ptr solver::mk_sle(pdd const& p, pdd const& q, unsigned dep) { + return m_constraints.sle(m_level, pos_t, p, q, mk_dep_ref(dep)); } - bool_var solver::new_slt(pdd const& p, pdd const& q, unsigned dep) { - return new_sle(q, p, dep, neg_t); + scoped_ptr solver::mk_slt(pdd const& p, pdd const& q, unsigned dep) { + return m_constraints.slt(m_level, pos_t, p, q, mk_dep_ref(dep)); } - void solver::add_eq(pdd const& p, unsigned dep) { assign_eh(new_eq(p, dep), true); } - void solver::add_diseq(pdd const& p, unsigned dep) { assign_eh(new_diseq(p, dep), true); } - void solver::add_ule(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_ule(p, q, dep), true); } - void solver::add_ult(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_ult(p, q, dep), true); } - void solver::add_sle(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_sle(p, q, dep), true); } - void solver::add_slt(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_slt(p, q, dep), true); } + void solver::new_constraint(scoped_ptr&& sc, bool activate) { + SASSERT(sc); + SASSERT(activate || sc->dep()); // if we don't activate the constraint, we need the dependency to access it again later. + constraint* c = m_constraints.insert(std::move(sc)); + LOG("New constraint: " << *c); + m_original.push_back(c); + m_linear_solver.new_constraint(*c); + if (activate && !is_conflict()) + activate_constraint_base(c); + } - void solver::assign_eh(bool_var v, bool is_true) { - constraint* c = get_bv2c(v); + void solver::new_eq(pdd const& p, unsigned dep) { new_constraint(mk_eq(p, dep), false); } + void solver::new_diseq(pdd const& p, unsigned dep) { new_constraint(mk_diseq(p, dep), false); } + void solver::new_ule(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ule(p, q, dep), false); } + void solver::new_ult(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ult(p, q, dep), false); } + void solver::new_sle(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_sle(p, q, dep), false); } + void solver::new_slt(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_slt(p, q, dep), false); } + + void solver::add_eq(pdd const& p, unsigned dep) { new_constraint(mk_eq(p, dep), true); } + void solver::add_diseq(pdd const& p, unsigned dep) { new_constraint(mk_diseq(p, dep), true); } + void solver::add_ule(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ule(p, q, dep), true); } + void solver::add_ult(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ult(p, q, dep), true); } + void solver::add_sle(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_sle(p, q, dep), true); } + void solver::add_slt(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_slt(p, q, dep), true); } + + void solver::assign_eh(unsigned dep, bool is_true) { + constraint* c = m_constraints.lookup_external(dep); if (!c) { - LOG("WARN: there is no constraint for bool_var " << v); + LOG("WARN: there is no constraint for dependency " << dep); return; } if (is_conflict()) return; - SASSERT(c->is_undef()); - c->assign_eh(is_true); - LOG("Activate constraint: " << *c); - add_watch(*c); - m_assign_eh_history.push_back(v); - m_trail.push_back(trail_instr_t::assign_eh_i); - c->narrow(*this); - m_linear_solver.activate_constraint(*c); + activate_constraint_base(c); } @@ -238,10 +234,15 @@ namespace polysat { void solver::propagate() { push_qhead(); - while (can_propagate()) - propagate(m_search[m_qhead++].first); - + while (can_propagate()) { + auto const& item = m_search[m_qhead++]; + if (item.is_assignment()) + propagate(item.var()); + else + propagate(item.lit()); + } linear_propagate(); + SASSERT(wlist_invariant()); } void solver::linear_propagate() { @@ -252,7 +253,15 @@ namespace polysat { default: break; } - SASSERT(wlist_invariant()); + } + + void solver::propagate(sat::literal lit) { + LOG_H2("Propagate boolean literal " << lit); + constraint* c = m_constraints.lookup(lit.var()); + SASSERT(c); + SASSERT(!c->is_undef()); + SASSERT(c->is_positive() == !lit.sign()); + // c->narrow(*this); } void solver::propagate(pvar v) { @@ -284,7 +293,9 @@ namespace polysat { } void solver::pop_levels(unsigned num_levels) { - LOG("Pop " << num_levels << " levels; current level is " << m_level); + SASSERT(m_level >= num_levels); + unsigned const target_level = m_level - num_levels; + LOG("Pop " << num_levels << " levels (lvl " << m_level << " -> " << target_level << ")"); m_linear_solver.pop(num_levels); while (num_levels > 0) { switch (m_trail.back()) { @@ -303,44 +314,50 @@ namespace polysat { } case trail_instr_t::viable_i: { auto p = m_viable_trail.back(); + LOG_V("Undo viable_i"); m_viable[p.first] = p.second; m_viable_trail.pop_back(); break; } case trail_instr_t::assign_i: { - auto v = m_search.back().first; + auto v = m_search.back().var(); + LOG_V("Undo assign_i: v" << v); m_free_vars.unassign_var_eh(v); m_justification[v] = justification::unassigned(); - m_search.pop_back(); + m_search.pop(); + break; + } + 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); + m_bvars.unassign(lit); + m_search.pop(); break; } case trail_instr_t::just_i: { auto v = m_cjust_trail.back(); + LOG_V("Undo just_i"); m_cjust[v].pop_back(); m_cjust_trail.pop_back(); break; } - case trail_instr_t::assign_eh_i: { - auto bvar = m_assign_eh_history.back(); - constraint* c = get_bv2c(bvar); - erase_watch(*c); - c->unassign_eh(); - m_assign_eh_history.pop_back(); - break; - } default: UNREACHABLE(); } m_trail.pop_back(); } - pop_constraints(m_constraints); + pop_constraints(m_original); pop_constraints(m_redundant); + m_constraints.release_level(m_level + 1); + SASSERT(m_level == target_level); } - void solver::pop_constraints(scoped_ptr_vector& cs) { + void solver::pop_constraints(ptr_vector& cs) { VERIFY(invariant(cs)); while (!cs.empty() && cs.back()->level() > m_level) { - erase_watch(*cs.back()); + deactivate_constraint(*cs.back()); cs.pop_back(); } } @@ -354,7 +371,7 @@ namespace polysat { } void solver::add_watch(constraint &c, pvar v) { - LOG("watching v" << v << " of constraint " << c); + LOG("Watching v" << v << " in constraint " << c); m_watch[v].push_back(&c); } @@ -387,23 +404,21 @@ namespace polysat { } void solver::decide(pvar v) { + LOG("Decide v" << v); IF_LOGGING(log_viable(v)); rational val; switch (find_viable(v, val)) { case dd::find_t::empty: - LOG("Conflict: no value for pvar " << v); // NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing) // (fail here in debug mode so we notice if we miss some) DEBUG_CODE( UNREACHABLE(); ); set_conflict(v); break; case dd::find_t::singleton: - LOG("Propagation: pvar " << v << " := " << val << " (due to unique value)"); // NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search assign_core(v, val, justification::propagation(m_level)); break; case dd::find_t::multiple: - LOG("Decision: pvar " << v << " := " << val); push_level(); assign_core(v, val, justification::decision(m_level)); break; @@ -415,31 +430,50 @@ namespace polysat { ++m_stats.m_num_decisions; else ++m_stats.m_num_propagations; - LOG("pvar " << v << " := " << val << " by " << j); + LOG("v" << v << " := " << val << " by " << j); SASSERT(is_viable(v, val)); - SASSERT(std::all_of(m_search.begin(), m_search.end(), [v](auto p) { return p.first != v; })); + SASSERT(std::all_of(assignment().begin(), assignment().end(), [v](auto p) { return p.first != v; })); m_value[v] = val; - m_search.push_back(std::make_pair(v, val)); + m_search.push_assignment(v, val); m_trail.push_back(trail_instr_t::assign_i); m_justification[v] = j; m_linear_solver.set_value(v, val); } void solver::set_conflict(constraint& c) { - LOG("conflict: " << c); - SASSERT(m_conflict.empty()); + LOG("Conflict: " << c); + SASSERT(!is_conflict()); m_conflict.push_back(&c); } void solver::set_conflict(pvar v) { - SASSERT(m_conflict.empty()); + SASSERT(!is_conflict()); m_conflict.append(m_cjust[v]); - LOG("conflict for pvar " << v << ": " << m_conflict); if (m_cjust[v].empty()) m_conflict.push_back(nullptr); + LOG("Conflict for v" << v << ": " << m_conflict); + } + + void solver::set_marks(constraint const& 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) { + 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. @@ -460,128 +494,168 @@ namespace polysat { LOG_H2("Resolve conflict"); ++m_stats.m_num_conflicts; - SASSERT(!m_conflict.empty()); + SASSERT(is_conflict()); - if (m_conflict.size() == 1 && !m_conflict[0]) { + if (m_conflict.units().size() == 1 && !m_conflict.units()[0]) { report_unsat(); return; } pvar conflict_var = null_var; - scoped_ptr lemma; - reset_marks(); - for (constraint* c : m_conflict) - for (auto v : c->vars()) { - set_mark(v); - if (!has_viable(v)) { - SASSERT(conflict_var == null_var || conflict_var == v); // at most one variable can be empty - conflict_var = v; - } + scoped_clause lemma; + for (auto v : m_conflict.vars(m_constraints)) + if (!has_viable(v)) { + SASSERT(conflict_var == null_var || conflict_var == v); // at most one variable can be empty + conflict_var = v; } + reset_marks(); + m_bvars.reset_marks(); + set_marks(m_conflict); - if (conflict_var != null_var) { + if (m_conflict.clauses().empty() && conflict_var != null_var) { LOG_H2("Conflict due to empty viable set for pvar " << conflict_var); - clause new_lemma; - if (forbidden_intervals::explain(*this, m_conflict, conflict_var, new_lemma)) { - LOG_H3("Lemma from forbidden intervals (size: " << new_lemma.size() << ")"); - for (constraint* c : new_lemma) - LOG("Literal: " << *c); - SASSERT(new_lemma.size() > 0); - if (new_lemma.size() == 1) { - lemma = new_lemma.detach()[0]; - SASSERT(lemma); - lemma->assign_eh(true); - reset_marks(); - for (auto v : lemma->vars()) + scoped_clause new_lemma; + if (forbidden_intervals::explain(*this, m_conflict.units(), conflict_var, new_lemma)) { + SASSERT(new_lemma); + clause& cl = *new_lemma.get(); + LOG_H3("Lemma from forbidden intervals (size: " << cl.size() << ")"); + for (sat::literal lit : cl) { + LOG("Literal: " << lit); + constraint* c = m_constraints.lookup(lit.var()); + for (auto v : c->vars()) set_mark(v); - m_conflict.reset(); - m_conflict.push_back(lemma.get()); - // continue normally - } - else { - SASSERT(m_disjunctive_lemma.empty()); - reset_marks(); - for (constraint* c : new_lemma) { - m_disjunctive_lemma.push_back(c->bvar()); - insert_bv2c(c->bvar(), c); - for (auto v : c->vars()) - set_mark(v); - } - m_redundant_clauses.push_back(std::move(new_lemma)); - backtrack(m_search.size()-1, lemma); - SASSERT(pending_disjunctive_lemma()); - m_conflict.reset(); - return; } + SASSERT(cl.size() > 0); + lemma = std::move(new_lemma); + m_conflict.reset(); + m_conflict.push_back(lemma.get()); + reset_marks(); + m_bvars.reset_marks(); + set_marks(*lemma.get()); } } - + for (unsigned i = m_search.size(); i-- > 0; ) { - pvar v = m_search[i].first; - LOG_H2("Working on pvar " << v); - if (!is_marked(v)) - continue; - justification& j = m_justification[v]; - LOG("Justification: " << j); - if (j.level() <= base_level()) { - report_unsat(); - return; - } - if (j.is_decision()) { - learn_lemma(v, lemma.detach()); - revert_decision(v); - return; - } - SASSERT(j.is_propagation()); - scoped_ptr new_lemma = resolve(v); - if (!new_lemma) { - backtrack(i, lemma); - return; - } - if (new_lemma->is_always_false()) { - learn_lemma(v, new_lemma.get()); + auto const& item = m_search[i]; + if (item.is_assignment()) { + // Resolve over variable assignment + pvar v = item.var(); + LOG_H2("Working on pvar " << v); + if (!is_marked(v)) + continue; + justification& j = m_justification[v]; + LOG("Justification: " << j); + if (j.level() <= base_level()) { + report_unsat(); + return; + } + if (j.is_decision()) { + revert_decision(v, lemma); + return; + } + SASSERT(j.is_propagation()); + scoped_clause new_lemma = resolve(v); + if (!new_lemma) { + backtrack(i, lemma); + return; + } + if (new_lemma.is_always_false(*this)) { + clause* cl = new_lemma.get(); + learn_lemma(v, std::move(new_lemma)); + m_conflict.reset(); + m_conflict.push_back(cl); + report_unsat(); + return; + } + if (!new_lemma.is_currently_false(*this)) { + backtrack(i, lemma); + return; + } + lemma = std::move(new_lemma); + reset_marks(); + m_bvars.reset_marks(); + set_marks(*lemma.get()); m_conflict.reset(); - m_conflict.push_back(new_lemma.detach()); - report_unsat(); - return; + m_conflict.push_back(lemma.get()); } - if (!new_lemma->is_currently_false(*this)) { - backtrack(i, lemma); - return; + else { + // Resolve over boolean literal + SASSERT(item.is_boolean()); + sat::literal const lit = item.lit(); + LOG_H2("Working on boolean literal " << lit); + sat::bool_var const var = lit.var(); + if (!m_bvars.is_marked(var)) + continue; + if (m_bvars.level(var) <= base_level()) { + report_unsat(); + return; + } + if (m_bvars.is_decision(var)) { + revert_bool_decision(lit, lemma); + return; + } + SASSERT(m_bvars.is_propagation(var)); + clause* other = m_bvars.reason(var); + // TODO: boolean resolution + NOT_IMPLEMENTED_YET(); } - lemma = new_lemma.detach(); - reset_marks(); - for (auto w : lemma->vars()) - set_mark(w); - m_conflict.reset(); - m_conflict.push_back(lemma.get()); } report_unsat(); } - void solver::backtrack(unsigned i, scoped_ptr& lemma) { - add_lemma(lemma.detach()); + void solver::backtrack(unsigned i, scoped_clause& lemma) { do { - auto v = m_search[i].first; - if (!is_marked(v)) - continue; - justification& j = m_justification[v]; - if (j.level() <= base_level()) - break; - if (j.is_decision()) { - revert_decision(v); - return; + auto const& item = m_search[i]; + if (item.is_assignment()) { + // Backtrack over variable assignment + auto v = item.var(); + LOG_H2("Working on pvar " << v); + if (!is_marked(v)) + continue; + justification& j = m_justification[v]; + if (j.level() <= base_level()) + break; + if (j.is_decision()) { + revert_decision(v, lemma); + return; + } + // retrieve constraint used for propagation + // add variables to COI + SASSERT(j.is_propagation()); + for (auto* c : m_cjust[v]) { + for (auto w : c->vars()) + set_mark(w); + if (c->bvar() != sat::null_bool_var) + m_bvars.set_mark(c->bvar()); + m_conflict.units().push_back(c); + } } - // retrieve constraint used for propagation - // add variables to COI - SASSERT(j.is_propagation()); - for (auto* c : m_cjust[v]) { - for (auto w : c->vars()) - set_mark(w); - m_conflict.push_back(c); + else { + // Backtrack over boolean literal + SASSERT(item.is_boolean()); + sat::literal lit = item.lit(); + LOG_H2("Working on boolean literal " << lit); + sat::bool_var var = lit.var(); + SASSERT(m_bvars.is_assigned(var)); + if (!m_bvars.is_marked(var)) + continue; + // NOTE: currently, we should never reach this point (but check) + // UNREACHABLE(); + + if (m_bvars.level(var) <= base_level()) + break; + if (m_bvars.is_decision(var)) { + revert_bool_decision(lit, lemma); + return; + } + SASSERT(m_bvars.is_propagation(var)); + // Note: here, bvar being marked need not mean it's part of the reason (could come from a cjust) + clause* other = m_bvars.reason(var); + NOT_IMPLEMENTED_YET(); } } - while (i-- > 0); + while (i-- > 0); + // TODO: learn lemma report_unsat(); } @@ -593,10 +667,11 @@ namespace polysat { void solver::unsat_core(unsigned_vector& deps) { deps.reset(); p_dependency_ref conflict_dep(m_dm); - for (auto* c : m_conflict) { + for (auto* c : m_conflict.units()) if (c) conflict_dep = m_dm.mk_join(c->dep(), conflict_dep); - } + for (auto* c : m_conflict.clauses()) + conflict_dep = m_dm.mk_join(c->dep(), conflict_dep); m_dm.linearize(conflict_dep, deps); } @@ -607,13 +682,46 @@ namespace polysat { * We add 'p == 0' as a lemma. The lemma depends on the dependencies used * to derive p, and the level of the lemma is the maximal level of the dependencies. */ - void solver::learn_lemma(pvar v, constraint* c) { - if (!c) + void solver::learn_lemma(pvar v, scoped_clause&& lemma) { + if (!lemma) return; - LOG("Learning: " << *c); + LOG("Learning: " << lemma); SASSERT(m_conflict_level <= m_justification[v].level()); + if (lemma.is_owned_unit()) { + scoped_ptr c = lemma.detach_constraints()[0]; + SASSERT(lemma[0].var() == c->bvar()); + SASSERT(!lemma[0].sign()); // that case is handled incorrectly atm + learn_lemma_unit(v, std::move(c)); + } + else + learn_lemma_clause(v, std::move(lemma)); + } + + void solver::learn_lemma_unit(pvar v, scoped_ptr&& lemma) { + SASSERT(lemma); + constraint* c = lemma.get(); + add_lemma_unit(std::move(lemma)); + push_cjust(v, c); + activate_constraint_base(c); + } + + void solver::learn_lemma_clause(pvar v, scoped_clause&& lemma) { + SASSERT(lemma); + clause& cl = *lemma.get(); + add_lemma_clause(std::move(lemma)); + // Guess one of the new literals + constraint* c = nullptr; + while (true) { + unsigned next_idx = cl.next_guess(); + SASSERT(next_idx < cl.size()); // must succeed for at least one + sat::literal lit = cl[next_idx]; + c = m_constraints.lookup(lit.var()); + c->assign(!lit.sign()); + if (!c->is_currently_false(*this)) + break; + } + decide_bool(sat::literal(c->bvar()), &cl); push_cjust(v, c); - add_lemma(c); } /** @@ -627,7 +735,7 @@ namespace polysat { * In general form it can rely on factoring. * Root finding can further prune viable. */ - void solver::revert_decision(pvar v) { + void solver::revert_decision(pvar v, scoped_clause& reason) { rational val = m_value[v]; LOG_H3("Reverting decision: pvar " << v << " -> " << val); SASSERT(m_justification[v].is_decision()); @@ -636,12 +744,18 @@ namespace polysat { backjump(m_justification[v].level()-1); // Since decision "v -> val" caused a conflict, we may keep all // viability restrictions on v and additionally exclude val. - push_viable(v); - m_viable[v] = viable; + // TODO: viability restrictions on 'v' must have happened before decision on 'v'. Do we really need to save/restore m_viable here? + SASSERT(m_viable[v] == viable); // check this with assertion + SASSERT(m_cjust[v] == just); // check this with assertion + // push_viable(v); + // m_viable[v] = viable; + // for (unsigned i = m_cjust[v].size(); i < just.size(); ++i) + // push_cjust(v, just[i]); + add_non_viable(v, val); - for (unsigned i = m_cjust[v].size(); i < just.size(); ++i) - push_cjust(v, just[i]); - for (constraint* c : m_conflict) { + learn_lemma(v, std::move(reason)); + + for (constraint* c : m_conflict.units()) { // Add the conflict as justification for the exclusion of 'val' push_cjust(v, c); // NOTE: in general, narrow may change the conflict. @@ -649,6 +763,7 @@ namespace polysat { c->narrow(*this); } m_conflict.reset(); + narrow(v); if (m_justification[v].is_unassigned()) { m_free_vars.del_var_eh(v); @@ -656,6 +771,92 @@ namespace polysat { } } + void solver::revert_bool_decision(sat::literal lit, scoped_clause& reason) { + sat::bool_var const var = lit.var(); + LOG_H3("Reverting boolean decision: " << lit); + SASSERT(m_bvars.is_decision(var)); + backjump(m_bvars.level(var) - 1); + + bool contains_var = std::any_of(reason.begin(), reason.end(), [var](sat::literal reason_lit) { return reason_lit.var() == var; }); + bool contains_opp = std::any_of(reason.begin(), reason.end(), [lit](sat::literal reason_lit) { return reason_lit == ~lit; }); + SASSERT(contains_var && contains_opp); // TODO: hm... + clause* reason_cl = reason.get(); + add_lemma_clause(std::move(reason)); + propagate_bool(~lit, reason_cl); + + clause* lemma = m_bvars.lemma(var); + unsigned next_idx = lemma->next_guess(); + sat::literal next_lit = (*lemma)[next_idx]; + // If the guess is the last literal then do a propagation, otherwise a decision + if (next_idx == lemma->size() - 1) + propagate_bool(next_lit, lemma); + else + decide_bool(next_lit, lemma); + } + + void solver::decide_bool(sat::literal lit, clause* lemma) { + push_level(); + LOG_H2("Decide boolean literal " << lit << " @ " << m_level); + assign_bool_backtrackable(lit, nullptr, lemma); + } + + void solver::propagate_bool(sat::literal lit, clause* reason) { + LOG("Propagate boolean literal " << lit << " @ " << m_level << " by " << show_deref(reason)); + SASSERT(reason); + assign_bool_backtrackable(lit, reason, nullptr); + } + + /// Assign a boolean literal and put it on the search stack, + /// and activate the corresponding constraint. + void solver::assign_bool_backtrackable(sat::literal lit, clause* reason, clause* lemma) { + assign_bool_core(lit, reason, lemma); + + 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); + } + + /// Activate a constraint at the base level. + /// Used for external unit constraints and unit consequences. + void solver::activate_constraint_base(constraint* c) { + SASSERT(c); + assign_bool_core(sat::literal(c->bvar()), nullptr, nullptr); + activate_constraint(*c, true); + // c must be in m_original or m_redundant so it can be deactivated properly when popping the base level + SASSERT( + std::count(m_original.begin(), m_original.end(), c) + std::count(m_redundant.begin(), m_redundant.end(), c) == 1 + // std::any_of(m_original.begin(), m_original.end(), [c](constraint* d) { return c == d; }) + // || std::any_of(m_redundant.begin(), m_redundant.end(), [c](constraint* d) { return c == d; }) + ); + } + + /// Assign a boolean literal and activate the corresponding constraint + void solver::assign_bool_core(sat::literal lit, clause* reason, clause* lemma) { + LOG("Assigning boolean literal: " << lit); + m_bvars.assign(lit, m_level, reason, lemma); + } + + /// Activate constraint immediately + void solver::activate_constraint(constraint& c, bool is_true) { + LOG("Activating constraint: " << c); + SASSERT(m_bvars.value(c.bvar()) == to_lbool(is_true)); + c.assign(is_true); + add_watch(c); + c.narrow(*this); + m_linear_solver.activate_constraint(c); + } + + /// Deactivate constraint immediately + void solver::deactivate_constraint(constraint& c) { + LOG("Deactivating constraint: " << c); + erase_watch(c); + c.unassign(); + } + void solver::backjump(unsigned new_level) { LOG_H3("Backjumping to level " << new_level << " from level " << m_level); unsigned num_levels = m_level - new_level; @@ -666,15 +867,19 @@ namespace polysat { /** * Return residue of superposing p and q with respect to v. */ - constraint* solver::resolve(pvar v) { + scoped_clause solver::resolve(pvar v) { + scoped_clause result; SASSERT(!m_cjust[v].empty()); SASSERT(m_justification[v].is_propagation()); LOG("resolve pvar " << v); if (m_cjust[v].size() != 1) return nullptr; constraint* d = m_cjust[v].back(); - constraint* res = d->resolve(*this, v); + scoped_ptr res = d->resolve(*this, v); LOG("resolved: " << show_deref(res)); + if (res) { + res->assign(true); + } return res; } @@ -685,23 +890,40 @@ namespace polysat { } - void solver::add_lemma(constraint* c) { - if (!c) + // Add lemma to storage but do not activate it + void solver::add_lemma_unit(scoped_ptr&& lemma) { + if (!lemma) return; - LOG("Lemma: " << *c); - SASSERT(!c->is_undef()); - SASSERT(!get_bv2c(c->bvar())); - insert_bv2c(c->bvar(), c); - add_watch(*c); - m_redundant.push_back(c); - for (unsigned i = m_redundant.size() - 1; i-- > 0; ) { - auto* c1 = m_redundant[i + 1]; - auto* c2 = m_redundant[i]; + LOG("Lemma: " << show_deref(lemma)); + constraint* c = m_constraints.insert(lemma.detach()); + insert_constraint(m_redundant, c); + } + + // Add lemma to storage but do not activate it + void solver::add_lemma_clause(scoped_clause&& lemma) { + if (!lemma) + return; + LOG("Lemma: " << lemma); + ptr_vector constraints = lemma.detach_constraints(); + for (constraint* c : constraints) + m_constraints.insert(c); + + clause* clause = lemma.detach(); + m_redundant_clauses.push_back(clause); + + // TODO: also update clause->m_next_guess (probably needs to sort the literals too) + } + + void solver::insert_constraint(ptr_vector& cs, constraint* c) { + cs.push_back(c); + for (unsigned i = cs.size() - 1; i-- > 0; ) { + auto* c1 = cs[i + 1]; + auto* c2 = cs[i]; if (c1->level() >= c2->level()) break; - m_redundant.swap(i, i + 1); + std::swap(cs[i], cs[i+1]); } - SASSERT(invariant(m_redundant)); + SASSERT(invariant(cs)); } void solver::reset_marks() { @@ -735,16 +957,18 @@ namespace polysat { } std::ostream& solver::display(std::ostream& out) const { - for (auto p : m_search) { + for (auto p : assignment()) { auto v = p.first; auto lvl = m_justification[v].level(); out << "v" << v << " := " << p.second << " @" << lvl << "\n"; out << m_viable[v] << "\n"; } - for (auto* c : m_constraints) - out << *c << "\n"; + out << "Original:\n"; + for (auto* c : m_original) + out << "\t" << *c << "\n"; + out << "Redundant:\n"; for (auto* c : m_redundant) - out << *c << "\n"; + out << "\t" << *c << "\n"; return out; } @@ -755,7 +979,7 @@ namespace polysat { } bool solver::invariant() { - invariant(m_constraints); + invariant(m_original); invariant(m_redundant); return true; } @@ -763,7 +987,7 @@ namespace polysat { /** * constraints are sorted by levels so they can be removed when levels are popped. */ - bool solver::invariant(scoped_ptr_vector const& cs) { + bool solver::invariant(ptr_vector const& cs) { unsigned sz = cs.size(); for (unsigned i = 0; i + 1 < sz; ++i) VERIFY(cs[i]->level() <= cs[i + 1]->level()); @@ -775,9 +999,11 @@ namespace polysat { */ bool solver::wlist_invariant() { constraints cs; - cs.append(m_constraints.size(), m_constraints.data()); + 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; int64_t num_watches = 0; for (auto const& wlist : m_watch) { auto n = std::count(wlist.begin(), wlist.end(), c); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 3bbc4692d..580fba0fa 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -19,13 +19,16 @@ Author: #include #include "util/statistics.h" +#include "math/polysat/boolean.h" #include "math/polysat/constraint.h" #include "math/polysat/eq_constraint.h" #include "math/polysat/var_constraint.h" #include "math/polysat/ule_constraint.h" #include "math/polysat/justification.h" #include "math/polysat/linear_solver.h" +#include "math/polysat/search_state.h" #include "math/polysat/trail.h" +#include "math/polysat/log.h" namespace polysat { @@ -43,6 +46,7 @@ namespace polysat { friend class eq_constraint; friend class var_constraint; friend class ule_constraint; + friend class clause; friend class forbidden_intervals; friend class linear_solver; @@ -56,28 +60,24 @@ namespace polysat { dep_value_manager m_value_manager; small_object_allocator m_alloc; poly_dep_manager m_dm; - constraints m_conflict; - constraints m_stash_just; + constraints_and_clauses m_conflict; + // constraints m_stash_just; var_queue m_free_vars; stats m_stats; uint64_t m_max_conflicts { std::numeric_limits::max() }; uint64_t m_max_decisions { std::numeric_limits::max() }; - // Per constraint state - scoped_ptr_vector m_constraints; - scoped_ptr_vector m_redundant; - vector m_redundant_clauses; - - bool_var_vector m_disjunctive_lemma; - bool_var_vector m_assign_eh_history; - // Map boolean variables to constraints - bool_var m_next_bvar = 2; // TODO: later, bool vars come from external supply - ptr_vector m_bv2constraint; - void insert_bv2c(bool_var bv, constraint* c) { m_bv2constraint.setx(bv, c, nullptr); } - void erase_bv2c(bool_var bv) { m_bv2constraint[bv] = nullptr; } - constraint* get_bv2c(bool_var bv) const { return m_bv2constraint.get(bv, nullptr); } + bool_var_manager m_bvars; + + // Per constraint state + constraint_manager m_constraints; + ptr_vector m_original; + ptr_vector m_redundant; + scoped_ptr_vector m_redundant_clauses; + + svector m_disjunctive_lemma; // Per variable information vector m_viable; // set of viable values. @@ -89,16 +89,25 @@ namespace polysat { vector m_vars; unsigned_vector m_size; // store size of variables. - // search state that lists assigned variables - vector> m_search; + search_state m_search; + assignment_t const& assignment() const { return m_search.assignment(); } - unsigned m_qhead { 0 }; + // (old, remove later) + // using bool_clauses = ptr_vector; + // vector m_bool_value; // value of boolean literal (indexed by literal) + // vector m_bool_watch; // watch list into clauses (indexed by literal) + // // scoped_ptr_vector m_bool_clauses; // NOTE: as of now, external clauses will only be units! So this is not needed. + // svector m_bool_units; // externally asserted unit clauses, via assign_eh + // scoped_ptr_vector m_bool_redundant; // learned clause storage + + unsigned m_qhead { 0 }; // next item to propagate (index into m_search) unsigned m_level { 0 }; svector m_trail; unsigned_vector m_qhead_trail; vector> m_viable_trail; unsigned_vector m_cjust_trail; + ptr_vector m_activate_trail; unsigned_vector m_base_levels; // External clients can push/pop scope. @@ -122,6 +131,7 @@ namespace polysat { void push_cjust(pvar v, constraint* c) { if (m_cjust[v].contains(c)) // TODO: better check (flag on constraint?) return; + LOG_V("cjust[v" << v << "] += " << *c); m_cjust[v].push_back(c); m_trail.push_back(trail_instr_t::just_i); m_cjust_trail.push_back(v); @@ -177,15 +187,24 @@ namespace polysat { void push_level(); void pop_levels(unsigned num_levels); - void pop_constraints(scoped_ptr_vector& cs); + void pop_constraints(ptr_vector& cs); + + void assign_bool_backtrackable(sat::literal lit, clause* reason, clause* lemma); + void activate_constraint_base(constraint* 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 decide_bool(sat::literal lit, clause* lemma); + void propagate_bool(sat::literal lit, clause* reason); void assign_core(pvar v, rational const& val, justification const& j); - bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); } bool should_search(); + 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); @@ -202,9 +221,13 @@ namespace polysat { bool is_marked(pvar v) const { return m_clock == m_marks[v]; } void set_mark(pvar v) { m_marks[v] = m_clock; } + void set_marks(constraints_and_clauses const& cc); + void set_marks(constraint const& c); + void set_marks(clause const& cl); + unsigned m_conflict_level { 0 }; - constraint* resolve(pvar v); + scoped_clause resolve(pvar v); bool can_decide() const { return !m_free_vars.empty(); } void decide(); @@ -214,23 +237,36 @@ namespace polysat { void linear_propagate(); p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); } + p_dependency_ref mk_dep_ref(unsigned dep) { return p_dependency_ref(mk_dep(dep), m_dm); } bool is_conflict() const { return !m_conflict.empty(); } bool at_base_level() const; unsigned base_level() const; - void resolve_conflict(); - void backtrack(unsigned i, scoped_ptr& lemma); + void resolve_conflict(); + void resolve_conflict_clause(scoped_clause& lemma); + void backtrack(unsigned i, scoped_clause& lemma); void report_unsat(); - void revert_decision(pvar v); - void learn_lemma(pvar v, constraint* c); + void revert_decision(pvar v, scoped_clause& reason); + void revert_bool_decision(sat::literal lit, scoped_clause& reason); + void learn_lemma(pvar v, scoped_clause&& lemma); + void learn_lemma_unit(pvar v, scoped_ptr&& lemma); + void learn_lemma_clause(pvar v, scoped_clause&& lemma); void backjump(unsigned new_level); - void add_lemma(constraint* c); + void add_lemma_unit(scoped_ptr&& lemma); + void add_lemma_clause(scoped_clause&& lemma); - bool_var new_constraint(constraint* c); + scoped_ptr mk_eq(pdd const& p, unsigned dep); + scoped_ptr mk_diseq(pdd const& p, unsigned dep); + scoped_ptr mk_ule(pdd const& p, pdd const& q, unsigned dep); + scoped_ptr mk_ult(pdd const& p, pdd const& q, unsigned dep); + scoped_ptr mk_sle(pdd const& p, pdd const& q, unsigned dep); + scoped_ptr mk_slt(pdd const& p, pdd const& q, unsigned dep); + void new_constraint(scoped_ptr&& c, bool activate); + static void insert_constraint(ptr_vector& cs, constraint* c); bool invariant(); - bool invariant(scoped_ptr_vector const& cs); + static bool invariant(ptr_vector const& cs); bool wlist_invariant(); public: @@ -258,7 +294,7 @@ namespace polysat { * Returns the disjunctive lemma that should be learned, * or an empty vector if check_sat() terminated for a different reason. */ - bool_var_vector get_lemma() { return m_disjunctive_lemma; } + svector get_lemma() { return m_disjunctive_lemma; } bool pending_disjunctive_lemma() { return !m_disjunctive_lemma.empty(); } /** @@ -285,12 +321,12 @@ namespace polysat { * Create polynomial constraints (but do not activate them). * Each constraint is tracked by a dependency. */ - bool_var new_eq(pdd const& p, unsigned dep = null_dependency); - bool_var new_diseq(pdd const& p, unsigned dep = null_dependency); - bool_var new_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency, csign_t sign = pos_t); - bool_var new_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency); - bool_var new_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency, csign_t sign = pos_t); - bool_var new_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency); + void new_eq(pdd const& p, unsigned dep); + void new_diseq(pdd const& p, unsigned dep); + void new_ule(pdd const& p, pdd const& q, unsigned dep); + void new_ult(pdd const& p, pdd const& q, unsigned dep); + void new_sle(pdd const& p, pdd const& q, unsigned dep); + void new_slt(pdd const& p, pdd const& q, unsigned dep); /** Create and activate polynomial constraints. */ void add_eq(pdd const& p, unsigned dep = null_dependency); @@ -304,7 +340,7 @@ namespace polysat { * Activate the constraint corresponding to the given boolean variable. * Note: to deactivate, use push/pop. */ - void assign_eh(bool_var v, bool is_true); + void assign_eh(unsigned dep, bool is_true); /** * main state transitions. diff --git a/src/math/polysat/trail.h b/src/math/polysat/trail.h index 392603a90..bac489b6e 100644 --- a/src/math/polysat/trail.h +++ b/src/math/polysat/trail.h @@ -23,7 +23,7 @@ namespace polysat { viable_i, assign_i, just_i, - assign_eh_i, + assign_bool_i, }; diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h index 392490964..f799ff70c 100644 --- a/src/math/polysat/types.h +++ b/src/math/polysat/types.h @@ -51,7 +51,4 @@ namespace polysat { typedef obj_ref p_dependency_ref; typedef ref_vector p_dependency_refv; - typedef int bool_var; // see smt_types.h - typedef svector bool_var_vector; // see smt_types.h - } diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index d0ed1d73d..e5022fa04 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -19,19 +19,22 @@ Author: namespace polysat { std::ostream& ule_constraint::display(std::ostream& out) const { - return out << m_lhs << (sign() == pos_t ? " <=u " : " >u ") << m_rhs << " [" << m_status << "]"; + out << m_lhs << (sign() == pos_t ? " <=u " : " >u ") << m_rhs << " @" << level(); + if (is_undef()) + out << " [inactive]"; + return out; } - constraint* ule_constraint::resolve(solver& s, pvar v) { + scoped_ptr ule_constraint::resolve(solver& s, pvar v) { return nullptr; } void ule_constraint::narrow(solver& s) { SASSERT(!is_undef()); - LOG("Assignment: " << s.m_search); - auto p = lhs().subst_val(s.m_search); + LOG("Assignment: " << s.assignment()); + auto p = lhs().subst_val(s.assignment()); LOG("Substituted LHS: " << lhs() << " := " << p); - auto q = rhs().subst_val(s.m_search); + auto q = rhs().subst_val(s.assignment()); LOG("Substituted RHS: " << rhs() << " := " << q); if (is_always_false(p, q)) { @@ -103,14 +106,14 @@ namespace polysat { } bool ule_constraint::is_currently_false(solver& s) { - auto p = lhs().subst_val(s.m_search); - auto q = rhs().subst_val(s.m_search); + auto p = lhs().subst_val(s.assignment()); + auto q = rhs().subst_val(s.assignment()); return is_always_false(p, q); } bool ule_constraint::is_currently_true(solver& s) { - auto p = lhs().subst_val(s.m_search); - auto q = rhs().subst_val(s.m_search); + auto p = lhs().subst_val(s.assignment()); + auto q = rhs().subst_val(s.assignment()); VERIFY(!is_undef()); if (is_positive()) return p.is_val() && q.is_val() && p.val() <= q.val(); @@ -129,6 +132,7 @@ namespace polysat { return false; if (deg1 == 0 && deg2 == 0) { + return false; UNREACHABLE(); // this case is not useful for conflict resolution (but it could be handled in principle) // i is empty or full, condition would be this constraint itself? return true; @@ -183,8 +187,8 @@ namespace polysat { SASSERT(!y_coeff.is_zero()); // Concrete values of evaluable terms - auto e1s = e1.subst_val(s.m_search); - auto e2s = e2.subst_val(s.m_search); + auto e1s = e1.subst_val(s.assignment()); + auto e2s = e2.subst_val(s.assignment()); SASSERT(e1s.is_val()); SASSERT(e2s.is_val()); @@ -243,7 +247,7 @@ namespace polysat { out_neg_cond = nullptr; } else - out_neg_cond = constraint::eq(level(), s.m_next_bvar++, is_trivial ? neg_t : pos_t, condition_body, m_dep); + out_neg_cond = s.m_constraints.eq(level(), is_trivial ? neg_t : pos_t, condition_body, s.mk_dep_ref(null_dependency)); if (is_trivial) { if (is_positive()) diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index bf9de43da..545421da4 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -21,8 +21,8 @@ namespace polysat { pdd m_lhs; pdd m_rhs; public: - ule_constraint(unsigned lvl, bool_var bvar, csign_t sign, pdd const& l, pdd const& r, p_dependency_ref const& dep): - constraint(lvl, bvar, sign, dep, ckind_t::ule_t), m_lhs(l), m_rhs(r) { + ule_constraint(constraint_manager& m, unsigned lvl, csign_t sign, pdd const& l, pdd const& r, p_dependency_ref const& dep): + constraint(m, lvl, sign, dep, ckind_t::ule_t), m_lhs(l), m_rhs(r) { m_vars.append(l.free_vars()); for (auto v : r.free_vars()) if (!m_vars.contains(v)) @@ -32,7 +32,7 @@ namespace polysat { pdd const& lhs() const { return m_lhs; } pdd const& rhs() const { return m_rhs; } std::ostream& display(std::ostream& out) const override; - constraint* resolve(solver& s, pvar v) override; + scoped_ptr resolve(solver& s, pvar v) override; bool is_always_false(pdd const& lhs, pdd const& rhs); bool is_always_false() override; bool is_currently_false(solver& s) override; diff --git a/src/math/polysat/var_constraint.cpp b/src/math/polysat/var_constraint.cpp index 2c788f553..dd7b03c98 100644 --- a/src/math/polysat/var_constraint.cpp +++ b/src/math/polysat/var_constraint.cpp @@ -21,7 +21,7 @@ namespace polysat { return out << "v" << m_var << ": " << m_viable << "\n"; } - constraint* var_constraint::resolve(solver& s, pvar v) { + scoped_ptr var_constraint::resolve(solver& s, pvar v) { UNREACHABLE(); return nullptr; } diff --git a/src/math/polysat/var_constraint.h b/src/math/polysat/var_constraint.h index 9d2a0380e..7e07d82e4 100644 --- a/src/math/polysat/var_constraint.h +++ b/src/math/polysat/var_constraint.h @@ -29,11 +29,11 @@ namespace polysat { pvar m_var; bdd m_viable; public: - var_constraint(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const & b, p_dependency_ref const& dep): - constraint(lvl, bvar, sign, dep, ckind_t::bit_t), m_var(v), m_viable(b) {} + var_constraint(constraint_manager& m, unsigned lvl, csign_t sign, pvar v, bdd const & b, p_dependency_ref const& dep): + constraint(m, lvl, sign, dep, ckind_t::bit_t), m_var(v), m_viable(b) {} ~var_constraint() override {} std::ostream& display(std::ostream& out) const override; - constraint* resolve(solver& s, pvar v) override; + scoped_ptr resolve(solver& s, pvar v) override; void narrow(solver& s) override; bool is_always_false() override; bool is_currently_false(solver& s) override; diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 347987c35..164c3e20e 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -12,7 +12,9 @@ namespace polysat { }; struct scoped_solver : public solver_scope, public solver { - scoped_solver(std::string name): solver(lim), m_name(name) {} + scoped_solver(std::string name): solver(lim), m_name(name) { + std::cout << "\nSTART: " << m_name << "\n"; + } std::string m_name; lbool m_last_result = l_undef; diff --git a/src/util/dependency.h b/src/util/dependency.h index 84a7084e1..0a63dfc37 100644 --- a/src/util/dependency.h +++ b/src/util/dependency.h @@ -44,6 +44,7 @@ public: public: unsigned get_ref_count() const { return m_ref_count; } bool is_leaf() const { return m_leaf == 1; } + value const& leaf_value() const { SASSERT(is_leaf()); return static_cast(this)->m_value; } }; private: diff --git a/src/util/sat_literal.h b/src/util/sat_literal.h index f8be2eb3f..1e587644e 100644 --- a/src/util/sat_literal.h +++ b/src/util/sat_literal.h @@ -17,6 +17,7 @@ Author: #pragma once #include "util/lbool.h" +#include "util/approx_set.h" #include "util/vector.h" #include "util/uint_set.h" @@ -93,6 +94,8 @@ namespace sat { inline bool operator==(literal const & l1, literal const & l2) { return l1.m_val == l2.m_val; } inline bool operator!=(literal const & l1, literal const & l2) { return l1.m_val != l2.m_val; } + inline std::ostream & operator<<(std::ostream & out, sat::literal l) { if (l == sat::null_literal) out << "null"; else out << (l.sign() ? "-" : "") << l.var(); return out; } + typedef svector literal_vector; typedef std::pair literal_pair; @@ -160,7 +163,7 @@ namespace sat { struct dimacs_lit { literal m_lit; - dimacs_lit(literal l):m_lit(l) {} + explicit dimacs_lit(literal l):m_lit(l) {} }; inline std::ostream & operator<<(std::ostream & out, dimacs_lit const & dl) { @@ -189,6 +192,3 @@ namespace sat { } }; - -inline std::ostream & operator<<(std::ostream & out, sat::literal l) { if (l == sat::null_literal) out << "null"; else out << (l.sign() ? "-" : "") << l.var(); return out; } - diff --git a/src/util/util.h b/src/util/util.h index 3470f59c0..8d3682943 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -269,6 +269,11 @@ public: return *this; } + scoped_ptr& operator=(scoped_ptr&& other) { + *this = other.detach(); + return *this; + }; + T * detach() { T* tmp = m_ptr; m_ptr = nullptr;