diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index e9604e04b..8059c0735 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -11,5 +11,6 @@ def_module_params(module_name='lp', ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'), ('lcube', BOOL, True, 'use the largest cube test for integer feasibility'), ('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'), + ('cut_period', UINT, 4, 'period (in final_check calls) for the integer cut/cube heuristics (find_cube, hnf, gomory); a smaller value calls them more often'), )) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 63836aafa..52d8ea4f0 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -45,5 +45,11 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_dio_run_gcd = lp_p.dio_run_gcd(); m_lcube = lp_p.lcube(); m_lcube_flips = lp_p.lcube_flips(); + unsigned cut_period = lp_p.cut_period(); + if (cut_period == 0) + cut_period = 1; + m_int_find_cube_period = cut_period; + m_int_gomory_cut_period = cut_period; + m_hnf_cut_period = cut_period; m_max_conflicts = p.max_conflicts(); }