mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +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 15:12:54 -07:00
parent d7456dc2a7
commit cec0cdce33
2 changed files with 42 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -373,16 +373,16 @@ namespace polysat {
} }
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 (r.is_val() && rval.is_non_zero()) {
backtrack(i);
return;
}
if (r.is_val()) {
report_unsat(); report_unsat();
return; return;
} }
if (j.is_decision()) { if (j.is_decision()) {
revert_decision(i); revert_decision(p, i);
return;
}
if (!rval.is_non_zero()) {
backtrack(i);
return; return;
} }
SASSERT(j.is_propagation()); SASSERT(j.is_propagation());
@ -422,21 +422,41 @@ namespace polysat {
// are in the unsat core that is produced as a side-effect // are in the unsat core that is produced as a side-effect
} }
void solver::revert_decision(unsigned i) { void solver::revert_decision(pdd const& p, unsigned i) {
auto v = m_search[i];
SASSERT(m_justification[v].is_decision());
//
// TBD: compute level and dependencies for p
// Dependencies should be accumulated during resolve_conflict
// the level is computed from the free variables in p (except v)
// it should correspond to the implication level.
//
unsigned level = 0;
u_dependency* deps = nullptr;
constraint* c = constraint::eq(level, p, deps);
m_cjust[v].push_back(c);
m_redundant.push_back(c);
add_watch(*c);
SASSERT(invariant(m_redundant)); // TBD enforce level invariant
//
// 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, learn_and_backjump
// and set a new conflict.
//
} }
void solver::learn_and_backjump(pdd const& lemma, unsigned new_level) { void solver::backjump(unsigned new_level) {
unsigned num_levels = m_level - new_level; unsigned num_levels = m_level - new_level;
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.
} }
/** /**
* resolve polynomials associated with unit propagating on v * resolve polynomials associated with unit propagating on v
* producing polynomial that isolates v to lowest degree * producing polynomial that isolates v to lowest degree

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

@ -179,8 +179,8 @@ namespace polysat {
void resolve_conflict(); void resolve_conflict();
void backtrack(unsigned i); void backtrack(unsigned i);
void report_unsat(); void report_unsat();
void revert_decision(unsigned i); void revert_decision(pdd const& p, unsigned i);
void learn_and_backjump(pdd const& lemma, unsigned new_level); void backjump(unsigned new_level);
bool can_decide() const { return !m_free_vars.empty(); } bool can_decide() const { return !m_free_vars.empty(); }
void decide(rational & val, unsigned& var); void decide(rational & val, unsigned& var);
@ -201,8 +201,7 @@ namespace polysat {
~solver(); ~solver();
/** /**
* Self-contained satisfiability checker. * End-game satisfiability checker.
* Main mode is to have external solver drive state machine.
*/ */
lbool check_sat(); lbool check_sat();
@ -216,7 +215,6 @@ namespace polysat {
*/ */
pdd var(unsigned v) { return m_vars[v]; } pdd var(unsigned v) { return m_vars[v]; }
/** /**
* Add polynomial constraints * Add polynomial constraints
* Each constraint is tracked by a dependency. * Each constraint is tracked by a dependency.
@ -237,6 +235,10 @@ namespace polysat {
bool can_propagate(); bool can_propagate();
void propagate(); void propagate();
/**
* External context managment.
* Adds so-called user-scope.
*/
void push(); void push();
void pop(unsigned num_scopes); void pop(unsigned num_scopes);