use native sdiv

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/ast/sls/sls_bv_eval.cpp

@@ -724,11 +724,11 @@ namespace sls {
         case OP_BSMOD:
         case OP_BSMOD_I:
         case OP_BSMOD0:
+            return true;
+        default:
         case OP_BSDIV:
         case OP_BSDIV_I:
         case OP_BSDIV0:
-            return true;
-        default:
             return false;
         }
     }
@@ -916,15 +916,17 @@ namespace sls {
         case OP_BSMUL_OVFL:
             verbose_stream() << mk_pp(e, m) << "\n";
             return false;
+        case OP_BSDIV:
+        case OP_BSDIV_I:
+        case OP_BSDIV0:
+            return try_repair_sdiv(assign_value(e), wval(e, 0), wval(e, 1), i);
         case OP_BSREM:
         case OP_BSREM_I:
         case OP_BSREM0:
         case OP_BSMOD:
         case OP_BSMOD_I:
         case OP_BSMOD0:
-        case OP_BSDIV:
-        case OP_BSDIV_I:
-        case OP_BSDIV0:
+
             UNREACHABLE();
             // these are currently compiled to udiv and urem.
             // there is an equation that enforces equality between the semantics
@@ -1223,6 +1225,51 @@ namespace sls {
         return a.set_random(m_rand);
     }
 
+
+    bool bv_eval::try_repair_sdiv(bvect const& e, bvval& a, bvval& b, unsigned i) {
+
+        bool sign_a = a.sign();
+        bool sign_b = b.sign();
+        bool sign_e = e.get(a.bw - 1);
+
+        // y = 0, x >= 0 -> -1
+        if (i == 0 && b.is_zero() && a.is_ones(e) && a.try_set(m_zero))
+            return true;
+        if (i == 0 && b.is_zero() && a.is_ones(e) && a.try_set_bit(a.bw - 1, false))
+            return true;
+
+        if (i == 1 && !sign_a && a.is_ones(e) && b.try_set(m_zero))
+            return true;
+
+        // y = 0, x < 0 -> 1
+        if (i == 0 && b.is_zero() && a.is_one(e) && a.try_set(m_minus_one))
+            return true;
+
+        if (i == 1 && sign_a && a.is_one(e) && b.try_set(m_zero))
+            return true;
+
+        // x = 0, y != 0 -> 0
+        if (i == 0 && a.is_zero(e) && !b.is_zero() && a.try_set(m_zero))
+            return true;
+        if (i == 1 && a.is_zero(e) && a.is_zero() && b.try_set_bit(ctx.rand(a.bw), true))
+            return true;
+
+        // e = x udiv y
+        // e = 0 => x != ones
+        // y = 0 => e = -1        // nothing to repair on a
+        // e != -1 => max(y) >=u e
+
+        //IF_VERBOSE(0, verbose_stream() << "sdiv " << e << " " << a << " " << b << "\n";);
+
+        // e = udiv(abs(x), abs(y))
+        // x > 0, y < 0 -> -e
+        // x < 0, y > 0 -> -e
+        // x > 0, y > 0 -> e
+        // x < 0, y < 0 -> e
+
+        return try_repair_udiv(e, a, b, i);
+    }
+
     bool bv_eval::try_repair_bnot(bvect const& e, bvval& a) {
         for (unsigned i = 0; i < a.nw; ++i)
             m_tmp[i] = ~e[i];        

src/ast/sls/sls_bv_eval.h

@@ -110,6 +110,7 @@ namespace sls {
         bool try_repair_lshr1(bvect const& e, bvval const& a, bvval& b);
         bool try_repair_ashr0(bvect const& e, bvval& a, bvval const& b);
         bool try_repair_ashr1(bvect const& e, bvval const& a, bvval& b);
+        bool try_repair_sdiv(bvect const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_bit2bool(bvval& a, unsigned idx);
         bool try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i);
@@ -126,6 +127,7 @@ namespace sls {
         bool try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_eq(bool is_true, bvval& a, bvval const& b);
         bool try_repair_eq(app* e, unsigned i);
+
         bool try_repair_int2bv(bvect const& e, expr* arg);
         void add_p2_1(bvval const& a, bvect& t) const;
 

src/ast/sls/sls_bv_lookahead.cpp

@@ -587,8 +587,16 @@ namespace sls {
 #endif
 
 #if 1
-                        if (allow_costly_flips(mt)) 
+                        if (allow_costly_flips(mt))
                             ctx.flip(v);                        
+                        else if (false) {
+                            sat::bool_var_set rotated;
+                            unsigned budget = 100;
+                            bool rot = ctx.try_rotate(v, rotated, budget);
+                            (void)rot;
+                            TRACE("bv", tout << "rotate " << v << " " << rot << " " << rotated << "\n";);
+                            verbose_stream() << "rotate " << v << " " << rot << " " << rotated << "\n";
+                        }
 #endif
 
                     }

src/ast/sls/sls_bv_terms.cpp

@@ -40,7 +40,7 @@ namespace sls {
     expr_ref bv_terms::ensure_binary(expr* e) {
         expr* x, * y;
         expr_ref r(m);
-        if (bv.is_bv_sdiv(e, x, y) || bv.is_bv_sdiv0(e, x, y) || bv.is_bv_sdivi(e, x, y))
+        if (false && (bv.is_bv_sdiv(e, x, y) || bv.is_bv_sdiv0(e, x, y) || bv.is_bv_sdivi(e, x, y)))
             r = mk_sdiv(x, y);
         else if (bv.is_bv_smod(e, x, y) || bv.is_bv_smod0(e, x, y) || bv.is_bv_smodi(e, x, y))
             r = mk_smod(x, y);

src/util/uint_set.h

@@ -369,3 +369,8 @@ inline std::ostream& operator<<(std::ostream& out, indexed_uint_set const& s) {
     for (unsigned i : s) out << i << " ";
     return out;
 }
+
+inline std::ostream& operator<<(std::ostream& out, tracked_uint_set const& s) {
+    for (unsigned i : s) out << i << " ";
+    return out;
+}