Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat

src/math/polysat/saturation.cpp

@@ -1700,19 +1700,19 @@ namespace polysat {
         if (y1 == null_var && y2 == null_var)
             return false;
         y = (y1 == null_var) ? y2 : y1;
+        if (!s.is_assigned(y))
+            return false;
         rational y0 = s.get_value(y);
 
         vector<signed_constraint> bounds;
         rational x_min, x_max;
-        if (!s.m_viable.has_max_forbidden(x, a_l_b.as_signed_constraint(), x_min, x_max, bounds))
+        if (!s.m_viable.has_max_forbidden(x, a_l_b.as_signed_constraint(), x_max, x_min, bounds))
             return false;
 
-        VERIFY(x_min != x_max);
-        // [x_min, x_max[ is allowed interval.
+        // retrieved maximal forbidden interval [x_max, x_min[.
+        // [x_min, x_max[ is the allowed interval.
         // compute [x_min, x_max - 1]
-        
-        // From forbidden interval [x_min, x_max[ compute
-        // allowed range: [x_max, x_min - 1]
+        VERIFY(x_min != x_max);
         SASSERT(0 <= x_min && x_min <= m.max_value());
         SASSERT(0 <= x_max && x_max <= m.max_value());
         rational M = m.two_to_N();

src/math/polysat/solver.cpp

@@ -904,6 +904,10 @@ namespace polysat {
             if (m_bvars.is_true(lit))  // may happen if we only use the clause to justify a new constraint; it is not a real lemma
                 return std::nullopt;
             if (!m_bvars.is_assigned(lit)) {
+                DEBUG_CODE({
+                    if (lit2cnstr(lit).eval(*this) != l_undef)
+                        LOG("WARNING: missed evaluation of literal: " << lit_pp(*this, lit));
+                });
                 SASSERT(!is_propagation);
                 is_propagation = true;
                 continue;

src/math/polysat/ule_constraint.cpp

@@ -53,6 +53,20 @@ Note:
 
      It can be seen as an instance of lemma 5.2 of Supratik and John.
 
+
+Useful equivalences:
+
+    - p <= q    <=>   q - p <= -p - 1           (periodicity 3 if used for rewriting)
+                <=>   -q - 1 <= p - q - 1       (after rewriting twice)
+
+    - p <= q    <=>   p <= p - q - 1
+
+    - p <= q    <=>   -q - 1 <= -p - 1          (combine previous rules)
+
+    - p <= q    <=>   q - p <= q                (another combination)
+
+    - p <= q    ==>   p == 0  ||  -q <= -p
+
 --*/
 
 #include "math/polysat/constraint.h"
@@ -98,6 +112,9 @@ namespace {
             is_positive = true;
         }
 #endif
+
+        // -1 <= p  -->   p + 1 <= 0
+        // 1 <= p   -->   p - 1 <= -2           (--> p > 0 later)
         // k <= p   -->   p - k <= - k - 1
         if (lhs.is_val()) {
             pdd k = lhs;
@@ -106,6 +123,18 @@ namespace {
         }
         // NSB: why this?
 
+        // p + 1 <= p  -->  p + 1 <= 0
+        // p <= p - 1  -->  p <= 0
+        //
+        // p + k <= p       -->  p + k <= k - 1
+        // p     <= p - k   -->  p     <= k - 1
+        if ((lhs - rhs).is_val()) {
+            pdd k = lhs - rhs;
+            rhs = k - 1;
+        }
+
+        // TODO: rewrite if p - q has less variables than p, q themselves? or if one of the rules allows separating variables.
+
         // p >  -2   -->   p + 1 <= 0
         // p <= -2   -->   p + 1 >  0
         if (rhs.is_val() && (rhs + 2).is_zero()) {

src/math/polysat/variable_elimination.cpp

@@ -697,15 +697,15 @@ namespace polysat {
         pdd a_pi = get_pseudo_inverse(a, a_parity);
 #else
         pdd a_pi = s.pseudo_inv(a);
-        //precondition.insert(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?)
-        precondition.insert(~s.parity_at_most(a, a_parity));
+        //precondition.insert_eval(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?)
+        precondition.insert_eval(~s.parity_at_most(a, a_parity));
 #endif
         
         pdd shift = a;
         
         if (a_parity > 0) {
             shift = s.lshr(a1, a1.manager().mk_val(a_parity));
-            precondition.insert(~s.eq(rational::power_of_two(a_parity) * shift, a1)); // TODO: Or s.parity_at_least(a1, a_parity) but we want to reuse the variable introduced by the shift
+            precondition.insert_eval(~s.eq(rational::power_of_two(a_parity) * shift, a1)); // TODO: Or s.parity_at_least(a1, a_parity) but we want to reuse the variable introduced by the shift
         }
         LOG("Forced elimination: " << a_pi * (-b) * shift + b1);
         LOG("a: " << a);

src/math/polysat/viable.cpp

@@ -744,10 +744,9 @@ namespace polysat {
             return false;
         entry const* e0 = e;
 
-
         do {
             entry const* n = e->next();
-            while (n != first) {
+            while (n != e0) {
                 entry const* n1 = n->next();
                 if (n1 == e)
                     break;
@@ -756,16 +755,21 @@ namespace polysat {
                         break;
                 n = n1;
             }
+            if (e == n) {
+                SASSERT_EQ(e, e0);
+                // VERIFY(false);
+                return false;
+            }
 
             if (e == e0) {
-                out_hi = n->interval.lo_val();
+                out_lo = n->interval.lo_val();
                 if (!n->interval.lo().is_val())
-                    out_c.push_back(s.eq(n->interval.lo(), out_hi));                                
+                    out_c.push_back(s.eq(n->interval.lo(), out_lo));
             }
             else if (n == e0) {
-                out_lo = e->interval.hi_val();
+                out_hi = e->interval.hi_val();
                 if (!e->interval.hi().is_val())
-                    out_c.push_back(s.eq(e->interval.hi(), out_lo));                
+                    out_c.push_back(s.eq(e->interval.hi(), out_hi));
             }            
             else if (!e->interval.is_full()) {
                 auto const& hi = e->interval.hi();