deal with non-termination in new arithmetic solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Oct 27, 2023 · 52d16a1 · 52d16a1
1 parent f6c9ead
commit 52d16a1
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 10 deletions.
diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
@@ -386,12 +386,12 @@ namespace arith {
         ctx.push(push_back_vector<svector<std::pair<euf::th_eq, bool>>>(m_delayed_eqs));
     }
 
-    void solver::mk_diseq_axiom(euf::th_eq const& e) {
-        if (is_bool(e.v1()))
+    void solver::mk_diseq_axiom(theory_var v1, theory_var v2) {
+        if (is_bool(v1))
             return;
         force_push();
-        expr* e1 = var2expr(e.v1());
-        expr* e2 = var2expr(e.v2());
+        expr* e1 = var2expr(v1);
+        expr* e2 = var2expr(v2);
         if (e1->get_id() > e2->get_id())
             std::swap(e1, e2);
         if (m.are_distinct(e1, e2))

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
@@ -896,6 +896,9 @@ namespace arith {
     }
 
     bool solver::assume_eqs() {
+        if (delayed_assume_eqs())
+            return true;
+
         TRACE("arith", display(tout););
         random_update();
         m_model_eqs.reset();
@@ -944,8 +947,15 @@ namespace arith {
                 continue;
             literal eq = eq_internalize(n1, n2);
             ctx.mark_relevant(eq);
-            if (s().value(eq) != l_true)
+            switch (s().value(eq)) {
+            case l_true:
+                break;
+            case l_undef:
                 return true;
+            case l_false:
+                mk_diseq_axiom(v1, v2);
+                return true;
+            }
         }
         return false;
     }
@@ -1018,13 +1028,14 @@ namespace arith {
             st = sat::check_result::CR_GIVEUP;
             break;
         }
-
+            
         if (assume_eqs()) {
             ++m_stats.m_assume_eqs;
             return sat::check_result::CR_CONTINUE;
         }
         if (!check_delayed_eqs()) 
             return sat::check_result::CR_CONTINUE;
+
         if (ctx.get_config().m_arith_ignore_int && int_undef)
             return sat::check_result::CR_GIVEUP;
         if (m_not_handled != nullptr) {
@@ -1106,7 +1117,7 @@ namespace arith {
             if (p.second)
                 new_eq_eh(e);
             else if (is_eq(e.v1(), e.v2())) {
-                mk_diseq_axiom(e);
+                mk_diseq_axiom(e.v1(), e.v2());
                 found_diseq = true;
                 break;
             }
@@ -1467,8 +1478,6 @@ namespace arith {
             add_lemmas();
             break;
         case l_true:
-            if (assume_eqs())
-                return l_false;
             break;
         case l_undef:
             break;

diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
@@ -355,7 +355,7 @@ namespace arith {
         literal is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const;
         void assert_bound(bool is_true, api_bound& b);
         void mk_eq_axiom(bool is_eq, euf::th_eq const& eq);
-        void mk_diseq_axiom(euf::th_eq const& eq);
+        void mk_diseq_axiom(theory_var v1, theory_var v2);
         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);