mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

reorg resolution loop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-01 14:46:18 -07:00
parent 303c41395d
commit 018835f1db
2 changed files with 34 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/math/polysat/polysat.cpp
View file

@ -366,25 +366,23 @@ namespace polysat {
v = m_search[i]; v = m_search[i];
if (!is_marked(v)) if (!is_marked(v))
continue; continue;
justification& j = m_justification[v];
if (j.level() <= base_level()) {
report_unsat();
return;
}
pdd r = resolve(v, p); pdd r = resolve(v, p);
pdd rval = r.subst_val(sub); pdd rval = r.subst_val(sub);
if (!rval.is_non_zero()) { if (!rval.is_non_zero()) {
backtrack(); backtrack(i);
return; return;
} }
if (r.is_val()) { if (r.is_val()) {
// TBD: UNSAT, set conflict report_unsat();
SASSERT(!r.is_zero());
// learn_lemma(r, deps);
return; return;
} }
justification& j = m_justification[v];
if (j.is_decision()) { if (j.is_decision()) {
// TBD: revert value and add constraint revert_decision(i);
// propagate if new value is given uniquely
// set conflict if viable set is empty
// adding r and reverting last decision.
// m_search.size() - i;
return; return;
} }
SASSERT(j.is_propagation()); SASSERT(j.is_propagation());
@ -393,14 +391,15 @@ namespace polysat {
set_mark(w); set_mark(w);
p = r; p = r;
} }
UNREACHABLE(); report_unsat();
} }
void solver::backtrack() { void solver::backtrack(unsigned i) {
unsigned i = m_search.size();
do { do {
auto v = m_search[i]; auto v = m_search[i];
justification& j = m_justification[v]; justification& j = m_justification[v];
if (j.level() <= base_level())
break;
if (j.is_decision()) { if (j.is_decision()) {
// TBD: flip last decision. // TBD: flip last decision.
// subtract value from viable // subtract value from viable
@ -415,9 +414,16 @@ namespace polysat {
} }
while (i-- > 0); while (i-- > 0);
// unsat report_unsat();
// r = 1; }
// learn_and_backjump(r, m_search.size());
void solver::report_unsat() {
// dependencies for variables that are currently marked and below base level
// are in the unsat core that is produced as a side-effect
}
void solver::revert_decision(unsigned i) {
} }
void solver::learn_and_backjump(pdd const& lemma, unsigned new_level) { void solver::learn_and_backjump(pdd const& lemma, unsigned new_level) {
@ -425,6 +431,7 @@ namespace polysat {
SASSERT(num_levels > 0); SASSERT(num_levels > 0);
pop_levels(num_levels); pop_levels(num_levels);
m_trail.pop_scope(num_levels); m_trail.pop_scope(num_levels);
// TBD: add new constraints & lemmas. // TBD: add new constraints & lemmas.
} }
@ -489,7 +496,11 @@ namespace polysat {
} }
bool solver::at_base_level() const { bool solver::at_base_level() const {
return m_level == 0 || (!m_scopes.empty() && m_level == m_scopes.back()); return m_level == base_level();
}
unsigned solver::base_level() const {
return m_scopes.empty() ? 0 : m_scopes.back();
} }
std::ostream& solver::display(std::ostream& out) const { std::ostream& solver::display(std::ostream& out) const {

7
src/math/polysat/polysat.h
View file

@ -120,7 +120,7 @@ namespace polysat {
unsigned m_qhead { 0 }; unsigned m_qhead { 0 };
unsigned m_level { 0 }; unsigned m_level { 0 };
unsigned_vector m_scopes; // user-scopes. External clients can push/pop scope unsigned_vector m_scopes; // user-scopes. External clients can push/pop scope.
// conflict state // conflict state
@ -174,9 +174,12 @@ namespace polysat {
bool is_conflict() const { return nullptr != m_conflict; } bool is_conflict() const { return nullptr != m_conflict; }
bool at_base_level() const; bool at_base_level() const;
unsigned base_level() const;
void resolve_conflict(); void resolve_conflict();
void backtrack(); void backtrack(unsigned i);
void report_unsat();
void revert_decision(unsigned i);
void learn_and_backjump(pdd const& lemma, unsigned new_level); void learn_and_backjump(pdd const& lemma, unsigned new_level);
bool can_decide() const { return !m_free_vars.empty(); } bool can_decide() const { return !m_free_vars.empty(); }