mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

yada yada

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-21 19:57:17 -07:00
parent 2ee971ef68
commit 67e419d20d
2 changed files with 138 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -82,7 +82,7 @@ namespace polysat {
m_justification.push_back(justification::unassigned());
m_viable.push_back(m_bdd.mk_true());
m_vdeps.push_back(m_dep_manager.mk_empty());
m_pdeps.push_back(vector<pdd>());
m_cjust.push_back(constraints());
m_watch.push_back(ptr_vector<constraint>());
m_activity.push_back(0);
m_vars.push_back(sz2pdd(sz).mk_var(v));
@ -97,7 +97,7 @@ namespace polysat {
m_free_vars.del_var_eh(v);
m_viable.pop_back();
m_vdeps.pop_back();
m_pdeps.pop_back();
m_cjust.pop_back();
m_value.pop_back();
m_justification.pop_back();
m_watch.pop_back();
@ -227,7 +227,7 @@ namespace polysat {
if (p.is_non_zero()) {
// we could tag constraint to allow early substitution before
// swapping watch variable in case we can detect conflict earlier.
set_conflict(v, c);
set_conflict(c);
return false;
}
@ -249,7 +249,9 @@ namespace polysat {
unsigned sz = p.power_of_2();
VERIFY(a.mult_inverse(sz, inv_a));
rational val = mod(inv_a * -b, rational::power_of_two(sz));
assign(other_var, val, justification::propagation(m_level, &c));
m_cjust[other_var].push_back(&c);
m_trail.push(push_back_vector(m_cjust[other_var]));
propagate(other_var, val, justification::propagation(m_level));
return false;
}
@ -260,6 +262,14 @@ namespace polysat {
return false;
}
void solver::propagate(unsigned var, rational const& val, justification const& j) {
SASSERT(j.is_propagation());
if (is_viable(var, val))
assign_core(var, val, j);
else
set_conflict(*m_cjust[var].back());
}
void solver::inc_level() {
m_trail.push(value_trail(m_level));
++m_level;
@ -279,10 +289,6 @@ namespace polysat {
}
}
bool solver::can_decide() {
return !m_free_vars.empty();
}
void solver::decide(rational & val, unsigned& var) {
SASSERT(can_decide());
inc_level();
@ -293,15 +299,6 @@ namespace polysat {
assign_core(var, val, justification::decision(m_level));
}
void solver::assign(unsigned var, rational const& val, justification const& j) {
if (is_viable(var, val))
assign_core(var, val, j);
else {
SASSERT(!j.is_decision());
// TBD: set conflict, assumes justification is a propagation.
}
}
void solver::assign_core(unsigned var, rational const& val, justification const& j) {
SASSERT(is_viable(var, val));
m_trail.push(var_unassign(*this));
@ -310,18 +307,108 @@ namespace polysat {
m_justification[var] = j;
}
bool solver::is_conflict() {
return m_conflict != nullptr;
}
/**
* Conflict resolution.
* - m_conflict is a constraint 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
* 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.
* 6. Otherwise, add accumulated constraints to explanation for the next viable solution, prune
* viable solutions by excluding the previous guess.
*/
unsigned solver::resolve_conflict(unsigned_vector& deps) {
SASSERT(m_conflict);
constraint& c = *m_conflict;
m_conflict = nullptr;
pdd p = c.p();
reset_marks();
for (auto v : c.vars())
set_mark(v);
unsigned v = UINT_MAX;
unsigned i = m_search.size();
vector<std::pair<unsigned, rational>> sub;
for (auto w : m_search)
sub.push_back(std::make_pair(w, m_value[w]));
void solver::set_conflict(unsigned v, constraint& c) {
m_conflict = &c;
m_conflict_var = v;
}
unsigned resolve_conflict(unsigned_vector& deps) {
for (; i-- > 0; ) {
v = m_search[i];
if (!is_marked(v))
continue;
pdd q = isolate(v);
pdd r = resolve(v, q, p);
pdd rval = r.subst_val(sub);
if (!rval.is_non_zero())
goto backtrack;
if (r.is_val()) {
SASSERT(!r.is_zero());
// TBD: UNSAT, set conflict
return 0;
}
justification& j = m_justification[v];
if (j.is_decision()) {
// TBD: revert value and add constraint
// propagate if new value is given uniquely
// set conflict if viable set is empty
// adding r and reverting last decision.
break;
}
SASSERT(j.is_propagation());
for (auto w : r.free_vars())
set_mark(w);
p = r;
}
UNREACHABLE();
backtrack:
do {
v = m_search[i];
justification& j = m_justification[v];
if (j.is_decision()) {
// TBD: flip last decision.
}
}
while (i-- > 0);
return 0;
}
/**
* resolve polynomials associated with unit propagating on v
* producing polynomial that isolates v to lowest degree
* and lowest power of 2.
*/
pdd solver::isolate(unsigned v) {
if (m_cjust[v].empty())
return sz2pdd(m_size[v]).zero();
pdd p = m_cjust[v][0]->p();
for (unsigned i = m_cjust[v].size(); i-- > 1; ) {
// TBD reduce with respect to v
}
return p;
}
/**
* Return residue of superposing p and q with respect to v.
*/
pdd solver::resolve(unsigned v, pdd const& p, pdd const& q) {
// TBD remove as much trace of v as possible.
return p;
}
void solver::reset_marks() {
m_marks.reserve(m_vars.size());
m_clock++;
if (m_clock != 0)
return;
m_clock++;
m_marks.fill(0);
}
bool solver::can_learn() {
return false;

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

@ -92,18 +92,17 @@ namespace polysat {
class justification {
justification_k m_kind;
constraint* m_c { nullptr };
unsigned m_level;
justification(justification_k k, unsigned lvl, constraint* c): m_kind(k), m_c(c), m_level(lvl) {}
justification(justification_k k, unsigned lvl): m_kind(k), m_level(lvl) {}
public:
justification(): m_kind(justification_k::unassigned), m_c(nullptr) {}
static justification unassigned() { return justification(justification_k::unassigned, 0, nullptr); }
static justification decision(unsigned lvl) { return justification(justification_k::decision, lvl, nullptr); }
static justification propagation(unsigned lvl, constraint* c) { return justification(justification_k::propagation, lvl, c); }
justification(): m_kind(justification_k::unassigned) {}
static justification unassigned() { return justification(justification_k::unassigned, 0); }
static justification decision(unsigned lvl) { return justification(justification_k::decision, lvl); }
static justification propagation(unsigned lvl) { return justification(justification_k::propagation, lvl); }
bool is_decision() const { return m_kind == justification_k::decision; }
bool is_unassigned() const { return m_kind == justification_k::unassigned; }
bool is_propagation() const { return m_kind == justification_k::propagation; }
justification_k kind() const { return m_kind; }
constraint& get_constraint() const { return *m_c; }
unsigned level() const { return m_level; }
std::ostream& display(std::ostream& out) const;
};
@ -112,6 +111,8 @@ namespace polysat {
class solver {
typedef ptr_vector<constraint> constraints;
trail_stack& m_trail;
scoped_ptr_vector<dd::pdd_manager> m_pdd;
dd::bdd_manager m_bdd;
@ -125,10 +126,10 @@ namespace polysat {
// Per variable information
vector<bdd> m_viable; // set of viable values.
ptr_vector<u_dependency> m_vdeps; // dependencies for viable values
vector<vector<pdd>> m_pdeps; // dependencies in polynomial form
vector<rational> m_value; // assigned value
vector<justification> m_justification; // justification for variable assignment
vector<ptr_vector<constraint>> m_watch; // watch list datastructure into constraints.
vector<constraints> m_cjust; // constraints used for justification
vector<constraints> m_watch; // watch list datastructure into constraints.
unsigned_vector m_activity;
vector<pdd> m_vars;
unsigned_vector m_size; // store size of variables.
@ -139,7 +140,6 @@ namespace polysat {
unsigned m_level { 0 };
// conflict state
unsigned m_conflict_var { UINT_MAX };
constraint* m_conflict { nullptr };
unsigned size(unsigned var) const { return m_size[var]; }
@ -164,7 +164,6 @@ namespace polysat {
void inc_level();
void assign(unsigned var, rational const& val, justification const& j);
void assign_core(unsigned var, rational const& val, justification const& j);
bool is_assigned(unsigned var) const { return !m_justification[var].is_unassigned(); }
@ -172,10 +171,20 @@ namespace polysat {
void propagate(unsigned v);
bool propagate(unsigned v, constraint& c);
bool propagate_eq(unsigned v, constraint& c);
void propagate(unsigned var, rational const& val, justification const& j);
void erase_watch(unsigned v, constraint& c);
void set_conflict(unsigned v, constraint& c);
void clear_conflict() { m_conflict = nullptr; m_conflict_var = UINT_MAX; }
void set_conflict(constraint& c) { m_conflict = &c; }
void clear_conflict() { m_conflict = nullptr; }
unsigned_vector m_marks;
unsigned m_clock { 0 };
void reset_marks();
bool is_marked(unsigned v) const { return m_clock == m_marks[v]; }
void set_mark(unsigned v) { m_marks[v] = m_clock; }
pdd isolate(unsigned v);
pdd resolve(unsigned v, pdd const& p, pdd const& q);
/**
* push / pop are used only in self-contained mode from check_sat.
@ -227,15 +236,10 @@ namespace polysat {
bool can_propagate();
void propagate();
bool can_decide();
bool can_decide() const { return !m_free_vars.empty(); }
void decide(rational & val, unsigned& var);
/**
* external decision
*/
void assign(unsigned var, rational const& val) { inc_level(); assign(var, val, justification::decision(m_level)); }
bool is_conflict();
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.