mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

inline propagation when adding new viable

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-08 20:31:14 -08:00
parent e26d597917
commit cc4ed602e5
5 changed files with 57 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

43
src/sat/smt/polysat/core.cpp
View file

@ -164,11 +164,7 @@ namespace polysat {
viable_conflict(m_var);
return l_false;
case find_t::singleton: {
auto p = var2pdd(m_var).mk_var(m_var);
auto sc = m_constraints.eq(p, var_value);
TRACE("bv", tout << "check-propagate v" << m_var << " := " << var_value << " " << sc << "\n");
auto d = s.propagate(sc, m_viable.explain(), "viable-propagate");
propagate_assignment(m_var, var_value, d);
viable_propagate(m_var, var_value);
return l_false;
}
case find_t::multiple: {
@ -301,6 +297,14 @@ namespace polysat {
decay_activity();
}
void core::viable_propagate(pvar v, rational const& var_value) {
auto p = var2pdd(v).mk_var(v);
auto sc = m_constraints.eq(p, var_value);
TRACE("bv", tout << "check-propagate v" << v << " := " << var_value << " " << sc << "\n");
auto d = s.propagate(sc, m_viable.explain(), "viable-propagate");
propagate_assignment(v, var_value, d);
}
void core::propagate_assignment(constraint_id idx) {
auto [sc, dep, value] = m_constraint_index[idx.id];
@ -333,8 +337,18 @@ namespace polysat {
return;
v = w;
}
if (v != null_var && !m_viable.add_unitary(v, idx, m_values[v]))
viable_conflict(v);
if (v != null_var) {
switch (m_viable.add_unitary(v, idx, m_values[v])) {
case find_t::empty:
viable_conflict(v);
break;
case find_t::singleton:
viable_propagate(v, m_values[v]);
break;
default:
break;
}
}
else if (v == null_var && weak_eval(sc) == l_false) {
auto ex = explain_weak_eval(sc);
ex.push_back(dep);
@ -388,9 +402,18 @@ namespace polysat {
auto v1 = vars[1];
if (!is_assigned(v0) || is_assigned(v1))
continue;
// detect unitary, add to viable, detect conflict?
if (value != l_undef && !m_viable.add_unitary(v1, { idx }, m_values[v]))
viable_conflict(v1);
if (value != l_undef) {
switch (m_viable.add_unitary(v1, { idx }, m_values[v1])) {
case find_t::empty:
viable_conflict(v1);
break;
case find_t::singleton:
viable_propagate(v1, m_values[v1]);
break;
default:
break;
}
}
}
SASSERT(m_watch[v].size() == sz && "size of watch list was not changed");
m_watch[v].shrink(j);

1
src/sat/smt/polysat/core.h
View file

@ -79,6 +79,7 @@ namespace polysat {
void del_var();
void viable_conflict(pvar v);
void viable_propagate(pvar v, rational const& var_value);
bool is_assigned(pvar v) { return !m_justification[v].is_null(); }
void propagate_assignment(constraint_id idx);

2
src/sat/smt/polysat/forbidden_intervals.h
View file

@ -25,7 +25,7 @@ namespace polysat {
struct fi_record {
eval_interval interval;
vector<signed_constraint> side_cond;
vector<signed_constraint> src; // only units may have multiple src (as they can consist of contracted bit constraints)
vector<signed_constraint> src; // there is either 0 or 1 src.
vector<dependency> deps;
rational coeff;
unsigned bit_width = 0; // number of lower bits; TODO: should move this to viable::entry; where the coeff/bit-width is adapted accordingly

39
src/sat/smt/polysat/viable.cpp
View file

@ -103,10 +103,10 @@ namespace polysat {
if (n)
continue;
++rounds;
if (!check_fixed_bits(v, lo))
continue;
++rounds;
if (!check_disequal_lin(v, lo))
continue;
if (!check_equal_lin(v, lo))
@ -125,8 +125,6 @@ namespace polysat {
m_overlaps.reset();
c.get_bitvector_suffixes(v, m_overlaps);
std::sort(m_overlaps.begin(), m_overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.v) < c.size(y.v); });
//display_state(verbose_stream());
//display(verbose_stream());
}
@ -518,18 +516,21 @@ namespace polysat {
*/
dependency_vector viable::explain() {
dependency_vector result;
uint_set seen;
auto last = m_explain.back();
auto after = last;
TRACE("bv", display_explain(tout));
auto unmark = [&]() {
for (auto e : m_explain)
e.e->marked = false;
};
auto explain_entry = [&](entry* e) {
auto index = e->constraint_index;
if (!index.is_null() && seen.contains(index.id))
if (e->marked)
return;
if (!index.is_null())
seen.insert(index.id);
e->marked = true;
if (m_var != e->var)
result.push_back(offset_claim(m_var, { e->var, 0 }));
for (auto const& sc : e->side_cond)
@ -542,6 +543,7 @@ namespace polysat {
if (last.e->interval.is_full()) {
explain_entry(last.e);
SASSERT(m_explain.size() == 1);
unmark();
return result;
}
@ -564,6 +566,7 @@ namespace polysat {
auto sc = cs.eq(last.e->interval.hi() + 1, first.e->interval.lo());
result.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
}
unmark();
return result;
}
@ -638,29 +641,29 @@ namespace polysat {
/*
* Register constraint at index 'idx' as unitary in v.
*/
bool viable::add_unitary(pvar v, constraint_id idx, rational& var_value) {
find_t viable::add_unitary(pvar v, constraint_id idx, rational& var_value) {
if (c.is_assigned(v))
return true;
return find_t::multiple;
auto [sc, d, truth_value] = c.m_constraint_index[idx.id];
SASSERT(truth_value != l_undef);
if (truth_value == l_false)
sc = ~sc;
if (!sc.is_linear())
return true;
return find_t::multiple;
entry* ne = alloc_entry(v, idx);
if (!m_forbidden_intervals.get_interval(sc, v, *ne)) {
m_alloc.push_back(ne);
return true;
return find_t::multiple;
}
// verbose_stream() << "v" << v << " " << sc << " " << ne->interval << "\n";
if (ne->interval.is_currently_empty()) {
m_alloc.push_back(ne);
return true;
return find_t::multiple;
}
if (ne->coeff == 1)
@ -739,7 +742,7 @@ namespace polysat {
IF_VERBOSE(0, verbose_stream() << "Check: always true " << "x*" << ne->coeff << " not in " << ne->interval << " " << new_hi << "\n");
// empty
m_alloc.push_back(ne);
return true;
return find_t::multiple;
}
ne->coeff = 1;
@ -752,15 +755,9 @@ namespace polysat {
m_explain.push_back({ ne, rational::zero() });
m_fixed_bits.reset();
m_var = v;
return false;
return find_t::empty;
}
switch (find_viable(v, var_value)) {
case find_t::empty:
return false;
default:
break;
}
return true;
return find_viable(v, var_value);
}
void viable::ensure_var(pvar v) {

6
src/sat/smt/polysat/viable.h
View file

@ -49,10 +49,11 @@ namespace polysat {
struct entry final : public dll_base<entry>, public fi_record {
/// whether the entry has been created by refinement (from constraints in 'fi_record::src')
bool refined = false;
/// whether the entry is part of the current set of intervals, or stashed away for backtracking
/// whether the entry is part of the current set of intervals, or stashed away for backtracking
bool active = true;
pvar var = null_var;
constraint_id constraint_index;
bool marked = false;
void reset() {
// dll_base<entry>::init(this); // we never did this in alloc_entry either
@ -61,6 +62,7 @@ namespace polysat {
active = true;
var = null_var;
constraint_index = constraint_id::null();
marked = false;
}
};
@ -164,7 +166,7 @@ namespace polysat {
/*
* Register constraint at index 'idx' as unitary in v.
*/
bool add_unitary(pvar v, constraint_id, rational& value);
find_t add_unitary(pvar v, constraint_id, rational& value);
/*
* Ensure data-structures tracking variable v.