mirror of
https://github.com/Z3Prover/z3
synced 2026-08-14 01:36:48 +00:00
becb995757
## 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> |
||
|---|---|---|
| .. | ||
| bound_analyzer_on_row.h | ||
| CMakeLists.txt | ||
| column.h | ||
| column_namer.h | ||
| core_solver_pretty_printer.cpp | ||
| core_solver_pretty_printer.h | ||
| core_solver_pretty_printer_def.h | ||
| cross_nested.h | ||
| dense_matrix.cpp | ||
| dense_matrix.h | ||
| dense_matrix_def.h | ||
| dioph_eq.cpp | ||
| dioph_eq.h | ||
| emonics.cpp | ||
| emonics.h | ||
| explanation.h | ||
| factorization.cpp | ||
| factorization.h | ||
| factorization_factory_imp.cpp | ||
| factorization_factory_imp.h | ||
| general_matrix.h | ||
| gomory.cpp | ||
| gomory.h | ||
| hnf.h | ||
| hnf_cutter.cpp | ||
| hnf_cutter.h | ||
| horner.cpp | ||
| horner.h | ||
| implied_bound.h | ||
| incremental_vector.h | ||
| indexed_value.h | ||
| indexed_vector.cpp | ||
| indexed_vector.h | ||
| indexed_vector_def.h | ||
| int_branch.cpp | ||
| int_branch.h | ||
| int_cube.cpp | ||
| int_cube.h | ||
| int_gcd_test.cpp | ||
| int_gcd_test.h | ||
| int_solver.cpp | ||
| int_solver.h | ||
| lar_constraints.h | ||
| lar_core_solver.cpp | ||
| lar_core_solver.h | ||
| lar_core_solver_def.h | ||
| lar_solver.cpp | ||
| lar_solver.h | ||
| lar_term.h | ||
| lia_move.h | ||
| lp_api.h | ||
| lp_bound_propagator.h | ||
| lp_core_solver_base.cpp | ||
| lp_core_solver_base.h | ||
| lp_core_solver_base_def.h | ||
| lp_params_helper.pyg | ||
| lp_primal_core_solver.cpp | ||
| lp_primal_core_solver.h | ||
| lp_primal_core_solver_def.h | ||
| lp_primal_core_solver_tableau_def.h | ||
| lp_settings.cpp | ||
| lp_settings.h | ||
| lp_settings_def.h | ||
| lp_types.h | ||
| lp_utils.h | ||
| matrix.cpp | ||
| matrix.h | ||
| matrix_def.h | ||
| mon_eq.cpp | ||
| monic.h | ||
| monomial_bounds.cpp | ||
| monomial_bounds.h | ||
| nex.h | ||
| nex_creator.cpp | ||
| nex_creator.h | ||
| nla_basics_lemmas.cpp | ||
| nla_basics_lemmas.h | ||
| nla_coi.cpp | ||
| nla_coi.h | ||
| nla_common.cpp | ||
| nla_common.h | ||
| nla_core.cpp | ||
| nla_core.h | ||
| nla_defs.h | ||
| nla_divisions.cpp | ||
| nla_divisions.h | ||
| nla_grobner.cpp | ||
| nla_grobner.h | ||
| nla_intervals.cpp | ||
| nla_intervals.h | ||
| nla_monotone_lemmas.cpp | ||
| nla_monotone_lemmas.h | ||
| nla_order_lemmas.cpp | ||
| nla_order_lemmas.h | ||
| nla_powers.cpp | ||
| nla_powers.h | ||
| nla_pp.cpp | ||
| nla_solver.cpp | ||
| nla_solver.h | ||
| nla_tangent_lemmas.cpp | ||
| nla_tangent_lemmas.h | ||
| nla_throttle.cpp | ||
| nla_throttle.h | ||
| nla_throttle_example.cpp | ||
| nla_types.h | ||
| nra_solver.cpp | ||
| nra_solver.h | ||
| numeric_pair.h | ||
| permutation_matrix.cpp | ||
| permutation_matrix.h | ||
| permutation_matrix_def.h | ||
| random_updater.cpp | ||
| random_updater.h | ||
| random_updater_def.h | ||
| stacked_vector.h | ||
| static_matrix.cpp | ||
| static_matrix.h | ||
| static_matrix_def.h | ||
| test_bound_analyzer.h | ||
| var_eqs.h | ||
| var_register.h | ||