port equality propagation changes to new core

src/sat/smt/arith_axioms.cpp

@@ -482,4 +482,28 @@ namespace arith {
         return all_divs_valid;
     }
 
+    void solver::fixed_var_eh(theory_var v, lp::constraint_index ci1, lp::constraint_index ci2, rational const& bound) {
+        theory_var w = euf::null_theory_var;
+        enode* x = var2enode(v);
+        if (bound.is_zero()) 
+            w = lp().local_to_external(get_zero(a.is_int(x->get_expr())));
+        else if (bound.is_one())
+            w = lp().local_to_external(get_one(a.is_int(x->get_expr())));
+        else if (!m_value2var.find(bound, w))
+            return;
+        enode* y = var2enode(w);
+        if (x->get_sort() != y->get_sort())
+            return;
+        if (x->get_root() == y->get_root())
+            return;
+        SASSERT(a.is_numeral(y->get_expr()));
+        reset_evidence();
+        set_evidence(ci1, m_core, m_eqs);
+        set_evidence(ci2, m_core, m_eqs);
+        ++m_stats.m_fixed_eqs;
+        auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, x, y);
+        ctx.propagate(x, y, jst->to_index());
+    }
+
+
 }

src/sat/smt/arith_internalize.cpp

@@ -496,6 +496,7 @@ namespace arith {
                     vi = lp().add_var(v, a.is_int(term));
                     add_def_constraint_and_equality(vi, lp::GE, st.offset());
                     add_def_constraint_and_equality(vi, lp::LE, st.offset());
+                    register_fixed_var(v, st.offset());
                     return v;
                 }
                 if (!st.offset().is_zero()) {
@@ -674,5 +675,24 @@ namespace arith {
         return false;
     }
 
+    struct solver::undo_value : public trail {
+        solver& s;
+        undo_value(solver& s):s(s) {}
+        void undo() override {
+            s.m_value2var.erase(s.m_fixed_values.back());
+            s.m_fixed_values.pop_back();
+        }
+    };
+
+
+    void solver::register_fixed_var(theory_var v, rational const& value) {
+        if (m_value2var.contains(value)) 
+            return;
+        m_fixed_values.push_back(value);
+        m_value2var.insert(value, v);
+        ctx.push(undo_value(*this));
+    }
+
+
 }
 

src/sat/smt/arith_solver.cpp

@@ -299,8 +299,6 @@ namespace arith {
             return;
         enode* n1 = var2enode(uv);
         enode* n2 = var2enode(vv);
-        if (!ctx.is_shared(n1) || !ctx.is_shared(n2))
-            return;
         expr* e1 = n1->get_expr();
         expr* e2 = n2->get_expr();
         if (m.is_ite(e1) || m.is_ite(e2))
@@ -394,12 +392,13 @@ namespace arith {
 
     }
 
-    void solver::propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, api_bound& b, rational const& value) {
+    void solver::propagate_eqs(lp::tv t, lp::constraint_index ci1, lp::lconstraint_kind k, api_bound& b, rational const& value) {
-        if (k == lp::GE && set_lower_bound(t, ci, value) && has_upper_bound(t.index(), ci, value)) {
+        lp::constraint_index ci2;
-            fixed_var_eh(b.get_var(), value);
+        if (k == lp::GE && set_lower_bound(t, ci1, value) && has_upper_bound(t.index(), ci2, value)) {
+            fixed_var_eh(b.get_var(), ci1, ci2, value);
         }
-        else if (k == lp::LE && set_upper_bound(t, ci, value) && has_lower_bound(t.index(), ci, value)) {
+        else if (k == lp::LE && set_upper_bound(t, ci1, value) && has_lower_bound(t.index(), ci2, value)) {
-            fixed_var_eh(b.get_var(), value);
+            fixed_var_eh(b.get_var(), ci1, ci2, value);
         }
     }
 

src/sat/smt/arith_solver.h

@@ -310,7 +310,7 @@ namespace arith {
         void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r);
         api_bound* mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound);
         lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true);
-        void fixed_var_eh(theory_var v1, rational const& bound) {}
+        void fixed_var_eh(theory_var v1, lp::constraint_index ci1, lp::constraint_index ci2, rational const& bound);
         bool set_upper_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); }
         bool set_lower_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); }
         bool set_bound(lp::tv tv, lp::constraint_index ci, rational const& v, bool is_lower);
@@ -324,6 +324,11 @@ namespace arith {
             return is_registered_var(v) && m_model_is_initialized;
         }
 
+        vector<rational>     m_fixed_values;
+        map<rational, theory_var, rational::hash_proc, rational::eq_proc> m_value2var;
+        struct undo_value;
+        void register_fixed_var(theory_var v, rational const& value);
+
         // solving
         void report_equality_of_fixed_vars(unsigned vi1, unsigned vi2);
         void reserve_bounds(theory_var v);

src/sat/smt/bv_internalize.cpp

@@ -453,7 +453,7 @@ namespace bv {
 
         for (unsigned i = 0; i < sz; ++i) {
             numeral div = power2(i);
-            rhs = m_autil.mk_idiv(e, m_autil.mk_int(div));
+            rhs = (i == 0) ? e : m_autil.mk_idiv(e, m_autil.mk_int(div));
             rhs = m_autil.mk_mod(rhs, m_autil.mk_int(2));
             rhs = mk_eq(rhs, m_autil.mk_int(1));
             lhs = n_bits.get(i);