From 9275930f50bdcee198af09c4cb843ce56aee5ca2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Dec 2022 13:38:51 -0800 Subject: [PATCH] fix bug in add-overflow propagation, move to use viable to mind for bounds Signed-off-by: Nikolaj Bjorner --- src/math/polysat/saturation.cpp | 88 ++++++--------------------------- src/math/polysat/viable.cpp | 19 ++++--- src/math/polysat/viable.h | 2 +- 3 files changed, 27 insertions(+), 82 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index c6405e0c5..f8da38a4b 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -1133,13 +1133,13 @@ namespace polysat { } /** - * x <= x + y & x <= n => y = 0 or y >= N - n - * x < x + y & x <= n => y >= N - n - * -x >= -x - y & x <= n => y = 0 or y >= N - n - * -x > -x - y & x <= n => y >= N - n + * x >= x + y & x <= n => y = 0 or y >= N - n + * x > x + y & x <= n => y >= N - n + * -x <= -x - y & x <= n => y = 0 or y >= N - n + * -x < -x - y & x <= n => y >= N - n */ bool saturation::try_add_overflow_bound(pvar x, conflict& core, inequality const& axb_l_y) { - set_rule("[x] x <= x + y & x <= n => y = 0 or y >= 2^N - n"); + set_rule("[x] x >= x + y & x <= n => y = 0 or y >= 2^N - n"); signed_constraint y_eq_0, x_ge_bound; auto& m = s.var2pdd(x); pdd y = m.zero(); @@ -1155,16 +1155,15 @@ namespace polysat { if (!axb_l_y.is_strict()) m_lemma.insert_eval(y_eq_0); m_lemma.insert_eval(~x_ge_bound); - verbose_stream() << "ADD overflow bound " << axb_l_y << "\n"; return propagate(x, core, axb_l_y, s.uge(y, m.two_to_N() - bound)); } /** * Match one of the patterns: - * x <= x + y - * x < x + y - * -x >= -x - y - * -x > -x - y + * x >= x + y + * x > x + y + * -x <= -x - y + * -x < -x - y */ bool saturation::is_add_overflow(pvar x, inequality const& i, pdd& y) { auto& m = s.var2pdd(x); @@ -1172,12 +1171,12 @@ namespace polysat { pdd a = X; if (i.lhs().degree(x) != 1 || i.rhs().degree(x) != 1) return false; - if (i.lhs() == X) { - i.rhs().factor(x, 1, a, y); + if (i.rhs() == X) { + i.lhs().factor(x, 1, a, y); if (a.is_one()) return true; } - if (i.rhs() == -X) { + if (i.lhs() == -X) { i.rhs().factor(x, 1, a, y); if ((-a).is_one()) { y = -y; @@ -1187,71 +1186,12 @@ namespace polysat { return false; } - /** - * Just search core for literal of the form x <= bound - * TODO - * - more general bounnds obtained from forbidden interval extraction: x + k1 <= x + k2 - * such that the forbidden interval includes -1. - * - in other words, use viable set to probe for bounds instead of literals - * - not just core, but query over all assigned literals? - * - look for optimal bounds, not just the first? - * - General comment: integrate with indexing: only assigned literals containing x are useful. - * - then index on patterns or features of literals? - */ bool saturation::has_upper_bound(pvar x, conflict& core, rational& bound, signed_constraint& x_le_bound) { - - bool found = s.m_viable.has_upper_bound(x, bound, x_le_bound); - verbose_stream() << "found " << found << "\n"; - - auto& m = s.var2pdd(x); - pdd y = s.var(x); - for (auto const& c : core) { - if (!c->is_ule()) - continue; - auto i = inequality::from_ule(c); - if (!is_x_l_Y(x, i, y)) - continue; - if (!y.is_val()) - continue; - bound = y.val(); - if (i.is_strict() && bound == 0) - continue; - if (i.is_strict()) - bound = bound - 1; - if (bound == m.max_value()) - continue; - x_le_bound = c; - return true; - } - return false; + return s.m_viable.has_upper_bound(x, bound, x_le_bound); } bool saturation::has_lower_bound(pvar x, conflict& core, rational& bound, signed_constraint& x_ge_bound) { - - bool found = s.m_viable.has_lower_bound(x, bound, x_ge_bound); - verbose_stream() << "found " << found << "\n"; - - auto& m = s.var2pdd(x); - pdd y = s.var(x); - for (auto const& c : core) { - if (!c->is_ule()) - continue; - auto i = inequality::from_ule(c); - if (!is_Y_l_x(x, i, y)) - continue; - if (!y.is_val()) - continue; - bound = y.val(); - if (i.is_strict() && bound == m.max_value()) - continue; - if (i.is_strict()) - bound = bound + 1; - if (bound == 0) - continue; - x_ge_bound = c; - return true; - } - return false; + return s.m_viable.has_lower_bound(x, bound, x_ge_bound); } /* diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 66a0ac40c..f4d960352 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -643,40 +643,45 @@ namespace polysat { return query(v, hi); } + // TBD: generalize to multiple intervals? + // Multiple intervals could be used to constrain upper/lower bounds, not just the last one. bool viable::has_upper_bound(pvar v, rational& out_hi, signed_constraint& out_c) { entry const* first = m_units[v]; entry const* e = first; do { if (!e->refined) { - verbose_stream() << "has-upper-bound " << e->src << " " << e->interval << "\n"; auto const& lo = e->interval.lo(); auto const& hi = e->interval.hi(); if (lo.is_val() && hi.is_val() && lo.val() > hi.val()) { out_c = e->src; out_hi = lo.val() - 1; + // verbose_stream() << "Upper bound v" << v << " " << out_hi << " " << out_c << "\n"; return true; } } e = e->next(); } while (e != first); - return false; } - bool viable::has_lower_bound(pvar v, rational& out_hi, signed_constraint& out_c) { + bool viable::has_lower_bound(pvar v, rational& out_lo, signed_constraint& out_c) { entry const* first = m_units[v]; entry const* e = first; do { if (!e->refined) { - verbose_stream() << "has-upper-bound " << e->src << " " << e->interval << "\n"; + auto const& lo = e->interval.lo(); + auto const& hi = e->interval.hi(); + if (lo.is_val() && hi.is_val() && (lo.val() == 0 || lo.val() > hi.val())) { + out_c = e->src; + out_lo = hi.val(); + // verbose_stream() << "Lower bound " << v << " " << out_lo << " " << out_c << "\n"; + return true; + } } e = e->next(); } while (e != first); - - return false; - return false; } diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index cb1feb822..a4f3f6b24 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -195,7 +195,7 @@ namespace polysat { * Query for an lower bound literal for v together with justification. * @return true if a non-trivial lower bound is found, return justifying constraint. */ - bool has_lower_bound(pvar v, rational& out_hi, signed_constraint& out_c); + bool has_lower_bound(pvar v, rational& out_lo, signed_constraint& out_c); /** * Find a next viable value for variable.