mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

introduce user-push/pop

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

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

@ -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<constraint>& cs, unsigned_vector& deps) {
}
std::ostream& solver::display(std::ostream& out) const {
for (auto* c : m_constraints)
out << *c << "\n";

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

@ -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<constraint>& cs, unsigned_vector& deps);
void push();
void pop(unsigned num_scopes);
std::ostream& display(std::ostream& out) const;
};