[coz3-deepperf-fix] lp: hoist loop-invariant pivot reads in HNF pivot_column_non_fractional

[levnach]

Summary

Hoists loop-invariant matrix reads out of the hot inner loop of pivot_column_non_fractional in the Hermite Normal Form (HNF) computation used by z3's linear-arithmetic integer solver. The arithmetic is unchanged; the patch only removes repeated permutation-indexed mpq accesses from an O(n2) elimination loop.

Hotspot

lp::hnf_calc::pivot_column_non_fractional<M> (src/math/lp/hnf.h:130) performs the Bareiss-style fraction-free Gaussian elimination step over a matrix m:

for (unsigned j = r + 1; j < m.column_count(); ++j)
    for (unsigned i = r + 1; i < m.row_count(); ++i)
        m[i][j] = (r > 0) ? (m[r][r]*m[i][j] - m[i][r]*m[r][j]) / m[r-1][r-1]
                          : (m[r][r]*m[i][j] - m[i][r]*m[r][j]);

For general_matrix, every m[a][b] builds a temporary ref_row and performs two permutation-array indirections (row and column permutation lookups in src/math/lp/general_matrix.h) before the underlying vector access. Inside this double loop the terms m[r][r], m[r-1][r-1] and m[r][j] are re-read on every iteration even though they are invariant, so those redundant indexed reads dominate the loop cost.

Change and complexity argument

Rows <= r are never written by this loop — it only assigns m[i][j] for i > r, j > r — so the three pivot entries in rows <= r are loop-invariant:

• m[r][r] and m[r-1][r-1] are invariant across both loops → bind m[r][r] to a reference and take a pointer to m[r-1][r-1] once before the outer loop. The pointer is nullptr when r == 0, which also encodes the existing "no division" case with a single branch.
• m[r][j] is invariant across the inner i loop → hoist it to a reference at the top of the outer j loop.
• m[i][j] is bound to a reference so it is indexed once per iteration instead of three times (two reads + one write).

This turns O(n2) repeated permutation-indexed mpq reads into O(1)/O(n) hoisted reads. The operands, operation order, and division are identical to the original, so the computed matrix is bit-for-bit the same.

Measurements

Profiled with callgrind (z3 built with the same configuration, model_validate=true) on a representative integer-arithmetic problem that exercises the HNF cut generator:

• Target function instructions: 6,793,150,548 → 6,241,093,226 (0.9187×; its share of total drops 15.2% → 14.5%).
• Total program instructions: 44,727,385,309 → 43,036,726,143 (0.9622×).
• Wall-clock: 5.53s → 4.89s (~11.6% faster).
• Differential correctness preserved: identical solver output before and after the change.

Logic class

Integer linear arithmetic — the HNF-based cut generation path in the lp int-solver.

[Copilot]

Pull request overview

This PR optimizes the Hermite Normal Form (HNF) fraction-free elimination step used in Z3’s integer linear arithmetic path by hoisting loop-invariant matrix element accesses out of the hot nested loops in lp::hnf_calc::pivot_column_non_fractional.

Changes:

• Hoist invariant pivot entries (m[r][r], m[r-1][r-1]) outside the nested elimination loops.
• Hoist m[r][j] outside the inner i loop and bind m[i][j] once per iteration to reduce repeated permutation-indexed accesses.
• Preserve arithmetic behavior while reducing repeated general_matrix indexing overhead in the O(n²) update.

[levnach]

@angelica-moreira , @NikolajBjorner : another pleasant surprise from the AI gods.