From 8c775f55a1a91df38595f0c5b63a17105a0f9f4e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 18 Dec 2022 12:26:30 -0800
Subject: [PATCH] adding stub for non-overflow lemma (disabled as not seen to
 be of use)

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bv_rewriter.cpp |  4 +++
 src/math/polysat/saturation.cpp  | 46 +++++++++++++++++++++++++++++---
 src/math/polysat/saturation.h    |  5 ++++
 3 files changed, 51 insertions(+), 4 deletions(-)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 516248e24..8333295e5 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -37,6 +37,7 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
     m_ite2id = p.bv_ite2id();
     m_le_extra = p.bv_le_extra();
     m_le2extract = p.bv_le2extract();
+    m_le2extract = false; // 
     set_sort_sums(p.bv_sort_ac());
 }
 
@@ -1724,6 +1725,9 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
         }
     }
 
+    if (!m_le2extract)
+        return BR_FAILED;
+
     if (!v1.is_zero() && new_args.size() == 1) {
         v1 = m_util.norm(v1, sz);
 #ifdef _TRACE
diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index fcdea9403..c678f00d7 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -44,11 +44,22 @@ namespace polysat {
     }
 
     bool saturation::perform(pvar v, signed_constraint const& c, conflict& core) {
-        if (!c->is_ule())
-            return false;
         if (c.is_currently_true(s))
             return false;
-        auto i = inequality::from_ule(c);
+
+        if (c->is_ule()) {
+            auto i = inequality::from_ule(c);
+            return try_inequality(v, i, core);
+        }
+
+#if 0
+        if (c->is_umul_ovfl()) 
+            return try_umul_ovfl(v, c, core);
+#endif
+        return false;
+    }
+
+    bool saturation::try_inequality(pvar v, inequality const& i, conflict& core) {
         if (try_mul_bounds(v, core, i))
             return true;
         if (try_parity(v, core, i))
@@ -72,6 +83,29 @@ namespace polysat {
         return false;
     }
 
+    bool saturation::try_umul_ovfl(pvar v, signed_constraint const& c, conflict& core) {
+        set_rule("[x] ~ovfl(x, y) => y = 0 or x <= x * y");
+        SASSERT(c->is_umul_ovfl());
+        if (!c.is_negative())
+            return false;
+        auto const& ovfl = c->to_umul_ovfl();
+        auto V = s.var(v);
+        auto p = ovfl.p(), q = ovfl.q();
+        // TODO could relax condition to be that V occurs in p
+        if (q == V) 
+            std::swap(p, q);
+        signed_constraint q_eq_0;
+        if (p == V && is_forced_diseq(q, 0, q_eq_0)) {
+            // ~ovfl(V,q) => q = 0 or V <= V*q
+            m_lemma.reset();
+            m_lemma.insert_eval(q_eq_0);
+            if (propagate(core, c, s.ule(p, p * q)))
+                return true;
+        }
+        return false;
+    }
+
+
     signed_constraint saturation::ineq(bool is_strict, pdd const& lhs, pdd const& rhs) {
         if (is_strict)
             return s.ult(lhs, rhs);
@@ -80,6 +114,10 @@ namespace polysat {
     }
 
     bool saturation::propagate(conflict& core, inequality const& crit, signed_constraint c) {
+        return propagate(core, crit.as_signed_constraint(), c);
+    }
+
+    bool saturation::propagate(conflict& core, signed_constraint const& crit, signed_constraint c) {
         if (is_forced_true(c))
             return false;
 
@@ -97,7 +135,7 @@ namespace polysat {
         // The current assumptions on how conflict lemmas are used do not accomodate propagation it seems.
         //
 
-        m_lemma.insert(~crit.as_signed_constraint());
+        m_lemma.insert(~crit);
 
         IF_VERBOSE(10, verbose_stream() << "propagate " << m_rule << " ";
                    for (auto lit : m_lemma) verbose_stream() << s.lit2cnstr(lit) << " ";
diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h
index 18cf2aa83..5bb0ebb58 100644
--- a/src/math/polysat/saturation.h
+++ b/src/math/polysat/saturation.h
@@ -31,6 +31,7 @@ namespace polysat {
         bool is_non_overflow(pdd const& x, pdd const& y, signed_constraint& c);
         signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
 
+        bool propagate(conflict& core, signed_constraint const& crit1, signed_constraint c);
         bool propagate(conflict& core, inequality const& crit1, signed_constraint c);
         bool add_conflict(conflict& core, inequality const& crit1, signed_constraint c);
         bool add_conflict(conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint c);
@@ -119,6 +120,10 @@ namespace polysat {
 
         bool is_forced_true(signed_constraint const& sc);
 
+        bool try_inequality(pvar v, inequality const& i, conflict& core);
+
+        bool try_umul_ovfl(pvar v, signed_constraint const& c, conflict& core);
+
     public:
         saturation(solver& s);
         void perform(pvar v, conflict& core);