From 1b171b3350db05e1b520a9f32186dce1f0c81805 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Thu, 9 Jul 2026 04:24:45 -0700 Subject: [PATCH] lp: hoist loop-invariant pivot reads in hnf pivot_column_non_fractional In the Bareiss-style fractional-free elimination step, the inner double loop re-reads m[r][r], m[r-1][r-1] and m[r][j] on every iteration. For general_matrix each m[a][b] builds a temporary ref_row and performs two permutation-array indirections (row/column permutation lookups) before the actual vector access, so these repeated reads dominate the loop. Rows <= r are never written by this loop, so those three entries are loop-invariant. Bind m[r][r] and m[r][j] to references (the latter hoisted out of the inner i-loop) and take a pointer to m[r-1][r-1] once, guarding the r == 0 case that skips the division. Also bind m[i][j] to a reference to avoid indexing it three times per iteration. This turns O(n^2) repeated permutation-indexed mpq reads into O(1)/O(n) hoisted reads with no change in the computed result. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/hnf.h | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/math/lp/hnf.h b/src/math/lp/hnf.h index 5ee6301ab2..e40bae4714 100644 --- a/src/math/lp/hnf.h +++ b/src/math/lp/hnf.h @@ -129,16 +129,21 @@ bool prepare_pivot_for_lower_triangle(M &m, unsigned r) { template void pivot_column_non_fractional(M &m, unsigned r, bool & overflow, const mpq & big_number) { SASSERT(!is_zero(m[r][r])); + // rows <= r are not written below, so these pivot entries are loop-invariant + const auto & mrr = m[r][r]; + const mpq * denom = r > 0 ? &m[r - 1][r - 1] : nullptr; for (unsigned j = r + 1; j < m.column_count(); ++j) { - for (unsigned i = r + 1; i < m.row_count(); ++i) { - if ( - (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])) - >= big_number) { + const auto & mrj = m[r][j]; + for (unsigned i = r + 1; i < m.row_count(); ++i) { + auto & mij = m[i][j]; + mij = mrr * mij - m[i][r] * mrj; + if (denom) + mij /= *denom; + if (mij >= big_number) { overflow = true; return; } - SASSERT(is_integer(m[i][j])); + SASSERT(is_integer(mij)); } } }