fix internalization for quot/rem

src/ast/euf/euf_bv_plugin.cpp

@@ -104,8 +104,8 @@ namespace euf {
     }
 
     void bv_plugin::merge_eh(enode* x, enode* y) {
-        SASSERT(x == x->get_root());
+        if (!bv.is_bv(x->get_expr()))
-        SASSERT(x == y->get_root());
+            return;
 
         TRACE("bv", tout << "merge_eh " << g.bpp(x) << " == " << g.bpp(y) << "\n");
         SASSERT(!m_internal);

src/sat/smt/intblast_solver.cpp

@@ -36,6 +36,7 @@ namespace intblast {
                 continue;
             if (any_of(*clause, [&](auto lit) { return s.value(lit) == l_true && !is_bv(lit); }))
                 continue;
+            // TBD: if we associate "status" with clauses, we can also remove theory axioms from polysat
             sat::literal selected_lit = sat::null_literal;
             for (auto lit : *clause) {
                 if (s.value(lit) != l_true)
@@ -269,27 +270,34 @@ namespace intblast {
                     m_trail.push_back(a.mk_mul(args));
                     break;
                 case OP_ULEQ:
+                    bv_expr = ap->get_arg(0);
                     m_trail.push_back(a.mk_le(mk_mod(args.get(0)), mk_mod(args.get(1))));
                     break;
                 case OP_UGEQ:
+                    bv_expr = ap->get_arg(0);
                     m_trail.push_back(a.mk_ge(mk_mod(args.get(0)), mk_mod(args.get(1))));
                     break;
                 case OP_ULT:
+                    bv_expr = ap->get_arg(0);
                     m_trail.push_back(a.mk_lt(mk_mod(args.get(0)), mk_mod(args.get(1))));
                     break;
                 case OP_UGT:
+                    bv_expr = ap->get_arg(0);
                     m_trail.push_back(a.mk_gt(mk_mod(args.get(0)), mk_mod(args.get(1))));
                     break;
                 case OP_SLEQ: 
+                    bv_expr = ap->get_arg(0);
                     m_trail.push_back(a.mk_le(mk_smod(args.get(0)), mk_smod(args.get(1))));
                     break;
                 case OP_SGEQ:
                     m_trail.push_back(a.mk_ge(mk_smod(args.get(0)), mk_smod(args.get(1))));
                     break;
                 case OP_SLT:
+                    bv_expr = ap->get_arg(0);
                     m_trail.push_back(a.mk_lt(mk_smod(args.get(0)), mk_smod(args.get(1))));
                     break;
                 case OP_SGT:
+                    bv_expr = ap->get_arg(0);
                     m_trail.push_back(a.mk_gt(mk_smod(args.get(0)), mk_smod(args.get(1))));
                     break;
                 case OP_BNEG:
@@ -342,6 +350,12 @@ namespace intblast {
                     m_trail.push_back(m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_idiv(x, y)));
                     break;
                 }
+                case OP_BUMUL_NO_OVFL: {
+                    expr* x = args.get(0), * y = args.get(1);
+                    bv_expr = ap->get_arg(0);
+                    m_trail.push_back(a.mk_lt(a.mk_mul(mk_mod(x), mk_mod(y)), a.mk_int(bv_size())));
+                    break;
+                }
                 case OP_BNOT:
                 case OP_BNAND:
                 case OP_BNOR:

src/sat/smt/polysat/polysat_core.cpp

@@ -108,6 +108,7 @@ namespace polysat {
         m_watch.push_back({});
         m_var_queue.mk_var_eh(v);
         m_viable.ensure_var(v);
+        m_values.push_back(rational::zero());
         s.trail().push(mk_add_var(*this));
         return v;
     }
@@ -118,6 +119,7 @@ namespace polysat {
         m_activity.pop_back();
         m_justification.pop_back();
         m_watch.pop_back();
+        m_values.pop_back();
         m_var_queue.del_var_eh(v);
     }
 

src/sat/smt/polysat/polysat_viable.cpp

@@ -67,13 +67,17 @@ namespace polysat {
     };
 
     viable::entry* viable::alloc_entry(pvar var, unsigned constraint_index) {
+        entry* e = nullptr;
         if (m_alloc.empty())
-            return alloc(entry);
+            e = alloc(entry);
-        auto* e = m_alloc.back();
+        else {
+            e = m_alloc.back();
+            m_alloc.pop_back();
+        }
         e->reset();
         e->var = var;
         e->constraint_index = constraint_index;
-        m_alloc.pop_back();
+        
         return e;
     }
 

src/sat/smt/polysat_internalize.cpp

@@ -192,32 +192,54 @@ namespace polysat {
 
     void solver::internalize_udiv_i(app* e) {
         expr* x, *y;
-        VERIFY(bv.is_bv_udivi(e, x, y) || bv.is_bv_udiv(e, x, y));
+        expr_ref rm(m);
-        app_ref rm(bv.mk_bv_urem_i(x, y), m);
+        if (bv.is_bv_udivi(e, x, y))
+            rm = bv.mk_bv_urem_i(x, y);
+        else if (bv.is_bv_udiv(e, x, y))
+            rm = bv.mk_bv_urem(x, y);
+        else
+            UNREACHABLE();
         internalize(rm);
     }
 
-    void solver::internalize_urem_i(app* e) {
+    void solver::internalize_urem_i(app* rem) {
         expr* x, *y;
-        if (expr2enode(e))
+        euf::enode* n = expr2enode(rem);
+        SASSERT(n && n->is_attached_to(get_id()));
+        theory_var v = n->get_th_var(get_id());
+        if (m_var2pdd_valid.get(v, false))
             return;
-        VERIFY(bv.is_bv_uremi(e, x, y) || bv.is_bv_urem(e, x, y));
+        expr_ref quot(m);
-        auto [quot, rem] = quot_rem(x, y);
+        if (bv.is_bv_uremi(rem, x, y))
-        internalize_set(e, rem);
+            quot = bv.mk_bv_udiv_i(x, y);
-        internalize_set(bv.mk_bv_udiv_i(x, y), quot);
+        else if (bv.is_bv_urem(rem, x, y))
+            quot = bv.mk_bv_udiv(x, y);
+        else
+            UNREACHABLE();
+        m_var2pdd_valid.setx(v, true, false);
+        ctx.internalize(quot);
+        m_var2pdd_valid.setx(v, false, false);
+        quot_rem(quot, rem, x, y);
     }
     
-    std::pair<pdd, pdd> solver::quot_rem(expr* x, expr* y) {
+    void solver::quot_rem(expr* quot, expr* rem, expr* x, expr* y) {
         pdd a = expr2pdd(x);
         pdd b = expr2pdd(y);
+        euf::enode* qn = expr2enode(quot);
+        euf::enode* rn = expr2enode(rem);
         auto& m = a.manager();
         unsigned sz = m.power_of_2();
-        if (b.is_zero())
+        if (b.is_zero()) {
             // By SMT-LIB specification, b = 0 ==> q = -1, r = a.
-            return { m.mk_val(m.max_value()), a };
+            internalize_set(quot, m.mk_val(m.max_value()));
-
+            internalize_set(rem, a);
-        if (b.is_one())
+            return;
-            return { a, m.zero() };
+        }
+        if (b.is_one()) {
+            internalize_set(quot, a);
+            internalize_set(rem, m.zero());
+            return;
+        }
 
         if (a.is_val() && b.is_val()) {
             rational const av = a.val();
@@ -231,19 +253,13 @@ namespace polysat {
             SASSERT(b.val() * q.val() + r.val() <= m.max_value());
             SASSERT(r.val() <= (b * q + r).val());
             SASSERT(r.val() < b.val());
-            return { std::move(q), std::move(r) };
+            internalize_set(quot, q);
+            internalize_set(rem, r);
+            return;
         }       
         
-        expr* quot = bv.mk_bv_udiv_i(x, y);
+        pdd r = var2pdd(rn->get_th_var(get_id()));
-        expr* rem = bv.mk_bv_urem_i(x, y);
+        pdd q = var2pdd(qn->get_th_var(get_id()));
-
-        ctx.internalize(quot);
-        ctx.internalize(rem);
-        auto quotv = expr2enode(quot)->get_th_var(get_id());
-        auto remv  = expr2enode(rem)->get_th_var(get_id());
-
-        pdd q = var2pdd(quotv);
-        pdd r = var2pdd(remv);
 
         // Axioms for quotient/remainder
         // 
@@ -267,7 +283,6 @@ namespace polysat {
         if (!c_eq.is_always_false())
             add_polysat_clause("[axiom] quot_rem 5", { ~c_eq, m_core.eq(q + 1) }, false);
 
-        return { std::move(q), std::move(r) };
     }
 
     void solver::internalize_div_rem(app* e, bool is_div) {

src/sat/smt/polysat_solver.h

@@ -126,7 +126,7 @@ namespace polysat {
         pdd var2pdd(euf::theory_var v);
         void internalize_set(expr* e, pdd const& p);
         void internalize_set(euf::theory_var v, pdd const& p);
-        std::pair<pdd, pdd> quot_rem(expr* x, expr* y);
+        void quot_rem(expr* quot, expr* rem, expr* x, expr* y);
 
 
         // callbacks from core