From 2df104d9f0b457c528f91b880d4e0d8f4bb7f387 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Apr 2021 17:26:54 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/math/polysat/polysat.cpp | 75 +++++++++++++++++++++--------------- src/math/polysat/polysat.h | 53 ++++++++++++++++++++----- src/util/dependency.h | 68 ++++++++++++++++++++------------ 3 files changed, 130 insertions(+), 66 deletions(-) diff --git a/src/math/polysat/polysat.cpp b/src/math/polysat/polysat.cpp index 7c29e47d8..ed4b62025 100644 --- a/src/math/polysat/polysat.cpp +++ b/src/math/polysat/polysat.cpp @@ -45,6 +45,18 @@ namespace polysat { return !b.is_false(); } + void solver::add_non_viable(unsigned var, rational const& val) { + bdd value = m_bdd.mk_true(); + for (unsigned k = size(var); k-- > 0; ) + value &= val.get_bit(k) ? m_bdd.mk_var(k) : m_bdd.mk_nvar(k); + m_viable[var] &= !value; + } + + lbool solver::find_viable(unsigned var, rational & val) { + return l_false; + } + + struct solver::t_del_var : public trail { solver& s; t_del_var(solver& s): s(s) {} @@ -55,6 +67,8 @@ namespace polysat { solver::solver(trail_stack& s): m_trail(s), m_bdd(1000), + m_dep_manager(m_value_manager, m_alloc), + m_lemma_dep(nullptr, m_dep_manager), m_free_vars(m_activity) { } @@ -102,7 +116,8 @@ namespace polysat { } void solver::add_eq(pdd const& p, unsigned dep) { - constraint* c = constraint::eq(m_level, p, m_dep_manager.mk_leaf(dep)); + p_dependency_ref d(m_dep_manager.mk_leaf(dep), m_dep_manager); + constraint* c = constraint::eq(m_level, p, d); m_constraints.push_back(c); add_watch(*c); } @@ -135,7 +150,7 @@ namespace polysat { void solver::assign(unsigned var, unsigned index, bool value, unsigned dep) { m_viable[var] &= value ? m_bdd.mk_var(index) : m_bdd.mk_nvar(index); - m_trail.push(vector_value_trail(m_vdeps, var)); + m_trail.push(vector_value_trail(m_vdeps, var)); m_vdeps[var] = m_dep_manager.mk_join(m_vdeps[var], m_dep_manager.mk_leaf(dep)); if (m_viable[var].is_false()) { // TBD: set conflict @@ -357,8 +372,7 @@ namespace polysat { m_conflict = nullptr; pdd p = c.p(); m_lemma_level = c.level(); - m_lemma_deps.reset(); - m_lemma_deps.push_back(c.dep()); + m_lemma_dep = c.dep(); unsigned new_lemma_level = 0; reset_marks(); for (auto v : c.vars()) @@ -442,29 +456,34 @@ namespace polysat { auto v = m_search[i]; SASSERT(m_justification[v].is_decision()); SASSERT(m_lemma_level <= m_justification[v].level()); - // - // TBD: convert m_lemma_deps into deps. - // the scope of the new constraint should be confined to - // m_lemma_level so could be below the current user scope. - // What to do in this case is TBD. - // - unsigned level = m_lemma_level; - u_dependency* deps = nullptr; - constraint* c = constraint::eq(level, p, deps); + constraint* c = constraint::eq(m_lemma_level, p, m_lemma_dep); m_cjust[v].push_back(c); add_lemma(c); - // - // TBD: remove current value from viable - // m_values[v] - // - // 1. undo levels until i - // 2. find a new decision if there is one, - // propagate if decision is singular, - // otherwise if there are no viable decisions, backjump - // and set a new conflict. - // - } + add_non_viable(v, m_value[v]); + // TBD conditions for when backjumping applies to be clarified. + unsigned new_level = m_justification[v].level(); + backjump(new_level); + // + // find a new decision if there is one, + // propagate if decision is singular, + // otherwise if there are no viable decisions, backjump + // and set a new conflict. + // + rational value; + switch (find_viable(v, value)) { + case l_true: + // unit propagation + break; + case l_undef: + // branch + break; + case l_false: + // no viable. + break; + } + } + void solver::backjump(unsigned new_level) { unsigned num_levels = m_level - new_level; SASSERT(num_levels > 0); @@ -490,10 +509,6 @@ namespace polysat { /** * Return residue of superposing p and q with respect to v. - * - * TBD: should also collect dependencies (deps) - * and maximal level of constraints so learned lemma - * is given the appropriate level. */ pdd solver::resolve(unsigned v, pdd const& p, unsigned& resolve_level) { resolve_level = 0; @@ -507,7 +522,7 @@ namespace polysat { // add parity condition to presere falsification degree = r.degree(v); resolve_level = std::max(resolve_level, c->level()); - m_lemma_deps.push_back(c->dep()); + m_lemma_dep = m_dep_manager.mk_join(m_lemma_dep.get(), c->dep()); } } } @@ -538,14 +553,12 @@ namespace polysat { void solver::push() { push_level(); - m_dep_manager.push_scope(); m_scopes.push_back(m_level); } void solver::pop(unsigned num_scopes) { unsigned base_level = m_scopes[m_scopes.size() - num_scopes]; pop_levels(m_level - base_level - 1); - m_dep_manager.pop_scope(num_scopes); } bool solver::at_base_level() const { diff --git a/src/math/polysat/polysat.h b/src/math/polysat/polysat.h index 07fad7642..ec714eaee 100644 --- a/src/math/polysat/polysat.h +++ b/src/math/polysat/polysat.h @@ -30,6 +30,23 @@ namespace polysat { typedef dd::pdd pdd; typedef dd::bdd bdd; + struct dep_value_manager { + void inc_ref(unsigned) {} + void dec_ref(unsigned) {} + }; + + struct dep_config { + typedef dep_value_manager value_manager; + typedef unsigned value; + typedef small_object_allocator allocator; + static const bool ref_count = false; + }; + + typedef dependency_manager poly_dep_manager; + typedef poly_dep_manager::dependency p_dependency; + + typedef obj_ref p_dependency_ref; + enum ckind_t { eq_t, ule_t, sle_t }; class constraint { @@ -37,20 +54,20 @@ namespace polysat { ckind_t m_kind; pdd m_poly; pdd m_other; - u_dependency* m_dep; + p_dependency_ref m_dep; unsigned_vector m_vars; - constraint(unsigned lvl, pdd const& p, pdd const& q, u_dependency* dep, ckind_t k): + constraint(unsigned lvl, pdd const& p, pdd const& q, p_dependency_ref& dep, ckind_t k): m_level(lvl), m_kind(k), m_poly(p), m_other(q), m_dep(dep) { m_vars.append(p.free_vars()); if (q != p) for (auto v : q.free_vars()) - m_vars.insert(v); - } + m_vars.insert(v); + } public: - static constraint* eq(unsigned lvl, pdd const& p, u_dependency* d) { + static constraint* eq(unsigned lvl, pdd const& p, p_dependency_ref& d) { return alloc(constraint, lvl, p, p, d, ckind_t::eq_t); } - static constraint* ule(unsigned lvl, pdd const& p, pdd const& q, u_dependency* d) { + static constraint* ule(unsigned lvl, pdd const& p, pdd const& q, p_dependency_ref& d) { return alloc(constraint, lvl, p, q, d, ckind_t::ule_t); } ckind_t kind() const { return m_kind; } @@ -58,7 +75,7 @@ namespace polysat { pdd const & lhs() const { return m_poly; } pdd const & rhs() const { return m_other; } std::ostream& display(std::ostream& out) const; - u_dependency* dep() const { return m_dep; } + p_dependency* dep() const { return m_dep; } unsigned_vector& vars() { return m_vars; } unsigned level() const { return m_level; } }; @@ -97,7 +114,10 @@ namespace polysat { trail_stack& m_trail; scoped_ptr_vector m_pdd; dd::bdd_manager m_bdd; - u_dependency_manager m_dep_manager; + dep_value_manager m_value_manager; + small_object_allocator m_alloc; + poly_dep_manager m_dep_manager; + p_dependency_ref m_lemma_dep; var_queue m_free_vars; // Per constraint state @@ -106,7 +126,7 @@ namespace polysat { // Per variable information vector m_viable; // set of viable values. - ptr_vector m_vdeps; // dependencies for viable values + ptr_vector m_vdeps; // dependencies for viable values vector m_value; // assigned value vector m_justification; // justification for variable assignment vector m_cjust; // constraints used for justification @@ -132,6 +152,20 @@ namespace polysat { */ bool is_viable(unsigned var, rational const& val); + /** + * register that val is non-viable for var. + */ + void add_non_viable(unsigned var, rational const& val); + + + /** + * Find a next viable value for varible. + * l_false - there are no viable values. + * l_true - there is only one viable value left. + * l_undef - there are multiple viable values, return a guess + */ + lbool find_viable(unsigned var, rational & val); + /** * undo trail operations for backtracking. * Each struct is a subclass of trail and implements undo(). @@ -169,7 +203,6 @@ namespace polysat { void set_mark(unsigned v) { m_marks[v] = m_clock; } unsigned m_lemma_level { 0 }; - ptr_vector m_lemma_deps; pdd isolate(unsigned v); pdd resolve(unsigned v, pdd const& p, unsigned& resolve_level); diff --git a/src/util/dependency.h b/src/util/dependency.h index 7ccba716a..84a7084e1 100644 --- a/src/util/dependency.h +++ b/src/util/dependency.h @@ -107,11 +107,8 @@ private: } void unmark_todo() { - typename ptr_vector::iterator it = m_todo.begin(); - typename ptr_vector::iterator end = m_todo.end(); - for (; it != end; ++it) { - (*it)->unmark(); - } + for (auto* d : m_todo) + d->unmark(); m_todo.reset(); } @@ -193,30 +190,47 @@ public: return false; } - void linearize(dependency * d, vector & vs) { - if (d) { - m_todo.reset(); - d->mark(); - m_todo.push_back(d); - unsigned qhead = 0; - while (qhead < m_todo.size()) { - d = m_todo[qhead]; - qhead++; - if (d->is_leaf()) { - vs.push_back(to_leaf(d)->m_value); - } - else { - for (unsigned i = 0; i < 2; i++) { - dependency * child = to_join(d)->m_children[i]; - if (!child->is_marked()) { - m_todo.push_back(child); - child->mark(); - } + void linearize(vector& vs) { + unsigned qhead = 0; + while (qhead < m_todo.size()) { + dependency * d = m_todo[qhead]; + qhead++; + if (d->is_leaf()) { + vs.push_back(to_leaf(d)->m_value); + } + else { + for (unsigned i = 0; i < 2; i++) { + dependency * child = to_join(d)->m_children[i]; + if (!child->is_marked()) { + m_todo.push_back(child); + child->mark(); } } } - unmark_todo(); } + unmark_todo(); + } + + void linearize(dependency * d, vector & vs) { + if (!d) + return; + m_todo.reset(); + d->mark(); + m_todo.push_back(d); + linearize(vs); + } + + void linearize(ptr_vector& deps, vector & vs) { + if (deps.empty()) + return; + m_todo.reset(); + for (auto* d : deps) { + if (d && !d->is_marked()) { + d->mark(); + m_todo.push_back(d); + } + } + linearize(vs); } }; @@ -303,6 +317,10 @@ public: void linearize(dependency * d, vector & vs) { return m_dep_manager.linearize(d, vs); } + + void linearize(ptr_vector& d, vector & vs) { + return m_dep_manager.linearize(d, vs); + } void reset() { m_allocator.reset();