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

### 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).

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

---------

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/math/lp/lar_solver.cpp

@@ -63,6 +63,7 @@ namespace lp {
         unsigned_vector m_row_bounds_to_replay;
         u_dependency_manager m_dependencies;
         svector<constraint_index> m_tmp_dependencies;
+        ptr_vector<u_dependency>  m_tmp_witnesses;
 
         u_dependency* m_crossed_bounds_deps = nullptr;
         lpvar m_crossed_bounds_column = null_lpvar;
@@ -1132,6 +1133,32 @@ namespace lp {
             ex.push_back(ci);
     }
 
+    // Linearize the bound witnesses of all fixed columns in the row together, so the
+    // mark bits walk each dependency sub-DAG shared between columns only once.
+    // When lp.batch_explain_fixed_in_row is disabled, fall back to explaining each
+    // fixed column independently (the pre-batching behavior).
+    void lar_solver::explain_fixed_in_row(unsigned row, explanation& ex) {
+        if (!settings().batch_explain_fixed_in_row()) {
+            for (auto const& c : get_row(row))
+                if (column_is_fixed(c.var()))
+                    explain_fixed_column(c.var(), ex);
+            return;
+        }
+        auto& witnesses = m_imp->m_tmp_witnesses;
+        witnesses.reset();
+        for (auto const& c : get_row(row)) {
+            if (!column_is_fixed(c.var()))
+                continue;
+            const column& ul = m_imp->m_columns[c.var()];
+            witnesses.push_back(ul.lower_bound_witness());
+            witnesses.push_back(ul.upper_bound_witness());
+        }
+        m_imp->m_tmp_dependencies.reset();
+        m_imp->m_dependencies.linearize(witnesses, m_imp->m_tmp_dependencies);
+        for (auto ci : m_imp->m_tmp_dependencies)
+            ex.push_back(ci);
+    }
+
     void lar_solver::remove_fixed_vars_from_base() {
         // this will allow to disable and restore the tracking of the touched rows
         flet<indexed_uint_set*> f(get_core_solver().m_r_solver.m_touched_rows, nullptr);

src/math/lp/lar_solver.h

@@ -521,6 +521,7 @@ public:
     }
 
     void explain_fixed_column(unsigned j, explanation& ex);
+    void explain_fixed_in_row(unsigned row, explanation& ex);
     u_dependency* join_deps(u_dependency* a, u_dependency *b) { return dep_manager().mk_join(a, b); }
     const constraint_set & constraints() const;
     void push();

src/math/lp/lp_bound_propagator.h

@@ -248,22 +248,16 @@ public:
 
     void explain_fixed_in_row(unsigned row, explanation& ex) {
         TRACE(eq, tout << lp().get_row(row) << std::endl);
-        for (const auto& c : lp().get_row(row))
-            if (lp().column_is_fixed(c.var()))
-                lp().explain_fixed_column(c.var(), ex);
+        lp().explain_fixed_in_row(row, ex);
     }
 
     unsigned explain_fixed_in_row_and_get_base(unsigned row, explanation& ex) {
-        unsigned base = UINT_MAX;
         TRACE(eq, tout << lp().get_row(row) << std::endl);
-        for (const auto& c : lp().get_row(row)) {
-            if (lp().column_is_fixed(c.var())) {
-                lp().explain_fixed_column(c.var(), ex);
-            } 
-            else if (lp().is_base(c.var())) {
+        lp().explain_fixed_in_row(row, ex);
+        unsigned base = UINT_MAX;
+        for (const auto& c : lp().get_row(row))
+            if (!lp().column_is_fixed(c.var()) && lp().is_base(c.var()))
                 base = c.var();
-            }
-        }
         return base;
     }
     

src/math/lp/lp_params_helper.pyg

@@ -15,5 +15,6 @@ def_module_params(module_name='lp',
                           ('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'),
                           ('int_hammer_period', UINT, 4, 'period (in final_check calls) for the integer cut/cube heuristics (find_cube, hnf, gomory); a smaller value calls them more often'),
                           ('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'),
+                          ('batch_explain_fixed_in_row', BOOL, True, 'linearize the bound witnesses of all fixed columns in a row in a single dependency pass (de-duplicating shared sub-DAGs) instead of explaining each fixed column independently'),
                          ))
                          

src/math/lp/lp_settings.cpp

@@ -46,6 +46,7 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
     m_dio_calls_period_decrease = lp_p.dio_calls_period_decrease();
     m_dio_run_gcd = lp_p.dio_run_gcd();
     m_random_hammers = lp_p.random_hammers();
+    m_batch_explain_fixed_in_row = lp_p.batch_explain_fixed_in_row();
     m_lcube = lp_p.lcube();
     m_lcube_flips = lp_p.lcube_flips();
     unsigned hammer_period = lp_p.int_hammer_period();

src/math/lp/lp_settings.h

@@ -268,6 +268,7 @@ private:
     unsigned         m_dio_calls_period_decrease = 2;
     bool             m_dio_run_gcd = true;
     bool             m_random_hammers = true;
+    bool             m_batch_explain_fixed_in_row = true;
     bool             m_lcube = true;
     unsigned         m_lcube_flips = 16;
 public:
@@ -279,6 +280,8 @@ public:
     unsigned & dio_calls_period_decrease() { return m_dio_calls_period_decrease; }
     bool random_hammers() const { return m_random_hammers; }
     bool & random_hammers() { return m_random_hammers; }
+    bool batch_explain_fixed_in_row() const { return m_batch_explain_fixed_in_row; }
+    bool & batch_explain_fixed_in_row() { return m_batch_explain_fixed_in_row; }
     bool print_external_var_name() const { return m_print_external_var_name; }
     bool propagate_eqs() const { return m_propagate_eqs;}
     unsigned hnf_cut_period() const { return m_hnf_cut_period; }