weed out some bugs, add more bv op support in intblast and polysat solvers

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

src/sat/smt/polysat/core.cpp

@@ -140,14 +140,14 @@ namespace polysat {
         for (; i < sz && j < 2; ++i)
             if (!is_assigned(vars[i]))
                 std::swap(vars[i], vars[j++]);
-        sc.set_num_watch(i);
+        sc.set_num_watch(j);
-        if (i > 0)
+        if (j > 0)
             add_watch(idx, vars[0]);
-        if (i > 1)
+        if (j > 1)
             add_watch(idx, vars[1]);
         IF_VERBOSE(10, verbose_stream() << "add watch " << sc << " " << vars << "  ";
-                    if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") ";
+                    if (j > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") ";
-                    if (vars.size() > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") ";
+                    if (j > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") ";
                     verbose_stream() << "\n");
         s.trail().push(mk_add_watch(*this));
         return idx;
@@ -227,7 +227,6 @@ namespace polysat {
         m_assignment.push(v , value);
         s.trail().push(mk_assign_var(v, *this));
 
-        return; 
         // update the watch lists for pvars
         // remove constraints from m_watch[v] that have more than 2 free variables.
         // for entries where there is only one free variable left add to viable set 
@@ -242,7 +241,7 @@ namespace polysat {
             bool swapped = false;
             for (unsigned i = vars.size(); i-- > 2; ) {
                 if (!is_assigned(vars[i])) {
-                    verbose_stream() << "watch instead " << idx << " " << vars[i] << "instead of " << vars[0] << "\n";
+                    verbose_stream() << "watch instead " << vars[i] << " instead of " << vars[0] << " for " << idx << "\n";
                     add_watch(idx, vars[i]);
                     std::swap(vars[i], vars[0]);
                     swapped = true;

src/sat/smt/polysat/types.h

@@ -59,24 +59,6 @@ namespace polysat {
             return out << "v" << d.eq().first << " == v" << d.eq().second << "@" << d.level();
     }
 
-    struct trailing_bits {
-        unsigned length;
-        rational bits;
-        bool positive;
-        unsigned src_idx;
-    };
-
-    struct leading_bits {
-        unsigned length;
-        bool positive; // either all 0 or all 1
-        unsigned src_idx;
-    };
-
-    struct single_bit {
-        bool positive;
-        unsigned position;
-        unsigned src_idx;
-    };
 
     struct fixed_bits {
         unsigned hi = 0;

src/sat/smt/polysat/viable.h

@@ -33,6 +33,26 @@ namespace polysat {
         resource_out,
     };
 
+    struct trailing_bits {
+        unsigned length;
+        rational bits;
+        bool positive;
+        unsigned src_idx;
+    };
+
+    struct leading_bits {
+        unsigned length;
+        bool positive; // either all 0 or all 1
+        unsigned src_idx;
+    };
+
+    struct single_bit {
+        bool positive;
+        unsigned position;
+        unsigned src_idx;
+    };
+
+
     class core;
     class constraints;
 

src/sat/smt/polysat_internalize.cpp

@@ -139,20 +139,21 @@ namespace polysat {
         case OP_ZERO_EXT:         internalize_zero_extend(a); break;
         case OP_SIGN_EXT:         internalize_sign_extend(a); break; 
 
-            // polysat::solver should also support at least:
+        case OP_BSREM:          
+        case OP_BSREM_I:          
+        case OP_BSMOD:            
+        case OP_BSMOD_I:         
+        case OP_BSDIV:            
+        case OP_BSDIV_I:
+            expr2pdd(a);
+            m_delayed_axioms.push_back(a);            
+            ctx.push(push_back_vector(m_delayed_axioms));
+            break;
+
         case OP_BREDAND: // x == 2^K - 1        unary, return single bit, 1 if all input bits are set.
         case OP_BREDOR:  // x > 0               unary, return single bit, 1 if at least one input bit is set.
         case OP_BCOMP:   // x == y              binary, return single bit, 1 if the arguments are equal.
-        case OP_BSDIV:            
-        case OP_BSREM:            
-        case OP_BSMOD:     
-        case OP_BSDIV_I:            
-        case OP_BSREM_I:                        
-        case OP_BSMOD_I:
 
-            IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n");
-            NOT_IMPLEMENTED_YET();
-            return;
         default:
             IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n");
             NOT_IMPLEMENTED_YET();
@@ -263,7 +264,94 @@ namespace polysat {
         expr* x, * y;
         VERIFY(bv.is_bv_shl(n, x, y));
         m_core.shl(expr2pdd(x), expr2pdd(y), expr2pdd(n));
-    }  
+    }
+
+    bool solver::propagate_delayed_axioms() {
+        if (m_delayed_axioms_qhead == m_delayed_axioms.size())
+            return false;
+        ctx.push(value_trail(m_delayed_axioms_qhead));
+        for (; m_delayed_axioms_qhead < m_delayed_axioms.size() && !inconsistent(); ++m_delayed_axioms_qhead) {
+            app* e = m_delayed_axioms[m_delayed_axioms_qhead];
+            expr* x, *y;
+            if (bv.is_bv_sdiv(e, x, y))
+                axiomatize_sdiv(e, x, y);
+            else if (bv.is_bv_sdivi(e, x, y))
+                axiomatize_sdiv(e, x, y);
+            else if (bv.is_bv_srem(e, x, y))
+                axiomatize_srem(e, x, y);
+            else if (bv.is_bv_sremi(e, x, y))
+                axiomatize_srem(e, x, y);
+            else if (bv.is_bv_smod(e, x, y))
+                axiomatize_smod(e, x, y);
+            else if (bv.is_bv_smodi(e, x, y))
+                axiomatize_smod(e, x, y);
+            else
+                UNREACHABLE();
+        }
+        return true;
+    }
+
+    // y = 0 -> x
+    // else x - sdiv(x, y) * y
+    void solver::axiomatize_srem(app* e, expr* x, expr* y) {
+        unsigned sz = bv.get_bv_size(x);
+        sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz));
+        add_clause(~y_eq0, eq_internalize(e, x));
+        add_clause(y_eq0, eq_internalize(e, bv.mk_bv_mul(bv.mk_bv_sdiv(x, y), y)));
+    }
+
+    // u := umod(x, y)
+    // u = 0 ->  0
+    // y = 0 ->  x
+    // x < 0, y < 0 ->  -u
+    // x < 0, y >= 0 ->  y - u
+    // x >= 0, y < 0 ->  y + u
+    // x >= 0, y >= 0 ->  u
+    void solver::axiomatize_smod(app* e, expr* x, expr* y) {
+        unsigned sz = bv.get_bv_size(x);
+        expr* u = bv.mk_bv_urem(x, y);
+        rational N = rational::power_of_two(bv.get_bv_size(x));
+        expr* signx = bv.mk_ule(bv.mk_numeral(N / 2, sz), x);
+        expr* signy = bv.mk_ule(bv.mk_numeral(N / 2, sz), y);
+        sat::literal lsignx = mk_literal(signx);
+        sat::literal lsigny = mk_literal(signy);
+        sat::literal u_eq0 = eq_internalize(u, bv.mk_zero(sz)); 
+        sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz)); 
+        add_clause(~u_eq0, eq_internalize(e, bv.mk_zero(sz)));
+        add_clause(u_eq0, ~y_eq0, eq_internalize(e, x));
+        add_clause(~lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_neg(u)));
+        add_clause(y_eq0, ~lsignx, lsigny, eq_internalize(e, bv.mk_bv_sub(y, u)));
+        add_clause(y_eq0, lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_add(y, u)));
+        add_clause(y_eq0, lsignx, lsigny, eq_internalize(e, u));
+    }
+
+
+    // d = udiv(abs(x), abs(y))
+    // y = 0, x > 0 -> 1
+    // y = 0, x <= 0 -> -1
+    // x = 0, y != 0 -> 0
+    // x > 0, y < 0 -> -d
+    // x < 0, y > 0 -> -d
+    // x > 0, y > 0 -> d
+    // x < 0, y < 0 -> d
+    void solver::axiomatize_sdiv(app* e, expr* x, expr* y) {
+        unsigned sz = bv.get_bv_size(x);
+        rational N = rational::power_of_two(bv.get_bv_size(x));
+        expr* signx = bv.mk_ule(bv.mk_numeral(N/2, sz), x);
+        expr* signy = bv.mk_ule(bv.mk_numeral(N/2, sz), y);
+        expr* absx = m.mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N-1, sz), x), x);
+        expr* absy = m.mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N-1, sz), y), y);
+        expr* d = bv.mk_bv_udiv(absx, absy);
+        sat::literal lsignx = mk_literal(signx);
+        sat::literal lsigny = mk_literal(signy);
+        sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz));
+        add_clause(~y_eq0, ~lsignx, eq_internalize(e, bv.mk_numeral(1, sz)));
+        add_clause(~y_eq0, lsignx, eq_internalize(e, bv.mk_numeral(N-1, sz)));
+        add_clause(y_eq0, lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_neg(d)));
+        add_clause(y_eq0, ~lsignx, lsigny, eq_internalize(e, bv.mk_bv_neg(d)));
+        add_clause(y_eq0, lsignx, lsigny, eq_internalize(e, d));
+        add_clause(y_eq0, ~lsignx, ~lsigny, eq_internalize(e, d));
+    }    
 
     void solver::internalize_urem_i(app* rem) {
         expr* x, *y;

src/sat/smt/polysat_solver.cpp

@@ -52,7 +52,7 @@ namespace polysat {
     }
 
     bool solver::unit_propagate() {
-        return m_core.propagate();
+        return m_core.propagate() || propagate_delayed_axioms();
     }
 
     sat::check_result solver::check() {
@@ -266,32 +266,6 @@ namespace polysat {
 
     void solver::add_polysat_clause(char const* name, core_vector cs, bool is_redundant) {
         sat::literal_vector lits;
-        signed_constraint sc;
-        unsigned constraint_count = 0;
-        for (auto e : cs) {
-            if (std::holds_alternative<signed_constraint>(e)) {
-                sc = *std::get_if<signed_constraint>(&e);
-                constraint_count++;
-            }
-        }
-        if (constraint_count == 1) {
-            auto lit = ctx.mk_literal(constraint2expr(sc));
-            svector<euf::enode_pair> eqs;
-            for (auto e : cs) {
-                if (std::holds_alternative<dependency>(e)) {
-                    auto d = *std::get_if<dependency>(&e);
-                    if (d.is_literal())
-                        lits.push_back(d.literal());
-                    else if (d.is_eq()) {
-                        auto [v1, v2] = d.eq();
-                        eqs.push_back({ var2enode(v1), var2enode(v2) });
-                    }
-                }
-            }
-            ctx.propagate(lit, euf::th_explain::propagate(*this, lits, eqs, lit, nullptr));
-            return;
-        }
-
         for (auto e : cs) {
             if (std::holds_alternative<dependency>(e)) {
                 auto d = *std::get_if<dependency>(&e);

src/sat/smt/polysat_solver.h

@@ -130,6 +130,12 @@ namespace polysat {
         void internalize_udiv_i(app* e);
         void internalize_urem_i(app* e);
         void internalize_div_rem(app* e, bool is_div);
+        void axiomatize_srem(app* e, expr* x, expr* y);
+        void axiomatize_smod(app* e, expr* x, expr* y);
+        void axiomatize_sdiv(app* e, expr* x, expr* y);
+        unsigned m_delayed_axioms_qhead = 0;
+        ptr_vector<app> m_delayed_axioms;
+        bool propagate_delayed_axioms();
         void internalize_polysat(app* a);
         void assert_bv2int_axiom(app * n);
         void assert_int2bv_axiom(app* n);