From 2f992a7c9f7961b14a20c010c691c02606de48a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Apr 2023 09:28:44 -0700 Subject: [PATCH] adjust bounds Signed-off-by: Nikolaj Bjorner --- src/math/polysat/saturation.cpp | 12 ++++++++---- src/math/polysat/saturation.h | 2 +- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 16f514c05..d551ced9b 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -1724,16 +1724,15 @@ namespace polysat { } } - bool saturation::update_bounds_for_xs(rational const& x_min, rational const& x_max, rational& y_min, rational& y_max, rational const& y0, bilinear const& b1, bilinear const& b2, rational const& M, inequality const& a_l_b) { + bool saturation::update_bounds_for_xs(rational const& x_min, rational const& x_max, rational& y_min, rational& y_max, rational const& y0, bilinear b1, bilinear b2, rational const& M, inequality const& a_l_b) { VERIFY(x_min <= x_max); - rational d1 = b1.d; if (b1.eval(x_min, y0) < 0) - d1 += M; + b1.d += M; rational d2 = b2.d; if (b2.eval(x_min, y0) < 0) - d2 += M; + b2.d += M; IF_VERBOSE(2, verbose_stream() << "Adjusted for x in [" << x_min << "; " << x_max << "]\n"; @@ -1788,6 +1787,11 @@ namespace polysat { auto& m = s.var2pdd(x); pdd p = a_l_b.lhs(), q = a_l_b.rhs(); +#if 0 + // add this filter to remove useless bounds + if (q.is_zero()) + return false; +#endif if (p.degree(x) > 1 || q.degree(x) > 1) return false; if (p.degree(x) == 0 && q.degree(x) == 0) diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h index eb815986a..e57b2ce3a 100644 --- a/src/math/polysat/saturation.h +++ b/src/math/polysat/saturation.h @@ -132,7 +132,7 @@ namespace polysat { bool update_max(rational& y_max, rational const& x_min, rational const& x_max, bilinear const& b); bool update_bounds_for_xs(rational const& x_min, rational const& x_max, rational& y_min, rational& y_max, - rational const& y0, bilinear const& b1, bilinear const& b2, + rational const& y0, bilinear b1, bilinear b2, rational const& M, inequality const& a_l_b); void fix_values(pvar x, pvar y, pdd const& p); void fix_values(pvar y, pdd const& p);