From 49a7f8446da1042bd0208485cf8d89bfbdbaf88d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 24 Dec 2022 15:19:37 -0800 Subject: [PATCH] disable match_non_max and match_non_zero Signed-off-by: Nikolaj Bjorner --- src/math/polysat/forbidden_intervals.cpp | 4 ++-- src/math/polysat/saturation.cpp | 2 +- src/math/polysat/viable.cpp | 10 +++++++++- 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index a605faa89..22acc2b12 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -166,11 +166,11 @@ namespace polysat { _backtrack.released = true; // v > q - if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, c->to_ule().rhs(), fi)) + if (false && ok1 && !ok2 && match_non_zero(c, a1, b1, e1, c->to_ule().rhs(), fi)) return true; // p > v - if (!ok1 && ok2 && match_non_max(c, c->to_ule().lhs(), a2, b2, e2, fi)) + if (false && !ok1 && ok2 && match_non_max(c, c->to_ule().lhs(), a2, b2, e2, fi)) return true; if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero())) { diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index cc89073f8..c9cf8bfd2 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -69,7 +69,7 @@ namespace polysat { prop = true; if (try_transitivity(v, core, i)) prop = true; - if (try_factor_equality1(v, core, i)) + if (try_factor_equality2(v, core, i)) prop = true; if (try_infer_equality(v, core, i)) prop = true; diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 2e05c5b1d..1212d803a 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -172,9 +172,17 @@ namespace polysat { // NSB review: // the bounds added by x < p and p < x in forbidden_intervals - // match_non_max + // match_non_max, match_non_zero // use values that are approximations. Then the propagations in // try_assign_eval are incorrect. + // For example, x > p means x has forbidden interval [0, p + 1[, + // the numeric interval is [0, 1[, but p + 1 == 1 is not ensured + // even p may have free variables. + // the proper side condition on p + 1 is -1 > p or -2 >= p or p + 1 != 0 + // I am disabling match_non_max and match_non_zero from forbidden_interval + // The narrowing rules in ule_constraint already handle the bounds propagaitons + // as it propagates p != -1 and 0 != q (p < -1, q > 0), + // for (auto const& c : get_constraints(v)) { s.try_assign_eval(c);