Three uncalled helpers, six counters that are structurally always zero, and the Glucose-side telemetry is never printed

[InauguralPhysicist]

Dead helpers

These are defined in lib/solver.eigs and called from nowhere in the repo (.eigs, .sh and .py all checked):

• detach_clause_watches (solver.eigs:828) and its inner detach_watch_bucket (solver.eigs:812)
• prune_deleted_watches (solver.eigs:942)
• find_low_activity_learnt (solver.eigs:852) — superseded by the candidate scan inside reduce_learnt_db, and unlike that scan it has no glue-clause protection, so it would behave differently if it were ever wired back in

Counters that can never be nonzero

The three helpers above are the only writers of six counters, and those counters print on every CDCL line:

$ eigenscript minisat.eigs --cdcl --compact-policy eager tests/fixtures/pigeonhole_6_5.cnf
... compact_runs=25 watch_rebuilds=25
    watch_detaches=0 watch_detach_scans=0 watch_detach_removed=0
    watch_prunes=0 watch_prune_scans=0 watch_prune_removed=0

Six of the counters in the mode table are structurally zero — not "zero on this instance". For a repo whose second mission is the counter surface as a pressure inventory, they read as measured facts about watch maintenance when they are placeholders.

Telemetry that is computed but never printed

The reverse problem in minisat.eigs:192: cdcl_result returns these, and the CLI counters line omits all of them —

minimize_checks, minimize_removed, minimize_steps, lbd_kept_glue, lbd_improved, peak_learnts, max_level

That is the entire clause-minimisation and LBD signal, plus two of the three axes of the proof-shape triple the --proof-bench docs are built around. They are reachable from bench modes but not from a plain --cdcl run.

Suggested resolution

Either wire the helpers into the compaction path (compact_deleted_clauses currently rebuilds the whole watch table via rebuild_watches, where targeted detach/prune is the cheaper alternative the helpers were presumably written for) and let the counters become real, or delete the helpers and drop the six counters from the output. Splitting the difference — keeping the counters while the writers stay unreachable — is what makes the inventory misleading.

Separately, add the minimise/LBD/proof-shape counters to the --cdcl counters line, or document why they are bench-only.

Found while reviewing for #83-#86; no behaviour change, so nothing here shifts a banked measurement.

[InauguralPhysicist]

Partial overlap closed by #84/#85/#86 (PRs #90/#91/#93) — recording it here so
this issue does not go stale on the half that is already done.

The Glucose-side telemetry is now printed. The CLI counter line gained
lbd_kept_glue (which existed on the result dict and was never emitted),
plus the new var_rescales, clause_rescales, learnt_limit,
reduce_candidates and reduce_order_bound.

Two of those are worth knowing about because they answer a question the old
counters could not. reduce_order_bound counts reduce runs that had more
candidates than they intended to delete — the only runs where deletion order
decides anything. On pigeonhole 4-3 it is 0 (every learnt clause is glue, so
the sort never runs), and on Tseitin 4x4 under the pre-#86 DB schedule it was
40 of 451. That is why an A/B of the two deletion keys came back
byte-identical: the key had almost nothing to decide.

Still open from this issue: the three uncalled helpers, and the counters
that are structurally always zero. Those are untouched — worth re-checking the
"always zero" list against the current code, since #86 changed how often
reduction and compaction run and at least one of them (compact_runs on the
random-3SAT case) went from nonzero to zero under the shipped defaults, which
is the opposite direction and is handled in the suite by running that case on
the small-DB arm.