From 45e94ae7dd5ff0b81968906ea83cd1f96f58e3e6 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 7 Dec 2022 18:41:42 +0100
Subject: [PATCH] insert_eval

---
 src/math/polysat/saturation.cpp | 21 ++++++++++-----------
 src/test/polysat.cpp            |  3 ++-
 2 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index ee7cc1973..947beaad3 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -121,10 +121,9 @@ namespace polysat {
         if (!is_forced_false(c)) 
             return false;
 
-        // TODO: ??? this means that c is already on the search stack, so presumably the lemma won't help. Should check whether this case occurs.
-        // if (c.bvalue(s) == l_true)
-        //     return false;
-        SASSERT(c.bvalue(s) != l_true);
+        // Constraint c is already on the search stack, so the lemma will not derive anything new.
+        if (c.bvalue(s) == l_true)
+            return false;
 
         m_lemma.insert_eval(c);
         core.add_lemma(m_rule, m_lemma.build());
@@ -354,7 +353,7 @@ namespace polysat {
         if (!is_non_overflow(x, y, non_ovfl))
             return false;
         m_lemma.reset();
-        m_lemma.insert(~non_ovfl);
+        m_lemma.insert_eval(~non_ovfl);
         if (!xy_l_xz.is_strict())
             m_lemma.insert_eval(s.eq(x));
         return add_conflict(core, xy_l_xz, ineq(xy_l_xz.is_strict(), y, z));
@@ -397,7 +396,7 @@ namespace polysat {
             return false;
         pdd const& z_prime = l_y.lhs();
         m_lemma.reset();
-        m_lemma.insert(~non_ovfl);
+        m_lemma.insert_eval(~non_ovfl);
         return add_conflict(core, l_y, yx_l_zx, ineq(yx_l_zx.is_strict() || l_y.is_strict(), z_prime * x, z * x));
     }
 
@@ -437,7 +436,7 @@ namespace polysat {
         if (!is_non_overflow(x, y_prime, non_ovfl))
             return false;
         m_lemma.reset();
-        m_lemma.insert(~non_ovfl);
+        m_lemma.insert_eval(~non_ovfl);
         return add_conflict(core, yx_l_zx, z_l_y, ineq(z_l_y.is_strict() || yx_l_zx.is_strict(), y * x, y_prime * x));
     }
 
@@ -478,7 +477,7 @@ namespace polysat {
         if (!is_non_overflow(a, z, non_ovfl))
             return false;
         m_lemma.reset();
-        m_lemma.insert(~non_ovfl);
+        m_lemma.insert_eval(~non_ovfl);
         return add_conflict(core, y_l_ax, x_l_z, ineq(x_l_z.is_strict() || y_l_ax.is_strict(), y, a * z));
     }
 
@@ -602,9 +601,9 @@ namespace polysat {
         if (!is_non_overflow(a, X, non_ovfl)) 
             return false;
         m_lemma.reset();
-        m_lemma.insert(~s.eq(b, rational(-1)));
-        m_lemma.insert(~s.eq(y));
-        m_lemma.insert(~non_ovfl);
+        m_lemma.insert_eval(~s.eq(b, rational(-1)));
+        m_lemma.insert_eval(~s.eq(y));
+        m_lemma.insert_eval(~non_ovfl);
         if (propagate(core, axb_l_y, s.eq(X, 1)))
             return true;
         if (propagate(core, axb_l_y, s.eq(a, 1)))
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 85f5c8c62..f1d8707d6 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -1591,7 +1591,7 @@ void tst_polysat() {
     // test_polysat::test_ineq_axiom1(32, 1);
     // test_polysat::test_pop_conflict();
     // test_polysat::test_l2();
-    test_polysat::test_ineq1();
+    // test_polysat::test_ineq1();
     // test_polysat::test_quot_rem();
     // test_polysat::test_ineq_non_axiom1(32, 3);
     // test_polysat::test_monot_bounds_full();
@@ -1599,6 +1599,7 @@ void tst_polysat() {
     // test_polysat::test_quot_rem_incomplete();
     // test_polysat::test_monot();
     // test_polysat::test_fixed_point_arith_div_mul_inverse();
+    test_polysat::test_monot_bounds_simple(8);
     return;
 #endif