finally!

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/dd/dd_pdd.cpp

@@ -173,7 +173,7 @@ namespace dd {
         std::sort(s.begin(), s.end(), compare_level);
         pdd r(one());
         for (auto const& q : s) 
-            r = (r*mk_var(q.first)) + q.second;            
+            r = (r * mk_var(q.first)) + q.second;            
         return pdd(apply(p.root, r.root, pdd_subst_val_op), this);
     }
 
@@ -218,6 +218,7 @@ namespace dd {
             if (is_val(p) && is_val(q)) return imk_val(val(p) - val(q));
             if (m_semantics != mod2_e) break;
             op = pdd_add_op;
+            Z3_fallthrough;
         case pdd_add_op:
             if (is_zero(p)) return q;
             if (is_zero(q)) return p;
@@ -346,7 +347,8 @@ namespace dd {
                         push(make_node(level_p, lo(n), read(1)));
                         r = make_node(level_p, bd, read(1));
                         npop = 7;
-                    } else {
+                    } 
+                    else {
                         push(make_node(level_p, n, ac));
                         r = make_node(level_p, bd, read(1));
                         npop = 6;
@@ -942,6 +944,8 @@ namespace dd {
     * b := b1*v^m + b2
     * l >= m
     * q, r := quot_rem(a1, b1) 
+    * that is:
+    *     q * b1 + r = a1
     * r = 0
     * result := reduce(v, q*b2*v^{l-m}, b) + reduce(v, a2, b)
     */

src/math/polysat/mul_ovfl_constraint.cpp

@@ -49,26 +49,33 @@ namespace polysat {
         return out << "ovfl*(" << m_p << ", " << m_q << ")";       
     }
 
-    bool mul_ovfl_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q) const {
-        if (!is_positive && (p.is_zero() || q.is_zero() ||
-            p.is_one() || q.is_one()))
-            return true;
+    lbool mul_ovfl_constraint::eval(pdd const& p, pdd const& q) const {
+        if (p.is_zero() || q.is_zero() || p.is_one() || q.is_one())
+            return l_false;
+
         if (p.is_val() && q.is_val()) {
-            bool ovfl = p.val() * q.val() > p.manager().max_value();
-            return is_positive == ovfl;
+            if (p.val() * q.val() > p.manager().max_value())
+                return l_true;
+            else
+                return l_false;
+        }
+        return l_undef;
+    }
+
+    bool mul_ovfl_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q) const {
+        switch (eval(p, q)) {
+        case l_true: return !is_positive;
+        case l_false: return is_positive;
+        default: return false;
         }
-        return false;
     }
 
     bool mul_ovfl_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q) const {
-        if (is_positive && (p.is_zero() || q.is_zero() ||
-            p.is_one() || q.is_one()))
-            return true;
-        if (p.is_val() && q.is_val()) {
-            bool noovfl = p.val() * q.val() <= p.manager().max_value();
-            return is_positive == noovfl;
+        switch (eval(p, q)) {
+        case l_true: return is_positive;
+        case l_false: return !is_positive;
+        default: return false;
         }
-        return false;
     }
 
     bool mul_ovfl_constraint::is_always_false(bool is_positive) const {
@@ -124,11 +131,6 @@ namespace polysat {
         signed_constraint premise = is_positive ? s.ule(p0, p.val()) : s.ule(p.val(), p0);
         signed_constraint conseq = is_positive ? s.ule(bound, q0) : s.ult(q0, bound);
 
-        //std::cout << premise << "\n";
-        //std::cout << sc << "\n";
-        //std::cout << conseq << "\n";
-        //std::cout << "Already true " << conseq.is_currently_true(s) << "\n";
-
         SASSERT(premise.is_currently_true(s));
         SASSERT(bound * p.val() > max);
         SASSERT((bound - 1) * p.val() <= max);

src/math/polysat/mul_ovfl_constraint.h

@@ -26,6 +26,7 @@ namespace polysat {
         bool is_always_false(bool is_positive, pdd const& p, pdd const& q) const;
         bool is_always_true(bool is_positive, pdd const& p, pdd const& q) const;
         bool narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
+        lbool eval(pdd const& p, pdd const& q) const;
 
     public:
         ~mul_ovfl_constraint() override {}

src/math/polysat/viable.cpp

@@ -198,7 +198,7 @@ namespace polysat {
                     rational lambda_l = floor(coeff_val / e->coeff);
                     lo = val - lambda_l;                   
                 }
-                LOG("forbidden interval " << e->interval << " - " << val << " " << coeff_val << " [" << lo << ", " << hi << "[");
+                LOG("forbidden interval " << e->coeff << " * " << e->interval << " [" << lo << ", " << hi << "[");
                 SASSERT(hi <= max_value);
                 entry* ne = alloc_entry();
                 ne->src = e->src;

src/test/polysat.cpp

@@ -956,7 +956,7 @@ namespace polysat {
         s.add_eq(quot * y + rem - x);
         s.add_diseq(a - quot);
         s.add_noovfl(quot, y);     
-        // s.add_ult(rem, x);
+        s.add_ult(rem, x);
         s.check();
         s.expect_sat();
     }