Tactics and preprocessing preservation map

This audit accompanies tactics and preprocessing, checked against their implementations on 2026-10-01. The original pages and anchors remain available in the historical book.

Preserved identifies an explanatory destination for a current mechanism. Superseded names a correction or an intentionally different organization. Retained history identifies material preserved in the dated archive. Its experiments are not rerun by this audit. Archive paths and redirects are installed and checked at each build; reader acceptance and publication are separate.

Tactics

Original section	Disposition and destination
Introduction and algorithmic basis	Preserved in the chapter introduction and implemented subset, citing de Moura–Passmore §3 through the shared bibliography.
Implemented data structures	Preserved in representation, goal truth, and the model chapter.
Immutable strategy and compilation	Preserved in strategy identity; the lifetime requirements for stored term IDs and borrowed session objects limit strategy reuse.
Tacticals and probes	Preserved in composition and strategy identity, including retention of the final iteration’s model records and cooperative deadlines.
Production composition	Preserved in session-to-engine flow and preprocessing order. The initial passes run before profile selection.
Exhaustive Boolean splitting	Preserved in splitting: complete alternatives, deterministic selection, model ownership, exponential storage growth, and the limit on selected atoms.
Sequential evaluation	Retained history: focused manifests, repeated measurements, branch costs and results. The new chapter makes no claim that splitting improves performance.
Composition verification	Current contracts preserved in checks; the runner and SLURM manifest remain linked. Earlier instructions and provenance remain in the dated record; the current composition workflow records procedures and tool limitations.
Deviations, invariants and complexity	Preserved across composition, identity, scope and paper subset. The blanket statement that incremental tactics are absent is superseded by the restricted set of tactics checked for incremental use.
Incremental execution contract	Preserved in incremental use and its links to both assumptions-engine designs.
Tactic-reference catalogue	Mechanisms preserved in both chapters; builders, parameters and tactic counters are listed in the tactic reference.
Unrepresented transformations and portfolio limitations	Preserved in session portfolios, strategy identity and limitations: no tactic parser, learned portfolio, or isolated parallel executor.

Preprocessing

Original section	Disposition and destination
Introduction and arithmetic atom canonicalization	Current scheduling and the two distinct normal forms preserved in execution order and arithmetic normalization, linked to LRA. Dated A/B comparisons and default decisions remain history.
Experimental QF_UF portfolio	Fallback conditions based on the result and reason code preserved in session portfolios. Screens, family-specific observations and rejected configurations remain history.
Boolean unit propagation	Preserved in round order and facts, including retained units, sharing and model records.
Forced atom propagation	Preserved in facts and representation: congruence, known disequalities, retained facts and later finite-domain use.
Solved constants and Gaussian elimination	Preserved in definition elimination, integer profiles, and conversion example. Historical measurements remain at the old location.
Monotone elimination, preconditions and reconstruction	Preserved in one-sided variables and the model conversion chapter. The local attribution note remains the rule’s design reference.
Historical monotone examples and counters	Current repair rule and counter purpose preserved in final passes and evidence. Development examples and measurements remain history; their old helper locations are not current API guidance.
Pure literals and theory atoms	Preserved with a concrete contradiction in propagating facts.
Real-equality lowering	Preserved in normalization boundary. The implementation also handles Int; the new text makes that explicit. The test for equalities introduced by later passes remains part of the composition checks.
ITE lowering	Preserved in extended terms and integer input translation. Growth controls are distinguished from mandatory elimination.
Constant ITE simplification	Current CITE subset, cache scope, identities valid for integers, and ordering preserved in extended terms. Arena-growth test linked through correctness checks. Timing and the evidence for enabling the pass by default stay at the old location.
Constructor versus pass work	Preserved in core representation and final Boolean normalization. The current bounded second pass is explained rather than restoring unconditional constructor flattening.
Equality bridge	Preserved with the diamond example and scope in equality consequences.
Finite-domain clauses	Preserved in finite domains: scans before and after simplification, distinctness, numeral restrictions, existing equality atoms, known disequalities, equality definitions and growth. July probe results remain history.
UF symmetry breaking	Preserved in symmetry: invariance, fixed terms, value precedence, exclusion of terms affected by the permutations, and model-renaming justification. Historical solver comparisons remain history.
Implementation notes	Current profile, fixed-point and adaptive behavior preserved in profiles and order. Historical tuning observations remain at this link.
Mixed-theory opportunities	Retained research record. Current purification is explained in combination; proposals are not presented as additional implemented preprocessing passes.
Current status	Superseded as the current narrative by the profile and pass descriptions checked against the code. Historical counts and formerly deferred work remain dated evidence.
Paper traceability	Preserved and qualified in sources; bibliography identifies papers, while earlier development inspiration stays retrospective. No old solver implementation is an implementation source.
Structural selector design	Selection semantics preserved in profiles; thresholds and analysis costs appear in the policy reference.
Structural selector evaluation	Retained history, including the rejected default promotion. The current selector remains legacy.

Evidence identities

The original chapters retain the detailed experiment tables. Relevant run-log entries include:

• 2026-08-30-tactic-refactor-full-slurm-comparison and 2026-08-31-tactic-refactor-infrastructure-profile: refactoring comparison and investigation of tactic infrastructure costs.

• 2026-09-01-tactic-composition-slurm-short-circuit-audit and 2026-09-01-tactic-composition-slurm-merge-gate: composition coverage, including why a later leaf need not execute on an already settled input.

• 2026-08-12-structural-implies-benchmark-f88bc87 and 2026-08-17-arithmetic-canonicalization-default-off-979d911: selector/rewrite and canonicalization decisions with their measured scope.

• 2026-09-06-lead16-cite-simplification-133177-133466 and 2026-09-07-cite-hoisting-lifetime-slurm-134014: CITE evaluation and the later allocation-boundary repair. The later repair is not silently covered by the earlier evaluation.

Historical local runs are provenance, not instructions to run current solver batches locally. This rewrite ran documentation checks only.

Reference and workflow destinations

The complete tactic inventory and policy reference preserve builders, counters, selector thresholds and analysis costs. The composition workflow covers supported profiles, revision checks, activity requirements and separate model validation. The fuzzing guide also covers seed staging and integer/finite-domain procedures.

This audit covers the named chapters and selector note. It does not mark every linked literature note or open lead as migrated, and it does not assign reader acceptance. Their file-level migration records remain in force.