mirror of
https://github.com/Z3Prover/z3
synced 2026-07-15 11:35:42 +00:00
ef554ad480
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> |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||