[coz3-deepperf-fix] Batch fixed-column bound-witness linearization per row in lar_solver

[levnach]

Summary

lp_bound_propagator::explain_fixed_in_row explained every fixed column of a row
independently, calling lar_solver::explain_fixed_column once per fixed column
(src/math/lp/lar_solver.cpp). Each such call linearizes the lower- and
upper-bound witnesses of a single column — a BFS over the u_dependency DAG using
the dependency manager's mark bits — and inserts every reached leaf constraint into
the explanation.

Fixed columns of the same row routinely share large portions of their bound-witness
sub-DAGs (common ancestor constraints). The per-column scheme therefore re-traverses
those shared sub-DAGs and re-inserts their leaves once for every column, with an
independent mark/unmark cycle per column.

Change

Add lar_solver::explain_fixed_in_row(row, ex), which collects the lower/upper
witnesses of all fixed columns in the row and linearizes them together in a single
u_dependency_manager::linearize pass. lp_bound_propagator::explain_fixed_in_row
and explain_fixed_in_row_and_get_base now delegate to it; the base-column lookup in
the latter is unchanged. explain_fixed_column is kept for its single-column caller.

Why it is correct

explanation is a set — push_back deduplicates. Dependency reachability is
monotone, so the union of the per-column leaf sets equals the leaf set of the union
of all roots: the batched pass yields exactly the same explanation. The manager's
mark bits guarantee each shared sub-DAG node is visited once, and the
linearize(ptr_vector, ...) overload already skips null/duplicate roots.

Complexity

For a row with N fixed columns:

• before: O(Σ_j |witness-DAG(j)|) traversal + O(Σ_j leaves(j)) set insertions, with N mark/unmark cycles;
• after: O(|⋃_j witness-DAG(j)|) traversal + O(#distinct leaves) set insertions, with a single mark/unmark cycle.

Shared sub-DAGs are walked and their leaves inserted once instead of once per column.

Measured effect

Profiled with callgrind on a representative conflict-heavy QF_SLIA input
(model_validate=true, bounded run), baseline vs. patched:

• lp::lar_solver::explain_fixed_column on the hot path: 24,337,671,616 → 0
  retired instructions (59.2% → 0% of the run), replaced by the single batched
  traversal;
• total retired instructions: 41,113,093,210 → 35,983,363,256 (×0.875, ≈ 12.5%
  fewer) — the net work removed by de-duplicating shared sub-DAGs;
• wall-clock: 6.428 s → 6.079 s (≈ 5.4% faster);
• differential correctness preserved (identical results across the validation inputs).

[Copilot]

Pull request overview

This PR optimizes LP conflict explanation generation by batching dependency linearization for all fixed columns in a row, avoiding repeated traversals of shared bound-witness dependency sub-DAGs. It adds a row-level explanation helper in lar_solver and updates the bound propagator to use it.

Changes:

• Add lar_solver::explain_fixed_in_row(row, ex) that collects all lower/upper witnesses for fixed columns in a row and linearizes them in one u_dependency_manager::linearize(ptr_vector<...>, ...) pass.
• Update lp_bound_propagator row-explanation helpers to delegate to the new batched method (while keeping explain_fixed_column for single-column use).
• Introduce a reusable temporary ptr_vector<u_dependency> buffer (m_tmp_witnesses) in lar_solver’s implementation state.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
src/math/lp/lp_bound_propagator.h	Switch row-level fixed-column explanation to the new batched lar_solver API; keep base lookup logic intact.
src/math/lp/lar_solver.h	Declare the new explain_fixed_in_row API alongside explain_fixed_column.
src/math/lp/lar_solver.cpp	Implement batched witness collection + single-pass dependency linearization; add a temporary witness buffer in imp.