mirror of
https://github.com/Z3Prover/z3
synced 2026-05-17 07:29:28 +00:00
bed532442b
Three combined fixes to the lexicographic basis-reduction heuristic.
1. Monotonicity guard. The lexicographic scoring in reduce_pair can
accept moves with cost > cost(B=I) if they reduce the bound-collapse
excess. Across passes this lets the basis drift to C(B) > C(I), which
then bloats compute_deltas and triggers bail_tighten or wastes work in
find_feasible_solution. We maintain an unweighted running C(B) and
compare against the C(I) baseline taken right after build_matrix; if
the basis search did not strictly improve, operator() bails as
lia_move::undef. Restores the pre-lex 'never worse than plain
int_cube' invariant noted in the header.
2. Candidate magnitude cap. The new candidate set includes values of
the form floor((a +/- (width - base)) / b), where 'width' is the
raw bound interval. Wide-box columns (e.g. width = 1e6) produced
q values far outside the breakpoint range, seeding basis growth
that overflowed too_big() downstream. Add an explicit 64-bit
bitsize ceiling on candidates, well below LLL_CUBE_BITSIZE_LIMIT.
3. Hoist invariants out of reduce_pair. Eligibility, width, and
integral_unit are computed once per operator() call (init_pair_-
invariants). Row 1-norms are cached in m_row_sum_H/m_row_sum_B
and maintained incrementally on each accepted move; the inner
base = sum_{c != j} |M[r][c]| computation collapses from O(n) per
risk row per pair to O(1) (row_sum - |entry|). Per-pair cost in
the risk-row build drops from O((m+n)*n) to O(m+n); at the limits
(m=75, n=150, 8 passes, ~27 candidates) this is ~6-7x fewer mpq
ops per compute_basis call, with the dominant savings being the
per-row 'mpq base(0); base += abs(...)' GMP allocations.
Soundness is unchanged: the moves applied are still unimodular
column ops, and the rounding path still uses B^{-1} and B as before.
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
|
||
|---|---|---|
| .. | ||
| dd | ||
| grobner | ||
| hilbert | ||
| interval | ||
| lp | ||
| polynomial | ||
| realclosure | ||
| simplex | ||
| subpaving | ||