From deac00ada39da8da13e4bb6805c3f4506bb46bc6 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 26 Nov 2024 19:34:52 -0800
Subject: [PATCH] persist dio handler

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/dioph_eq.cpp   | 11 +++++++----
 src/math/lp/int_solver.cpp | 10 +++++-----
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 68ef62fc7..391cc418a 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -236,9 +236,8 @@ namespace lp {
         std_vector<unsigned> m_fresh_definitions;  // seems only needed in the debug
         // version in remove_fresh_vars
 
-        unsigned m_conflict_index =
-            -1;  // m_entries[m_conflict_index] gives the conflict
-        unsigned m_max_number_of_iterations = 1000;
+        unsigned m_conflict_index = -1;  // m_entries[m_conflict_index] gives the conflict
+        unsigned m_max_number_of_iterations = 100;
         unsigned m_number_of_iterations;
         struct branch {
             unsigned m_j = UINT_MAX;
@@ -355,6 +354,8 @@ namespace lp {
             m_entries.clear();
             m_var_register.clear();
             m_number_of_iterations = 0;
+            m_branch_stack.clear();
+            m_lra_level = 0;
             for (unsigned j = 0; j < lra.column_count(); j++) {
                 if (!lra.column_is_int(j) || !lra.column_has_term(j))
                     continue;
@@ -1102,7 +1103,9 @@ namespace lp {
             if (ret == lia_move::sat || ret == lia_move::conflict) {
                 return ret;
             }
-            SASSERT(ret == lia_move::undef);            
+            SASSERT(ret == lia_move::undef);
+            m_max_number_of_iterations = std::max((unsigned)5, (unsigned)m_max_number_of_iterations/2);
+            
             return lia_move::undef;
         }
 
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 6648c3684..43d490c75 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -34,6 +34,7 @@ namespace lp {
         int_solver&         lia;
         lar_solver&         lra;
         lar_core_solver&    lrac;
+        dioph_eq            m_dio;  
         unsigned            m_number_of_calls = 0;
         lar_term            m_t;  // the term to return in the cut
         bool                m_upper;           // cut is an upper bound
@@ -48,7 +49,7 @@ namespace lp {
             return lra.column_is_int(j) && (!lia.value_is_int(j));
         }
 
-        imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_gcd(lia)  {
+        imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_gcd(lia), m_dio(lia) {
             m_hnf_cut_period = settings().hnf_cut_period();
             m_dioph_eq_period = settings().m_dioph_eq_period;
         } 
@@ -169,18 +170,17 @@ namespace lp {
         }
 
         lia_move solve_dioph_eq() {
-            dioph_eq de(lia);
-            lia_move r = de.check();
+            lia_move r = m_dio.check();
 
             if (r == lia_move::conflict) {
-                de.explain(*this->m_ex);
+                m_dio.explain(*this->m_ex);
                 m_dioph_eq_period = settings().m_dioph_eq_period;
                 return lia_move::conflict;
             } else if (r == lia_move::branch)  {
                 m_dioph_eq_period = settings().m_dioph_eq_period;
                 return lia_move::branch;
             } 
-			return r;
+            return r;
         }
 
         lp_settings& settings() { return lra.settings(); }