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

working on viable explanations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-02 16:20:13 -08:00
parent b706434282
commit 21236dc80a
5 changed files with 53 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/dd/dd_pdd.cpp
View file

@ -1860,14 +1860,11 @@ namespace dd {
return (*this) * rational::power_of_two(n);
}
bool pdd::has_unit(pdd& x, pdd& rest) const {
if (is_val())
return false;
bool pdd::has_unit(pdd& x) const {
pdd r = *this;
while (!r.is_val()) {
if (r.hi().is_one()) {
x = m->mk_var(r.var());
rest = *this - x;
return true;
}
r = r.lo();

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

@ -441,7 +441,7 @@ namespace dd {
bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); }
bool is_offset() const { return !is_val() && lo().is_val() && hi().is_one(); }
bool is_binary() const { return m->is_binary(root); }
bool has_unit(pdd& x, pdd& rest) const;
bool has_unit(pdd& x) const;
bool is_monomial() const { return m->is_monomial(root); }
bool is_univariate() const { return m->is_univariate(root); }
bool is_univariate_in(unsigned v) const { return m->is_univariate_in(root, v); }

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

@ -84,6 +84,7 @@ namespace polysat {
}
find_t viable::find_viable(pvar v, rational& lo) {
verbose_stream() << "find viable v" << v << " starting with " << lo << "\n";
rational hi;
switch (find_viable(v, lo, hi)) {
case l_true:
@ -103,7 +104,9 @@ namespace polysat {
lbool viable::find_viable(pvar v, rational& val1, rational& val2) {
m_explain.reset();
m_ineqs.reset();
m_var = v;
m_value = nullptr;
m_num_bits = c.size(v);
m_fixed_bits.reset(v);
init_overlaps(v);
@ -128,6 +131,9 @@ namespace polysat {
}
else
val2 = val1 + 1;
// instead of m_value use linked list of entries?
m_value = alloc(pdd, c.value(val2, m_num_bits));
r = next_viable(val2);
@ -231,14 +237,29 @@ namespace polysat {
break;
// TODO check if admitted: layer.entries = e;
m_explain.push_back(e);
if (e->interval.is_full())
return l_false;
auto hi = e->interval.hi_val();
if (wrapped && start <= hi)
return l_false;
if (hi < e->interval.lo_val())
return l_false;
auto hi_val = e->interval.hi_val();
auto lo_val = e->interval.lo_val();
auto hi = e->interval.hi();
auto lo = e->interval.lo();
if (!m_value)
m_value = alloc(pdd, lo);
m_ineqs.push_back({ *m_value, lo, hi });
if (wrapped && start <= hi_val) {
verbose_stream() << "WRAPPED\n";
return l_false;
}
if (hi_val < lo_val)
wrapped = true;
val1 = hi;
val1 = hi_val;
m_value = alloc(pdd, hi);
SASSERT(val1 < p2b);
}
SASSERT(val1 < p2b);
@ -533,10 +554,17 @@ namespace polysat {
result.push_back(offset_claim(m_var, {e->var, 0}));
seen.insert(index.id);
for (auto const& sc : e->side_cond)
result.push_back(c.propagate(sc, c.explain_eval(sc)));
result.push_back(c.propagate(sc, c.explain_eval(sc)));
auto const& [sc, d, value] = c.m_constraint_index[index.id];
result.push_back(d);
}
for (auto [t, lo, hi] : m_ineqs) {
auto sc = cs.ult(t - lo, hi - lo);
verbose_stream() << "Overlap " << t << " in [" << lo << ", " << hi << "[: " << sc << "\n";
if (!sc.is_always_true())
result.push_back(c.propagate(sc, c.explain_eval(sc)));
}
result.append(m_fixed_bits.explain());
TRACE("bv", tout << "viable-explain v" << m_var << " - " << result.size() << "\n");
return result;
@ -656,6 +684,7 @@ namespace polysat {
}
if (ne->interval.is_full()) {
m_explain.reset();
m_ineqs.reset();
m_explain.push_back(ne);
m_fixed_bits.reset();
m_var = v;

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

@ -85,11 +85,15 @@ namespace polysat {
entry* get_entries(unsigned bit_width) const { layer const* l = get_layer(bit_width); return l ? l->entries : nullptr; }
};
// short for t in [lo,hi[
struct interval_member {
pdd t, lo, hi;
};
ptr_vector<entry> m_alloc;
vector<layers> m_units; // set of viable values based on unit multipliers, layered by bit-width in descending order
ptr_vector<entry> m_equal_lin; // entries that have non-unit multipliers, but are equal
ptr_vector<entry> m_diseq_lin; // entries that have distinct non-zero multipliers
ptr_vector<entry> m_diseq_lin; // entries that have distinct non-zero multipliers
vector<interval_member> m_ineqs; // inequalities to justify that values are not viable.
ptr_vector<entry> m_explain; // entries that explain the current propagation or conflict
bool well_formed(entry* e);
@ -126,6 +130,7 @@ namespace polysat {
bool refine_equal_lin(pvar v, rational const& val);
pvar m_var = null_var;
scoped_ptr<pdd> m_value; // the current symbolid value being checked for viability.
unsigned m_num_bits = 0;
fixed_bits m_fixed_bits;
offset_slices m_overlaps;

17
src/sat/smt/polysat_solver.cpp
View file

@ -383,25 +383,24 @@ namespace polysat {
expr_ref solver::constraint2expr(signed_constraint const& sc) {
expr_ref result(m);
switch (sc.op()) {
case ckind_t::ule_t: {
case ckind_t::ule_t: {
auto p = sc.to_ule().lhs();
auto q = sc.to_ule().rhs();
pdd x = p, r = p;
if (q.is_zero() && p.has_unit(x, r)) {
pdd x = p;
if (q.is_zero() && p.has_unit(x)) {
auto l = pdd2expr(x);
auto h = pdd2expr(-r);
result = m.mk_eq(l, h);
auto r = pdd2expr(x - p);
result = m.mk_eq(l, r);
}
else {
auto l = pdd2expr(p);
auto h = pdd2expr(q);
auto r = pdd2expr(q);
if (p == q)
result = m.mk_true();
else if (q.is_zero())
result = m.mk_eq(l, h);
result = m.mk_eq(l, r);
else
result = bv.mk_ule(l, h);
result = bv.mk_ule(l, r);
}
if (sc.sign())
result = m.mk_not(result);