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

bugfixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-29 15:13:11 -08:00
parent 97225b7d8f
commit 03e012c1d8
14 changed files with 167 additions and 139 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/euf/euf_bv_plugin.cpp
View file

@ -97,7 +97,10 @@ namespace euf {
enode* bv_plugin::mk_value(rational const& v, unsigned sz) {
auto e = bv.mk_numeral(v, sz);
return mk(e, 0, nullptr);
auto n = mk(e, 0, nullptr);
if (m_ensure_th_var)
m_ensure_th_var(n);
return n;
}
void bv_plugin::propagate_merge(enode* x, enode* y) {
@ -331,7 +334,7 @@ namespace euf {
v = div(v, rational::power_of_two(lo));
if (hi + 1 != width(n))
v = mod(v, rational::power_of_two(hi + 1));
return mk(bv.mk_numeral(v, hi - lo + 1), 0, nullptr);
return mk_value(v, hi - lo + 1);
}
return mk(bv.mk_extract(hi, lo, n->get_expr()), 1, &n);
}

7
src/ast/euf/euf_bv_plugin.h
View file

@ -41,11 +41,10 @@ namespace euf {
bv_util bv;
slice_info_vector m_info; // indexed by enode::get_id()
enode_vector m_xs, m_ys;
std::function<void(enode*)> m_ensure_th_var;
bool is_concat(enode* n) const { return bv.is_concat(n->get_expr()); }
bool is_concat(enode* n, enode*& a, enode*& b) { return is_concat(n) && (a = n->get_arg(0), b = n->get_arg(1), true); }
bool is_extract(enode* n, unsigned& lo, unsigned& hi) { expr* body; return bv.is_extract(n->get_expr(), lo, hi, body); }
@ -109,6 +108,8 @@ namespace euf {
void propagate() override;
void undo() override;
void set_ensure_th_var(std::function<void(enode*)>& f) { m_ensure_th_var = f; }
std::ostream& display(std::ostream& out) const override;

2
src/ast/euf/euf_egraph.cpp
View file

@ -160,7 +160,7 @@ namespace euf {
}
void egraph::add_th_eq(theory_id id, theory_var v1, theory_var v2, enode* c, enode* r) {
TRACE("euf_verbose", tout << "eq: " << v1 << " == " << v2 << "\n";);
TRACE("euf", tout << "eq: " << v1 << " == " << v2 << " - " << bpp(c) << " == " << bpp(r) << "\n";);
m_new_th_eqs.push_back(th_eq(id, v1, v2, c, r));
m_updates.push_back(update_record(update_record::new_th_eq()));
++m_stats.m_num_th_eqs;

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

@ -46,6 +46,7 @@ namespace polysat {
virtual lbool eval(assignment const& a) const = 0;
virtual void activate(core& c, bool sign, dependency const& d) = 0;
virtual void propagate(core& c, lbool value, dependency const& d) = 0;
virtual bool is_linear() const { return false; }
};
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
@ -74,14 +75,15 @@ namespace polysat {
bool is_always_false() const { return eval() == l_false; }
bool is_currently_true(core& c) const;
bool is_currently_false(core& c) const;
bool is_linear() const { return m_constraint->is_linear(); }
lbool eval(assignment& a) const;
lbool eval() const { return m_sign ? ~m_constraint->eval() : m_constraint->eval();}
ckind_t op() const { return m_op; }
bool is_ule() const { return m_op == ule_t; }
bool is_umul_ovfl() const { return m_op == umul_ovfl_t; }
bool is_smul_fl() const { return m_op == smul_fl_t; }
ule_constraint const& to_ule() const { return *reinterpret_cast<ule_constraint*>(m_constraint); }
umul_ovfl_constraint const& to_umul_ovfl() const { return *reinterpret_cast<umul_ovfl_constraint*>(m_constraint); }
ule_constraint const& to_ule() const { SASSERT(is_ule()); return *reinterpret_cast<ule_constraint*>(m_constraint); }
umul_ovfl_constraint const& to_umul_ovfl() const { SASSERT(is_umul_ovfl()); return *reinterpret_cast<umul_ovfl_constraint*>(m_constraint); }
bool is_eq(pvar& v, rational& val);
std::ostream& display(std::ostream& out) const;
};

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

@ -168,8 +168,7 @@ namespace polysat {
switch (m_viable.find_viable(m_var, m_value)) {
case find_t::empty:
TRACE("bv", tout << "viable-conflict v" << m_var << "\n");
s.set_conflict(m_viable.explain(), "viable-conflict");
viable_conflict(m_var);
return sat::check_result::CR_CONTINUE;
case find_t::singleton: {
auto p = var2pdd(m_var).mk_var(m_var);
@ -180,7 +179,6 @@ namespace polysat {
return sat::check_result::CR_CONTINUE;
}
case find_t::multiple: {
do {
try_again:
dependency d = null_dependency;
@ -273,6 +271,12 @@ namespace polysat {
return true;
}
void core::viable_conflict(pvar v) {
TRACE("bv", tout << "viable-conflict v" << v << "\n");
m_var_queue.activity_increased_eh(v);
s.set_conflict(m_viable.explain(), "viable-conflict");
}
void core::propagate_assignment(constraint_id idx) {
auto [sc, dep, value] = m_constraint_index[idx.id];
@ -280,6 +284,10 @@ namespace polysat {
if (value == l_false)
sc = ~sc;
TRACE("bv", tout << "propagate " << sc << " using " << dep << " := " << value << "\n");
if (sc.is_always_false()) {
s.set_conflict({dep}, "infeasible assignment");
return;
}
if (sc.is_eq(m_var, m_value))
propagate_assignment(m_var, m_value, dep);
else
@ -301,7 +309,7 @@ namespace polysat {
v = w;
}
if (v != null_var && !m_viable.add_unitary(v, idx))
s.set_conflict(m_viable.explain(), "viable-conflict");
viable_conflict(v);
}
void core::propagate_assignment(pvar v, rational const& value, dependency dep) {
@ -353,8 +361,8 @@ namespace polysat {
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}))
s.set_conflict(m_viable.explain(), "viable-conflict");
if (value != l_undef && !m_viable.add_unitary(v1, { idx }))
viable_conflict(v1);
}
SASSERT(m_watch[v].size() == sz && "size of watch list was not changed");
m_watch[v].shrink(j);

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

@ -77,6 +77,8 @@ namespace polysat {
void del_var();
void viable_conflict(pvar v);
bool is_assigned(pvar v) { return !m_justification[v].is_null(); }
void propagate_assignment(constraint_id idx);
void propagate_eval(constraint_id idx);

1
src/sat/smt/polysat/saturation.cpp
View file

@ -167,7 +167,6 @@ namespace polysat {
// Ovfl(x, y) & ~Ovfl(y, z) ==> x > z
void saturation::try_umul_ovfl(pvar v, umul_ovfl const& sc) {
auto p = sc.p(), q = sc.q();
auto& C = c.cs();
auto match_mul_arg = [&](auto const& sc2) {

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

@ -53,7 +53,7 @@ namespace polysat {
};
struct constraint_iterator {
core& c;
std::function<bool(signed_constraint const& sc)> const& m_filter;
std::function<bool(signed_constraint const& sc)> m_filter;
constraint_iterator(core& c, std::function<bool(signed_constraint const& sc)> const& filter) :
c(c), m_filter(filter) {}
constraint_filter begin() const { return constraint_filter(c, m_filter, 0); }

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

@ -35,6 +35,7 @@ namespace polysat {
std::ostream& display(std::ostream& out) const override;
lbool eval() const override;
lbool eval(assignment const& a) const override;
bool is_linear() const override { return lhs().is_linear() && rhs().is_linear(); }
void activate(core& c, bool sign, dependency const& dep);
void propagate(core& c, lbool value, dependency const& dep) {}
bool is_eq() const { return m_rhs.is_zero(); }

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

@ -38,6 +38,7 @@ namespace polysat {
lbool eval(assignment const& a) const override;
void activate(core& c, bool sign, dependency const& dep) override;
void propagate(core& c, lbool value, dependency const& dep) override;
bool is_linear() const override { return p().is_linear() && q().is_linear(); }
};

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

@ -183,78 +183,56 @@ namespace polysat {
}
/*
* v in [lo, hi[:
* - hi >= v: forward(v) := hi
* - hi < v: l_false
* 2^k v in [lo, hi[:
* - hi > 2^k v: forward(v) := hi//2^k + 2^k(v//2^k)
* - hi <= 2^k v: forward(v) := hi//2^k + 2^k(v//2^k + 1) unless it overflows.
* w is a suffix of v of width w.width <= v.width with forbidden 2^l w not in [lo, hi[ and 2^l v[w.width-1:0] in [lo, hi[.
* - set k := l + v.width - w.width, lo' := 2^{v.width-w.width} lo, hi' := 2^{v.width-w.width} hi.
* In either case we are checking a constraint $v[u-1:0]\not\in[lo, hi[$
* where $u := w'-k-1$ and using it to compute $\forward(v)$.
* Thus, suppose $v[u-1:0] \in [lo, hi[$.
* - $lo < hi$: $\forward(v) := \forward(2^u v[w-1:w-u] + hi)$.
* - $lo > hi$, $v[w-1:w-u]+1 = 2^{w-u}$: $\forward(v) := \bot$
* - $lo > hi$, $v[w-1:w-u]+1 < 2^{w-u}$: $\forward(v) := \forward(2^u (v[w-1:w-u]+1) + hi)$
*/
lbool viable::next_viable_layer(pvar w, layer& layer, rational& val) {
if (!layer.entries)
return l_true;
unsigned v_width = m_num_bits;
unsigned w_width = c.size(w);
unsigned l = w_width - layer.bit_width;
SASSERT(v_width >= w_width);
SASSERT(layer.bit_width <= w_width);
unsigned w_width = c.size(w);
unsigned b_width = layer.bit_width;
SASSERT(b_width <= w_width);
SASSERT(w_width <= v_width);
bool is_zero = val.is_zero(), wrapped = false;
rational val1 = val;
rational const& p2l = rational::power_of_two(l);
rational const& p2w = rational::power_of_two(w_width);
while (true) {
if (l > 0)
val1 *= p2l;
if (w_width < v_width || l > 0)
val1 = mod(val1, p2w);
rational const& p2v = rational::power_of_two(v_width);
rational const& p2b = rational::power_of_two(b_width);
if (b_width < v_width)
val1 = mod(val1, p2b);
rational start = val1;
while (true) {
auto e = find_overlap(val1, layer.entries);
if (!e) {
if (l > 0)
val1 /= p2l;
break;
}
if (!e)
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 (hi < val1) {
if (is_zero)
return l_false;
if (w_width == v_width && l == 0)
return l_false;
// start from 0 and find the next viable value within this layer.
val1 = 0;
if (hi < e->interval.lo_val())
wrapped = true;
}
if (wrapped && start <= hi)
return l_false;
val1 = hi;
SASSERT(val1 < p2w);
// p2l * x = val1 = hi
if (l > 0)
val1 = hi / p2l;
SASSERT(val1.is_int());
SASSERT(val1 < p2b);
}
SASSERT(val1 < p2w);
if (w_width < v_width) {
if (l > 0)
NOT_IMPLEMENTED_YET();
rational val2 = val;
SASSERT(val1 < p2b);
if (b_width < v_width) {
rational val2 = clear_lower_bits(val, b_width);
if (wrapped) {
val2 = mod(div(val2, p2w) + 1, p2w) * p2w;
if (val2 == 0)
val2 += p2b;
if (val2 >= p2v)
return l_false;
}
else
val2 = clear_lower_bits(val2, w_width);
val = val1 + val2;
}
else if (l > 0) {
NOT_IMPLEMENTED_YET();
}
else
val = val1;
@ -264,7 +242,6 @@ namespace polysat {
// Find interval that contains 'val', or, if no such interval exists, null.
viable::entry* viable::find_overlap(rational const& val, entry* entries) {
SASSERT(entries);
// display_all(std::cerr << "entries:\n\t", 0, entries, "\n\t");
entry* const first = entries;
entry* e = entries;
do {
@ -557,6 +534,10 @@ namespace polysat {
if (value == l_false)
sc = ~sc;
if (!sc.is_linear()) {
return true;
}
entry* ne = alloc_entry(v, idx);
if (!m_forbidden_intervals.get_interval(sc, v, *ne)) {
m_alloc.push_back(ne);
@ -573,72 +554,88 @@ namespace polysat {
if (ne->coeff == 1)
intersect(v, ne);
else if (ne->coeff == -1)
insert(ne, v, m_diseq_lin, entry_kind::diseq_e);
insert(ne, v, m_diseq_lin, entry_kind::diseq_e);
else if (!ne->coeff.is_power_of_two())
insert(ne, v, m_equal_lin, entry_kind::equal_e);
else if (ne->interval.is_full())
insert(ne, v, m_equal_lin, entry_kind::equal_e);
else {
unsigned const w = c.size(v);
unsigned const k = ne->coeff.parity(w);
// unsigned const lo_parity = ne->interval.lo_val().parity(w);
// unsigned const hi_parity = ne->interval.hi_val().parity(w);
SASSERT(k > 0);
IF_VERBOSE(1, display_one(verbose_stream() << "try to reduce entry: ", v, ne) << "\n");
IF_VERBOSE(3, display_one(verbose_stream() << "try to reduce entry: ", v, ne) << "\n");
if (k > 0 && ne->coeff.is_power_of_two()) {
// reduction of coeff gives us a unit entry
//
// 2^k a x \not\in [ lo ; hi [
//
// new_lo = lo[w-1:k] if lo[k-1:0] = 0
// lo[w-1:k] + 1 otherwise
//
// new_hi = hi[w-1:k] if hi[k-1:0] = 0
// hi[w-1:k] + 1 otherwise
//
// Reference: Fig. 1 (dtrim) in BitvectorsMCSAT
//
pdd const& pdd_lo = ne->interval.lo();
pdd const& pdd_hi = ne->interval.hi();
rational const& lo = ne->interval.lo_val();
rational const& hi = ne->interval.hi_val();
// reduction of coeff gives us a unit entry
//
// 2^k x \not\in [ lo ; hi [
//
// new_lo = lo[w-1:k] if lo[k-1:0] = 0
// lo[w-1:k] + 1 otherwise
//
// new_hi = hi[w-1:k] if hi[k-1:0] = 0
// hi[w-1:k] + 1 otherwise
//
// Reference: Fig. 1 (dtrim) in BitvectorsMCSAT
//
//
// Suppose new_lo = new_hi
// Then since ne is not full, then lo != hi
// Cases
// lo < hi, 2^k|lo, new_lo = lo / 2^k != new_hi = hi / 2^k
// lo < hi, not 2^k|lo, 2^k|hi, new_lo = lo / 2^k + 1, new_hi = hi / 2^k
// new_lo = new_hi -> empty
// k = 3, lo = 1, hi = 8, new_lo = 1, new_hi = 1
// lo < hi, not 2^k|lo, not 2^k|hi, new_lo = lo / 2^k + 1, new_hi = hi / 2^k + 1
// new_lo = new_hi -> empty
// k = 3, lo = 1, hi = 2, new_lo = 1 div 2^3 + 1 = 1, new_hi = 2 div 2^3 + 1 = 1
// lo > hi
rational new_lo = machine_div2k(lo, k);
if (mod2k(lo, k).is_zero())
ne->side_cond.push_back(cs.eq(pdd_lo * rational::power_of_two(w - k)));
else {
new_lo += 1;
ne->side_cond.push_back(~cs.eq(pdd_lo * rational::power_of_two(w - k)));
}
pdd const& pdd_lo = ne->interval.lo();
pdd const& pdd_hi = ne->interval.hi();
rational const& lo = ne->interval.lo_val();
rational const& hi = ne->interval.hi_val();
rational new_hi = machine_div2k(hi, k);
if (mod2k(hi, k).is_zero())
ne->side_cond.push_back(cs.eq(pdd_hi * rational::power_of_two(w - k)));
else {
new_hi += 1;
ne->side_cond.push_back(~cs.eq(pdd_hi * rational::power_of_two(w - k)));
}
// we have to update also the pdd bounds accordingly, but it seems not worth introducing new variables for this eagerly
// new_lo = lo[:k] etc.
// TODO: for now just disable the FI-lemma if this case occurs
ne->valid_for_lemma = false;
if (new_lo == new_hi) {
// empty or full
// if (ne->interval.currently_contains(rational::zero()))
NOT_IMPLEMENTED_YET();
}
ne->coeff = machine_div2k(ne->coeff, k);
ne->interval = eval_interval::proper(pdd_lo, new_lo, pdd_hi, new_hi);
ne->bit_width -= k;
display_one(std::cerr << "reduced entry: ", v, ne) << "\n";
LOG("reduced entry to unit in bitwidth " << ne->bit_width);
intersect(v, ne);
rational new_lo = machine_div2k(lo, k);
pdd lo_eq = pdd_lo * rational::power_of_two(w - k);
if (mod2k(lo, k).is_zero()) {
if (!lo_eq.is_zero())
ne->side_cond.push_back(cs.eq(lo_eq));
}
else {
new_lo += 1;
new_lo = machine_div2k(new_lo, k);
if (!lo_eq.is_val() || lo_eq.is_zero())
ne->side_cond.push_back(~cs.eq(lo_eq));
}
rational new_hi = machine_div2k(hi, k);
pdd hi_eq = pdd_hi * rational::power_of_two(w - k);
if (mod2k(hi, k).is_zero()) {
if (!hi_eq.is_zero())
ne->side_cond.push_back(cs.eq(hi_eq));
}
else {
new_hi += 1;
new_hi = machine_div2k(new_hi, k);
if (!hi_eq.is_val() || hi_eq.is_zero())
ne->side_cond.push_back(~cs.eq(hi_eq));
}
// we have to update also the pdd bounds accordingly, but it seems not worth introducing new variables for this eagerly
// new_lo = lo[:k] etc.
if (new_lo == new_hi) {
// empty
verbose_stream() << "always true " << "x*" << ne->coeff << " not in " << ne->interval << "\n";
m_alloc.push_back(ne);
return true;
}
// TODO: later, can reduce according to shared_parity
// unsigned const shared_parity = std::min(coeff_parity, std::min(lo_parity, hi_parity));
insert(ne, v, m_equal_lin, entry_kind::equal_e);
ne->coeff = 1;
ne->interval = eval_interval::proper(pdd_lo, new_lo, pdd_hi, new_hi);
ne->bit_width -= k;
intersect(v, ne);
}
if (ne->interval.is_full()) {
m_explain.reset();
@ -770,7 +767,6 @@ namespace polysat {
switch (k) {
case entry_kind::unit_e:
entry::remove_from(m_units[v].get_layer(e)->entries, e);
SASSERT(well_formed(m_units[v]));
break;
case entry_kind::equal_e:
entry::remove_from(m_equal_lin[v], e);
@ -782,6 +778,7 @@ namespace polysat {
UNREACHABLE();
break;
}
SASSERT(well_formed(m_units[v]));
m_alloc.push_back(e);
}
@ -879,19 +876,15 @@ namespace polysat {
std::ostream& viable::display(std::ostream& out) const {
for (unsigned v = 0; v < m_units.size(); ++v) {
bool first = true;
for (auto const& layer : m_units[v].get_layers()) {
if (!layer.entries)
continue;
if (first)
out << "v" << v << ": ";
first = false;
out << "v" << v << ": ";
if (layer.bit_width != c.size(v))
out << "width[" << layer.bit_width << "] ";
display_all(out, v, layer.entries, " ");
}
if (!first)
out << "\n";
}
}
return out;
}
@ -913,6 +906,7 @@ namespace polysat {
return true;
entry* first = e;
while (true) {
CTRACE("bv", !e->active, tout << "inactive entry v" << e->var << " " << e->interval << "\n"; display(tout));
if (!e->active)
return false;
@ -922,13 +916,17 @@ namespace polysat {
return false;
auto* n = e->next();
if (n != e && e->interval.currently_contains(n->interval))
if (n != e && e->interval.currently_contains(n->interval)) {
TRACE("bv", tout << "currently contains\n");
return false;
}
if (n == first)
break;
if (e->interval.lo_val() >= n->interval.lo_val())
if (e->interval.lo_val() >= n->interval.lo_val()) {
TRACE("bv", tout << "lo-val >= n->lo_val\n");
return false;
}
e = n;
}
return true;
@ -942,12 +940,18 @@ namespace polysat {
bool first = true;
unsigned prev_width = 0;
for (layer const& l : ls.get_layers()) {
if (!well_formed(l.entries))
if (!well_formed(l.entries)) {
TRACE("bv", tout << "entries are not well-formed\n");
return false;
if (!all_of(dll_elements(l.entries), [&l](entry const& e) { return e.bit_width == l.bit_width; }))
}
if (!all_of(dll_elements(l.entries), [&l](entry const& e) { return e.bit_width == l.bit_width; })) {
TRACE("bv", tout << "elements don't have same bit-width\n");
return false;
if (!first && prev_width >= l.bit_width)
}
if (!first && prev_width >= l.bit_width) {
TRACE("bv", tout << "previous width is " << prev_width << " vs " << l.bit_width << "\n");
return false;
}
first = false;
prev_width = l.bit_width;
}

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

@ -51,7 +51,6 @@ namespace polysat {
bool refined = false;
/// whether the entry is part of the current set of intervals, or stashed away for backtracking
bool active = true;
bool valid_for_lemma = true;
pvar var = null_var;
constraint_id constraint_index;
@ -60,7 +59,6 @@ namespace polysat {
fi_record::reset();
refined = false;
active = true;
valid_for_lemma = true;
var = null_var;
constraint_index = constraint_id::null();
}

1
src/sat/smt/polysat_egraph.cpp
View file

@ -117,7 +117,6 @@ namespace polysat {
void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function<void(euf::enode*, euf::enode*)>& consume_eq) {
euf::theory_var v = m_pddvar2var[pv];
euf::theory_var w = m_pddvar2var[pw];
verbose_stream() << "explain " << ctx.bpp(var2enode(v)) << " " << ctx.bpp(var2enode(w)) << "\n";
m_bv_plugin->explain_slice(var2enode(v), offset, var2enode(w), consume_eq);
}

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

@ -41,6 +41,16 @@ namespace polysat {
m_lemma(ctx.get_manager())
{
m_bv_plugin = alloc(euf::bv_plugin, ctx.get_egraph());
std::function<void(euf::enode*)> ensure_th_var = [&](euf::enode* n) {
if (get_th_var(n) != euf::null_theory_var)
return;
auto v = mk_var(n);
rational val;
unsigned sz = 0;
if (bv.is_numeral(n->get_expr(), val, sz))
internalize_set(v, m_core.value(val, sz));
};
m_bv_plugin->set_ensure_th_var(ensure_th_var);
ctx.get_egraph().add_plugin(m_bv_plugin);
}