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

clean

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-05 15:30:44 -07:00
parent b1cbd7d814
commit e77f2d3d4e
2 changed files with 87 additions and 101 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -38,23 +38,23 @@ namespace polysat {
return *m_pdd[sz];
}
bool solver::is_viable(unsigned var, rational const& val) {
bdd b = m_viable[var];
for (unsigned k = size(var); k-- > 0 && !b.is_false(); )
bool solver::is_viable(pvar v, rational const& val) {
bdd b = m_viable[v];
for (unsigned k = size(v); k-- > 0 && !b.is_false(); )
b &= val.get_bit(k) ? m_bdd.mk_var(k) : m_bdd.mk_nvar(k);
return !b.is_false();
}
void solver::add_non_viable(unsigned var, rational const& val) {
void solver::add_non_viable(pvar v, rational const& val) {
bdd value = m_bdd.mk_true();
for (unsigned k = size(var); k-- > 0; )
for (unsigned k = size(v); k-- > 0; )
value &= val.get_bit(k) ? m_bdd.mk_var(k) : m_bdd.mk_nvar(k);
m_viable[var] &= !value;
m_viable[v] &= !value;
}
lbool solver::find_viable(unsigned var, rational & val) {
lbool solver::find_viable(pvar v, rational & val) {
val = 0;
bdd viable = m_viable[var];
bdd viable = m_viable[v];
if (viable.is_false())
return l_false;
unsigned num_vars = 0;
@ -68,7 +68,7 @@ namespace polysat {
viable = viable.lo();
++num_vars;
}
if (num_vars == size(var))
if (num_vars == size(v))
return l_true;
return l_undef;
}
@ -86,6 +86,7 @@ namespace polysat {
m_dm(m_value_manager, m_alloc),
m_vdeps(m_dm),
m_conflict_dep(nullptr, m_dm),
m_stash_dep(nullptr, m_dm),
m_free_vars(m_activity) {
}
@ -103,7 +104,7 @@ namespace polysat {
}
unsigned solver::add_var(unsigned sz) {
unsigned v = m_viable.size();
pvar v = m_viable.size();
m_value.push_back(rational::zero());
m_justification.push_back(justification::unassigned());
m_viable.push_back(m_bdd.mk_true());
@ -119,7 +120,7 @@ namespace polysat {
void solver::del_var() {
// TODO also remove v from all learned constraints.
unsigned v = m_viable.size() - 1;
pvar v = m_viable.size() - 1;
m_free_vars.del_var_eh(v);
m_viable.pop_back();
m_vdeps.pop_back();
@ -165,18 +166,17 @@ namespace polysat {
// save for later
}
void solver::assign(unsigned var, unsigned index, bool value, unsigned dep) {
m_viable[var] &= value ? m_bdd.mk_var(index) : m_bdd.mk_nvar(index);
add_viable_dep(var, mk_dep(dep));
if (m_viable[var].is_false()) {
void solver::assign(pvar v, unsigned index, bool value, unsigned dep) {
m_viable[v] &= value ? m_bdd.mk_var(index) : m_bdd.mk_nvar(index);
add_viable_dep(v, mk_dep(dep));
if (m_viable[v].is_false()) {
// TBD: set conflict
}
}
void solver::add_viable_dep(unsigned var, p_dependency* dep) {
if (!dep)
return;
m_vdeps[var] = m_dm.mk_join(m_vdeps.get(var), dep);
void solver::add_viable_dep(pvar v, p_dependency* dep) {
if (dep)
m_vdeps[v] = m_dm.mk_join(m_vdeps.get(v), dep);
}
bool solver::can_propagate() {
@ -189,7 +189,7 @@ namespace polysat {
propagate(m_search[m_qhead++]);
}
void solver::propagate(unsigned v) {
void solver::propagate(pvar v) {
auto& wlist = m_watch[v];
unsigned i = 0, j = 0, sz = wlist.size();
for (; i < sz && !is_conflict(); ++i)
@ -200,7 +200,7 @@ namespace polysat {
wlist.shrink(j);
}
bool solver::propagate(unsigned v, constraint& c) {
bool solver::propagate(pvar v, constraint& c) {
switch (c.kind()) {
case ckind_t::eq_t:
return propagate_eq(v, c);
@ -213,7 +213,7 @@ namespace polysat {
return false;
}
bool solver::propagate_eq(unsigned v, constraint& c) {
bool solver::propagate_eq(pvar v, constraint& c) {
SASSERT(c.kind() == ckind_t::eq_t);
SASSERT(!c.vars().empty());
auto var = m_vars[v].var();
@ -271,9 +271,9 @@ namespace polysat {
return false;
}
void solver::propagate(unsigned var, rational const& val, constraint& c) {
if (is_viable(var, val))
assign_core(var, val, justification::propagation(m_level));
void solver::propagate(pvar v, rational const& val, constraint& c) {
if (is_viable(v, val))
assign_core(v, val, justification::propagation(m_level));
else
set_conflict(c);
}
@ -306,11 +306,12 @@ namespace polysat {
void solver::pop_assignment() {
while (!m_search.empty() && m_justification[m_search.back()].level() > m_level) {
undo_var(m_search.back());
pop_search();
m_search.pop_back();
m_sub.pop_back();
}
}
void solver::undo_var(unsigned v) {
void solver::undo_var(pvar v) {
m_justification[v] = justification::unassigned();
m_free_vars.unassign_var_eh(v);
m_cjust[v].reset();
@ -318,16 +319,6 @@ namespace polysat {
m_viable[v] = m_bdd.mk_true(); // TBD does not work with external bit-assignments
}
void solver::pop_search() {
m_search.pop_back();
m_sub.pop_back();
}
void solver::push_search(unsigned var, rational const& val) {
m_search.push_back(var);
m_value[var] = val;
m_sub.push_back(std::make_pair(var, val));
}
void solver::add_watch(constraint& c) {
auto const& vars = c.vars();
@ -345,7 +336,7 @@ namespace polysat {
erase_watch(vars[1], c);
}
void solver::erase_watch(unsigned v, constraint& c) {
void solver::erase_watch(pvar v, constraint& c) {
if (v == null_var)
return;
auto& wlist = m_watch[v];
@ -360,27 +351,32 @@ namespace polysat {
}
void solver::decide() {
rational val;
SASSERT(can_decide());
unsigned var = m_free_vars.next_var();
switch (find_viable(var, val)) {
decide(m_free_vars.next_var());
}
void solver::decide(pvar v) {
rational val;
switch (find_viable(v, val)) {
case l_false:
set_conflict(var);
set_conflict(v);
break;
case l_true:
assign_core(var, val, justification::propagation(m_level));
assign_core(v, val, justification::propagation(m_level));
break;
case l_undef:
push_level();
assign_core(var, val, justification::decision(m_level));
assign_core(v, val, justification::decision(m_level));
break;
}
}
void solver::assign_core(unsigned var, rational const& val, justification const& j) {
SASSERT(is_viable(var, val));
push_search(var, val);
m_justification[var] = j;
void solver::assign_core(pvar v, rational const& val, justification const& j) {
SASSERT(is_viable(v, val));
m_search.push_back(v);
m_value[v] = val;
m_sub.push_back(std::make_pair(v, val));
m_justification[v] = j;
}
void solver::set_conflict(constraint& c) {
@ -389,7 +385,7 @@ namespace polysat {
m_conflict_dep = nullptr;
}
void solver::set_conflict(unsigned v) {
void solver::set_conflict(pvar v) {
SASSERT(m_conflict_cs.empty());
m_conflict_cs.append(m_cjust[v]);
m_conflict_dep = m_vdeps.get(v);
@ -422,7 +418,7 @@ namespace polysat {
vector<pdd> ps = init_conflict();
for (unsigned i = m_search.size(); i-- > 0; ) {
unsigned v = m_search[i];
pvar v = m_search[i];
if (!is_marked(v))
continue;
justification& j = m_justification[v];
@ -512,7 +508,7 @@ namespace polysat {
* We add 'p == 0' as a lemma. The lemma depends on the dependencies used
* to derive p, and the level of the lemma is the maximal level of the dependencies.
*/
void solver::learn_lemma(unsigned v, pdd const& p) {
void solver::learn_lemma(pvar v, pdd const& p) {
SASSERT(m_conflict_level <= m_justification[v].level());
constraint* c = constraint::eq(m_conflict_level, p, m_conflict_dep);
m_cjust[v].push_back(c);
@ -530,28 +526,17 @@ namespace polysat {
unstash_deps(v);
add_non_viable(v, m_value[v]);
add_viable_dep(v, m_conflict_dep);
rational value;
switch (find_viable(v, value)) {
case l_true:
assign_core(v, value, justification::propagation(m_level));
break;
case l_undef:
push_level();
assign_core(v, value, justification::decision(m_level));
break;
case l_false:
set_conflict(v);
break;
}
decide(v);
}
void solver::stash_deps(unsigned v) {
// save vdeps[v] and cjust[v] aside
// they are removed by backtracking
void solver::stash_deps(pvar v) {
m_stash_dep = m_vdeps.get(v);
std::swap(m_stash_just, m_cjust[v]);
}
void solver::unstash_deps(unsigned v) {
// retrieve saved vdeps[v] and cjust[v]
void solver::unstash_deps(pvar v) {
m_vdeps[v] = m_stash_dep;
std::swap(m_stash_just, m_cjust[v]);
}
void solver::backjump(unsigned new_level) {
@ -565,7 +550,7 @@ namespace polysat {
* producing polynomial that isolates v to lowest degree
* and lowest power of 2.
*/
pdd solver::isolate(unsigned v, vector<pdd> const& ps) {
pdd solver::isolate(pvar v, vector<pdd> const& ps) {
pdd p = ps[0];
for (unsigned i = ps.size(); i-- > 1; ) {
// TBD reduce with respect to v
@ -576,7 +561,7 @@ namespace polysat {
/**
* Return residue of superposing p and q with respect to v.
*/
pdd solver::resolve(unsigned v, vector<pdd> const& ps) {
pdd solver::resolve(pvar v, vector<pdd> const& ps) {
auto const& cs = m_cjust[v];
pdd r = isolate(v, ps);
auto degree = r.degree(v);

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

@ -31,9 +31,10 @@ namespace polysat {
class solver;
typedef dd::pdd pdd;
typedef dd::bdd bdd;
typedef unsigned pvar;
const unsigned null_dependency = UINT_MAX;
const unsigned null_var = UINT_MAX;
const pvar null_var = UINT_MAX;
struct dep_value_manager {
void inc_ref(unsigned) {}
@ -124,9 +125,11 @@ namespace polysat {
dep_value_manager m_value_manager;
small_object_allocator m_alloc;
poly_dep_manager m_dm;
var_queue m_free_vars;
p_dependency_ref m_conflict_dep;
ptr_vector<constraint> m_conflict_cs;
p_dependency_ref m_stash_dep;
constraints m_stash_just;
var_queue m_free_vars;
// Per constraint state
scoped_ptr_vector<constraint> m_constraints;
@ -145,7 +148,7 @@ namespace polysat {
// search state that lists assigned variables
unsigned_vector m_search;
vector<std::pair<unsigned, rational>> m_sub;
vector<std::pair<pvar, rational>> m_sub;
unsigned m_qhead { 0 };
unsigned m_level { 0 };
@ -156,21 +159,21 @@ namespace polysat {
// conflict state
ptr_vector<constraint> m_conflict;
unsigned size(unsigned var) const { return m_size[var]; }
unsigned size(pvar v) const { return m_size[v]; }
/**
* check if value is viable according to m_viable.
*/
bool is_viable(unsigned var, rational const& val);
bool is_viable(pvar v, rational const& val);
/**
* register that val is non-viable for var.
*/
void add_non_viable(unsigned var, rational const& val);
void add_non_viable(pvar v, rational const& val);
/**
* Add dependency for variable viable range.
*/
void add_viable_dep(unsigned var, p_dependency* dep);
void add_viable_dep(pvar v, p_dependency* dep);
/**
@ -179,7 +182,7 @@ namespace polysat {
* l_true - there is only one viable value left.
* l_undef - there are multiple viable values, return a guess
*/
lbool find_viable(unsigned var, rational & val);
lbool find_viable(pvar v, rational & val);
/**
* undo trail operations for backtracking.
@ -196,40 +199,38 @@ namespace polysat {
void pop_assignment();
void pop_constraints(scoped_ptr_vector<constraint>& cs);
void push_search(unsigned v, rational const& val);
void pop_search();
void assign_core(pvar v, rational const& val, justification const& j);
void assign_core(unsigned var, rational const& val, justification const& j);
bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }
bool is_assigned(unsigned var) const { return !m_justification[var].is_unassigned(); }
void propagate(unsigned v);
bool propagate(unsigned v, constraint& c);
bool propagate_eq(unsigned v, constraint& c);
void propagate(unsigned var, rational const& val, constraint& c);
void erase_watch(unsigned v, constraint& c);
void propagate(pvar v);
bool propagate(pvar v, constraint& c);
bool propagate_eq(pvar v, constraint& c);
void propagate(pvar v, rational const& val, constraint& c);
void erase_watch(pvar v, constraint& c);
void erase_watch(constraint& c);
void add_watch(constraint& c);
void set_conflict(constraint& c);
void set_conflict(unsigned v);
void set_conflict(pvar v);
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; }
bool is_marked(pvar v) const { return m_clock == m_marks[v]; }
void set_mark(pvar v) { m_marks[v] = m_clock; }
unsigned m_conflict_level { 0 };
pdd isolate(unsigned v, vector<pdd> const& ps);
pdd resolve(unsigned v, vector<pdd> const& ps);
pdd isolate(pvar v, vector<pdd> const& ps);
pdd resolve(pvar v, vector<pdd> const& ps);
bool can_decide() const { return !m_free_vars.empty(); }
void decide();
void decide(pvar v);
void stash_deps(unsigned v);
void unstash_deps(unsigned 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); }
@ -242,9 +243,9 @@ namespace polysat {
void backtrack(unsigned i);
void report_unsat();
void revert_decision(unsigned i);
void learn_lemma(unsigned v, pdd const& p);
void learn_lemma(pvar v, pdd const& p);
void backjump(unsigned new_level);
void undo_var(unsigned v);
void undo_var(pvar v);
void add_lemma(constraint* c);
@ -276,12 +277,12 @@ namespace polysat {
/**
* Add variable with bit-size.
*/
unsigned add_var(unsigned sz);
pvar add_var(unsigned sz);
/**
* Create polynomial terms
*/
pdd var(unsigned v) { return m_vars[v]; }
pdd var(pvar v) { return m_vars[v]; }
/**
* Add polynomial constraints
@ -295,7 +296,7 @@ namespace polysat {
void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency);
void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency);
void assign(unsigned var, unsigned index, bool value, unsigned dep);
void assign(pvar v, unsigned index, bool value, unsigned dep);
/**
* main state transitions.