From 303c41395da7f7d5d731a513e7509dd2c7799189 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Apr 2021 12:36:18 -0700 Subject: [PATCH] introduce user-push/pop Signed-off-by: Nikolaj Bjorner --- src/math/polysat/polysat.cpp | 75 +++++++++++++++++++++++------------- src/math/polysat/polysat.h | 30 +++++++-------- 2 files changed, 64 insertions(+), 41 deletions(-) diff --git a/src/math/polysat/polysat.cpp b/src/math/polysat/polysat.cpp index 5dd7c9f38..af975cff1 100644 --- a/src/math/polysat/polysat.cpp +++ b/src/math/polysat/polysat.cpp @@ -63,7 +63,7 @@ namespace polysat { lbool solver::check_sat() { while (true) { if (is_conflict() && m_level == 0) return l_false; - else if (is_conflict()) resolve_conflict_core(); + else if (is_conflict()) resolve_conflict(); else if (can_propagate()) propagate(); else if (!can_decide()) return l_true; else decide(); @@ -348,7 +348,7 @@ namespace polysat { * 6. Otherwise, add accumulated constraints to explanation for the next viable solution, prune * viable solutions by excluding the previous guess. */ - unsigned solver::resolve_conflict() { + void solver::resolve_conflict() { SASSERT(m_conflict); constraint& c = *m_conflict; m_conflict = nullptr; @@ -368,12 +368,15 @@ namespace polysat { continue; pdd r = resolve(v, p); pdd rval = r.subst_val(sub); - if (!rval.is_non_zero()) - goto backtrack; + if (!rval.is_non_zero()) { + backtrack(); + return; + } if (r.is_val()) { - SASSERT(!r.is_zero()); // TBD: UNSAT, set conflict - return i; + SASSERT(!r.is_zero()); + // learn_lemma(r, deps); + return; } justification& j = m_justification[v]; if (j.is_decision()) { @@ -381,30 +384,43 @@ namespace polysat { // propagate if new value is given uniquely // set conflict if viable set is empty // adding r and reverting last decision. - break; + // m_search.size() - i; + return; } SASSERT(j.is_propagation()); + reset_marks(); for (auto w : r.free_vars()) set_mark(w); p = r; } UNREACHABLE(); - - backtrack: + } + + void solver::backtrack() { + unsigned i = m_search.size(); do { - v = m_search[i]; + auto v = m_search[i]; justification& j = m_justification[v]; if (j.is_decision()) { // TBD: flip last decision. + // subtract value from viable + // m_viable[v] -= m_value[v]; + if (m_viable[v].is_false()) + continue; + // + // pop levels to i + // choose a new value for v as a decision. + // } } while (i-- > 0); - - return 0; + + // unsat + // r = 1; + // learn_and_backjump(r, m_search.size()); } - void solver::resolve_conflict_core() { - unsigned new_level = resolve_conflict(); + void solver::learn_and_backjump(pdd const& lemma, unsigned new_level) { unsigned num_levels = m_level - new_level; SASSERT(num_levels > 0); pop_levels(num_levels); @@ -412,6 +428,7 @@ namespace polysat { // TBD: add new constraints & lemmas. } + /** * resolve polynomials associated with unit propagating on v @@ -431,6 +448,10 @@ 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) { auto degree = p.degree(v); @@ -456,19 +477,21 @@ namespace polysat { m_clock++; m_marks.fill(0); } + + void solver::push() { + push_level(); + 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); + } + + bool solver::at_base_level() const { + return m_level == 0 || (!m_scopes.empty() && m_level == m_scopes.back()); + } - bool solver::can_learn() { - return false; - } - - void solver::learn(constraint& c, unsigned_vector& deps) { - - } - - void solver::learn(vector& cs, unsigned_vector& deps) { - - } - std::ostream& solver::display(std::ostream& out) const { for (auto* c : m_constraints) out << *c << "\n"; diff --git a/src/math/polysat/polysat.h b/src/math/polysat/polysat.h index 8c04b31e3..07c1a77cd 100644 --- a/src/math/polysat/polysat.h +++ b/src/math/polysat/polysat.h @@ -120,6 +120,8 @@ namespace polysat { unsigned m_qhead { 0 }; unsigned m_level { 0 }; + unsigned_vector m_scopes; // user-scopes. External clients can push/pop scope + // conflict state constraint* m_conflict { nullptr }; @@ -169,7 +171,16 @@ namespace polysat { pdd isolate(unsigned v); pdd resolve(unsigned v, pdd const& p); void decide(); - void resolve_conflict_core(); + + bool is_conflict() const { return nullptr != m_conflict; } + bool at_base_level() const; + + void resolve_conflict(); + void backtrack(); + void learn_and_backjump(pdd const& lemma, unsigned new_level); + + bool can_decide() const { return !m_free_vars.empty(); } + void decide(rational & val, unsigned& var); bool invariant(); @@ -223,20 +234,9 @@ namespace polysat { bool can_propagate(); void propagate(); - bool can_decide() const { return !m_free_vars.empty(); } - void decide(rational & val, unsigned& var); - - bool is_conflict() const { return nullptr != m_conflict; } - /** - * Return number of scopes to backtrack and core in the shape of dependencies - * TBD: External vs. internal mode may need different signatures. - */ - unsigned resolve_conflict(); - - bool can_learn(); - void learn(constraint& c, unsigned_vector& deps); - void learn(vector& cs, unsigned_vector& deps); - + void push(); + void pop(unsigned num_scopes); + std::ostream& display(std::ostream& out) const; };