mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity

check hole_len

Browse source
This commit is contained in:
Jakob Rath 2024-04-02 16:28:45 +02:00
parent 47f28c6857
commit 88be5e6611
1 changed files with 8 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -902,7 +902,7 @@ again:
// //
// The hole can only be covered by lower intervals if // The hole can only be covered by lower intervals if
// //
// hole_size < 2^hole_bits // hole_len < 2^hole_bits
// //
// i.e., after->lo() - before->hi() < 2^hole_bits. // i.e., after->lo() - before->hi() < 2^hole_bits.
@ -919,18 +919,17 @@ again:
pdd t1 = before.e->interval.hi(); pdd t1 = before.e->interval.hi();
pdd t2 = after.e->interval.lo(); pdd t2 = after.e->interval.lo();
rational after_len = r_interval::len(after.e->interval.lo_val(), after.e->interval.hi_val(), rational::power_of_two(aew)); if (get_covered_interval(after).contains(before.value)) {
rational after_covered_lo = mod2k(after.value - after_len, m_num_bits); // this check is still needed as long as we do not prune the 'last' interval
auto after_covered_ivl = r_interval::proper(after_covered_lo, after.value);
// verbose_stream() << " after_len " << after_len << "\n";
// verbose_stream() << " after_covered_lo " << after_covered_lo << "\n";
// verbose_stream() << " after_covered_ivl " << after_covered_ivl << "\n";
SASSERT_EQ(after_covered_ivl.len(rational::power_of_two(m_num_bits)), after_len);
if (after_covered_ivl.contains(before.value)) {
verbose_stream() << " not a real hole (subsumption opportunity)\n"; verbose_stream() << " not a real hole (subsumption opportunity)\n";
return; return;
} }
SASSERT(!get_covered_interval(after).contains(before.value));
rational hole_len = r_interval::len(before.value, get_covered_interval(after).lo(), rational::power_of_two(m_num_bits));
SASSERT(hole_len < rational::power_of_two(hole_bits)); // otherwise we missed a conflict at lower bit-width
// no constraint needed for constant bounds // no constraint needed for constant bounds
if (t1.is_val() && t2.is_val()) if (t1.is_val() && t2.is_val())
return; return;