From 7c12a029e2aaa32efad8c180dc7e147dfc2ff53c Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 14 Mar 2025 05:17:33 -1000
Subject: [PATCH] detect non integral terms in dio

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/dioph_eq.cpp   | 11 ++++++++++-
 src/math/lp/dioph_eq.h     |  1 +
 src/math/lp/int_solver.cpp |  6 ++++--
 3 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 5f1b24c43..816fc19e7 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -331,6 +331,7 @@ namespace lp {
             return out;
         }
 
+        bool m_has_non_integral_term = false;
         std_vector<mpq> m_sum_of_fixed;
         var_register m_var_register;
         // the terms are stored in m_A and m_c
@@ -740,6 +741,7 @@ namespace lp {
             TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;);
             if (!lra.column_is_int(j)) {
                 TRACE("dio", tout << "ignored a non-integral column" << std::endl;);
+                m_has_non_integral_term = true;
                 return;
             }
 
@@ -2622,7 +2624,9 @@ namespace lp {
         // needed for the template bound_analyzer_on_row.h
         const lar_solver& lp() const { return lra; }
         lar_solver& lp() {return lra;}
-
+        bool has_non_integral_term() const {
+            return m_has_non_integral_term;
+        }
     };
     // Constructor definition
     dioph_eq::dioph_eq(int_solver& lia) {
@@ -2640,4 +2644,9 @@ namespace lp {
         m_imp->explain(ex);
     }
 
+    bool dioph_eq::has_non_integral_term() const {
+        return m_imp->has_non_integral_term();
+    }
+    
+
 }  // namespace lp
diff --git a/src/math/lp/dioph_eq.h b/src/math/lp/dioph_eq.h
index 08ee2f6f5..e266e7dd6 100644
--- a/src/math/lp/dioph_eq.h
+++ b/src/math/lp/dioph_eq.h
@@ -30,5 +30,6 @@ namespace lp {
         ~dioph_eq();
         lia_move check();
         void explain(lp::explanation&);
+        bool has_non_integral_term() const;
     };
 }
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index e146c271d..dd0dd255f 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -189,8 +189,10 @@ namespace lp {
         }
 
         bool should_gomory_cut() {
-            return (!all_columns_are_integral() ||(!settings().dio_eqs() || settings().dio_enable_gomory_cuts()))
-                && m_number_of_calls % settings().m_int_gomory_cut_period == 0;
+            bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() ||
+                                      m_dio.has_non_integral_term();
+
+            return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0;
         }
 
         bool should_solve_dioph_eq() {