mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

fixes to new value propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-09-05 17:58:47 -07:00
parent 33364c3f85
commit fe7dcb0394
3 changed files with 14 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/sls/sls_bv_eval.cpp
View file

@ -681,11 +681,13 @@ namespace sls {
return false; return false;
if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) { if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
commit_eval(e, to_app(arg)); commit_eval(e, to_app(arg));
IF_VERBOSE(11, verbose_stream() << "repair " << mk_bounded_pp(e, m) << " : " << mk_bounded_pp(arg, m) << " := " << wval(arg) << "\n";);
ctx.new_value_eh(arg); ctx.new_value_eh(arg);
return true; return true;
} }
if (m.is_eq(e) && bv.is_bv(arg) && try_repair_eq(e, i)) { if (m.is_eq(e) && bv.is_bv(arg) && try_repair_eq(e, i)) {
commit_eval(e, to_app(arg)); commit_eval(e, to_app(arg));
IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(arg, m) << " := " << wval(arg) << "\n";);
ctx.new_value_eh(arg); ctx.new_value_eh(arg);
return true; return true;
} }
@ -1339,7 +1341,6 @@ namespace sls {
} }
bool bv_eval::try_repair_uge(bool e, bvval& a, bvval const& b) { bool bv_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
//verbose_stream() << "try-repair-uge " << e << " " << a << " " << b << "\n";
if (e) { if (e) {
// a >= t // a >= t
return a.set_random_at_least(b.bits(), m_rand); return a.set_random_at_least(b.bits(), m_rand);
@ -1988,9 +1989,14 @@ namespace sls {
return false; return false;
} }
} }
//verbose_stream() << "repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
if (v.commit_eval()) if (v.eval == v.bits())
return true; return true;
//verbose_stream() << "repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
if (v.commit_eval()) {
ctx.new_value_eh(e);
return true;
}
//verbose_stream() << "could not repair up " << mk_bounded_pp(e, m) << " " << v << "\n"; //verbose_stream() << "could not repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
//for (expr* arg : *to_app(e)) //for (expr* arg : *to_app(e))
// verbose_stream() << mk_bounded_pp(arg, m) << " " << wval(arg) << "\n"; // verbose_stream() << mk_bounded_pp(arg, m) << " " << wval(arg) << "\n";

2
src/ast/sls/sls_bv_plugin.cpp
View file

@ -160,8 +160,6 @@ namespace sls {
if (ctx.is_true(e) != m_eval.bval1(e)) if (ctx.is_true(e) != m_eval.bval1(e))
ctx.flip(ctx.atom2bool_var(e)); ctx.flip(ctx.atom2bool_var(e));
} }
else
ctx.new_value_eh(e);
} }
else if (bv.is_bv(e)) { else if (bv.is_bv(e)) {
log(e, true, false); log(e, true, false);

7
src/ast/sls/sls_bv_valuation.cpp
View file

@ -181,6 +181,7 @@ namespace sls {
for (unsigned i = 0; i < nw; ++i) for (unsigned i = 0; i < nw; ++i)
m_bits[i] = eval[i]; m_bits[i] = eval[i];
SASSERT(well_formed()); SASSERT(well_formed());
return true; return true;
} }
@ -662,8 +663,10 @@ namespace sls {
} }
// a[hi_index:0] was incremented, but a[:hi_index+1] cannot be decremented. // a[hi_index:0] was incremented, but a[:hi_index+1] cannot be decremented.
// maximize a[:hi_index+1] to model wrap around behavior.
for (unsigned i = hi_index + 1; i < bw; ++i)
if (!fixed.get(i))
a.set(i, true);
} }
void bv_valuation::tighten_range() { void bv_valuation::tighten_range() {