From e77f2d3d4e364652494821d6b21509e0709f4dda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Apr 2021 15:30:44 -0700 Subject: [PATCH] clean Signed-off-by: Nikolaj Bjorner --- src/math/polysat/polysat.cpp | 127 +++++++++++++++-------------------- src/math/polysat/polysat.h | 61 ++++++++--------- 2 files changed, 87 insertions(+), 101 deletions(-) diff --git a/src/math/polysat/polysat.cpp b/src/math/polysat/polysat.cpp index 6ca795f2c..8cfe0fdd6 100644 --- a/src/math/polysat/polysat.cpp +++ b/src/math/polysat/polysat.cpp @@ -38,23 +38,23 @@ namespace polysat { return *m_pdd[sz]; } - bool solver::is_viable(unsigned var, rational const& val) { - bdd b = m_viable[var]; - for (unsigned k = size(var); k-- > 0 && !b.is_false(); ) + bool solver::is_viable(pvar v, rational const& val) { + bdd b = m_viable[v]; + for (unsigned k = size(v); k-- > 0 && !b.is_false(); ) b &= val.get_bit(k) ? m_bdd.mk_var(k) : m_bdd.mk_nvar(k); return !b.is_false(); } - void solver::add_non_viable(unsigned var, rational const& val) { + void solver::add_non_viable(pvar v, rational const& val) { bdd value = m_bdd.mk_true(); - for (unsigned k = size(var); k-- > 0; ) + for (unsigned k = size(v); k-- > 0; ) value &= val.get_bit(k) ? m_bdd.mk_var(k) : m_bdd.mk_nvar(k); - m_viable[var] &= !value; + m_viable[v] &= !value; } - lbool solver::find_viable(unsigned var, rational & val) { + lbool solver::find_viable(pvar v, rational & val) { val = 0; - bdd viable = m_viable[var]; + bdd viable = m_viable[v]; if (viable.is_false()) return l_false; unsigned num_vars = 0; @@ -68,7 +68,7 @@ namespace polysat { viable = viable.lo(); ++num_vars; } - if (num_vars == size(var)) + if (num_vars == size(v)) return l_true; return l_undef; } @@ -86,6 +86,7 @@ namespace polysat { m_dm(m_value_manager, m_alloc), m_vdeps(m_dm), m_conflict_dep(nullptr, m_dm), + m_stash_dep(nullptr, m_dm), m_free_vars(m_activity) { } @@ -103,7 +104,7 @@ namespace polysat { } unsigned solver::add_var(unsigned sz) { - unsigned v = m_viable.size(); + pvar v = m_viable.size(); m_value.push_back(rational::zero()); m_justification.push_back(justification::unassigned()); m_viable.push_back(m_bdd.mk_true()); @@ -119,7 +120,7 @@ namespace polysat { void solver::del_var() { // TODO also remove v from all learned constraints. - unsigned v = m_viable.size() - 1; + pvar v = m_viable.size() - 1; m_free_vars.del_var_eh(v); m_viable.pop_back(); m_vdeps.pop_back(); @@ -165,18 +166,17 @@ namespace polysat { // save for later } - 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); - add_viable_dep(var, mk_dep(dep)); - if (m_viable[var].is_false()) { + void solver::assign(pvar v, unsigned index, bool value, unsigned dep) { + m_viable[v] &= value ? m_bdd.mk_var(index) : m_bdd.mk_nvar(index); + add_viable_dep(v, mk_dep(dep)); + if (m_viable[v].is_false()) { // TBD: set conflict } } - void solver::add_viable_dep(unsigned var, p_dependency* dep) { - if (!dep) - return; - m_vdeps[var] = m_dm.mk_join(m_vdeps.get(var), dep); + void solver::add_viable_dep(pvar v, p_dependency* dep) { + if (dep) + m_vdeps[v] = m_dm.mk_join(m_vdeps.get(v), dep); } bool solver::can_propagate() { @@ -189,7 +189,7 @@ namespace polysat { propagate(m_search[m_qhead++]); } - void solver::propagate(unsigned v) { + void solver::propagate(pvar v) { auto& wlist = m_watch[v]; unsigned i = 0, j = 0, sz = wlist.size(); for (; i < sz && !is_conflict(); ++i) @@ -200,7 +200,7 @@ namespace polysat { wlist.shrink(j); } - bool solver::propagate(unsigned v, constraint& c) { + bool solver::propagate(pvar v, constraint& c) { switch (c.kind()) { case ckind_t::eq_t: return propagate_eq(v, c); @@ -213,7 +213,7 @@ namespace polysat { return false; } - bool solver::propagate_eq(unsigned v, constraint& c) { + bool solver::propagate_eq(pvar v, constraint& c) { SASSERT(c.kind() == ckind_t::eq_t); SASSERT(!c.vars().empty()); auto var = m_vars[v].var(); @@ -271,9 +271,9 @@ namespace polysat { return false; } - void solver::propagate(unsigned var, rational const& val, constraint& c) { - if (is_viable(var, val)) - assign_core(var, val, justification::propagation(m_level)); + void solver::propagate(pvar v, rational const& val, constraint& c) { + if (is_viable(v, val)) + assign_core(v, val, justification::propagation(m_level)); else set_conflict(c); } @@ -306,11 +306,12 @@ namespace polysat { void solver::pop_assignment() { while (!m_search.empty() && m_justification[m_search.back()].level() > m_level) { undo_var(m_search.back()); - pop_search(); + m_search.pop_back(); + m_sub.pop_back(); } } - void solver::undo_var(unsigned v) { + void solver::undo_var(pvar v) { m_justification[v] = justification::unassigned(); m_free_vars.unassign_var_eh(v); m_cjust[v].reset(); @@ -318,16 +319,6 @@ namespace polysat { m_viable[v] = m_bdd.mk_true(); // TBD does not work with external bit-assignments } - void solver::pop_search() { - m_search.pop_back(); - m_sub.pop_back(); - } - - void solver::push_search(unsigned var, rational const& val) { - m_search.push_back(var); - m_value[var] = val; - m_sub.push_back(std::make_pair(var, val)); - } void solver::add_watch(constraint& c) { auto const& vars = c.vars(); @@ -345,7 +336,7 @@ namespace polysat { erase_watch(vars[1], c); } - void solver::erase_watch(unsigned v, constraint& c) { + void solver::erase_watch(pvar v, constraint& c) { if (v == null_var) return; auto& wlist = m_watch[v]; @@ -360,27 +351,32 @@ namespace polysat { } void solver::decide() { - rational val; SASSERT(can_decide()); - unsigned var = m_free_vars.next_var(); - switch (find_viable(var, val)) { + decide(m_free_vars.next_var()); + } + + void solver::decide(pvar v) { + rational val; + switch (find_viable(v, val)) { case l_false: - set_conflict(var); + set_conflict(v); break; case l_true: - assign_core(var, val, justification::propagation(m_level)); + assign_core(v, val, justification::propagation(m_level)); break; case l_undef: push_level(); - assign_core(var, val, justification::decision(m_level)); + assign_core(v, val, justification::decision(m_level)); break; } } - void solver::assign_core(unsigned var, rational const& val, justification const& j) { - SASSERT(is_viable(var, val)); - push_search(var, val); - m_justification[var] = j; + void solver::assign_core(pvar v, rational const& val, justification const& j) { + SASSERT(is_viable(v, val)); + m_search.push_back(v); + m_value[v] = val; + m_sub.push_back(std::make_pair(v, val)); + m_justification[v] = j; } void solver::set_conflict(constraint& c) { @@ -389,7 +385,7 @@ namespace polysat { m_conflict_dep = nullptr; } - void solver::set_conflict(unsigned v) { + void solver::set_conflict(pvar v) { SASSERT(m_conflict_cs.empty()); m_conflict_cs.append(m_cjust[v]); m_conflict_dep = m_vdeps.get(v); @@ -422,7 +418,7 @@ namespace polysat { vector ps = init_conflict(); for (unsigned i = m_search.size(); i-- > 0; ) { - unsigned v = m_search[i]; + pvar v = m_search[i]; if (!is_marked(v)) continue; justification& j = m_justification[v]; @@ -512,7 +508,7 @@ 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(unsigned v, pdd const& p) { + void solver::learn_lemma(pvar v, pdd const& p) { SASSERT(m_conflict_level <= m_justification[v].level()); constraint* c = constraint::eq(m_conflict_level, p, m_conflict_dep); m_cjust[v].push_back(c); @@ -530,28 +526,17 @@ namespace polysat { unstash_deps(v); add_non_viable(v, m_value[v]); add_viable_dep(v, m_conflict_dep); - rational value; - switch (find_viable(v, value)) { - case l_true: - assign_core(v, value, justification::propagation(m_level)); - break; - case l_undef: - push_level(); - assign_core(v, value, justification::decision(m_level)); - break; - case l_false: - set_conflict(v); - break; - } + decide(v); } - void solver::stash_deps(unsigned v) { - // save vdeps[v] and cjust[v] aside - // they are removed by backtracking + void solver::stash_deps(pvar v) { + m_stash_dep = m_vdeps.get(v); + std::swap(m_stash_just, m_cjust[v]); } - void solver::unstash_deps(unsigned v) { - // retrieve saved vdeps[v] and cjust[v] + void solver::unstash_deps(pvar v) { + m_vdeps[v] = m_stash_dep; + std::swap(m_stash_just, m_cjust[v]); } void solver::backjump(unsigned new_level) { @@ -565,7 +550,7 @@ namespace polysat { * producing polynomial that isolates v to lowest degree * and lowest power of 2. */ - pdd solver::isolate(unsigned v, vector const& ps) { + pdd solver::isolate(pvar v, vector const& ps) { pdd p = ps[0]; for (unsigned i = ps.size(); i-- > 1; ) { // TBD reduce with respect to v @@ -576,7 +561,7 @@ namespace polysat { /** * Return residue of superposing p and q with respect to v. */ - pdd solver::resolve(unsigned v, vector const& ps) { + pdd solver::resolve(pvar v, vector const& ps) { auto const& cs = m_cjust[v]; pdd r = isolate(v, ps); auto degree = r.degree(v); diff --git a/src/math/polysat/polysat.h b/src/math/polysat/polysat.h index b217d35b9..61928209e 100644 --- a/src/math/polysat/polysat.h +++ b/src/math/polysat/polysat.h @@ -31,9 +31,10 @@ namespace polysat { class solver; typedef dd::pdd pdd; typedef dd::bdd bdd; + typedef unsigned pvar; const unsigned null_dependency = UINT_MAX; - const unsigned null_var = UINT_MAX; + const pvar null_var = UINT_MAX; struct dep_value_manager { void inc_ref(unsigned) {} @@ -124,9 +125,11 @@ namespace polysat { dep_value_manager m_value_manager; small_object_allocator m_alloc; poly_dep_manager m_dm; - var_queue m_free_vars; p_dependency_ref m_conflict_dep; ptr_vector m_conflict_cs; + p_dependency_ref m_stash_dep; + constraints m_stash_just; + var_queue m_free_vars; // Per constraint state scoped_ptr_vector m_constraints; @@ -145,7 +148,7 @@ namespace polysat { // search state that lists assigned variables unsigned_vector m_search; - vector> m_sub; + vector> m_sub; unsigned m_qhead { 0 }; unsigned m_level { 0 }; @@ -156,21 +159,21 @@ namespace polysat { // conflict state ptr_vector m_conflict; - unsigned size(unsigned var) const { return m_size[var]; } + unsigned size(pvar v) const { return m_size[v]; } /** * check if value is viable according to m_viable. */ - bool is_viable(unsigned var, rational const& val); + bool is_viable(pvar v, rational const& val); /** * register that val is non-viable for var. */ - void add_non_viable(unsigned var, rational const& val); + void add_non_viable(pvar v, rational const& val); /** * Add dependency for variable viable range. */ - void add_viable_dep(unsigned var, p_dependency* dep); + void add_viable_dep(pvar v, p_dependency* dep); /** @@ -179,7 +182,7 @@ namespace polysat { * 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); + lbool find_viable(pvar v, rational & val); /** * undo trail operations for backtracking. @@ -196,40 +199,38 @@ namespace polysat { void pop_assignment(); void pop_constraints(scoped_ptr_vector& cs); - void push_search(unsigned v, rational const& val); - void pop_search(); + void assign_core(pvar v, rational const& val, justification const& j); - void assign_core(unsigned var, rational const& val, justification const& j); + bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); } - bool is_assigned(unsigned var) const { return !m_justification[var].is_unassigned(); } - - void propagate(unsigned v); - bool propagate(unsigned v, constraint& c); - bool propagate_eq(unsigned v, constraint& c); - void propagate(unsigned var, rational const& val, constraint& c); - void erase_watch(unsigned v, constraint& c); + void propagate(pvar v); + bool propagate(pvar v, constraint& c); + bool propagate_eq(pvar v, constraint& c); + void propagate(pvar v, rational const& val, constraint& c); + void erase_watch(pvar v, constraint& c); void erase_watch(constraint& c); void add_watch(constraint& c); void set_conflict(constraint& c); - void set_conflict(unsigned v); + void set_conflict(pvar v); unsigned_vector m_marks; unsigned m_clock { 0 }; void reset_marks(); - bool is_marked(unsigned v) const { return m_clock == m_marks[v]; } - void set_mark(unsigned v) { m_marks[v] = m_clock; } + bool is_marked(pvar v) const { return m_clock == m_marks[v]; } + void set_mark(pvar v) { m_marks[v] = m_clock; } unsigned m_conflict_level { 0 }; - pdd isolate(unsigned v, vector const& ps); - pdd resolve(unsigned v, vector const& ps); + pdd isolate(pvar v, vector const& ps); + pdd resolve(pvar v, vector const& ps); bool can_decide() const { return !m_free_vars.empty(); } void decide(); + void decide(pvar v); - void stash_deps(unsigned v); - void unstash_deps(unsigned v); + void stash_deps(pvar v); + void unstash_deps(pvar v); p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); } @@ -242,9 +243,9 @@ namespace polysat { void backtrack(unsigned i); void report_unsat(); void revert_decision(unsigned i); - void learn_lemma(unsigned v, pdd const& p); + void learn_lemma(pvar v, pdd const& p); void backjump(unsigned new_level); - void undo_var(unsigned v); + void undo_var(pvar v); void add_lemma(constraint* c); @@ -276,12 +277,12 @@ namespace polysat { /** * Add variable with bit-size. */ - unsigned add_var(unsigned sz); + pvar add_var(unsigned sz); /** * Create polynomial terms */ - pdd var(unsigned v) { return m_vars[v]; } + pdd var(pvar v) { return m_vars[v]; } /** * Add polynomial constraints @@ -295,7 +296,7 @@ namespace polysat { void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency); void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency); - void assign(unsigned var, unsigned index, bool value, unsigned dep); + void assign(pvar v, unsigned index, bool value, unsigned dep); /** * main state transitions.