From becb9957575efdd32f7ef98d099634d9ae3f1e8f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Tue, 14 Jul 2026 13:04:12 -0700
Subject: [PATCH] lp: avoid heap allocation when relocating coefficients in
 static_matrix::remove_element (#10115)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

## Summary

Optimizes `lp::static_matrix<..>::remove_element`, reported as a hotspot
in
[Z3Prover/bench#3143](https://github.com/Z3Prover/bench/discussions/3143)
(the #1 exclusive-time function, ~19.6%, on
`inputs/issues/iss-5131/bug-1.smt2`).

`remove_element` uses swap-remove but **deep-copied** the relocated tail
coefficient:

```cpp
auto & rc = row_vals[row_offset] = row_vals.back(); // copy from the tail
```

In namespace `lp`, `mpq` is a typedef for the copyable `rational`, so
this copy-assign allocates a fresh bignum whenever the **source (the
tail)** is big — matching the `malloc`/`_int_malloc` entries in the
reported profile. The tail element is `pop_back`'d immediately
afterwards, so the allocation is wasteful.

## Change

A copy-assign allocates only when the **source** is big
(`mpz_manager::set` → `big_set`). So relocate the tail coefficient by
**swapping** exactly in that case — stealing its already-allocated
storage, zero `malloc`. When the tail is small, a plain copy never
allocates and is cheaper than swapping the `mpz` internals; the
destination's size is irrelevant. The column-cell relocation is
unchanged (a `column_cell` carries no coefficient).

Single-file change; no new parameters.

## Benchmarks

A/B produced by toggling the new code path against the original
deep-copy (via a temporary parameter, not included here).

- **rise-runner-2** (initial `is_big()||is_big()` variant): QF_LIA_small
neutral; certora identical outcomes, −1.5% paired solve-time.
- **128-core Linux box**, `run_on_dir.py`, `-max_workers 32` (final
tail-only variant):

| Set | Files | `-T` | Solved (new = orig) | Avg-time ratio new/orig |
Correctness |
|---|---|---|---|---|---|
| QF_LIA (SMT-LIB) | 6947 | 20s | 5817 ≈ 5815 | 1.00000 | identical (±2
timeout-edge) |
| certora | 308 | 120s | 186 = 186 | 0.9977 | identical, 0 unique
timeouts |
| QF_LRA (SMT-LIB 2025) | 1753 | 120s | 1552 = 1552 | 0.9985–0.9991 |
identical, 0 real regressions |

Consistently **correctness-neutral and marginally faster** (~0.1–0.5%)
on large-coefficient LP sets, flat on small-coefficient inputs. The
per-`remove_element` allocation saved is small relative to total solve
time, so the whole-solver delta is a fraction of a percent — a clean
micro-optimization with no downside.

## Validation
- `make`/`ninja` build clean; `test-z3 /a` — 92/92 pass.
- Baseline vs patched output byte-identical on the reported benchmark;
identical solve sets across all three benchmark suites above.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/math/lp/static_matrix_def.h | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h
index af07c4482e..31475fc6d4 100644
--- a/src/math/lp/static_matrix_def.h
+++ b/src/math/lp/static_matrix_def.h
@@ -462,12 +462,23 @@ namespace lp {
         column_cell& cs = m_columns[row_el_iv.var()][column_offset];
         unsigned row_offset = cs.offset();
         if (column_offset != column_vals.size() - 1) {
-            auto & cc = column_vals[column_offset] = column_vals.back(); // copy from the tail
+            auto & cc = column_vals[column_offset] = column_vals.back(); // column cells are tiny, a plain copy is optimal
             m_rows[cc.var()][cc.offset()].offset() = column_offset;
         }
     
         if (row_offset != row_vals.size() - 1) {
-            auto & rc = row_vals[row_offset] = row_vals.back(); // copy from the tail
+            row_cell<T> & rc   = row_vals[row_offset];
+            row_cell<T> & tail = row_vals.back();
+            rc.var()    = tail.var();
+            rc.offset() = tail.offset();
+            // Relocating the tail coefficient: a copy allocates a fresh bignum only when the
+            // source (tail) is big, so swap to steal the tail's storage exactly in that case.
+            // When the tail is small the copy never allocates and is cheaper than a swap. See
+            // Z3Prover/bench#3143.
+            if (tail.coeff().is_big())
+                rc.coeff().swap(tail.coeff());
+            else
+                rc.coeff() = tail.coeff();
             m_columns[rc.var()][rc.offset()].offset() = row_offset;
         }