From 19781df2bcdc72df5c02eb7fa16a0baaa762733d Mon Sep 17 00:00:00 2001
From: "z3prover-ci-bot[bot]"
 <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Date: Fri, 24 Jul 2026 12:46:52 -0700
Subject: [PATCH] [coz3-deepperf-fix] Avoid full-column rescan on each delta
 halving in lar_solver::init_model (#10217)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

## Summary

`lp::lar_solver::init_model()` (`src/math/lp/lar_solver.cpp`) picks an
infinitesimal `delta` that maps every distinct rational-pair column
value `(x, y)` to a *distinct* scalar `x + delta*y`, halving `delta`
whenever a collision is detected. The previous implementation rebuilt
**both** the set of distinct pairs and the set of scalars from a full
O(n) pass over all columns on *every* halving, and the pair set is
entirely independent of `delta`.

## Change

- Build the delta-invariant set of distinct column pairs
(`m_set_of_different_pairs`) **once**, before the halving loop.
- On each halving, only rebuild the scalar set by iterating over the
**distinct pairs** rather than rescanning all `n` columns (including
duplicates).

The collision test and the selected `delta` are unchanged: the loop
still halves `delta` whenever the number of distinct scalars is less
than the number of distinct pairs, and terminates when the scalar map is
injective. The early-`break` versus end-of-pass check produce the same
`delta` sequence because a size discrepancy on a full pass is exactly
the injectivity-failure condition.

## Cost argument

Let `n` = column count and `D` = number of *distinct* column pairs (`D ≤
n`), and `H` = number of halvings.

- Before: `O(H · n · log D)` — every halving re-inserts all `n` columns
into both sets.
- After: `O(n · log D + H · D · log D)` — the pair set is built once;
each halving touches only the `D` distinct pairs.

This removes the repeated full rescan from the halving loop and skips
redundant work for duplicate columns, turning a per-halving O(n) rebuild
into a one-time cost plus O(D) per halving.

## Evidence

Profiled under callgrind (deterministic instruction counts),
differential correctness preserved, static-analysis hygiene clean:

- Target function self-instructions: **2,695,433,533 → 2,084,074,808**
(−22.7%).
- Total program instructions ratio: **0.904** (−9.6%).
- Wall-time speedup: **~6.1%**.
- Differential correctness: identical results (no mismatches).

Logic class exercised: **QF_LRA / linear real arithmetic** model
construction.

<!-- gh-aw-workflow-id: coz3-deepperf-fix -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/coz3-deepperf-fix -->

---------

Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/math/lp/lar_solver.cpp | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index dcf5e2ef49..0eb204f19d 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1571,22 +1571,23 @@ namespace lp {
             return false;
 
         m_imp->m_delta = get_core_solver().find_delta_for_strict_bounds(m_imp->m_settings.m_epsilon);
-        unsigned j;
         unsigned n = get_core_solver().r_x().size();
+        // the set of distinct column values does not depend on m_delta, so collect it once
+        // and only rescan the distinct pairs when m_delta is halved
+        m_imp->m_set_of_different_pairs.clear();
+        for (unsigned j = 0; j < n; ++j)
+            m_imp->m_set_of_different_pairs.insert(get_core_solver().r_x(j));
+        bool collision;
         do {
-            m_imp->m_set_of_different_pairs.clear();
+            collision = false;
             m_imp->m_set_of_different_singles.clear();
-            for (j = 0; j < n; ++j) {
-                const numeric_pair<mpq>& rp = get_core_solver().r_x(j);
-                mpq x = rp.x + m_imp->m_delta * rp.y;
-                m_imp->m_set_of_different_pairs.insert(rp);
-                m_imp->m_set_of_different_singles.insert(x);
-                if (m_imp->m_set_of_different_pairs.size() != m_imp->m_set_of_different_singles.size()) {
-                    m_imp->m_delta /= mpq(2);
-                    break;
-                }
+            for (const numeric_pair<mpq>& rp : m_imp->m_set_of_different_pairs)
+                m_imp->m_set_of_different_singles.insert(rp.x + m_imp->m_delta * rp.y);
+            if (m_imp->m_set_of_different_singles.size() != m_imp->m_set_of_different_pairs.size()) {
+                m_imp->m_delta /= mpq(2);
+                collision = true;
             }
-        } while (j != n);
+        } while (collision);
         TRACE(lar_solver_model, tout << "delta = " << m_imp->m_delta << "\nmodel:\n";);
         return true;
     }