First version of refine_disequal_lin

src/math/dd/dd_pdd.h

@@ -405,7 +405,7 @@ namespace dd {
         bool is_zero() const { return m.is_zero(root); }
         bool is_linear() const { return m.is_linear(root); }
         bool is_var() const { return m.is_var(root); }
-        /** Polynomial is of the form: a * x + b */
+        /** Polynomial is of the form a * x + b for numerals a, b. */
         bool is_unilinear() const { return !is_val() && lo().is_val() && hi().is_val(); }
         bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } 
         bool is_binary() const { return m.is_binary(root); }

src/math/polysat/forbidden_intervals.cpp

@@ -47,17 +47,15 @@ namespace polysat {
         fi.coeff = 1;
         fi.src = c;
 
+        // eval(lhs) = a1*v + eval(e1) = a1*v + b1
+        // eval(rhs) = a2*v + eval(e2) = a2*v + b2
+        // We keep the e1, e2 around in case we need side conditions such as e1=b1, e2=b2.
         auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_ule().lhs(), fi.side_cond);
         auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), fi.side_cond);
         if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero()))
             return false;
         SASSERT(b1.is_val());
         SASSERT(b2.is_val());
-
-        // TBD: use fi.coeff = -1 to tell caller to treat it as a diseq_lin.
-        // record a1, a2, b1, b2 for fast access, add non_unit side conditions on b1 = e1, b2 = e2?
-        if (a1 != a2 && !a1.is_zero() && !a2.is_zero())
-            return false;
    
         _backtrack.released = true;
 
@@ -67,6 +65,8 @@ namespace polysat {
             return true;
         if (match_linear3(c, a1, b1, e1, a2, b2, e2, fi))
             return true;
+        if (match_linear4(c, a1, b1, e1, a2, b2, e2, fi))
+            return true;
 
         _backtrack.released = false;
         return false;
@@ -88,12 +88,16 @@ namespace polysat {
         pdd e = m.zero();
         unsigned const deg = p.degree(v);
         if (deg == 0)
+            // p = 0*v + e
             e = p;
         else if (deg == 1)
+            // p = q*v + e
             p.factor(v, 1, q, e);
         else
             return std::tuple(false, rational(0), q, e);
 
+        // r := eval(q)
+        // Add side constraint q = r.
         if (!q.is_val()) {
             pdd r = q.subst_val(s.assignment());
             if (!r.is_val())
@@ -221,6 +225,30 @@ namespace polysat {
         return false;
     }
 
+    /**
+     * e1 + t <= e2 + t', with t = a1*y, t' = a2*y, a1 != a2, a1, a2 non-zero
+     */
+    bool forbidden_intervals::match_linear4(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 (a1 != a2 && !a1.is_zero() && !a2.is_zero()) {
+            // NOTE: we don't have an interval here in the same sense as in the other cases.
+            // We use the interval to smuggle out the values a1,b1,a2,b2 without adding additional fields.
+            // to_interval flips a1,b1 with a2,b2 for negative constraints, which we also need for this case.
+            auto lo = b1;
+            rational lo_val = a1;
+            auto hi = b2;
+            rational hi_val = a2;
+            // We use fi.coeff = -1 to tell the caller to treat it as a diseq_lin.
+            fi.coeff = -1;
+            fi.interval = to_interval(c, false, fi.coeff, lo_val, lo, hi_val, hi);
+            add_non_unit_side_conds(fi, b1, e1, b2, e2);
+            return true;
+        }
+        return false;
+    }
+
     void forbidden_intervals::add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2) {
         if (fi.coeff == 1)
             return;

src/math/polysat/forbidden_intervals.h

@@ -45,6 +45,11 @@ namespace polysat {
             rational const & a2, pdd const& b2, pdd const& e2,
             fi_record& fi);
 
+        bool match_linear4(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);
+
         void add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2);
 
     public:

src/math/polysat/viable.cpp

@@ -276,7 +276,67 @@ namespace polysat {
         auto* e = m_diseq_lin[v];
         if (!e)
             return true;
-        LOG("refine-disequal-lin is TBD");
+        entry* first = e;
+        rational const& max_value = s.var2pdd(v).max_value();
+        rational mod_value = max_value + 1;
+
+        do {
+            LOG("refine-disequal-lin for src: " << e->src);
+            // We have:
+            //      a1*v + b1 >  a2*v + b2  if e->src.is_positive()
+            //      a1*v + b1 >= a2*v + b2  if e->src.is_negative()
+            // Note that e->interval is meaningless in this case,
+            // we just use it to transport the values a1,b1,a2,b2.
+            rational const& a1 = e->interval.lo_val();
+            rational const& b1 = e->interval.lo().val();
+            rational const& a2 = e->interval.hi_val();
+            rational const& b2 = e->interval.hi().val();
+            rational lhs = a1 * val + b1;
+            rational rhs = a2 * val + b2;
+
+            auto delta_l = [&](rational const& val) {
+                rational m1 = ceil((rhs + 1) / a2);
+                int corr = e->src.is_negative() ? 1 : 0;
+                rational m3 = (lhs - rhs + corr) / (a1 - a2);
+                if (m3 <= 0)
+                    m3 = m1;  // remove m3 from the minimum
+
+                return std::min(m1, m3) - 1;
+            };
+            auto delta_u = [&](rational const& val) {
+                rational m1 = ceil((mod_value - lhs) / a1);
+                rational m2 = mod_value - val;
+                int corr = e->src.is_negative() ? 1 : 0;
+                rational m3 = (lhs - rhs + corr) / (a2 - a1);
+                if (m3 <= 0)
+                    m3 = m2;  // remove m3 from the minimum
+
+                return std::min(m1, std::min(m2, m3)) - 1;
+            };
+
+            if (lhs > rhs || (e->src.is_negative() && lhs == rhs)) {
+                rational lo = val - delta_l(val);
+                rational hi = val + delta_u(val) + 1;
+
+                // TODO: increase interval
+                LOG("refine-disequal-lin: " << " [" << lo << ", " << hi << "[");
+                // SASSERT(false);
+
+                SASSERT(0 <= lo);
+                SASSERT(hi <= max_value);
+                pdd lop = s.var2pdd(v).mk_val(lo);
+                pdd hip = s.var2pdd(v).mk_val(hi);
+                entry* ne = alloc_entry();
+                ne->src = e->src;
+                ne->side_cond = e->side_cond;
+                ne->coeff = 1;
+                ne->interval = eval_interval::proper(lop, lo, hip, hi);
+                intersect(v, ne);
+                return false;
+            }
+            e = e->next();
+        }
+        while (e != first);
         return true;
     }
 
@@ -313,6 +373,7 @@ namespace polysat {
         }         
         while (e != first);
         return false;
+#undef CHECK_RETURN
     }
 
     bool viable::is_viable(pvar v, rational const& val) { 

src/math/polysat/viable.h

@@ -74,7 +74,8 @@ namespace polysat {
 
         /**
          * update state of viable for pvar v
-         * based on affine constraints
+         * based on affine constraints.
+         * Returns true if the state has been changed.
          */
         bool intersect(pvar v, signed_constraint const& c);