mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

Merge 4cb997c128 into 82a0d42970

Browse source
This commit is contained in:
Lev Nachmanson 2026-07-14 11:52:04 -07:00 • committed by GitHub
commit 1a49d5288e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/lp/static_matrix_def.h
View file

@ -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<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: 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;
}