mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

cosmetic updates to bounds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-04-05 16:40:18 -07:00
parent 2f992a7c9f
commit 00306731f6
2 changed files with 9 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1592,8 +1592,8 @@ namespace polysat {
* 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,
bilinear& b, rational* x_split) {
bool saturation::adjust_bound(rational const& x_min, rational const& x_max, rational const& y0,
rational const& M, bilinear& b, rational& x) {
SASSERT(x_min <= x_max);
rational A = b.a*y0 + b.b;
rational B = b.c*y0 + b.d;
@ -1615,26 +1615,23 @@ namespace polysat {
// If min + offset < 0, then [min,max] contains a multiple of M.
if (min + offset < 0) {
if (!x_split)
return false;
// A*x_split + B + offset = 0
// x_split = -(B+offset)/A
if (A >= 0) {
rational x = ceil((-offset-B) / A);
x = ceil((-offset - B) / A);
// [x_min; x_split-1] maps to interval < 0
// [x_split; x_max] maps to interval >= 0
VERIFY(b.eval(x, y0) >= 0);
VERIFY(b.eval(x-1, y0) < 0);
VERIFY(x_min <= x && x <= x_max);
*x_split = x;
} else {
rational x = floor((-offset-B) / A) + 1;
}
else {
x = floor((-offset - B) / A) + 1;
// [x_min; x_split-1] maps to interval >= 0
// [x_split; x_max] maps to interval < 0
VERIFY(b.eval(x, y0) < 0);
VERIFY(b.eval(x-1, y0) >= 0);
VERIFY(x_min <= x && x <= x_max);
*x_split = x;
}
}
@ -1848,9 +1845,9 @@ namespace polysat {
rational x_sp1 = x_min;
rational x_sp2 = x_min;
if (!adjust_bound(x_min, x_max, y0, M, b1, &x_sp1))
if (!adjust_bound(x_min, x_max, y0, M, b1, x_sp1))
return false;
if (!adjust_bound(x_min, x_max, y0, M, b2, &x_sp2))
if (!adjust_bound(x_min, x_max, y0, M, b2, x_sp2))
return false;
if (x_sp1 > x_sp2)

2
src/math/polysat/saturation.h
View file

@ -126,7 +126,7 @@ namespace polysat {
bool extract_linear_form(pdd const& q, pvar& y, rational& a, rational& b);
bool extract_bilinear_form(pvar x, pdd const& p, pvar& y, bilinear& b);
bool adjust_bound(rational const& x_min, rational const& x_max, rational const& y0, rational const& M,
bilinear& b, rational* x_split);
bilinear& b, rational& x_split);
bool update_min(rational& y_min, rational const& x_min, rational const& x_max,
bilinear const& b);
bool update_max(rational& y_max, rational const& x_min, rational const& x_max,