port fixes to intblast

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Mar 9, 2024 · 361e04a · 361e04a
1 parent dcaacf5
commit 361e04a
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 5 deletions.
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
@@ -1531,7 +1531,7 @@ namespace lp {
         SASSERT(all_vars_are_registered(coeffs));
         lar_term* t = new lar_term(coeffs);
         subst_known_terms(t);
-        SASSERT(t->is_empty() == false);
+        SASSERT (!t->is_empty());
         m_terms.push_back(t);
         lpvar ret = A_r().column_count();
         add_row_from_term_no_constraint(t, ext_i);
@@ -2266,12 +2266,22 @@ namespace lp {
         return false;
     }
 
+    bool lar_solver::are_equal(lpvar j, lpvar k) {
+        vector<std::pair<mpq, lpvar>> coeffs;        
+        coeffs.push_back(std::make_pair(mpq(1), j));
+        coeffs.push_back(std::make_pair(mpq(-1), k));
+        lar_term t(coeffs);
+        subst_known_terms(&t);
+        return t.is_empty();
+    }
+
     std::pair<constraint_index, constraint_index> lar_solver::add_equality(lpvar j, lpvar k) {
         vector<std::pair<mpq, lpvar>> coeffs;
 
         coeffs.push_back(std::make_pair(mpq(1), j));
         coeffs.push_back(std::make_pair(mpq(-1), k));
         unsigned ej = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var
+
 
         if (get_column_value(j) != get_column_value(k))
             set_status(lp_status::UNKNOWN);

diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
@@ -559,6 +559,7 @@ class lar_solver : public column_namer {
         return m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis();
     }
 
+    bool are_equal(lpvar j, lpvar k);
     std::pair<constraint_index, constraint_index> add_equality(lpvar j, lpvar k);
 
     u_dependency* get_bound_constraint_witnesses_for_column(unsigned j) {

diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
@@ -331,15 +331,17 @@ namespace arith {
         expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
         expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
 
+        // 0 <= n < 2^sz
+
+        add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
+        add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
+
         if (a.is_band(n)) {
-
-            // 0 <= x&y < 2^sz
+
             // x&y <= x
             // x&y <= y
             // TODO? x = y => x&y = x
 
-            add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
-            add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
             add_clause(mk_literal(a.mk_le(n, x)));
             add_clause(mk_literal(a.mk_le(n, y)));
         }
@@ -537,6 +539,8 @@ namespace arith {
         euf::enode* n2 = var2enode(v2);
         lpvar w1 = register_theory_var_in_lar_solver(v1);
         lpvar w2 = register_theory_var_in_lar_solver(v2);
+        if (lp().are_equal(w1, w2))
+            return;
         auto cs = lp().add_equality(w1, w2);            
         add_eq_constraint(cs.first, n1, n2);
         add_eq_constraint(cs.second, n1, n2);