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

can handle equal size now, weaken fixed_claim to avoid crash

Browse source
This commit is contained in:
Jakob Rath 2024-02-02 16:40:58 +01:00
parent 52c6fd98fd
commit 85ef6b721e
1 changed files with 15 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -676,28 +676,14 @@ namespace polysat {
rational const& lo = e->interval.lo_val();
rational const& hi = e->interval.hi_val();
if (v_sz == y_sz) {
#if 0
// TODO: copy interval over?
rational const& w_lo = lo;
rational const& w_hi = hi;
verbose_stream() << "=> v" << w << " not in [" << w_lo << ";" << w_hi << "[\n";
auto sc = ~cs.ult(c.var(w) - w_lo, w_hi - w_lo);
dependency_vector deps;
deps.append(result); // explains e
deps.push_back(offset_claim{m_var, slice}); // v = w
auto exp = c.propagate(sc, deps);
if (c.inconsistent()) {
verbose_stream() << "YYY inconsistent " << sc << " " << exp << "\n";
}
#endif
return;
}
r_interval const v_ivl = r_interval::proper(lo, hi);
verbose_stream() << "propagate interval " << v_ivl << " from v" << m_var << " to v" << w << "[" << y_sz << "]" << "\n";
// TODO: by the time we call viable::assign, m_fixed_bits only contains a single slice with 'value'.
// if we had access to the actually fixed slices (not just fixed because of the latest assignment),
// we could chop off fixed and non-fixed parts according to actually fixed slices;
// getting rid of the distinction into two separate cases below.
// more general interval, without taking into account fixed values
{
r_interval const yz_ivl = chop_off_upper(v_ivl, x_sz, y_sz + z_sz); // chop off x-part
@ -713,7 +699,7 @@ namespace polysat {
auto sc = ~cs.ult(w_shift * (c.var(w) - y_ivl.lo()), w_shift * (y_ivl.hi() - y_ivl.lo()));
dependency_vector deps;
deps.append(e_deps); // explains e
deps.push_back(offset_claim{m_var, slice}); // explains v[...] = y
deps.push_back(offset_claim{m_var, slice}); // explains m_var[...] = w
auto exp = c.propagate(sc, deps, "propagate from containing slice (general)");
if (c.inconsistent()) {
verbose_stream() << "XXX1 inconsistent " << sc << " " << exp << "\n";
@ -727,7 +713,8 @@ namespace polysat {
// tighter interval, but depends on fixed values
{
rational const x_value = x_sz > 0 ? machine_div2k(value, y_sz + z_sz) : rational(0);
rational const var_x_value = x_sz > 0 ? machine_div2k(value, y_sz + z_sz) : rational(0);
rational const x_value = x_sz > 0 ? mod2k(machine_div2k(value, y_sz + z_sz), x_sz) : rational(0);
rational const z_value = z_sz > 0 ? mod2k(value, z_sz) : rational(0);
r_interval const yz_ivl = chop_off_upper(v_ivl, x_sz, y_sz + z_sz, &x_value); // chop off x-part
r_interval const y_ivl = chop_off_lower(yz_ivl, y_sz, z_sz, &z_value); // chop off z-part
@ -739,13 +726,16 @@ namespace polysat {
}
else if (!y_ivl.is_empty()) {
// proper interval
verbose_stream() << "=> v" << w << "[" << y_sz << "] not in " << y_ivl << "\n";
verbose_stream() << "=> v" << w << "[" << y_sz << "] not in " << y_ivl << " using x=" << x_value << " z=" << z_value << "\n";
auto sc = ~cs.ult(w_shift * (c.var(w) - y_ivl.lo()), w_shift * (y_ivl.hi() - y_ivl.lo()));
dependency_vector deps;
deps.append(e_deps); // explains e
deps.push_back(offset_claim{m_var, slice}); // explains v[...] = y
if (x_sz > 0)
deps.push_back(fixed_claim{m_var, x_value, y_sz + z_sz, x_sz}); // v[upper] = x_value
deps.push_back(offset_claim{m_var, slice}); // explains m_var[...] = w
if (x_sz > 0) {
deps.push_back(fixed_claim{m_var, var_x_value, y_sz + z_sz, x_sz + (c.size(m_var) - v_sz)}); // m_var[upper] = var_x_value
// stronger but crashes in bv_plugin::explain_slice, TODO: why?
// deps.push_back(fixed_claim{m_var, x_value, y_sz + z_sz, x_sz}); // v[upper] = x_value
}
if (z_sz > 0)
deps.push_back(fixed_claim{m_var, z_value, 0, z_sz}); // v[lower] = z_value
auto exp = c.propagate(sc, deps, "propagate from containing slice (fixed)");