resurrect old bounds propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Oct 14, 2023 · 5619ed0 · 5619ed0
1 parent a39d4ad
commit 5619ed0
Showing 1 changed file with 20 additions and 10 deletions.
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
@@ -161,18 +161,28 @@ namespace nla {
                 return true;
             }
 
-            if (rational(dep.upper(range)).root(p, r) && (p % 2 == 1 || c().has_upper_bound(v))) {
-                SASSERT(p % 2 == 1 || c().get_upper_bound(v) >= 0);
+            if (rational(dep.upper(range)).root(p, r)) {
                 // v = -2, [-4,-3]^3 < v^3 -> add bound v <= -3
                 // v = -2, [-1,+1]^2 < v^2 -> add bound v >= -1
-                ++c().lra.settings().stats().m_nla_propagate_bounds;
-                auto le = dep.upper_is_open(range) ? llc::LT : llc::LE;
-                new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value");
-                lemma &= ex;
-                if (p % 2 == 0)
-                    lemma.explain_existing_upper_bound(v);
-                lemma |= ineq(v, le, r);                
-                return true;
+
+                if ((p % 2 == 1) || c().val(v).is_pos()) {
+                    ++c().lra.settings().stats().m_nla_propagate_bounds;
+                    auto le = dep.upper_is_open(range) ? llc::LT : llc::LE;
+                    new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value");
+                    lemma &= ex;
+                    lemma |= ineq(v, le, r);
+                    return true;
+                }
+
+                if (p % 2 == 0 && c().val(v).is_neg()) {
+                    ++c().lra.settings().stats().m_nla_propagate_bounds;
+                    SASSERT(!r.is_neg());
+                    auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE;
+                    new_lemma lemma(c(), "propagate value - root case - upper bound of range is below negative value");
+                    lemma &= ex;
+                    lemma |= ineq(v, ge, -r);
+                    return true;
+                }
             }
         }