From 4cb997c1281900b685f63dbace5327b6c9ba48af Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 13 Jul 2026 09:39:07 -0700 Subject: [PATCH] lp: avoid heap allocation when relocating coefficients in static_matrix::remove_element remove_element uses swap-remove but deep-copied the relocated tail coefficient. In namespace lp the coefficient type is rational (copyable), so this allocates on the heap for large coefficients. Since the tail element is popped right after, relocate large coefficients by swapping instead, avoiding the allocation; small coefficients still use a plain copy (cheaper than swapping mpz internals). Reported in Z3Prover/bench#3143 (remove_element was the top hotspot). Verified correctness-neutral (identical results, 92/92 unit tests); ~1.5% faster on the certora large-coefficient set, neutral on small-coefficient inputs. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: fd5693e4-3b1d-4dac-b3be-2942ae6f31f8 --- src/math/lp/static_matrix_def.h | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h index af07c4482e..325b956fc5 100644 --- a/src/math/lp/static_matrix_def.h +++ b/src/math/lp/static_matrix_def.h @@ -462,12 +462,22 @@ 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 & rc = row_vals[row_offset]; + row_cell & tail = row_vals.back(); + rc.var() = tail.var(); + rc.offset() = tail.offset(); + // Relocating the tail coefficient: swap to steal an already allocated (big) value and + // avoid a heap allocation; for small coefficients a direct copy is cheaper than swapping + // the mpz internals. See Z3Prover/bench#3143. + if (rc.coeff().is_big() || tail.coeff().is_big()) + rc.coeff().swap(tail.coeff()); + else + rc.coeff() = tail.coeff(); m_columns[rc.var()][rc.offset()].offset() = row_offset; }