mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

general form migration

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-13 13:00:47 -07:00
parent 7025d85da3
commit a0d112b7b0
3 changed files with 114 additions and 68 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/dd/dd_pdd.h
View file

@ -402,6 +402,7 @@ namespace dd {
pdd reduce(pdd const& other) const { return m.reduce(*this, other); }
bool different_leading_term(pdd const& other) const { return m.different_leading_term(*this, other); }
void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) const { m.factor(*this, v, degree, lc, rest); }
bool resolve(unsigned v, pdd const& other, pdd& result) { return m.resolve(v, *this, other, result); }
pdd subst_val(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val(*this, s); }
pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }

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

@ -291,12 +291,15 @@ namespace polysat {
m_search.pop_back();
}
}
// Base approach just clears all assignments.
// TBD approach allows constraints to constrain bits of v. They are
// added to cjust and affect viable outside of search.
void solver::undo_var(pvar v) {
m_justification[v] = justification::unassigned();
m_free_vars.unassign_var_eh(v);
m_cjust[v].reset();
m_viable[v] = m_bdd.mk_true(); // TBD does not work with external bit-assignments
m_viable[v] = m_bdd.mk_true();
}
@ -359,28 +362,27 @@ namespace polysat {
}
void solver::set_conflict(constraint& c) {
SASSERT(m_conflict_cs.empty());
m_conflict_cs.push_back(&c);
SASSERT(m_conflict.empty());
m_conflict.push_back(&c);
}
void solver::set_conflict(pvar v) {
SASSERT(m_conflict_cs.empty());
m_conflict_cs.append(m_cjust[v]);
SASSERT(m_conflict.empty());
m_conflict.append(m_cjust[v]);
if (m_cjust[v].empty())
m_conflict_cs.push_back(nullptr);
m_conflict.push_back(nullptr);
}
/**
* Conflict resolution.
* - m_conflict_cs are constraints that are infeasible in the current assignment.
* - m_conflict_dep are dependencies for infeasibility
* 1. walk m_search from top down until last variable in m_conflict_cs.
* - m_conflict are constraints that are infeasible in the current assignment.
* 1. walk m_search from top down until last variable in m_conflict.
* 2. resolve constraints in m_cjust to isolate lowest degree polynomials
* using variable.
* Use Olm-Seidl division by powers of 2 to preserve invertibility.
* 3. resolve conflict with result of resolution.
* 4. If the resulting equality is still infeasible continue, otherwise bail out
* 4. If the resulting lemma is still infeasible continue, otherwise bail out
* and undo the last assignment by accumulating conflict trail (but without resolution).
* 5. When hitting the last decision, determine whether conflict polynomial is asserting,
* If so, apply propagation.
@ -392,22 +394,21 @@ namespace polysat {
*/
void solver::resolve_conflict() {
if (m_conflict_cs.size() == 1 && !m_conflict_cs[0]) {
SASSERT(!m_conflict.empty());
if (m_conflict.size() == 1 && !m_conflict[0]) {
report_unsat();
return;
}
if (m_conflict_cs.size() > 1) {
revert_decision(m_search.size()-1);
return;
}
constraint* c = m_conflict_cs[0];
scoped_ptr<constraint> lemma;
reset_marks();
for (auto v : c->vars())
set_mark(v);
for (constraint* c : m_conflict) {
SASSERT(c);
for (auto v : c->vars())
set_mark(v);
}
for (unsigned i = m_search.size(); i-- > 0; ) {
pvar v = m_search[i].first;
if (!is_marked(v))
@ -419,45 +420,60 @@ namespace polysat {
}
if (j.is_decision()) {
learn_lemma(v, lemma.detach());
revert_decision(i);
return;
}
constraint* new_lemma = resolve(v, lemma.get());
if (!new_lemma) {
backtrack(i);
return;
}
lemma = new_lemma;
// TBD: this assumes lemma is an equality.
pdd r = lemma->p();
pdd rval = r.subst_val(m_search);
if (r.is_val() && rval.is_never_zero()) {
report_unsat();
return;
}
if (!rval.is_never_zero()) {
backtrack(i);
revert_decision(v);
return;
}
SASSERT(j.is_propagation());
scoped_ptr<constraint> new_lemma = resolve(v);
if (!new_lemma) {
backtrack(i, lemma);
return;
}
if (is_always_false(*new_lemma)) {
learn_lemma(v, new_lemma.get());
m_conflict.reset();
m_conflict.push_back(new_lemma.detach());
report_unsat();
return;
}
if (!eval_to_false(*new_lemma)) {
backtrack(i, lemma);
return;
}
lemma = new_lemma.detach();
reset_marks();
for (auto w : lemma->vars())
set_mark(w);
c = lemma.get();
m_conflict.reset();
m_conflict.push_back(lemma.get());
}
report_unsat();
}
void solver::backtrack(unsigned i) {
void solver::backtrack(unsigned i, scoped_ptr<constraint>& lemma) {
if (lemma) {
m_conflict.push_back(lemma.get());
add_lemma(lemma.detach());
}
do {
auto v = m_search[i].first;
if (!is_marked(v))
continue;
justification& j = m_justification[v];
if (j.level() <= base_level())
break;
if (j.is_decision()) {
revert_decision(i);
revert_decision(v);
return;
}
// retrieve constraint used for propagation
// add variables to COI
SASSERT(j.is_propagation());
for (auto* c : m_cjust[v]) {
for (auto w : c->vars())
set_mark(w);
m_conflict.push_back(c);
}
}
while (i-- > 0);
report_unsat();
@ -465,21 +481,19 @@ namespace polysat {
void solver::report_unsat() {
backjump(base_level());
SASSERT(m_conflict_cs.empty());
m_conflict_cs.push_back(nullptr);
SASSERT(!m_conflict.empty());
}
void solver::unsat_core(unsigned_vector& deps) {
deps.reset();
p_dependency_ref conflict_dep(m_dm);
for (auto* c : m_conflict_cs) {
for (auto* c : m_conflict) {
if (c)
conflict_dep = m_dm.mk_join(c->dep(), conflict_dep);
}
m_dm.linearize(conflict_dep, deps);
}
/**
* The polynomial p encodes an equality that the decision was infeasible.
* The effect of this function is that the assignment to v is undone and replaced
@ -497,22 +511,24 @@ namespace polysat {
/**
* variable v was assigned by a decision at position i in the search stack.
* TODO: we could resolve constraints in cjust[v] against each other to
* obtain stronger propagation. Example:
* (x + 1)*P = 0 and (x + 1)*Q = 0, where gcd(P,Q) = 1, then we have x + 1 = 0.
* We refer to this process as narrowing.
* In general form it can rely on factoring.
* Root finding can further prune viable.
*/
void solver::revert_decision(unsigned i) {
auto v = m_search[i].first;
void solver::revert_decision(pvar v) {
rational val = m_value[v];
SASSERT(m_justification[v].is_decision());
stash_deps(v);
m_conflict.append(m_cjust[v]);
backjump(m_justification[v].level()-1);
unstash_deps(v);
add_non_viable(v, m_value[v]);
SASSERT(m_cjust[v].empty());
m_cjust[v].append(m_conflict);
m_conflict.reset();
add_non_viable(v, val);
decide(v);
}
void solver::stash_deps(pvar v) {
}
void solver::unstash_deps(pvar v) {
}
void solver::backjump(unsigned new_level) {
unsigned num_levels = m_level - new_level;
@ -523,10 +539,43 @@ namespace polysat {
/**
* Return residue of superposing p and q with respect to v.
*/
constraint* solver::resolve(pvar v, constraint* c) {
constraint* solver::resolve(pvar v) {
SASSERT(!m_cjust[v].empty());
SASSERT(m_justification[v].is_propagation());
if (m_conflict.size() > 1)
return nullptr;
if (m_cjust[v].size() > 1)
return nullptr;
constraint* c = m_conflict[0];
constraint* d = m_cjust[v].back();
if (c->is_eq() && d->is_eq()) {
pdd p = c->p();
pdd q = d->p();
pdd r = p;
if (!p.resolve(v, q, r))
return nullptr;
p_dependency_ref dep(m_dm);
dep = m_dm.mk_join(c->dep(), d->dep());
unsigned level = std::max(c->level(), d->level());
return constraint::eq(level, r, dep);
}
return nullptr;
}
bool solver::is_always_false(constraint& c) {
if (c.is_eq())
return c.p().is_never_zero();
return false;
}
bool solver::eval_to_false(constraint& c) {
if (c.is_eq()) {
pdd r = c.p().subst_val(m_search);
return r.is_never_zero();
}
return false;
}
void solver::add_lemma(constraint* c) {
add_watch(*c);
m_redundant.push_back(c);

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

@ -128,7 +128,7 @@ namespace polysat {
dep_value_manager m_value_manager;
small_object_allocator m_alloc;
poly_dep_manager m_dm;
constraints m_conflict_cs;
constraints m_conflict;
constraints m_stash_just;
var_queue m_free_vars;
@ -155,9 +155,6 @@ namespace polysat {
unsigned_vector m_base_levels; // External clients can push/pop scope.
// conflict state
ptr_vector<constraint> m_conflict;
unsigned size(pvar v) const { return m_size[v]; }
/**
* check if value is viable according to m_viable.
@ -221,15 +218,12 @@ namespace polysat {
unsigned m_conflict_level { 0 };
constraint* resolve(pvar v, constraint* c);
constraint* resolve(pvar v);
bool can_decide() const { return !m_free_vars.empty(); }
void decide();
void decide(pvar v);
void stash_deps(pvar v);
void unstash_deps(pvar v);
p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); }
bool is_conflict() const { return !m_conflict.empty(); }
@ -237,13 +231,15 @@ namespace polysat {
unsigned base_level() const;
void resolve_conflict();
void backtrack(unsigned i);
void backtrack(unsigned i, scoped_ptr<constraint>& lemma);
void report_unsat();
void revert_decision(unsigned i);
void revert_decision(pvar v);
void learn_lemma(pvar v, constraint* c);
void backjump(unsigned new_level);
void undo_var(pvar v);
void add_lemma(constraint* c);
bool is_always_false(constraint& c);
bool eval_to_false(constraint& c);