mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-26 22:17:54 +00:00
Code Activity

fix prefix

Browse source
This commit is contained in:
Jakob Rath 2024-05-14 18:54:29 +02:00
parent 705d94d883
commit 47d93037f7
1 changed files with 13 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -964,7 +964,7 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
rational const store_val = mod2k(machine_div2k(e.value, abw), store_sz); rational const store_val = mod2k(machine_div2k(e.value, abw), store_sz);
prefix = prefix * rational::power_of_two(store_sz) + store_val; prefix = prefix * rational::power_of_two(store_sz) + store_val;
#if DEBUG_EXPLAIN #if DEBUG_EXPLAIN
verbose_stream() << " store_val = " << store_val << "\n"; verbose_stream() << " store_val = " << store_val << " (storing " << store_sz << " bits)\n";
verbose_stream() << " new stored prefix: " << prefix << "\n"; verbose_stream() << " new stored prefix: " << prefix << "\n";
#endif #endif
// for simplicity, we fix the evaluation of the stored upper bits // for simplicity, we fix the evaluation of the stored upper bits
@ -982,6 +982,14 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
deps.push_back(c.propagate(sc, c.explain_weak_eval(sc), "explain_overlap prefix evaluation")); deps.push_back(c.propagate(sc, c.explain_weak_eval(sc), "explain_overlap prefix evaluation"));
} }
// if there is wrap-around, increment prefix
if (after.e->interval.lo_val() > after.e->interval.hi_val()) {
prefix++;
#if DEBUG_EXPLAIN
verbose_stream() << " incremented stored prefix: " << prefix << "\n";
#endif
}
rational restore_val; rational restore_val;
if (ebw < abw) { if (ebw < abw) {
// restore bits from prefix // restore bits from prefix
@ -989,21 +997,13 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
/*rational const*/ restore_val = mod2k(prefix, restore_sz); /*rational const*/ restore_val = mod2k(prefix, restore_sz);
prefix = machine_div2k(prefix, restore_sz); prefix = machine_div2k(prefix, restore_sz);
#if DEBUG_EXPLAIN #if DEBUG_EXPLAIN
verbose_stream() << " restore_val = " << restore_val << "\n"; verbose_stream() << " restore_val = " << restore_val << " (restoring " << restore_sz << " bits)\n";
verbose_stream() << " new stored prefix: " << prefix << "\n"; verbose_stream() << " new stored prefix: " << prefix << "\n";
#endif #endif
// restore_val * rational::power_of_two(ebw) + t(?) // restore_val * rational::power_of_two(ebw) + t(?)
SASSERT(ebw < bw || aw != bw); SASSERT(ebw < bw || aw != bw);
} }
// if there is wrap-around, increment prefix
if (e.e->interval.lo_val() > e.e->interval.hi_val()) {
prefix++;
#if DEBUG_EXPLAIN
verbose_stream() << " incremented stored prefix: " << prefix << "\n";
#endif
}
if (ebw < bw || aw != bw) { if (ebw < bw || aw != bw) {
auto const& p2b = rational::power_of_two(bw); auto const& p2b = rational::power_of_two(bw);
auto const& p2eb = rational::power_of_two(bw - ebw); auto const& p2eb = rational::power_of_two(bw - ebw);
@ -1054,7 +1054,9 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
} }
if (ebw < abw) { if (ebw < abw) {
t = restore_val * rational::power_of_two(ebw) + t; // NOTE: currently we fix the stored prefix to the current value and evaluate t (see above)
// the value of t from e.value already has the correct prefix 'baked in'
// t = restore_val * rational::power_of_two(ebw) + t;
#if DEBUG_EXPLAIN #if DEBUG_EXPLAIN
verbose_stream() << " restored t: " << t << "\n"; verbose_stream() << " restored t: " << t << "\n";
#endif #endif