adjust the frequency of dio calls

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

Author: levnach

src/math/lp/dioph_eq.cpp

@@ -2085,15 +2085,6 @@ namespace lp {
             } 
             while (ret == lia_move::continue_with_check);
 
-            if (ret != lia_move::undef) 
-                return ret;
-            if (ret == lia_move::undef) {
-                lra.settings().dio_calls_period() *= 2;
-                if (lra.settings().dio_calls_period() >= 16) {
-                    lra.settings().dio_enable_gomory_cuts() = true;
-                    lra.settings().set_run_gcd_test(true);
-                }
-            }
             return ret;
         }
 

src/math/lp/int_solver.cpp

@@ -43,13 +43,15 @@ namespace lp {
         unsigned            m_hnf_cut_period;
         dioph_eq            m_dio;  
         int_gcd_test        m_gcd;
-
+        unsigned            m_initial_dio_calls_period;
+        
         bool column_is_int_inf(unsigned j) const {
             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_dio(lia), m_gcd(lia) {
             m_hnf_cut_period = settings().hnf_cut_period();
+            m_initial_dio_calls_period = settings().dio_calls_period();
         } 
 
         bool has_lower(unsigned j) const {
@@ -173,8 +175,18 @@ namespace lp {
 
             if (r == lia_move::conflict) {
                 m_dio.explain(*this->m_ex);
+                lia.settings().dio_calls_period() = m_initial_dio_calls_period;
+                lia.settings().dio_enable_gomory_cuts() = false;
+                lia.settings().set_run_gcd_test(false);
                 return lia_move::conflict;
-            } 
+            }
+            if (r == lia_move::undef) {
+                lia.settings().dio_calls_period() *= 2;
+                if (lra.settings().dio_calls_period() >= 16) {
+                    lia.settings().dio_enable_gomory_cuts() = true;
+                    lia.settings().set_run_gcd_test(true);
+                }
+            }
             return r;
         }
 

src/math/lp/lp_params_helper.pyg

@@ -7,7 +7,7 @@ def_module_params(module_name='lp',
                           ('dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
                           ('dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
                           ('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'),
-                          ('dio_calls_period', UINT, 4, 'Period of calling the Diophantine handler in the final_check()'),
+                          ('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'),
                           ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),                          
                          ))