mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +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 018835f1db
commit a863a0e853
2 changed files with 42 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -373,16 +373,16 @@ namespace polysat {
}
pdd r = resolve(v, p);
pdd rval = r.subst_val(sub);
if (!rval.is_non_zero()) {
backtrack(i);
return;
}
if (r.is_val()) {
if (r.is_val() && rval.is_non_zero()) {
report_unsat();
return;
}
if (j.is_decision()) {
revert_decision(i);
revert_decision(p, i);
return;
}
if (!rval.is_non_zero()) {
backtrack(i);
return;
}
SASSERT(j.is_propagation());
@ -422,20 +422,40 @@ namespace polysat {
// 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;
SASSERT(num_levels > 0);
pop_levels(num_levels);
m_trail.pop_scope(num_levels);
// TBD: add new constraints & lemmas.
m_trail.pop_scope(num_levels);
}
/**
* resolve polynomials associated with unit propagating on v

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

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