From c37ab9b6a37f6b1fb579dd995a75807794a7f947 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 19 Jun 2026 07:47:24 -0700 Subject: [PATCH] lp: rename cut_period->int_hammer_period, random_period->random_hammers These knobs govern the integer cut/cube heuristics (the "hammers": find_cube, lcube, hnf, gomory, dio), not just cuts, so the names now reflect that. lp.int_hammer_period sets the shared firing period and lp.random_hammers toggles random vs deterministic gating. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/int_solver.cpp | 4 ++-- src/math/lp/lp_params_helper.pyg | 4 ++-- src/math/lp/lp_settings.cpp | 14 +++++++------- src/math/lp/lp_settings.h | 6 +++--- 4 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index b67a15e90..cb22b0635 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -195,7 +195,7 @@ namespace lp { lp_settings& settings() { return lra.settings(); } // Decide whether a periodic heuristic fires on this call. When - // random_period is enabled the gate is drawn at random with the same + // random_hammers is enabled the gate is drawn at random with the same // 1/period expected rate instead of a deterministic "every k-th call" // modulus: a deterministic period can phase-lock with the search on // some families and drown the solver in conflicts while another handler @@ -203,7 +203,7 @@ namespace lp { bool hit_period(unsigned period) { if (period <= 1) return true; - if (settings().random_period()) + if (settings().random_hammers()) return settings().random_next(period) == 0; return m_number_of_calls % period == 0; } diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index 86accb367..9fc7bb31f 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -11,7 +11,7 @@ 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'), - ('random_period', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'), + ('int_hammer_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'), + ('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'), )) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 5d537e1fd..6e9f2694b 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -43,14 +43,14 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums(); m_dio_calls_period = lp_p.dio_calls_period(); m_dio_run_gcd = lp_p.dio_run_gcd(); - m_random_period = lp_p.random_period(); + m_random_hammers = lp_p.random_hammers(); 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; + unsigned hammer_period = lp_p.int_hammer_period(); + if (hammer_period == 0) + hammer_period = 1; + m_int_find_cube_period = hammer_period; + m_int_gomory_cut_period = hammer_period; + m_hnf_cut_period = hammer_period; m_max_conflicts = p.max_conflicts(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 548d3b3f3..1744eafb0 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -264,7 +264,7 @@ private: bool m_dio_ignore_big_nums = false; unsigned m_dio_calls_period = 4; bool m_dio_run_gcd = true; - bool m_random_period = true; + bool m_random_hammers = true; bool m_lcube = true; unsigned m_lcube_flips = 16; public: @@ -272,8 +272,8 @@ public: unsigned lcube_flips() const { return m_lcube_flips; } unsigned dio_calls_period() const { return m_dio_calls_period; } unsigned & dio_calls_period() { return m_dio_calls_period; } - bool random_period() const { return m_random_period; } - bool & random_period() { return m_random_period; } + bool random_hammers() const { return m_random_hammers; } + bool & random_hammers() { return m_random_hammers; } 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; }