mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

lp: lazily skip move_non_basic_columns_to_bounds unless a cut will run

Browse source 
The standalone int_solver call to move_non_basic_columns_to_bounds runs an
O(#nonbasic) scan and, when columns drift, a full find_feasible_solution
re-solve on every check iteration. It is only a precondition for the HNF and
Gomory cut generators; int_branch and int_cube snap for themselves and the
Diophantine handler does not depend on it.

Gate the call behind (should_hnf_cut() || should_gomory_cut()) so a pure-branch
iteration no longer pays the cut precondition cost. The optimization is
controlled by the new boolean parameter lp.int_lazy_move_nb (default true);
setting it false reproduces the previous (master) behavior of always snapping.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-19 15:39:55 -07:00
parent a05be8a291
commit ef554ad480
4 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/int_solver.cpp
View file

@ -268,7 +268,9 @@ namespace lp {
if (r == lia_move::undef) r = patch_basic_columns();
if (r == lia_move::undef && should_find_cube()) r = int_cube(lia)();
if (r == lia_move::undef && should_find_lcube()) r = find_lcube();
if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds();
if (r == lia_move::undef &&
(!settings().int_lazy_move_nb() || should_hnf_cut() || should_gomory_cut()))
lra.move_non_basic_columns_to_bounds();
if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();
if (r == lia_move::undef && should_gomory_cut()) r = gomory(lia).get_gomory_cuts(2);
if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq();

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'),
('int_lazy_move_nb', BOOL, True, 'skip the standalone move_non_basic_columns_to_bounds call (and its find_feasible_solution re-solve) unless an HNF or Gomory cut will be attempted in this iteration; off reproduces the master behavior of always snapping'),
))

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

@ -45,5 +45,6 @@ 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();
m_int_lazy_move_nb = lp_p.int_lazy_move_nb();
m_max_conflicts = p.max_conflicts();
}

2
src/math/lp/lp_settings.h
View file

@ -266,7 +266,9 @@ private:
bool m_dio_run_gcd = true;
bool m_lcube = true;
unsigned m_lcube_flips = 16;
bool m_int_lazy_move_nb = true;
public:
bool int_lazy_move_nb() const { return m_int_lazy_move_nb; }
bool lcube() const { return m_lcube; }
unsigned lcube_flips() const { return m_lcube_flips; }
unsigned dio_calls_period() const { return m_dio_calls_period; }