From ff5ae4d1edf27c0cc3b9a9a1b1be3e08f2cf9e6d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 16 Mar 2025 10:24:44 -0700
Subject: [PATCH] add systematic way to combine lia_move results

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/dioph_eq.cpp | 41 +++++++++++++++-------------------------
 src/math/lp/lia_move.h   | 25 ++++++++++++++++++++++++
 2 files changed, 40 insertions(+), 26 deletions(-)

diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 48d50ac81..6dfa9f401 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -1247,6 +1247,7 @@ namespace lp {
                                    [k](const auto& c) {
                                        return c.var() == k;
                                    });
+            SASSERT(it != e_row.end());
             const mpq& k_coeff_in_e = it->coeff();
             bool is_one = k_coeff_in_e.is_one();
             SASSERT(is_one || k_coeff_in_e.is_minus_one());
@@ -1281,7 +1282,8 @@ namespace lp {
         lia_move subs_front_with_S_and_fresh(protected_queue& q, unsigned j) {
             process_fixed_in_espace();
             auto r = tighten_on_espace(j);
-            if (r == lia_move::conflict) return lia_move::conflict;
+            if (r == lia_move::conflict)
+                return lia_move::conflict;
             unsigned k = q.pop_front();
             if (!m_espace.has(k))
                 return lia_move::undef;            
@@ -1289,16 +1291,11 @@ namespace lp {
 
             SASSERT(can_substitute(k));
             lia_move ret;
-            if (is_substituted_by_fresh(k)) {
+            if (is_substituted_by_fresh(k)) 
                 ret = subs_qfront_by_fresh(k, q, j);
-            }
-            else {
+            else 
                 ret = subs_qfront_by_S(k, q, j);
-            }
-            if (ret == lia_move::conflict) 
-                return lia_move::conflict;
-            if (r == lia_move::continue_with_check) return r;
-            return ret;
+            return join(ret, r);
         }
 
         lar_term l_term_from_row(unsigned k) const {
@@ -1369,11 +1366,9 @@ namespace lp {
         
         lia_move subs_with_S_and_fresh(protected_queue& q, unsigned j) {
             lia_move r = lia_move::undef;
-            while (!q.empty()) {
+            while (!q.empty() && r != lia_move::conflict) {
                 lia_move ret = subs_front_with_S_and_fresh(q, j);
-                if (ret == lia_move::conflict) return lia_move::conflict;
-                if (ret == lia_move::continue_with_check)
-                    r = ret;
+                r = join(ret, r);
             }
             return r;
         }
@@ -1423,15 +1418,10 @@ namespace lp {
             );
             for (unsigned j : sorted_changed_terms) {
                 m_terms_to_tighten.remove(j);
-                auto r0 = tighten_bounds_for_term_column(j);
-                if (r0 == lia_move::conflict) {
-                    r = r0;
+                auto ret = tighten_bounds_for_term_column(j);
+                r = join(ret, r);
+                if (r == lia_move::conflict)
                     break;
-                }
-                else if (r0 == lia_move::continue_with_check)
-                    r = r0;
-                else if (r0 == lia_move::branch && r == lia_move::undef)
-                    r = r0;
             }
             for (unsigned j : processed_terms) 
                 m_terms_to_tighten.remove(j);
@@ -1783,14 +1773,13 @@ namespace lp {
             lia_move r;
             do {
                 r = rewrite_eqs(f_vector);
-                if (lra.settings().get_cancel_flag()) {
+                if (lra.settings().get_cancel_flag()) 
                     return lia_move::undef;
-                }
-                if (r == lia_move::conflict || r == lia_move::undef) {
+                if (r == lia_move::conflict || r == lia_move::undef) 
                     break;
-                }
                 SASSERT(m_changed_columns.size() == 0);
-            } while (f_vector.size());
+            }
+            while (f_vector.size());
 
             if (r == lia_move::conflict) {
                 if (m_conflict_index != UINT_MAX) {
diff --git a/src/math/lp/lia_move.h b/src/math/lp/lia_move.h
index a082efb06..a0cc7f627 100644
--- a/src/math/lp/lia_move.h
+++ b/src/math/lp/lia_move.h
@@ -53,6 +53,31 @@ namespace lp {
         return "strange";
     }
 
+    inline lia_move join(lia_move r1, lia_move r2) {
+        if (r1 == r2)
+            return r1;
+        if (r1 == lia_move::undef)
+            return r2;
+        if (r2 == lia_move::undef)
+            return r1;
+        if (r1 == lia_move::conflict || r2 == lia_move::conflict)
+            return lia_move::conflict;
+        if (r1 == lia_move::unsat || r2 == lia_move::unsat)
+            return lia_move::unsat;
+        if (r1 == lia_move::cancelled || r2 == lia_move::cancelled)
+            return lia_move::cancelled;
+        if (r1 == lia_move::sat || r2 == lia_move::sat)
+            return lia_move::sat;
+        if (r1 == lia_move::continue_with_check || r2 == lia_move::continue_with_check)
+            return lia_move::continue_with_check;
+        if (r1 == lia_move::cut || r2 == lia_move::cut)
+            return lia_move::cut;
+        if (r1 == lia_move::branch || r2 == lia_move::branch)
+            return lia_move::branch;
+        UNREACHABLE();
+        return r1;
+    }
+
     inline std::ostream& operator<<(std::ostream& out, lia_move const& m) {
         return out << lia_move_to_string(m);
     }