From 2c16f44c0ad2695f32a902e5d0a10da7e6919a4c Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Thu, 9 Jul 2026 07:02:47 -0700
Subject: [PATCH] [coz3-deepperf-fix] lp: hoist loop-invariant pivot reads in
 HNF pivot_column_non_fractional (#10073)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

## 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`:

```cpp
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.

<!-- gh-aw-workflow-id: coz3-deepperf-fix -->

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 <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));
         }
     }
 }