detect non integral terms in dio

Signed-off-by: Lev Nachmanson <[email protected]>

Author: levnach

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

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;
     };
 }

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() {