more saturation for overflow

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

src/sat/smt/polysat/saturation.cpp

@@ -175,7 +175,7 @@ namespace polysat {
     }
 
     // Ovfl(x, y) & ~Ovfl(y, z) ==> x > z
-    void saturation::try_umul_ovfl(pvar v, umul_ovfl const& sc) {
+    void saturation::try_umul_monotonicity(umul_ovfl const& sc) {
         auto p = sc.p(), q = sc.q();
         auto match_mul_arg = [&](auto const& sc2) {
             auto p2 = sc2.to_umul_ovfl().p(), q2 = sc2.to_umul_ovfl().q();
@@ -206,6 +206,103 @@ namespace polysat {
         }
     }
 
+    /**
+    * Expand the following axioms:
+    * Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k - 1
+    * Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k - 1 => 0x * 0y >= 2^{N-1}
+    * 
+    * ~Ovfl(x,y) & msb(x) >= k => msb(y) <= N - k - 1
+    * ~Ovfl(x,y) & msb(x) >= k & msb(y) >= N - k - 1 => 0x * 0y < 2^{N-1}
+    */
+    void saturation::try_umul_blast(umul_ovfl const& sc) {
+        auto x = sc.p();
+        auto y = sc.q();
+        if (!x.is_val())
+            return;
+        if (!y.is_val())
+            return;
+        auto N = x.manager().power_of_2();
+        auto d = c.get_dependency(sc.id());
+
+        auto vx = x.val();
+        auto vy = y.val();
+        auto bx = vx.get_num_bits();
+        auto by = vy.get_num_bits();
+        if (bx > by) {
+            std::swap(bx, by);
+            std::swap(x, y);
+        }
+
+        // Keep in mind that
+        // num-bits(0) = 1
+        // num-bits(1) = 1
+        // num-bits(2) = 2
+        // num-bits(4) = 3
+        // msb(0) = 0
+        // msb(1) = 0
+        // msb(2) = 1
+        // msb(3) = 1
+        // msb(2^N - 1) = N-1
+        // msb(x) >= k <=> x >= 2^k,    for k > 0
+        // msb(x) <= k <=> x < 2^{k+1}, for k + 1 < N
+
+        auto msb_ge = [&](pdd const& x, unsigned k) {
+            SASSERT(k > 0);
+            return C.uge(x, rational::power_of_two(k));
+        };
+
+        auto msb_le = [&](pdd const& x, unsigned k) {
+            SASSERT(k + 1 < N);
+            return C.ult(x, rational::power_of_two(k + 1));
+        };
+ 
+        if (sc.sign()) {
+            // Case ~Ovfl(x,y) is asserted by current assignment x * y is overflow
+            SASSERT(bx > 1 && by > 1);
+            SASSERT(bx + by >= N + 1);
+            auto k = bx - 1;
+            if (bx + by > N + 1) 
+                add_clause("~Ovfl(x, y) & msb(x) >= k => msb(y) <= N - k - 1", 
+                    {d, ~msb_ge(x, k), msb_le(y, N - k - 1)},
+                    true);            
+            else {
+                auto x1 = c.mk_zero_extend(1, x);
+                auto y1 = c.mk_zero_extend(1, y);                
+                add_clause("~Ovfl(x, y) & msb(x) >= k & msb(y) >= N - k - 1 => 0x * 0y < 2^{N-1}",
+                    { d, ~msb_ge(x, k),
+                         ~msb_ge(y, N - k - 1),
+                         C.ult(x1 * y1, rational::power_of_two(N - 1))
+                    }, true);
+            }
+        }
+        else {
+            // Case Ovfl(x,y) 
+            if (bx == 0) {
+                add_clause("Ovfl(x, y) => x > 1", { d, C.ugt(x, 1) }, true);
+            }
+            else if (bx + by < N + 1) {
+                SASSERT(bx <= by);
+                auto k = bx - 1;
+                add_clause("Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k - 1",
+                    { d, ~msb_le(x, k), msb_ge(y, N - k - 1) }, true);
+            }
+            else {
+                auto k = bx - 1;
+                auto x1 = c.mk_zero_extend(1, x);
+                auto y1 = c.mk_zero_extend(1, y);
+                add_clause("Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k - 1 = > 0x * 0y >= 2 ^ {N - 1}",
+                    { d, ~msb_le(x, k), ~msb_le(y, N - k - 1), C.uge(x1 * y1, rational::power_of_two(N - 1)) },
+                    true);
+            }
+        }
+    }
+
+
+    void saturation::try_umul_ovfl(pvar v, umul_ovfl const& sc) {
+        try_umul_monotonicity(sc);
+        try_umul_blast(sc);           
+    }
+
     void saturation::try_eq_resolve(pvar v, inequality const& i) {
         if (!i.rhs().is_zero() || i.is_strict())
             return;

src/sat/smt/polysat/saturation.h

@@ -65,6 +65,8 @@ namespace polysat {
         void try_ugt_y(pvar v, inequality const& i);
         void try_ugt_z(pvar z, inequality const& i);
         void try_umul_ovfl(pvar v, umul_ovfl const& sc);
+        void try_umul_monotonicity(umul_ovfl const& sc);
+        void try_umul_blast(umul_ovfl const& sc);
         void try_op(pvar v, signed_constraint& sc, dependency const& d);
 
         signed_constraint ineq(bool is_strict, pdd const& x, pdd const& y);       

src/sat/smt/polysat/types.h

@@ -149,6 +149,7 @@ namespace polysat {
         virtual void get_bitvector_super_slices(pvar v, offset_slices& out) = 0;
         virtual void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slice) = 0;
         virtual pdd  mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) = 0;
+        virtual pdd mk_zero_extend(unsigned sz, pdd const& p) = 0;
         virtual unsigned level(dependency const& d) = 0;
     };
 

src/sat/smt/polysat_internalize.cpp

@@ -858,6 +858,13 @@ namespace polysat {
         return expr2pdd(ite);
     }
 
+    pdd solver::mk_zero_extend(unsigned n, pdd const& p) {
+        expr_ref pe = pdd2expr(p);
+        auto ze = bv.mk_zero_extend(n, pe);
+        ctx.internalize(ze);
+        return expr2pdd(ze);
+    }
+
     dd::pdd solver::expr2pdd(expr* e) {
         return var2pdd(get_th_var(e));
     }

src/sat/smt/polysat_solver.h

@@ -225,6 +225,7 @@ namespace polysat {
         void get_bitvector_suffixes(pvar v, offset_slices& out) override;
         void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits) override;
         pdd  mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) override;
+        pdd mk_zero_extend(unsigned sz, pdd const& p) override;
         unsigned level(dependency const& d) override;
         dependency explain_slice(pvar v, pvar w, unsigned offset);