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

simplify

Browse source
This commit is contained in:
Jakob Rath 2023-02-20 16:28:31 +01:00
parent 1dea87a07a
commit 33a38ba96f
1 changed files with 3 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/polysat/saturation.cpp
View file

@ -1618,22 +1618,17 @@ namespace polysat {
rational max = A >= 0 ? x_max * A + B : x_min * A + B; rational max = A >= 0 ? x_max * A + B : x_min * A + B;
rational min = A >= 0 ? x_min * A + B : x_max * A + B; rational min = A >= 0 ? x_min * A + B : x_max * A + B;
VERIFY(min <= max); VERIFY(min <= max);
if (max - min >= M) if (max - min >= M) {
IF_VERBOSE(10, verbose_stream() << "adjust_bound: abort because max - min >= M\n");
return false; return false;
}
// k0 = min k. val + kM >= 0 // k0 = min k. val + kM >= 0
// = min k. k >= -val/M // = min k. k >= -val/M
// = ceil(-val/M) = -floor(val/M) // = ceil(-val/M) = -floor(val/M)
rational offset = rational::zero(); rational offset = rational::zero();
#if 0
if (max >= M)
offset = -M * floor(max / M);
else if (max < 0)
offset = M * floor((-max + M - 1) / M);
#else
if (max < 0 || max >= M) if (max < 0 || max >= M)
offset = -M * floor(max / M); offset = -M * floor(max / M);
#endif
d += offset; d += offset;
// If min + offset < 0, then [min,max] contains a multiple of M. // If min + offset < 0, then [min,max] contains a multiple of M.