mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

lp: hoist loop-invariant pivot reads in hnf pivot_column_non_fractional

Browse source 
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>
This commit is contained in:
Lev Nachmanson 2026-07-09 04:24:45 -07:00 • committed by GitHub
parent aa6dddbdf0
commit 1b171b3350
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/math/lp/hnf.h
View file

@ -129,16 +129,21 @@ bool prepare_pivot_for_lower_triangle(M &m, unsigned r) {
template <typename M>
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));
}
}
}