match additional cases in forbidden intervals

src/math/polysat/forbidden_intervals.cpp

@@ -54,22 +54,28 @@ namespace polysat {
         auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), fi.side_cond);
 
         _backtrack.released = true;
-                
+
+
+        // a*v <= 0, a odd
+        if (ok1 && ok2 && match_zero(c, a1, b1, e1, a2, b2, e2, fi))
+            return true;
+
         // v > q
+        // 2^k*a*v + b > 0
+        // TODO: is !ok2 required?
         if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, fi))
             return true;
 
         // p > v
         if (!ok1 && ok2 && match_non_max(c, a2, b2, e2, fi))
             return true;
-            
+
         if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero())) {
             _backtrack.released = false;
             return false;
         }
         SASSERT(b1.is_val());
         SASSERT(b2.is_val());
-   
 
         if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi))
             return true;
@@ -262,12 +268,36 @@ namespace polysat {
         return false;
     }
 
+    /**
+     * a*v <= 0, a odd
+     * forbidden interval for v is [1,0[
+     */
+    bool forbidden_intervals::match_zero(
+        signed_constraint const& c,
+        rational const & a1, pdd const& b1, pdd const& e1,
+        rational const & a2, pdd const& b2, pdd const& e2,
+        fi_record& fi) {
+        if (c.is_positive() && a1.is_odd() && b1.is_zero() && a2.is_zero() && b2.is_zero()) {
+            auto& m = e1.manager();
+            rational lo_val(1);
+            auto lo = m.one();
+            rational hi_val(0);
+            auto hi = m.zero();
+            fi.coeff = 1;
+            fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
+            if (b1 != e1)
+                fi.side_cond.push_back(s.eq(b1, e1));
+            if (b2 != e2)
+                fi.side_cond.push_back(s.eq(b2, e2));
+            return true;
+        }
+        return false;
+    }
+
     /** 
      * v > q
      * forbidden interval for v is [0,1[
      * 
-     * Generalizations todo:
-     *
      * v - k > q
      * forbidden interval for v is [k,k+1[
      * 
@@ -290,6 +320,21 @@ namespace polysat {
                 fi.side_cond.push_back(s.eq(b1, e1));
             return true;
         }
+        if (a1.is_odd() && b1.is_val() && !c.is_positive()) {
+            auto& m = e1.manager();
+            rational const& mod_value = m.two_to_N();
+            rational a1_inv;
+            VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv));
+            rational lo_val(mod(-b1.val() * a1_inv, mod_value));
+            auto lo = -e1 * a1_inv;
+            rational hi_val(mod(lo_val + 1, mod_value));
+            auto hi = lo + 1;
+            fi.coeff = 1;
+            fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
+            if (b1 != e1)
+                fi.side_cond.push_back(s.eq(b1, e1));
+            return true;
+        }
         return false;
     }
 
@@ -303,9 +348,18 @@ namespace polysat {
         signed_constraint const& c,
         rational const & a2, pdd const& b2, pdd const& e2,
         fi_record& fi) {
-        if (a2.is_one() && b2.is_zero() && !c.is_positive()) {
-            // todo
-            
+        if (a2.is_one() && b2.is_val() && !c.is_positive()) {
+            auto& m = e2.manager();
+            rational const& mod_value = m.two_to_N();
+            rational lo_val(mod(-b2.val() - 1, mod_value));
+            auto lo = -e2 - 1;
+            rational hi_val(mod(lo_val + 1, mod_value));
+            auto hi = -e2;
+            fi.coeff = 1;
+            fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
+            if (b2 != e2)
+                fi.side_cond.push_back(s.eq(b2, e2));
+            return true;
         }
         return false;
     }

src/math/polysat/forbidden_intervals.h

@@ -52,6 +52,11 @@ namespace polysat {
 
         void add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2);
 
+        bool match_zero(signed_constraint const& c,
+            rational const & a1, pdd const& b1, pdd const& e1,
+            rational const & a2, pdd const& b2, pdd const& e2,
+            fi_record& fi);
+
         bool match_non_zero(signed_constraint const& c,
             rational const & a1, pdd const& b1, pdd const& e1,
             fi_record& fi);

src/test/polysat.cpp

@@ -1069,6 +1069,22 @@ public:
         }
     }
 
+    static void test_fi_nonzero() {
+        scoped_solver s(__func__);
+        auto a = s.var(s.add_var(5));
+        auto b = s.var(s.add_var(5));
+        s.add_ult(b*b*b, 7*a + 6);
+        s.check();
+    }
+
+    static void test_fi_nonmax() {
+        scoped_solver s(__func__);
+        auto a = s.var(s.add_var(5));
+        auto b = s.var(s.add_var(5));
+        s.add_ult(a + 8, b*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() {
@@ -1321,6 +1337,10 @@ public:
 void tst_polysat() {
     using namespace polysat;
 
+    test_polysat::test_fi_nonzero();
+    test_polysat::test_fi_nonmax();
+    return;
+
     test_polysat::test_l2();
 
 #if 0