diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index c4de2c3ff..020c628aa 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -54,6 +54,7 @@ namespace lp { m_hnf_cut_period = settings().hnf_cut_period(); m_initial_dio_calls_period = settings().dio_calls_period(); m_patch_period = settings().m_int_patch_period; + SASSERT(m_patch_period > 0); } bool has_lower(unsigned j) const { @@ -159,8 +160,7 @@ namespace lp { } bool should_patch() { - // period == 0 means no throttling (old behavior) - return settings().m_int_patch_period == 0 || m_number_of_calls % m_patch_period == 0; + return m_number_of_calls % m_patch_period == 0; } lia_move patch_basic_columns() { @@ -172,12 +172,8 @@ namespace lp { patch_basic_column(j); if (!lra.has_inf_int()) { lia.settings().stats().m_patches_success++; - m_patch_period = std::max(1u, settings().m_int_patch_period); return lia_move::sat; } - // Only throttle if enabled (period > 0) - if (settings().m_int_patch_period > 0 && m_patch_period < 16) - m_patch_period *= 2; return lia_move::undef; } diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index a903ae343..de4e9d3fe 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -9,6 +9,6 @@ def_module_params(module_name='lp', ('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()'), ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'), - ('int_patch_period', UINT, 0, 'Period for patching integer columns (0 = no throttling, 1 = throttle adaptively)'), + ('int_patch_period', UINT, 1, 'Skip int_patch_period - 1 calls and then call the patching'), )) diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index f3745b87b..18faaf64f 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -239,7 +239,7 @@ 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_int_patch_period = 0; + unsigned m_int_patch_period = 1; private: unsigned m_hnf_cut_period = 4; bool m_int_run_gcd_test = true;