mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

minor changes to bounds propagation

Browse source
This commit is contained in:
Jakob Rath 2023-02-01 10:36:49 +01:00
parent 63f7001117
commit 9314ad3808
1 changed files with 16 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1596,8 +1596,7 @@ namespace polysat {
}
/**
* if !x_split: update d such that 0 <= a*x*y0 + b*x + c*y0 + d < M for every value x_min <= x <= x_max
* if x_split: update d such that -M < a*x*y0 + b*x + c*y0 + d < M for every value x_min <= x <= x_max, return x_split such that [x_min,x_split[ and [x_split,x_max] can fit into [0,M[
* Update d such that -M < a*x*y0 + b*x + c*y0 + d < M for every value x_min <= x <= x_max, return x_split such that [x_min,x_split[ and [x_split,x_max] can fit into [0,M[
* return false if there is no such d.
*/
bool saturation::adjust_bound(rational const& x_min, rational const& x_max, rational const& y0, rational const& M, rational const& a, rational const& b, rational const& c, rational& d, rational* x_split) {
@ -1610,14 +1609,22 @@ namespace polysat {
if (max - min >= M)
return false;
// k0 = min k. val + kM >= 0
// = min k. k >= -val/M
// = ceil(-val/M) = -floor(val/M)
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)
offset = -M * floor(max / M);
#endif
d += offset;
// If min + offset < 0, then [min,max] contained a multiple of M.
// If min + offset < 0, then [min,max] contains a multiple of M.
if (min + offset < 0) {
if (!x_split)
return false;
@ -1731,11 +1738,12 @@ namespace polysat {
VERIFY(x_min <= x_max);
// TODO: d +/- M would suffice here
rational d1 = dd1;
if (a1*x_min*y0 + b1*x_min + c1*y0 + d1 < 0)
d1 += M;
rational d2 = dd2;
VERIFY(adjust_bound(x_min, x_max, y0, M, a1, b1, c1, d1, nullptr));
VERIFY(adjust_bound(x_min, x_max, y0, M, a2, b2, c2, d2, nullptr));
if (a2*x_min*y0 + b2*x_min + c2*y0 + d2 < 0)
d2 += M;
IF_VERBOSE(2,
verbose_stream() << "Adjusted for x in [" << x_min << "; " << x_max << "]\n";
@ -1833,8 +1841,8 @@ namespace polysat {
verbose_stream() << "\n---\n\n";
verbose_stream() << "constraint " << lit_pp(s, a_l_b) << "\n";
verbose_stream() << "x = v" << x << "\n";
s.m_viable.display(verbose_stream(), x) << "\n";
verbose_stream() << "y = v" << y << "\n";
s.m_viable.display(verbose_stream() << "\nx-intervals:\n", x, "\n") << "\n";
verbose_stream() << "\n";
verbose_stream() << "x_min " << x_min << " x_max " << x_max << "\n";
verbose_stream() << "v" << y << " " << y0 << "\n";
@ -1851,6 +1859,7 @@ namespace polysat {
if (x_sp1 > x_sp2)
std::swap(x_sp1, x_sp2);
SASSERT(x_min <= x_sp1 && x_sp1 <= x_sp2 && x_sp2 <= x_max);
IF_VERBOSE(2,
verbose_stream() << "Adjusted\n";