mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

remove outdated assertions

Browse source
This commit is contained in:
Jakob Rath 2023-12-22 12:10:15 +01:00
parent 5ad4d1017e
commit f111bd4de3
1 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/polysat/viable.cpp
View file

@ -1657,7 +1657,7 @@ namespace polysat {
rational const& mod_value = rational::power_of_two(w); rational const& mod_value = rational::power_of_two(w);
unsigned const first_relevant_for_conflict = relevant_entries.size(); unsigned const first_relevant_for_conflict = relevant_entries.size();
LOG("layer " << w << " bits, to_cover: [" << to_cover_lo << "; " << mod(to_cover_lo + to_cover_len, mod_value) << "[ (len " << to_cover_len << ")"); LOG_H3("layer " << w << " bits, to_cover: [" << to_cover_lo << "; " << mod(to_cover_lo + to_cover_len, mod_value) << "[ (len " << to_cover_len << ")");
SASSERT(0 <= to_cover_lo); SASSERT(0 <= to_cover_lo);
SASSERT(to_cover_lo < mod_value); SASSERT(to_cover_lo < mod_value);
SASSERT(0 < to_cover_len); // non-empty search domain (but it may wrap) SASSERT(0 < to_cover_len); // non-empty search domain (but it may wrap)
@ -1700,6 +1700,10 @@ namespace polysat {
val = to_cover_lo; val = to_cover_lo;
rational const to_cover_hi = mod(to_cover_lo + to_cover_len, mod_value); // may be equal to to_cover_lo if to_cover_len is the full domain size rational const to_cover_hi = mod(to_cover_lo + to_cover_len, mod_value); // may be equal to to_cover_lo if to_cover_len is the full domain size
LOG("to_cover_lo = " << to_cover_lo);
LOG("to_cover_hi = " << to_cover_hi);
LOG("to_cover_len = " << to_cover_len);
LOG("mod_value = " << mod_value);
rational progress; // = 0 rational progress; // = 0
SASSERT(progress.is_zero()); SASSERT(progress.is_zero());
@ -1798,6 +1802,9 @@ namespace polysat {
SASSERT(!refine_bits<true>(v, val, w, fbi)); SASSERT(!refine_bits<true>(v, val, w, fbi));
SASSERT(val != next_val || next_dist == mod_value); SASSERT(val != next_val || next_dist == mod_value);
LOG("val = " << val);
LOG("next_val = " << next_val << ", next_dist = " << next_dist);
unsigned const lower_w = widths[w_idx - 1]; unsigned const lower_w = widths[w_idx - 1];
rational const lower_mod_value = rational::power_of_two(lower_w); rational const lower_mod_value = rational::power_of_two(lower_w);
rational const lower_cover_lo = mod(val, lower_mod_value); rational const lower_cover_lo = mod(val, lower_mod_value);
@ -1816,10 +1823,7 @@ namespace polysat {
rational const dist = distance(lower_cover_lo, a, lower_mod_value); rational const dist = distance(lower_cover_lo, a, lower_mod_value);
val = mod(val + dist, mod_value); val = mod(val + dist, mod_value);
progress += dist; progress += dist;
LOG("distance(val, cover_hi) = " << (to_cover_len == mod_value && val == to_cover_lo ? to_cover_len : distance(val, to_cover_hi, mod_value))); LOG("val = " << val << ", progress = " << progress);
LOG("distance(next_val, cover_hi) = " << distance(next_val, to_cover_hi, mod_value));
SASSERT_EQ((to_cover_len == mod_value && val == to_cover_lo ? to_cover_len : distance(val, to_cover_hi, mod_value)), to_cover_len - progress);
SASSERT((to_cover_len == mod_value && val == to_cover_lo ? to_cover_len : distance(val, to_cover_hi, mod_value)) >= distance(next_val, to_cover_hi, mod_value));
if (result == l_true) if (result == l_true)
return l_true; // done return l_true; // done