diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 58359ea6d..df93e4d09 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/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; } diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 5c1f8a7de..38b94f5f5 100644 --- a/src/math/lp/int_solver.cpp +++ b/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; } diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index 328a0be09..c3d50ab86 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/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'), ))