Statistics instrumentation and build profiles

Status: Open lead. Owner: unassigned.

Initial code inspection is complete. Whole-tree classification, implementation, and overhead measurements remain pending.

Primo has counters and timing statements throughout solver code. Investigate whether making diagnostic instrumentation optional at compile time improves readability and performance for release, competition, and library builds.

What the code currently does

Mechanism	Concrete cost or contract to audit
Statistics and its updates	Enum keys update dense arrays and remember first use. String keys also perform hash lookups; new extra keys allocate storage. Not every increment is a map update.
EUF merge/use-list counters	Plain field increments occur inside solver operations. These are cheaper than string-key updates, but their total cost and effect on generated code need measurement.
ScopedStatisticsTimer and CombinationTimer	Clock reads and publication of elapsed time; removing only the final increment would leave timing work behind.
Ackermann cost diagnostics	A dedicated traversal allocates scratch storage and groups applications to compute counters. A useful disabled mode must omit diagnostic computation, not just its output.
CLI statistics printing	--stats controls printing. It does not disable the instrumentation that produced the result.
SolveTerminator::terminate	Reads StatKey::TheoryConflicts to enforce a resource limit. This count is operational state and must survive disabling diagnostics.
EUF scheduling	Reads EufPropagationRounds to decide whether to run propagation. This is solver-control state stored alongside diagnostics.

The conflict budget also controls when the QF_UF session portfolio falls back to another configuration. Replacing every statistics operation with a no-op would therefore change solver behavior. Audit readers of local stats_ structures as well as util::Statistics; this table is an initial sample, not a completed whole-tree classification.

Proposed boundary

See also the concrete quantified-UF counter-publication gap below: availability must be distinguished from a reported zero.

Design preference: avoid string-key lookups on solver execution paths. Use typed counter IDs or component-local fields, resolving names when reporting. String-key diagnostics are acceptable only behind a build-time boundary that provably removes them from production builds. Do not rely on disabling printing or assumed compiler optimization.

Separate always-on solver-control state from optional diagnostic instrumentation. Resource budgets, cancellation/deadline clocks, adaptive heuristic inputs, and any counter required for correctness belong to the first category even when they are also reported as statistics. Optional reports may copy those values; they must not own their operational meaning.

Use an explicit build setting, provisionally PRIMO_ENABLE_DIAGNOSTIC_STATS, rather than deriving instrumentation from NDEBUG or CMAKE_BUILD_TYPE. Optimized builds with diagnostics are needed for development and experiments; optimized builds without them are candidates for deployment. Competition and library profiles should select the setting explicitly once both modes are qualified. This name and these profiles are proposals, not supported options.

A narrow macro can remove a diagnostic statement entirely, including its argument computation. A no-op function alone does not guarantee this: stats.record(expensive_diagnostic()) still evaluates the argument unless the compiler can prove it removable. A compile-time conditional or lazy callable can also serve the purpose. Keep the public operations few and typed, with consistent helpers for increment, accumulation, and scoped timing. Use typed IDs for timer publication too, rather than moving the same string lookup into a helper. Avoid scattered preprocessor branches throughout algorithm bodies. Move substantial diagnostic traversals into named helpers so the main algorithm remains clear.

Whichever mechanism is chosen, disabled instrumentation must skip all work done solely for statistics: argument construction, clock reads, scratch allocation, traversals, and aggregation. Diagnostic arguments must be free of solver side effects, and enabled operations must evaluate them exactly once. Keep invariant checks and solver mutations outside these wrappers. Preserve the existing backend boundary: this switch would govern Primo instrumentation; CaDiCaL’s own counters require a separate dependency-policy audit.

For the library API, keep the public type/layout contract consistent between the library and consumer. Prefer hiding diagnostic storage behind an implementation boundary; an internal build macro must not silently give callers a different public class layout. Report build capabilities and unavailable counters explicitly, rather than returning plausible zero counts for measurements that were never collected.

Investigation and acceptance

1. Classify every counter/timer and its readers as operational or diagnostic. Start with hot-loop updates, string-key publication, scoped timers, and diagnostic-only passes. Preserve algorithm-specific counters in the instrumented profile for paper-to-code and performance evidence.

2. Prototype the boundary in one representative component. Compare readability and inspect optimized code to confirm disabled diagnostic computations are absent. Exercise enabled and disabled modes, including non-evaluation of diagnostic arguments and exact-once evaluation when enabled.

3. Build and test both profiles in CI. Verify identical logical results and valid models, incremental behavior, conflict-budget exhaustion, portfolio fallback, and cancellation contracts. Apply the repository’s solver fuzz and model-validation gates to any implementation; inspect memory-sensitive layout changes with ASan. Wall-clock timeout outcomes can differ with speed.

4. Measure matching optimized builds from the same source revision/compiler and backend on representative UF, arithmetic, mixed, and incremental workloads. Repeat runs; record time/PAR2, memory, binary size, and profile metadata. Use external timing for comparisons so stripped measurements do not depend on the instrumentation under test. Do not infer overhead from the number of statistics statements alone.

5. Record the instrumentation setting in benchmark provenance and build/version output. Document counter availability and update report readers/tests that require diagnostics. Choose release/competition/library defaults only after correctness and performance evidence; keep a reproducible instrumented build.

The proposal is based on Primo’s instrumentation and its consumers identified above. Measurements must establish whether their overhead warrants a change.

Quantified UF can leave EUF counters unpublished

The October 27 paired measurement reports zero :euf.incremental.terms and :euf.incremental.backtracks on two successful quantified-UF UNSAT cases. These zeros cannot establish that no EUF work occurred. The quantified solver recipe uses online EUF. Its incremental closure buffers statistics with flush_live_stats=false. In EufTheoryComponent::check, partial checks return before flush_incremental_stats; only full checks flush. The shared solve loop can return UNSAT directly after the SAT backend, before a full theory check. Registering new atoms also resets the online execution object, so buffered statistics need a publication policy across both reset and final exit.

Audit all exit and replacement paths and add a flush contract before relying on these counters for quantified search comparisons. A regression should exercise an UNSAT result reached before a full model check and a lemma-growth reset. Keep this separate from collecting peak resident node counts or allocated bytes: the existing term counter is cumulative. This is an observed reporting gap and an implementation follow-up, not a solver fix included in the measurement.