diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 16d6a152e..2864650d3 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -2333,6 +2333,8 @@ namespace lp { ret = branching_on_undef(); m_max_of_branching_iterations = (unsigned)m_max_of_branching_iterations / 2; + if (ret == lia_move::undef) + lra.settings().dio_calls_period() *= 2; return ret; } diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index fed9fa21e..c2bb0800e 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -41,7 +41,6 @@ namespace lp { mpq m_k; // the right side of the cut hnf_cutter m_hnf_cutter; unsigned m_hnf_cut_period; - unsigned m_dioph_eq_period; dioph_eq m_dio; int_gcd_test m_gcd; @@ -51,7 +50,6 @@ namespace lp { 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_dioph_eq_period = settings().m_dioph_eq_period; } bool has_lower(unsigned j) const { @@ -193,7 +191,7 @@ namespace lp { } bool should_solve_dioph_eq() { - return lia.settings().dio_eqs() && m_number_of_calls % m_dioph_eq_period == 0; + return lia.settings().dio_eqs() && (m_number_of_calls % settings().dio_calls_period() == 0); } // HNF diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index a2ef9328e..b32b5c207 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -7,5 +7,6 @@ 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, 1, 'Period of calling the Diophantine handler in the final_check()'), )) \ No newline at end of file diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 2e3c464de..4df31abfc 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -39,4 +39,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf(); m_dio_branching_period = lp_p.dio_branching_period();m_dump_bound_lemmas = p.arith_dump_bound_lemmas(); m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums(); + m_dio_calls_period = lp_p.dio_calls_period(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 587e49e96..becec750f 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -243,7 +243,6 @@ public: unsigned column_number_threshold_for_using_lu_in_lar_solver = 4000; unsigned m_int_gomory_cut_period = 4; unsigned m_int_find_cube_period = 4; - unsigned m_dioph_eq_period = 1; private: unsigned m_hnf_cut_period = 4; bool m_int_run_gcd_test = true; @@ -262,8 +261,11 @@ private: unsigned m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening bool m_dump_bound_lemmas = false; bool m_dio_ignore_big_nums = false; + unsigned m_dio_calls_period = 1; public: + unsigned dio_calls_period() const { return m_dio_calls_period; } + unsigned & dio_calls_period() { return m_dio_calls_period; } bool print_external_var_name() const { return m_print_external_var_name; } bool propagate_eqs() const { return m_propagate_eqs;} unsigned hnf_cut_period() const { return m_hnf_cut_period; }