mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

lp: expose integer cut/cube period as lp.cut_period parameter

Browse source 
The find_cube, hnf and gomory integer heuristics were all throttled by a
hardcoded period of 4 (m_int_find_cube_period, m_hnf_cut_period,
m_int_gomory_cut_period). Make this value tunable through the new
lp.cut_period parameter (default 4, preserving current behavior) so the
period can be swept (e.g. 3/4/5) for benchmarking. A value of 0 is clamped
to 1.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-18 12:23:10 -07:00
parent 3bf4d2b53d
commit 35fea6f4d3
2 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/lp_params_helper.pyg
View file

@ -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'),
))

6
src/math/lp/lp_settings.cpp
View file

@ -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();
}