mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-12 06:00:53 +00:00
Code Activity

fix recursion in case of large gap

Browse source
This commit is contained in:
Jakob Rath 2023-11-29 13:17:10 +01:00
parent 39bee180de
commit 203df6babb
1 changed files with 21 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1653,13 +1653,30 @@ namespace polysat {
rational lower_cover_lo, lower_cover_hi; rational lower_cover_lo, lower_cover_hi;
if (distance(val, next_val, mod_value) >= lower_mod_value) { if (distance(val, next_val, mod_value) >= lower_mod_value) {
// NOTE: in this case we do not get the first viable value, but the one with smallest value in the lower bits.
// this is because we start the search in the recursive case at 0.
// if this is a problem, adapt to lower_cover_lo = mod(val, lower_mod_value), lower_cover_hi = ...
lower_cover_lo = 0; lower_cover_lo = 0;
lower_cover_hi = lower_mod_value; lower_cover_hi = lower_mod_value;
rational a;
lbool result = find_on_layer(v, w_idx - 1, widths, overlaps, fbi, lower_cover_lo, lower_cover_hi, a, refine_todo);
VERIFY(result != l_undef);
if (result == l_false)
return l_false; // conflict
SASSERT(result == l_true);
// replace lower bits of 'val' by 'a'
rational const val_lower = mod(val, lower_mod_value);
val = val - val_lower + a;
if (a < val_lower)
a += lower_mod_value;
LOG("distance(val, cover_hi) = " << distance(val, to_cover_hi, mod_value));
LOG("distance(next_val, cover_hi) = " << distance(next_val, to_cover_hi, mod_value));
SASSERT(distance(val, to_cover_hi, mod_value) >= distance(next_val, to_cover_hi, mod_value));
return l_true;
} }
else {
lower_cover_lo = mod(val, lower_mod_value); lower_cover_lo = mod(val, lower_mod_value);
lower_cover_hi = mod(next_val, lower_mod_value); lower_cover_hi = mod(next_val, lower_mod_value);
}
rational a; rational a;
lbool result = find_on_layer(v, w_idx - 1, widths, overlaps, fbi, lower_cover_lo, lower_cover_hi, a, refine_todo); lbool result = find_on_layer(v, w_idx - 1, widths, overlaps, fbi, lower_cover_lo, lower_cover_hi, a, refine_todo);
@ -1667,9 +1684,7 @@ namespace polysat {
return l_false; // conflict return l_false; // conflict
// replace lower bits of 'val' by 'a' // replace lower bits of 'val' by 'a'
// LOG("old val: " << val);
val = val - lower_cover_lo + a; val = val - lower_cover_lo + a;
// LOG("new val: " << val);
LOG("distance(val, cover_hi) = " << distance(val, to_cover_hi, mod_value)); LOG("distance(val, cover_hi) = " << distance(val, to_cover_hi, mod_value));
LOG("distance(next_val, cover_hi) = " << distance(next_val, to_cover_hi, mod_value)); LOG("distance(next_val, cover_hi) = " << distance(next_val, to_cover_hi, mod_value));
SASSERT(distance(val, to_cover_hi, mod_value) >= distance(next_val, to_cover_hi, mod_value)); SASSERT(distance(val, to_cover_hi, mod_value) >= distance(next_val, to_cover_hi, mod_value));