From 8c2f268506fd92d87022aa4f4e9b955ca7ed5c93 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 24 Jan 2022 17:03:49 +0100
Subject: [PATCH] fi disequal: add special treatment for v > -a*v

---
 src/math/polysat/viable.cpp | 27 ++++++++++++++++++++++++---
 src/test/polysat.cpp        | 24 ++++++++++++++++++++++++
 2 files changed, 48 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index ceefd7841..1b8c2f99c 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -327,10 +327,31 @@ namespace polysat {
             };
 
             if (lhs > rhs || (e->src.is_negative() && lhs == rhs)) {
-                rational lo = val - delta_l(val);
-                rational hi = val + delta_u(val) + 1;
+                rational lo;
+                rational hi;
+
+                // TODO: extract into separate function
+                if (e->src.is_negative() && a2.is_one() && b1.is_zero() && b2.is_zero()) {
+                    // special case:  v > -a*v for some numeral a
+                    rational const& a = mod(-a1, mod_value);
+                    if (val.is_zero()) {
+                        lo = 0;
+                        hi = ceil( (mod_value + 1) / (a + 1) );
+                    } else {
+                        rational const y = mod(-a * val, mod_value);
+                        lo = ceil( val + (y - max_value) / a );
+                        hi = ceil( (y + a*val + 1) / (a + 1) );
+                        // can always extend to 0
+                        if (lo.is_one())
+                            lo = 0;
+                    }
+                } else {
+                    // general case
+                    lo = val - delta_l(val);
+                    hi = val + delta_u(val) + 1;
+                    // TODO: increase interval
+                }
 
-                // TODO: increase interval
                 LOG("refine-disequal-lin: " << " [" << lo << ", " << hi << "[");
 
                 SASSERT(0 <= lo && lo <= val);
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index b90321358..0d79452d4 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -1097,6 +1097,29 @@ public:
         s.check();
     }
 
+    static void test_fi_disequal_mild() {
+        {
+            // small version
+            scoped_solver s(__func__);
+            auto a = s.var(s.add_var(6));
+            auto b = s.var(s.add_var(6));
+            // v > -3*v
+            s.add_eq(a - 3);
+            s.add_ult(-a*b, b);
+            s.check();
+        }
+        {
+            // large version
+            scoped_solver s(__func__);
+            auto a = s.var(s.add_var(256));
+            auto b = s.var(s.add_var(256));
+            // v > -100*v
+            s.add_eq(a - 100);
+            s.add_ult(-a*b, b);
+            s.check();
+        }
+    }
+
     // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
     // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
     // static void test_mixed_vars() {
@@ -1352,6 +1375,7 @@ void tst_polysat() {
     test_polysat::test_fi_zero();
     test_polysat::test_fi_nonzero();
     test_polysat::test_fi_nonmax();
+    test_polysat::test_fi_disequal_mild();
     return;
 
     test_polysat::test_l2();