Preprocessing

Primo exposes its shared preprocessing pipeline through --preprocessing-mode=off|basic|strong|auto. Preprocessing runs before final formula classification, so the mode applies to pure QF_UF, pure QF_LRA, QF_UFLRA, QF_LIA, QF_UFLIA, and propositional inputs; individual transformations remain shape-dependent and are no-ops when their recognizers do not apply. The CLI and CheckSatOptions::preprocessing_mode default is auto. For pure QF_LIA, auto deliberately maps to the audited substitution-only path. For QF_UFLIA, auto maps to the evaluated integer-safe Boolean/value-propagation profile described below. Explicit off preserves the substitution-only comparison path, while strong also enables the guarded integer numeral-domain machinery.

The former QF_UF-specific names have been removed. Use --preprocessing-mode and --auto-preprocess-selector; unknown legacy names are rejected by the command-line parser.

The repeated core round is assembled from named formula-valued tactics rather than a monolithic loop. Each phase accepts and returns the same goal type and preserves or extends its reconstruction value. The built-in strategy repeats the round to an ordered-assertion fixed point and retains the existing adaptive reachable-term shrink test; users select presets and options, not an exposed tactic language.

Preprocessing without search

CheckSatOptions::preprocess_only (CLI --preprocess-only) is a diagnostic for measuring preprocessing independently of search. In solver_session.cpp, ground goals run the ordinary preprocessing strategy and return unsat if all alternatives reduce to false; otherwise they return unknown, including for an empty goal. The option does not print transformed assertions. For quantified UF, the session returns unknown after the frontend, before solve_quantified_uf: ground preprocessing does not support binders. No SAT, theory, or quantifier search runs. Unsupported inputs remain unsupported. Terms and assertions retain their ordinary per-query frontend ownership; no preprocessed goal or model is exported. Use --stats for the counters.

The preprocess_only_never_starts_search regression in tests/unit/quantifier_solver_tests.cpp checks universal and existential inputs, unchanged ground outcomes, absence of search and generated instances, and rejection of quantified assertions in QF_UF.

Arithmetic atom canonicalization

With --arithmetic-atom-canonicalization, Primo canonicalizes Real linear comparisons and equalities immediately after frontend expansion and type checking, before the optional preprocessing modes described below. The pass scales rational coefficients to primitive integers, chooses a deterministic sign and TermId order, and rebuilds the predicate through TermManager. Existing hash-consing then gives equivalent forms such as 2a + 2b <= 2c and 4a + 4b <= 4c one canonical term before unit propagation, solve-eqs, equality bridging, automatic profile selection, or clausification sees them.

Real equality uses the same scaling; any nonzero factor is removable without reversing equality. Ordered predicates reverse when normalization removes a negative factor. When the option is enabled, later catch-up normalization handles atoms generated by preprocessing and mixed purification. The option is independent of --preprocessing-mode, so it can be enabled together with --preprocessing-mode=off. It defaults off because the first QF_LRA A/B changed the deterministic search trajectory and lost one net solve on the 237-file sample. The exact invariants, ownership, complexity, paper basis, and required tests are specified in Early LRA atom canonicalization.

auto currently defaults to the historical assertion-root selector. The opt-in --auto-preprocess-selector=structural mode instead analyzes the implicit top-level conjunction and finite-domain shape, so separate assertions and one equivalent asserted conjunction select the same profile. Its limits are exposed through --auto-preprocess-* and --auto-basic-*-limit options rather than embedded constants. It remains experimental pending fuzz and benchmark evaluation; Structural automatic preprocessing selection specifies its ownership, invariants, complexity, and counters.

• off disables the preprocessing loop;

• basic runs one pass of unit equality propagation;

• strong enables repeated preprocessing, equality bridging, finite-domain at-most-one clauses, opt-in finite-domain equality definitions, and finite-domain symmetry breaking;

• auto keeps equality bridging, finite-domain at-most-one clauses, and symmetry breaking when their recognizers apply. Guarded finite-domain equality definitions are available with --finite-domain-equality-definitions. The explicit strong preset removes the automatic equality-definition guards for experiments. A guarded single-assertion exception uses the lighter basic subset when the original formula has at most 15,000 reachable terms, at least 200 finite-domain choices, and a small accepted finite-domain symmetry group; --no-auto-basic-single disables this exception for same-binary A/B runs. If that branch also contains Boolean-valued UF predicate applications, Primo uses polarity phase for those syntactically single-polarity atoms; disable that narrower phase override with --no-auto-basic-single-predicate-polarity. A guarded small multi-assertion auto branch uses the basic subset when the input has more than one assertion, at most 10,000 assertions, and at most 20,000 initially reachable terms.

Associative Boolean flattening is separate from those presets and applies to all supported logics. Core And and Or terms retain nested DAG structure by default. --boolean-flatten-threshold N enables one explicit pre-pass over the reachable assertion DAG; 0, the default, disables it. The pass widens a same-kind child only when the resulting parent, including remaining direct children, stays within N. It does not split an explicitly wider SMT-LIB node. Clausification accepts nested nodes directly and does not enable this pass. See Boolean DAG representation and bounded associative flattening for ownership and complexity details.

Implication normalization is also separate and disabled by default. --boolean-implies-rewrite=clause rewrites only A => B forms that can expose one bounded clause: A must be a literal, while B must be a literal or an Or of literals. For example, p => (q or r) becomes (or (not p) q r). The resulting arity may not exceed --boolean-flatten-post-threshold; a zero threshold disables clause rewrites. --boolean-implies-rewrite=all performs the general equivalence A => B to (or (not A) B) without distribution. Both modes run after theory preprocessing and purification but before post-preprocessing Boolean flattening. They traverse Boolean structure and Boolean equality, while treating Boolean-valued UF applications as atomic so their arguments remain owned by the EUF normalization path.

basic and strong preprocessing on QF_LIA and QF_UFLIA first normalizes the Boolean skeleton to negation normal form. It pushes not through not, and, or, and => using De Morgan’s laws and the two implication polarities, but it performs no distributive expansion. Equality, arithmetic predicates, constants, and Boolean-valued uninterpreted applications are atomic boundaries. In particular, a Boolean term used as an argument to a UF application is not silently rewritten underneath that application. The iterative implementation stores positive and negative results for each source TermId, so its work and memo table are linear in the reachable Boolean DAG (at most two states per source node); newly constructed terms remain owned and hash-consed by TermManager.

QF_UFLIA selects this basic subset in auto mode. The September 2026 659-file SLURM evaluation solved 571 instances with it, compared with 549 for the substitution-only build at the same solver revision, and reduced PAR2 by 22.5%. All 3,000 generated answers agreed with Z3 and Dolmen directly accepted all 1,765 generated SAT models; the complete real-corpus model gate is recorded in docs/run-log.json. QF_LIA remains substitution-only in auto mode because this QF_UFLIA result does not establish a pure-LIA performance win.

The NNF step is the first leaf of the optional integer preprocessing suffix, after the capped solved-constant pass. The repeated round then uses Boolean units, forced theory-atom values, solved-constant substitution, and unit equality consequences. Gaussian candidate generation, equality bridging, ground substitution/congruence, monotone elimination, and UF symmetry remain disabled in this integer profile. :preprocessing.boolean-nnf.visited, .rewritten, and .terms-created expose whether the pass did work. This is an ordinary textbook equivalence rewrite rather than an implementation of an optimized paper algorithm; its local implementation contract is the bounded two-polarity DAG algorithm above, with unit tests for negative implications, sharing, and UF opacity.

The default command now enables the safe part of the predecessor performance profile:

./build/primo --uf-symmetry-breaking --preprocessing-passes 4 --eq-bridge \
  --prop-interval 32 --prop-assign-threshold 0.25 \
  --prop-delivery-budget 1000 input.smt2

The preprocessing flags in that command are defaults, so plain ./build/primo input.smt2 uses the same preprocessing unless an option overrides it. Plain Primo currently uses --euf-prop=auto: online callbacks are used for small EUF abstractions, while large EUF abstractions use conflict-only CaDiCaL callbacks to avoid repeated lazy post-model checks without enabling the currently expensive online propagation scan.

The exact legacy-style reproduction profile is:

./build/primo --qf-uf-profile=tuned-interesting input.smt2

It sets the same safe switches as the default and leaves the selected --preprocessing-mode mode at auto unless the user overrides it. It also keeps the legacy propagation tuning knobs available for experiments; select --euf-prop=online explicitly when reproducing online-propagation runs.

The individual legacy switches remain available for experiments and for reproducing narrower configurations:

• equality bridging under disjunctions, enabled with --eq-bridge or --preprocessing-mode=strong;

• unit equality propagation, enabled by the basic, strong, and auto preprocessing loops;

• experimental ground substitution from positive unit equalities, enabled with --ground-unit-substitution;

• guarded experimental ground substitution, enabled with --guarded-ground-unit-substitution;

• finite-domain at-most-one clauses, enabled by --preprocessing-mode=strong and by most of the default auto path. The guarded single-assertion exception reports :preprocessing.auto.basic-single and skips these clauses for a small finite-domain/symmetry shape. A same-run July 19, 2026 SLURM comparison on the 334-row user HTML set validated this selector: default solved 332 with PAR2 2828.629, while --no-auto-basic-single solved 331 with PAR2 3031.436. The guarded small multi-assertion branch intentionally skips these clauses because same-run July 19, 2026 SLURM comparisons showed that several compact operation-table rows benefited from the lighter basic encoding plus polarity phase;

• finite-domain equality definitions. In auto they are opt-in with --finite-domain-equality-definitions and bounded by --finite-domain-eqdefs-auto-domain-limit and --finite-domain-eqdefs-auto-clause-limit; large single-assertion formulas are additionally guarded by --finite-domain-eqdefs-auto-term-limit. --preprocessing-mode=strong keeps the historical unbounded expansion. Use --no-finite-domain-equality-definitions for ablations;

• solved-constant substitution for acyclic unit definitions, enabled by default and disabled with --no-solved-constant-substitution. The pass keeps exact tree-occurrence accounting for its definition-size guard, but memoizes each hash-consed subtree’s candidate-variable occurrence multiset so repeated macro-expanded DAG fragments are not recursively recounted from every parent;

• bounded ground-congruence clauses over applications already present in the formula, enabled by --ground-congruence;

• symmetry breaking over finite-domain choice disjunctions, enabled by default when preprocessing is enabled and explicitly controllable with --uf-symmetry-breaking / --no-uf-symmetry-breaking. Fixed-term value precedence inside accepted symmetry groups is controlled separately by --finite-domain-value-precedence / --no-finite-domain-value-precedence.

--no-eq-bridge, --no-uf-symmetry-breaking, and --theory-phase=auto are useful ablation or targeted-experiment switches. --preprocessing-mode=off disables the preprocessing loop and the finite-domain symmetry-breaking preprocessing step. --no-auto-basic-single-predicate-polarity disables the predicate-aware phase override for selected single-assertion finite-domain formulas. --no-auto-basic-multi disables the compact multi-assertion classifier for scripted option matrices, while --no-auto-basic-multi-polarity keeps that compact preprocessing branch but uses the ordinary theory-atom phase.

Experimental QF_UF Portfolio

--qf-uf-portfolio=basic-polarity runs a bounded first attempt with --preprocessing-mode=basic, --theory-phase=polarity, and a theory-conflict budget before falling back to the normal configured solve. The budget defaults to 2000 theory conflicts and is controlled by --qf-uf-portfolio-conflicts=N.

The first attempt is correctness-preserving because it solves the original SMT-LIB input after reparsing with a weaker preprocessing preset; if it returns sat or unsat, that answer is returned. If it reaches the theory-conflict budget, Primo discards that solver state, reparses the original input, and runs the ordinary configured solve. Statistics from the returned attempt include :portfolio.qf-uf.* counters that distinguish first-pass success from fallback.

This mode is intentionally opt-in. Local diagnostics on July 19, 2026 showed large wins on some satisfiable QG rows such as iso_brn_repgen033, but also fallback overhead on NEQ and PEQ rows. It must be evaluated on the full target manifest before being considered for any default profile.

./build/primo --preprocessing-mode=off input.smt2
./build/primo --preprocessing-mode=auto input.smt2
./build/primo --preprocessing-mode=strong input.smt2
./build/primo --eq-bridge input.smt2
./build/primo --uf-symmetry-breaking input.smt2
./build/primo --eq-bridge --preprocessing-passes 3 input.smt2
./build/primo --eq-bridge --preprocess-passes 3 input.smt2
./build/primo --qf-uf-portfolio=basic-polarity input.smt2

These passes are deliberately separate from the SAT backend. They create additional Boolean assertions over ordinary equality terms, then the existing Boolean clausifier and lazy EUF loop solve the strengthened formula.

The auto preset is a dispatcher between existing sound subsets, not a new inference rule. It was added after QF_UF archive profiling showed that finite-model encodings such as NEQ, PEQ, SEQ, and QG operation tables can need SAT-visible finite-domain structure, while unbounded equality-definition expansion can also flood unrelated instances with thousands of clauses. auto therefore keeps AMO clauses by default but keeps equality definitions opt-in. The single-assertion basic exception is an empirical classifier derived from the recorded 334-row option comparison: it only selects the existing basic subset when the original finite-domain scan finds at least 200 choices and the symmetry pass accepts a group with at most six non-value terms. It reports :preprocessing.auto.basic-single and can be disabled with --no-auto-basic-single; the default ordinary strong-auto branch reports :preprocessing.auto.strong. On the July 19, 2026 334-row SLURM comparison it selected 12 rows, gained PEQ014_size11, and reduced PAR2 by about 203 seconds against the same binary with the selector disabled. A follow-up local probe found that polarity phase helps the selected NEQ rows with Boolean UF predicate atoms, including NEQ023_size7, but regresses pure-equality PEQ rows; the implemented subset therefore gates this static phase override on :euf.predicate-atoms > 0 and reports :sat.phase.auto-basic-single-predicate-polarity. A same-binary SLURM comparison on the 334-row user HTML set showed no wrong answers and a clear improvement on the three rows where the override fired (NEQ006_size6, NEQ023_size7, and NEQ032_size6), while the raw whole-set PAR2 was dominated by unrelated timing variation on rows where the override was inactive. It does not address NEQ016_size8, which does not select the single-assertion basic branch. The basic-multi exception is a separate empirical classifier for compact multi-assertion QG rows and reports :preprocessing.auto.basic-multi. A later July 19, 2026 same-run SLURM comparison on the 334-row user HTML set validated enabling it by default after the auto-basic-single baseline: default and --no-auto-basic-multi both solved 332/334 with no wrong answers, while default reduced PAR2 by about 59 seconds overall and by about 115 seconds on the selected QG rows. The remaining NEQ gap is unchanged because those rows do not select the multi-assertion branch. The compact multi-assertion branch also has a separate phase ablation, --no-auto-basic-multi-polarity, because follow-up local QG diagnostics found mixed behavior: polarity phase is excellent for rows such as iso_brn_repgen033, but ordinary negative theory phase is much faster on iso_brn_repgen_sk032, iso_brn_repgen043, and iso_icl_nogen_sk004. When enabled, equality definitions must fit a domain-size and per-solve clause budget. For single-assertion formulas they must also fit the initial reachable-term limit, because a single top-level assertion may contain an entire operation-table encoding. Single-assertion formulas still run equality bridging with repeated unit-equality propagation so eq_diamond-style chains keep the fast bridge path.

Very large already-flat assertion batches are a separate case. Goel hardware instances can arrive as tens of thousands of top-level clauses; running repeated nonclausal preprocessing over those batches can grow the assertion set and dominate solving time. In auto mode, batches above 10,000 top-level assertions therefore skip the repeated preprocessing loop and go directly to Boolean abstraction and EUF. The default solved-constant substitution pass is still run once on these batches because it is linear over the visible assertions, does not generate clauses, and is guarded against definition-size blowups. Explicit --preprocessing-mode=basic and --preprocessing-mode=strong still force the full preprocessing loop for ablation or targeted experiments. This auto decision is reported by :preprocessing.auto.large-assertion-skip.

The large-batch guard was accepted after profiling 2018-Goel-hwbench/QF_UF_firewire_tree.5.prop3_ab_reg_max: default auto preprocessing grew the instance to 94,530 assertions and took about 56 seconds locally, while the guarded path skipped preprocessing and solved in about 5.3 seconds. The follow-up 120-second full QF_UF SLURM run results/slurm-qfuf-full-forced-atoms-autoskip-120s-110529/ solved 7,492/7,503 instances with zero wrong answers and PAR2 7047.416.

Unit equality propagation runs after optional generated preprocessing facts are appended. It collects equalities asserted at top level, including equalities under top-level and, and simplifies equality atoms decided by that unit closure. This is what turns bridge facts from diamond formulas into an immediate pre-SAT contradiction with the final disequality.

The temporary closure used by this pass is theory::equality:: IncrementalCongruenceClosure, the same use-list/lookup implementation used for incremental EUF checks over core::TermId values. Preprocessing assertions have unconditional reasons, so the closure does not build congruence explanation paths while deriving simplification-only consequences.

The forced-atom and unit-equality passes share one equality-query registration scanner. Because terms are hash-consed, the scanner treats each assertion batch as a DAG: a pass-local vector<bool> indexed by TermId records visited nodes across all assertions using the same temporary closure. The vector is sized after formula construction, the scan does not create terms, and it is destroyed before the closure, so its indices remain stable for its complete lifetime. Repeated occurrences increment :preprocessing.equality-query.memo-hits instead of recursively registering the same equality endpoints again; :preprocessing.equality-query.nodes counts first visits. This changes only work accounting, not which equality nodes or endpoint subterms enter the closure.

The motivating CPAchecker Problem01_00 profile contained only 4,362 distinct terms but made 35,267,698 duplicate closure-registration calls while walking shared Boolean subterms by occurrence. On committed revision 9b9a035, the same instance solves in 0.04 seconds and reports 7,335 first visits, 25,328 DAG memo hits, 1,914 closure add requests, and 1,684 already-seen hits. In the matching 1,284-file SLURM run, this pass recovered 35 additional instances over the preceding probe-reuse revision without losing a solve.

IncrementalCongruenceClosure::add_term also checks its existing seen_ vector before asking the TermManager for its current size. A hit is valid because a seen term was type-checked, had all children registered, and had its application signature installed before the earlier call returned. Requests and fast-path hits are reported by :preprocessing.equality-query.add-term-requests and :preprocessing.equality-query.add-term-seen-hits. This is ordinary DAG memoization around the existing congruence-closure algorithm, not a new congruence-closure algorithm or an implementation of an additional paper.

When no top-level unit equalities are present, the pass returns the assertion vector unchanged after inspecting only the top-level conjunction structure. When the only equality nodes are the unit equalities themselves, it also returns unchanged. Otherwise, simplification of repeated hash-consed Boolean subterms is memoized for the duration of the pass.

--ground-unit-substitution additionally uses the same collected non-Boolean unit equalities for a bounded ground substitution pass. The pass preserves the unit equalities as explicit assertions, rebuilds the remaining assertion DAG modulo those equalities, and then lets the normal TermManager simplifiers collapse equality, disequality, and, or, and implication structure. This is a nonclausal simplification subset: it only uses positive equalities visible at top level or under top-level conjunction, does not inspect equalities hidden under disjunction, negation, implication, or predicates, and deliberately avoids rewriting Bool-sorted equivalence classes. The option is not part of the default profile yet: local probes showed useful substitutions but no reliable solve-time win on PEQ/SEQ targets. Its effect is reported by :preprocessing.unit-equality.substitution-units and :preprocessing.unit-equality.substitutions.

--guarded-ground-unit-substitution computes the same candidate rewrite but keeps it only when cheap preprocessing metrics predict a useful SAT/EUF shape: the reachable term count must shrink by at least five percent, or the pass must perform at least 1500 rewrites while adding at most 1000 assertions. Accepted and rejected candidates are counted by :preprocessing.unit-equality.substitution-accepted and :preprocessing.unit-equality.substitution-rejected. These thresholds are empirical campaign gates, not a theorem; they are meant to preserve the PEQ/NEQ wins found in the targeted 120s SLURM campaign while filtering PEQ/SEQ cases where substitution only adds unit equality pressure.

--preprocessing-passes N controls the repeated preprocessing loop. Each pass can add bridge facts and then simplify with Boolean and unit equalities. The default is four passes. 0 disables the loop unless the strong preset or the auto single-assertion path is selected. Those paths run at least three passes because bridge facts and forced atoms can expose further unit-equality simplifications. Finite-domain AMO clauses, equality-definition clauses, and symmetry constraints are emitted once after the repeated simplification loop so generated lemmas are not fed back into every pass.

Control of this loop is implemented by the formula-level tactic API described in Tactic architecture: one preprocessing-round leaf owns the established pass order, and the preprocessing-fixed-point repeat tactical owns termination and adaptive continuation. Assertions move into and out of the tactic goal without changing their TermManager ownership. Model-reconstruction and forced-atom records are immutable goal attributes. The production strategy still returns one goal because no current preprocessing phase introduces a disjunction. The migration changes orchestration only; the individual algorithms, option meanings, and defaults are unchanged.

:preprocessing.changed-passes counts rounds that change the ordered assertion vector, including a round that immediately produces true or false. Attribute-only updates do not keep the loop running. :preprocessing.adaptive-passes counts only extra rounds that are actually scheduled after an inconclusive shrinking result.

The fixed pass count is a baseline cap, not always a hard stop. After the cap is reached, Primo may run up to four additional adaptive passes when the previous pass reduced the number of unique reachable formula terms by at least ten percent. This keeps useful simplification chains going on formulas that are still collapsing, while preventing clause-generating preprocessing from continuing merely because it can append more facts. Adaptive extension is reported by :preprocessing.adaptive-passes; the measured formula sizes are reported by :preprocessing.term-size.initial and :preprocessing.term-size.final.

The adaptive continuation is configurable. --preprocessing-adaptive-extra-passes N sets the maximum number of passes beyond --preprocessing-passes; 0 disables adaptive continuation. --preprocessing-adaptive-shrink-percent N sets the required reachable-term shrink threshold, from 0 to 100. primo --help prints the active defaults for these and the other CLI options from their bound configuration values. Help descriptions deliberately do not repeat numeric or Boolean defaults, so changing a C++ default cannot leave a second hand-maintained value behind in the prose.

Boolean Unit Propagation

Each preprocessing pass collects top-level unit facts for user Bool constants, including facts under top-level and and negative facts of the form (not p). If both polarities are present, the constant is left untouched and the SAT layer keeps the contradiction.

Collected unit facts simplify Boolean structure, Boolean equalities, and guarded formulas through the normal TermManager constructors. The unit facts themselves are preserved as assertions because SMT-LIB Bool is a first-class sort: a Boolean constant may also occur as an argument to an uninterpreted function, and the EUF solver must still see the asserted Boolean fact. Recursive rebuilding copies child TermId vectors before rewriting children. This is an ownership invariant: TermManager may intern new terms while a child is being simplified, so preprocessing must not keep references into term storage across recursive calls.

Rebuilding is memoized for the duration of one propagation call. The cache maps each hash-consed input TermId to its rewritten TermId and the number of unit replacements in that subtree. Reusing the saved replacement count preserves the existing occurrence-based rewrites statistic even though a shared DAG subtree is traversed once. The cache owns only term handles and is destroyed before the TermManager; it cannot outlive or mutate term storage. This changes repeated DAG traversal from tree-size work to expected linear work in the number of distinct visited terms. :preprocessing.boolean-units.memo-hits and :preprocessing.boolean-units.memo-misses expose that behavior.

The pass deliberately does not rewrite inside uninterpreted-function applications and does not collect frontend $primo_bool_arg_* auxiliaries as substitution facts. Those auxiliaries encode equivalences for compound Boolean arguments, and erasing them can hide predicate-congruence conflicts. The pass is therefore a bounded Boolean simplifier, not global Boolean propagation through the EUF term language.

Forced Atom Propagation

After Bool-constant unit propagation, each preprocessing pass also runs a forced-atom simplifier over the current assertion conjunction. The pass follows the standard SAT-preprocessing unit-simplification idea: collect top-level atom facts, rebuild compound formulas under those facts, and keep the unit facts as assertions so Boolean abstraction and EUF still see the original hypotheses.

The collected atoms are:

• user Bool constants, excluding frontend $primo_bool_arg_* auxiliaries;

• Bool-valued uninterpreted applications, such as predicate atoms;

• equality atoms;

• negated forms of the same atoms.

Exact atoms seen in both polarities are not used for rewriting. This avoids making simplification order-dependent on already-inconsistent input; the SAT/EUF layers still receive the contradictory facts.

Positive equality units additionally seed a temporary congruence closure. Negative equality units are retained as known disequalities. When rebuilding compound formulas, equality atoms are folded to true if the closure proves the endpoints equal and folded to false if their equality would contradict a known disequality modulo the positive closure. This catches common QF_UF patterns such as a disequality unit eliminating one branch of a disjunction, or transitive equalities contradicting a disequality before SAT search.

After the temporary closure is saturated, negative equality units are indexed by their unordered pair of congruence-class representatives. This keeps the rewriter’s disequality test proportional to the number of equality atoms being rebuilt instead of scanning every known disequality for every query. The index is local to one preprocessing pass and the original disequality assertions remain in the output.

This pass uses the same temporary incremental closure as unit equality propagation. The closure gives preprocessing affected-use-list congruence updates instead of the older all-pairs saturation scaffold, but it remains a pre-SAT simplifier: generated equalities and disequalities are preserved as assertions rather than hidden inside preprocessing state.

The pass does not rewrite inside uninterpreted-function applications. A Bool-valued predicate atom may be replaced when it occurs as a formula atom, but Boolean terms used as arguments to uninterpreted functions remain represented by the existing frontend auxiliaries and EUF facts.

Activation is reported by :preprocessing.forced-atoms.facts, :preprocessing.forced-atoms.disequalities, and :preprocessing.forced-atoms.rewrites. When the exact-atom-only branch uses the Boolean rewriter, :preprocessing.forced-atoms.memo-hits and :preprocessing.forced-atoms.memo-misses report its pass-local DAG cache. The temporary congruence-closure branch has separate rewriting machinery and leaves these two counters at zero.

Solved-Constant Substitution

Primo runs a small solved-equation preprocessing pass after forced-atom propagation. The pass is a local design-note implementation of the standard satisfiability-preserving first-order simplification rule for free constants: if a visible unit equality has the form x = t, where x is a non-Boolean uninterpreted constant and x does not occur in t, then x may be eliminated by rewriting the assertion conjunction with t.

This is not a full solve-eqs tactic. The implemented subset is deliberately bounded:

• candidates are collected only from top-level assertions and top-level conjuncts;

• only non-Boolean constants are eliminated;

• definitions whose right-hand side contains the eliminated constant are rejected;

• definitions that depend on another simultaneously solved constant are rejected for this pass and may be exposed in a later preprocessing pass;

• definitions larger than 64 tree nodes, or whose occurrence-count product would exceed 200,000 added nodes, are rejected to avoid accidental blowups;

• all terms are rebuilt through core::TermManager, preserving hash-consing and sort checks.

The pass also records each accepted x -> t replacement as the directed model reconstruction equality x = t; the left child remains the eliminated constant and the right child remains its surviving definition. When get-model is requested, tactic goals carry those entries in a typed ModelConversionChain. Both model adapters replay substitutions in reverse preprocessing order, assigning only eliminated constants from their definitions. Each batch is a simultaneous update evaluated against the following stage’s interpretation. This applies to UF and both arithmetic sorts, not only Real postsolve. The session checks original assertions in debug builds or with --check-model. Later passes may eliminate symbols used by earlier definitions, which is why forward replay is insufficient. Treating the log as undirected equalities is also incorrect: stale values for both constants can alternately overwrite each other and prevent model construction from terminating.

The directed/symmetric distinction was exercised by the early arithmetic-atom canonicalization gate. Its first exact SLURM run found a finite-domain model whose canonical equality orientation made the old undirected postsolve loop oscillate. That historical repair distinguished directed substitutions from retained theory facts. The shared model redesign now preserves this distinction in typed conversion steps rather than replaying an undirected postsolve map. The minimized QF_LRA regression and the historical corrected 3,500-row Dolmen gate cover that defect; later qualification is in Finalized model interpretations.

The reconstruction trail is owned by the preprocessing result objects in src/smt/preprocessing.hpp: BooleanUnitPropagationResult::assignments, ForcedAtomPropagationResult::assignments, SolvedConstantSubstitutionResult::substitutions, and GroundEqualitySubstitutionResult::substitutions. These vectors contain only hash-consed core::TermId handles. Preprocessing tactics append the appropriate typed steps to goal-owned immutable reconstruction state before the shared core::TermManager is destroyed. build_typed_model and assemble_component_model share the conversion semantics: eliminated constants are restored, while retained Boolean/ground-unit facts are checked at their replay stage. Neither printer nor term arena history completes definitions. Future rewrites that remove user-visible facts must supply an appropriate conversion before they can be enabled under get-model.

The pass is reported by:

• :preprocessing.solve-eqs.candidates;

• :preprocessing.solve-eqs.accepted;

• :preprocessing.solve-eqs.rewrites;

• :preprocessing.solve-eqs.rejected-cycles;

• :preprocessing.solve-eqs.rejected-blowups.

Use --no-solved-constant-substitution for ablation. Broader equation solving, including Boolean constants, equalities hidden under disjunction, and context-safe conditional definitions from lowered ITE chains, remains future work and needs a separate design note before implementation.

This pass now also fires for QF_LRA: Real equality (x = t) is a genuine Equality node throughout the entire preprocessing pipeline (the frontend builds it via the same sort-agnostic mk_eq used for uninterpreted sorts), so x = 5 is eliminated the same way an EUF definitional equality would be, with the rewrite propagating through arithmetic subterms (Plus/Times/ Le/Lt) as well. See “Real-Equality Lowering” below for the pass that converts Real equality to Le/Lt form, which runs after this one so solve-eqs (and eq-bridging, forced-atom/unit-equality propagation) see the Real case at all.

Gaussian Elimination

The plain solve-eqs recognizer above only catches the shape x = t with a bare, non-Boolean constant on one side – it misses (a) a single equation with a nonzero coefficient but no bare-variable side, e.g. 2x = 5, and (b) a genuine system where no single equation alone defines a variable but several row-reduced together do, e.g. 2x+3y=5 and x-y=1. Standard LP presolve (“doubleton/multi-row equality substitution”, see Bixby’s survey referenced from docs/papers/lra-related-work.md) covers both.

--gaussian-elimination row-reduces (Gauss-Jordan, exact util::Rational arithmetic, no floating point) the system of all Real-sorted equalities collected from the same top-level-assertion/top-level-conjunct scope as plain solve-eqs. Each variable that ends up with a pivot row after full reduction becomes an ordinary SolvedConstantCandidate, merged into the same candidate list the plain recognizer produces and run through the exact same cycle-rejection/occurrence-counting/blowup-rejection/rewrite pipeline – no separate accept/reject logic. Pivot order is deterministic (variables sorted by TermId) for fuzz-test reproducibility. Bounded by two defensive caps (number of equations, number of eligible variables) to keep the O(equations^2 x variables) elimination cost from blowing up on adversarial input; exceeding either cap makes the pass bail out cleanly (contributes zero candidates, no crash/hang). Reported by :preprocessing.solve-eqs.gaussian-candidates, alongside the existing solve-eqs stats (which already aggregate across both candidate sources).

A genuinely contradictory system (e.g. 2x+3y=5 and 2x+3y=6) is not specially detected by this pass – the contradictory row simply never becomes anyone’s pivot and is silently dropped; the contradiction is still caught soundly by the ordinary LRA tableau once the (possibly still partially-substituted) assertions reach it. No unsoundness, just no early detection.

Default on (CheckSatOptions::gaussian_elimination = true, --no-gaussian-elimination for ablation). Landed opt-in (2026-07-25) since this is materially new algorithmic machinery (row reduction), not just a recognizer extension; promoted to default-on the same day after a campaign-tier Slurm fuzz gate (3000 fuzzsmt cases plus opfuzz/yinyang mutation shards, 0 crashes/wrong-answers/bug triggers) – see docs/arithmetic.md’s Milestone roadmap and docs/run-log.json.

Monotone (One-Sided) Variable Elimination

--monotone-elimination (opt-in, default off) discharges real variables that every constraint pushes the same way.

If, after accounting for Boolean polarity, every atom mentioning x bounds it in one direction only, then no finite bound opposes x, so some extreme value satisfies all of them at once. Each such atom is replaced by the constant its own occurrence needs – true where it occurs positively, false where it occurs negatively. This is Fourier-Motzkin elimination of a single-sign variable: with no opposing bounds to pair against, the combination step is empty and every constraint mentioning the variable is simply dropped. See Monotone (one-sided) variable elimination: what to cite for what is and is not being cited.

The saving is mostly Boolean. The atom leaves the CNF and the clauses it satisfies disappear; a smaller tableau is the secondary effect. On a LassoRanker instance the pass folded only 21 atoms and removed no tableau rows at all, yet cut runtime 12.19s to 7.84s – the smaller Boolean structure produced a better search.

The pass runs immediately after Real-Equality Lowering, so equalities have already become Le/Lt pairs.

Preconditions, all conservative

A variable is disqualified – left entirely alone – unless it is a 0-ary Real Constant whose every occurrence is a linear leaf of a Le/Lt atom. Specifically:

• Real equalities pin both directions, so they disqualify.

• Uninterpreted applications are opaque: a real under f(...) disqualifies.

• Mixed polarity disqualifies. Input is not in NNF, so polarity is tracked through Not and Implies rather than assumed; one atom reached at both polarities forces its variables two-sided.

• An atom with any leaf model reconstruction could not evaluate disqualifies every variable in that atom, not just that leaf. Otherwise a discharged constraint could be left unrepairable when the model is built.

Model reconstruction

The current implementation is ComponentModelBuilder::replay_monotone in typed_model_builder.cpp, with the corresponding fragment-adapter operation in component_model_assembler.cpp. Each restored variable gets a fresh shared evaluator epoch, and discharged constraints are checked after the batch. Unconstrained constants already have total values in the base interpretation; replay does not silently invent a missing application result or change a fixed function table. The worked examples and old check_sat.cpp line references below describe the earlier implementation of the same one-sided rule, not current source locations or guaranteed printed numeral choices.

Eliminated variables are absent from the tableau, so they are valued after the solve, from the constraints that were discharged. Each constraint is re-derived against the model and yields a bound; the variable takes one unit past the tightest of them, which clears strict and non-strict bounds alike.

No dependency ordering is needed, which is worth stating because the obvious design is both more expensive and wrong. Note first that this is not because such variables are symmetric – they are not. In x > y the two are pushed opposite ways (x up, y down), and that asymmetry is exactly what makes the atom dischargeable. What order-independence says is only that valuing them in either order yields a satisfying model, not the same one. Two variables sharing one atom depend on each other, and a topological scheme would call that a cycle and discard sound eliminations. Instead: for any discharged atom, the eliminated variable valued last sees every other leaf already valued, so that atom yields a real bound on it, and going far enough satisfies all of its constraints including that one. An earlier variable does not skip the atom – it still derives a bound from it, but against whatever placeholder value the other leaf currently has (see below), which the later variable’s own turn then supersedes with its real value.

Historical validation of this rule: temporarily reversing the valuation order and re-running model validation over 120 benchmark files gave 108 valid models and 0 invalid, with some models differing in their values from the forward order. x > y ∧ x > 10 ∧ y < 3, for instance, yields x = 11, y = 2 forward and x = 11, y = -1 reversed – both satisfying. The solver tests below assert exact values and so do encode the current (forward, TermId-sorted) order; that order is deterministic, so they are stable, but a value mismatch there means the order moved, not necessarily that soundness broke.

One subtlety is load-bearing and has a regression test. Folding an atom discharges it for every variable in it, so a variable that was itself disqualified can lose its last constraint and vanish from the tableau. Such a variable must have a total value rather than be skipped as unvalued. The old implementation pinned it to zero; the current builder supplies a base-model value before replay. Skipping its bound produced models that violated the constraint the pass had discharged.

Historical worked examples

apply_monotone_eliminations (check_sat.cpp:5551) processes the eliminated variables in a fixed order. For each one, it walks its discharged atoms and, for every other leaf in an atom, reads that leaf’s current model value – assigning it 0 on the spot if it has none yet (check_sat.cpp:5583-5587). That single mechanism is what produces both the order-dependent-but-valid models above and the vanish-to-zero case below.

Order-independence, worked. Take x > y ∧ x > 10 ∧ y < 3 again, x pushed up (only lower bounds) and y pushed down (only upper bounds).

Forward (x then y):

• x: x > 10 gives bound 10. x > y needs y, which has no value yet, so y is pinned to 0 and the atom gives bound 0. Tightest lower bound is max(10, 0) = 10, so x = 10 + 1 = 11.

• y: x > y now sees x = 11, giving bound 11. y < 3 gives bound 3. Tightest upper bound is min(11, 3) = 3, so y = 3 - 1 = 2.

Result: x = 11, y = 2. Check against the original formula: 11 > 2, 11 > 10, 2 < 3 – all hold.

Reversed (y then x):

• y: x > y needs x, unvalued, so x is pinned to 0; the atom gives bound 0. y < 3 gives bound 3. Tightest upper bound is min(0, 3) = 0, so y = 0 - 1 = -1.

• x: x > 10 gives bound 10. x > y now sees y = -1, giving bound -1. Tightest lower bound is max(10, -1) = 10, so x = 10 + 1 = 11.

Result: x = 11, y = -1 – a different model, and still satisfying: 11 > -1, 11 > 10, -1 < 3.

Vanish-to-zero, worked. ψ = (x > 10) ∧ (v < x) ∧ (x2 < 0) ∧ (x2 < v). x is pushed up by both of its atoms; x2 is pushed down by both of its atoms; v is pushed two ways at once – v < x bounds it above, x2 < v bounds it below – so v is disqualified (MonotoneSide::Both, preprocessing.cpp:3844). Both of v’s atoms are folded anyway, since each is also in the atom list of an eliminated variable (x and x2 respectively), so v ends up with no tableau row at all, and – unlike x and y above – no entry of its own in eliminated to give it a final value.

Processing x then x2:

• x: x > 10 gives bound 10. v < x needs v, unvalued, so v is pinned to 0; the atom gives bound 0. Tightest is max(10, 0) = 10, so x = 11.

• x2: x2 < 0 gives bound 0. x2 < v now sees v = 0, giving bound 0. Tightest is min(0, 0) = 0, so x2 = 0 - 1 = -1.

v’s pin from x’s step is never revisited – v has no entry in eliminated to overwrite it – so it stays 0. Result: x = 11, x2 = -1, v = 0. Check against ψ: 11 > 10, 0 < 11, -1 < 0, -1 < 0 – all hold, and it is exactly v’s pinned 0 that makes the last two checks pass.

A disqualified variable in the middle of a chain, worked. The vanish case above needed three variables because v had to be disqualified by something other than the two atoms that fold it away. A two-atom chain gets there with only three variables total, and it is the middle one that disappears:

χ = (z < x) ∧ (x < y)

• z occurs only in z < x: for z, this is Hi (bounded above by x). One atom, trivially one-directional – eligible, pushed down.

• y occurs only in x < y: for y, this is Lo (bounded below by x). One atom – eligible, pushed up.

• x occurs in both: Lo from z < x (bounded below by z) and Hi from x < y (bounded above by y). Both sides marked – MonotoneSide::Both – so x is disqualified, not z or y. It is the endpoints of the chain that are monotone; the interior variable is exactly the one being bounded from both directions, which is the ordinary meaning of “not monotone.”

Folding does not care that x is disqualified: z < x folds because it is in z’s (eliminated) atom list, and x < y folds because it is in y’s. Both atoms mention x, and both get folded regardless – an atom only needs one validly eliminated participant. So x loses every atom that mentioned it and vanishes from the tableau by the same mechanism as v above: a disqualified variable whose every remaining atom happens to be folded away by some other, validly eliminated variable it shares that atom with.

How each variable gets its value is different, and worth separating out. z and y are real entries in eliminated: their own step in apply_monotone_eliminations walks their discharged atoms, derives a bound, and assigns them one unit past it – an actual, formula-derived value. x has no such step; it is never processed as an eliminated variable, because it is not one. Its value comes entirely as a side effect of whichever of z or y happens to be reconstructed first and needs x’s value to evaluate its own atom’s rest term (check_sat.cpp:5578-5587): finding no value for x yet, that step assigns it 0 on the spot and moves on. Nothing about x itself – neither its two atoms nor any notion of “the middle of a chain” – is consulted; 0 is not derived from χ, it is the generic placeholder every unvalued leaf gets, and it happens to stick because x has no entry of its own to overwrite it later.

Reconstructing z then y:

• z (pushed down): z < x – x unvalued, pinned to 0 – bound 0. Tightest is 0, so z = 0 - 1 = -1.

• y (pushed up): x < y – x already 0 from z’s step – bound 0. Tightest is 0, so y = 0 + 1 = 1.

Result: z = -1, x = 0, y = 1. Check against χ: -1 < 0, 0 < 1 – both hold. Reconstructing y before z instead pins x during y’s step rather than z’s, but x is still pinned to the same generic 0 either way, since the pin never reads anything about x’s own atoms – unlike the x/y order-independence example above, where swapping the order changed the result because both variables there had their own bound-deriving entry.

Counters

:preprocessing.monotone-elimination.candidates, .variables, and .atoms-folded.

The pure-literal rule does not transfer to theory atoms

Recorded 2026-08-05 because it is an inviting mistake, and because Primo has a mechanism (--pure-theory-filter) close enough to it to be misread as one.

In propositional SAT the pure-literal rule is free: if p occurs only positively, set p := true and delete every clause containing it. The same move is unsound for theory atoms, and turns sat into unsat:

(declare-fun x () Real) (declare-fun d () Bool)
(assert (or (>= x 10) d))   ; A = (>= x 10) occurs ONLY positively
(assert (<= x 0))           ; a clause that does not mention A at all

This is sat – take d, leave A false. Apply the rule (force A, delete its clause) and the result is (>= x 10) AND (<= x 0), which is unsat. Verified with z3, 2026-08-05.

The reason is worth stating precisely, because it is the whole distinction: A occurs nowhere else syntactically, but its meaning constrains x, which is shared with another constraint through the theory. Syntactic purity is not semantic independence. In SAT the two coincide, which is why the rule is free there.

What Primo does instead is sound, and is deliberately not this. --pure-theory-filter (EUF And Congruence Closure) never forces a value and never deletes a clause. It only omits a literal from the theory assignment when that literal has the opposite polarity to all of the atom’s occurrences – because such an assignment cannot be what satisfies any clause, so the theory need not check its consistency. Dropping a constraint from a consistency check is safe in a way that adding one is not.

With one precondition, which this passage originally omitted. The justification silently assumes the atom’s value can be flipped freely, which holds only when the atom’s meaning to the theory is exhausted by its propositional occurrences. An atom that is also a term the theory reasons about – a Bool constant used as a function argument – breaks that, and filtering it produced a wrong answer on 2026-08-26. The full argument and the rule for future mechanisms are in EUF And Congruence Closure‘s Why it is sound, and the precondition that makes it so. The sentence above is still true of every atom that meets the precondition; it is not true unconditionally.

The sound preprocessing cousin is about variables, not atoms. If a real variable x occurs only one-sided – every constraint mentioning it pushes x the same direction, after accounting for Boolean polarity – then x can be sent to its extreme and all those constraints discharged. This is the Fourier-Motzkin observation that eliminating a variable occurring with only one sign generates zero new constraints, and it is the LP-presolve notion of a dominated column. The counterexample above is correctly excluded: x there is pushed up by one constraint and down by another.

Not implemented, and it does not help the tropical family. A screen over constraint-199552 finds 927 of its 954 real variables pinned by the definitional equalities ((= lKc (+ a b))), which are two-sided by construction, leaving 27 one-sided candidates – see The tropical-matrix family: what the formulas actually say. Whether it pays on the LP-shaped families (latendresse, miplib) is unknown: the quick screen used here matches only flat atoms and silently skips nested arithmetic such as (<= (+ (* 2 x) y) 5), which is most of what those families contain, so its counts for them are artifacts and were discarded. A real evaluation needs a polarity-aware pass over the actual term structure, not a regex.

Real-Equality Lowering

Real is a total order, so t1 = t2 <=> t1 <= t2 AND t2 <= t1. Rather than adding disequality case-split machinery to LraTableau/OnlineLraPropagator for negated Real equality, Primo lowers every Real-sorted Equality node to And(Le(t1,t2), Le(t2,t1)) – so NOT(t1=t2) reduces to ordinary Boolean structure (NOT(AND(Le,Le))) that BooleanClausifier’s existing Tseitin/CNF machinery already handles, and CDCL branching over the two Le atoms explores t1<t2 vs t1>t2 for free, with no bespoke case-split code anywhere.

This lowering runs once, at the final equality-producing boundary of the preprocessing pipeline. Solve-eqs, equality bridging, forced-atom propagation, unit-equality congruence closure, symmetry breaking, finite-domain AMO, and finite-domain equality definitions all run first. This ordering matters in both directions: those passes need genuine Real Equality nodes as input, and the symmetry/finite-domain passes may produce new equality clauses of their own. Lowering therefore rewrites the complete generated assertion set before monotone elimination, mixed purification, BooleanClausifier, or theory dispatch. No native Real equality from that assertion pipeline is allowed to reach the LRA atom layer. The mixed Nelson-Oppen coordinator has a separate internal path for layering a SAT-assigned-true shared interface equality onto a final LRA check; Equality and disequality documents that narrow exception.

An earlier ordering lowered the input assertions before appending raw finite-domain AMO clauses. A Real-domain choice could consequently reintroduce (not (= x v)) after lowering and reach LRA as an unsupported native disequality. The end-to-end finite-Real-domain regressions and the permanent finite-domain fuzz gate protect this composition invariant.

When --guarded-real-equality-lowering is enabled, a guarded disjunction with exactly one Real equality child lowers by distributing the guard directly:

(or G (= x y))  ==>  (and (or G (<= x y))
                          (or G (<= y x)))

This is a local Boolean rewrite, not a separate arithmetic propagator. It keeps LRA as the only arithmetic checker while avoiding the extra Tseitin variable that would be introduced by first rewriting the equality to an inner And(Le,Le) under the Or. The option deliberately does not distribute disjunctions with multiple Real equality children, where the direct CNF expansion would either blow up or require a more careful clausification strategy.

Reported by :preprocessing.real-equality-lowering.lowered and :preprocessing.real-equality-lowering.guarded-distributed. The basic Real equality lowering is not optional – it is load-bearing for correctness – but the guarded distribution shortcut is opt-in (--guarded-real-equality-lowering) because the first tropical-matrix measurement was mixed.

ITE Lowering

core::TermKind::Ite is a term kind, so an ITE survives parsing and reaches preprocessing. Two leaves handle it, in order: simplify-extended-terms rewrites, then lower-extended-terms encodes what is left. Lowering is the second entry of the unconditional initial sequence in prepare_and_execute_preprocessing_strategy – it runs before the preprocessing mode is consulted, so --preprocessing-mode=off cannot skip it and no term of this kind can reach clausification or a theory solver. Boolean ITEs are lowered to Boolean connectives; non-Boolean ITEs use a fresh constant plus two guarded equalities, counted by :preprocessing.ite.boolean and :preprocessing.ite.auxiliaries.

Two consequences of the ITE being a hash-consed term rather than a parse-time expansion. Identical ITEs share one auxiliary instead of allocating one per occurrence, since the lowering walk is memoized on the term. And (ite c a a) and a constant condition fold in TermManager::mk_ite, which a parse-time expansion could not do.

For the common assignment shape:

(= x (ite c a b))

simplify-extended-terms distributes the equality over the branches, avoiding the auxiliary entirely:

(and (=> c (= x a))
     (=> (not c) (= x b)))

This used to be a rule in the frontend that matched an operand which was syntactically an (ite ...), carried by a symbolic step planner in dispatch_equality. As a term rewrite it also fires on an ITE reached through a let binding, or produced by an earlier rewrite, or hidden behind a nullary define-fun – none of which a rule matching S-expression shape could see – and dispatch_equality is now a plain chainable fold, 100 lines shorter.

The rule fires only on an ITE with one parent. It is sound for any ITE but profitable only for an unshared one, and the arithmetic is one-sided. Lowering pays once per hash-consed ITE – one auxiliary and two guarded equalities, shared by every parent because the walk is memoized on the term – and then one equality per parent. Distribution pays the guard structure per parent, every time. So on an ITE with n parents it trades one auxiliary for roughly n extra nodes. count_parent_edges counts parent edges over the assertion DAG and the rule declines anything above one, counted by :preprocessing.ite.equality-distribution-blocked. This is the same hazard lead 16’s compression piece names for chains: extend only through subterms occurring once, so a multiply-occurring tail keeps its sharing.

The pass is bounded, not run to a fixed point. --extended-simplification-rounds (default 1) sets how many bottom-up traversals run. One traversal cannot see the nodes its own rules create, so (= u (ite c a (ite d e f))) distributes once and leaves the inner ITE to lowering; more rounds reach further down. That looked like a defect and is not: each distribution doubles its assertion, so iterating to a fixed point is exponential. Measured on nec-smt/large/getoption_directories/prp-4-113.smt2 (1.6MB), an unbounded run reached 116s and 23GB where the same file with the leaf off preprocesses in 3.0s and 254MB, converging only after 32 rounds. The bound is what makes the rule safe; it is not a thoroughness knob.

It fires only when it actually retires the ITE, which means only when neither branch is itself an ITE. --no-ite-equality-distribution drops it entirely; the rest of the leaf runs either way. Everything else in simplify-extended-terms – the equal-branch collapse, the negated-condition normalization, the nested same-condition merge, the Boolean-ITE-to-connective rules, the div/mod/ abs identities – shrinks what it touches, so the leaf as a whole and this one rule need separate verdicts. Without that test the rule is a net loss. Preprocessed size and auxiliary count over the whole 13,306-file QF_LIA division, one binary, relative to running no leaf at all (jobs 132066 and 132106), with the unguarded rule:

configuration	size	ite auxiliaries	size on nec-smt
leaf off (--extended-simplification-rounds 0)	—	—	—
default (distribution off)	-1.27%	-2.67%	-2.16%
--ite-equality-distribution	+5.75%	-3.03%	+9.91%
… with --extended-simplification-rounds 2	+8.78%	-14.84%	+15.14%
… with --extended-simplification-rounds 4	+16.78%	-15.51%	+28.90%

The default is the only arm that beats not running the leaf on both metrics: the rest of the leaf pays for itself and this rule does not. Distribution buys 0.36 percentage points more auxiliary reduction than the other rules manage alone, and pays 7 percentage points of formula size for it. More rounds are the same trade, only more of it.

Outside nec-smt the rule is very nearly free – size -0.03% and 30% fewer auxiliaries over 10,447 files – so this default is not a statement that the rewrite is bad everywhere. It is 4,368 auxiliaries there against 25 million on nec-smt, and the family carrying the weight decides.

Why it loses on nec-smt specifically: the ITEs there are nested chains, and the rule collects almost nothing on one. On nec-smt/large/getoption_directories/prp-4-113.smt2 the distribution fires 18,867 times and removes 20 auxiliaries (40,284 to 40,264), for +58,023 reachable nodes – 3.08 nodes per firing, which is just the guard structure and nothing anomalous. Distributing (= u (ite c a (ite d e f))) removes the outer ITE’s auxiliary and hands back (= u (ite d e f)), which needs one regardless. The benefit only arrives once the whole chain is distributed, which is what the round count buys and why it buys it at an exponential price. On a family whose ITEs are single rather than nested – everything outside nec-smt – the first firing is also the last, the auxiliary really does go away, and the rule is a small win.

Constant if-then-else simplification

simplify-constant-ites, on by default, --no-cite-simplification to drop it. Decision Procedures for Linear Arithmetic (Bromberger’s thesis) sect. 8.2.3, crediting Kim/Somenzi/Jin; piece 1 of lead 16.

A constant if-then-else is a term built only from numbers and ite. An atom comparing one against a constant can be decided branch by branch: if every leaf of the tree compares the same way the atom collapses to true or false, and otherwise the comparison is pushed inside the ite and each branch decided separately. Counters: :preprocessing.cite.atoms-visited, .atoms-simplified, .branches-collapsed.

Two deliberate departures from the source, both because the integers make its presentation unsound here. The thesis first normalises a CITE by pushing constant monomials and coefficients to the leaves; this pushes the comparison down instead, and hoists an ite above a scale or a sum only where that is an identity ((* k (ite c x y)) = (ite c (* k x) (* k y))), so no coefficient is ever divided out. And the collapse test reads the leaf set of the original term, which already accounts for the scale and the offset exactly.

hoist_ite_to_top borrows nodes from core::TermManager only while reading their inputs. It copies the coefficient and all three ITE child IDs before constructing either scaled branch, then builds the branches in separate statements. Term storage belongs to the manager; insertion may relocate its vector, invalidating a borrowed Term& but not a TermId. Reading another child through that reference after mk_times was a heap-use-after-free, even when both calls appeared as arguments of one mk_ite expression. The repair follows the original ownership rule in Architecture, not a new simplification algorithm; it adds only fixed-size ID copies and leaves the identity and asymptotic cost unchanged.

constant_ite_hoisting_survives_arena_growth fills the current arena allocation with distinct terms before simplifying a mixed-outcome comparison. It verifies that capacity grows and that the resulting Boolean term is correct for scales, sums, nested ITEs, and Int/Real sorts. The earlier scaled tests decided every leaf the same way and bypassed hoisting. The minimal default-profile input is benchmarks/regressions/qf_lia_scaled_ite_arena_growth.smt2; the targeted SLURM gate is scripts/slurm_cite_hoisting_fuzz_gate.sbatch. This lifetime repair does not address the separate QF_UFLIA model-completion bug.

The caches are not an optimisation. The csimp cache is keyed on (op, term, constant, side) and shared across the whole pass, as the thesis requires. Keying it per atom instead – which recomputes every shared CITE subterm for every atom mentioning it – cost 183 seconds against 2.8 on nec-smt’s largest file.

It runs before simplify-extended-terms, because csimp produces Boolean ites and the Boolean-ite rules in that leaf are what turn them into connectives. That is the thesis’s ITE compression step, which Primo already had: a three-deep (ite c t false) chain compresses fully through those rules plus hash-consing.

What it costs and what it buys. The formula grows and the auxiliaries fall sharply – on nec-smt/large/getoption_directories/prp-4-113.smt2, ITE auxiliaries 40284 to 10026 and preprocessed size 443762 to 1280886, with preprocessing alone going from 2.8s to 27s. The growth is inherent: an atom that only partly decides becomes a Boolean tree mirroring the CITE. Solve counts settle it decisively, on the full 13,306-file QF_LIA division at 60s (job 133466, one binary):

	solved	paired runtime
off	9061	–
on	9660 (+599)	geomean 0.830, total -20.5%
nec-smt (2780 files)	+599	geomean 0.612, total -36.1%
every other family	net 0	geomean 1.0045, total +0.9%

601 gained against 2 lost, no wrong answers and no disagreements, and every one of the 2780 nec-smt files carries a declared :status that all answers were checked against.

What belongs in a constructor and what does not

TermManager’s constructors do only what defines the representation: sort checks, constant folding, and the divisor sign normalization that makes (div x 3) and (- (div x (- 3))) the same node. Everything that rewrites an ITE – collapsing equal branches, normalizing a negated condition, merging a nested ITE on the same condition, turning Boolean branches into connectives – lives in simplify-extended-terms, along with the div/mod/abs identities (div/mod by one, (mod (mod x k) k), (div (mod x k) k), (abs (abs x)), (abs (mod x k))).

That split is not only tidiness. A constructor fold is permanently on and cannot be measured or disabled, and these rules are the trivial end of the if-then-else rewrite system in lead 16, whose own falsifier requires the techniques to be evaluated together because single-technique configurations measured worse than none at all. Rules that cannot be switched off cannot take part in that evaluation. Counters: :preprocessing.ite.rewrites, :preprocessing.ite.equality-distributed, :preprocessing.extended.arithmetic-rewrites.

--no-extended-simplification is that switch. It drops the simplify-extended-terms leaf and leaves lower-extended-terms in place, so the same input still solves, with the auxiliaries the rewrites would have avoided. Lowering has no switch and is not going to get one: the linear core has no case for these kinds, and a flag that could make one reach it would be a soundness hazard rather than an ablation. Use the flag for same-binary A/B in the style the rest of this document uses (--no-finite-domain-post-amo, --no-auto-basic-single).

Nothing but the frontend builds these four kinds, so one pass before lowering sees all of them; there is no layering argument for putting the rules earlier.

This is still a targeted rule set, not a full strong ITE simplifier. Primo does not yet perform global ITE hoisting, condition-aware ITE-chain simplification, or domain-specific ITE table compression. What changed is that those are now ordinary term rewrites rather than being blocked on representation: see the 2026-09-04 update to lead 16.

The fresh-constant fallback is still the encoding a primary source calls harmful, and making ITE a term does not by itself fix that – it removes the obstacle to fixing it. Decision Procedures for Linear Arithmetic (Bromberger’s thesis) §8.2.3 identifies exactly this lowering as structure-destroying and implements a pass to reverse it on inputs that arrive already lowered (rings_preprocessed versus rings). Its ablation on the full QF_LIA SMT-LIB division puts the combined if-then-else, defined-variable and pseudo-boolean preprocessing at +1693 solved, concentrated in nec-smt, rings, rings_preprocessed and pb2010 – 3449 files of Primo’s own QF_LIA corpus, of which every one of the 2780 nec-smt files contains both let and ite. Registered as lead 16, with the caveat that the two if-then-else techniques are measured to be worse individually than not applied at all.

Equality Bridge

The equality bridge targets equality-diamond formulas from the SMT-LIB QF_UF benchmarks, generated from the Strichman-Rozanov minimum-transitivity-constraints workshop benchmark family.

The pass scans or subformulas. For every branch, it computes the equality closure of equality atoms found directly in that branch or under nested and. If every branch implies the same equality between shared terms, the pass appends that equality as a new unit assertion.

Example:

(or (and (= x y) (= y z))
    (and (= x w) (= w z)))

Both branches imply x = z, so --eq-bridge appends (= x z).

For the diamond chain:

(or (and (= x_i y_i) (= y_i x_{i+1}))
    (and (= x_i z_i) (= z_i x_{i+1})))

each disjunction implies x_i = x_{i+1}. Adding these bridge equalities lets the ordinary EUF checker derive the final contradiction without exploring all branch combinations.

The implementation is intentionally conservative:

• it looks through or and and, but not through negation, implication, or predicates;

• it only adds equalities implied by every branch;

• it caps branch count and pair checks per or node;

• generated bridge equalities are ordinary TermId equality assertions.

Finite-Domain Clauses

The finite-domain recognizer has three AMO sources. The first is a raw preprocessing scan over the original QF_UF assertions, before Boolean-unit and forced-atom simplification can turn a full operation-table choice into a residual choice. It looks for explicit choice disjunctions of the form:

(or (= t c0) (= t c1) ... (= t cn))

and requires top-level pairwise disequalities among all candidate values. For each recognized domain, strong preprocessing appends SAT-visible at-most-one clauses:

(or (not (= t ci)) (not (= t cj)))

for every pair of distinct values. These are ordinary EUF theory lemmas: if ci and cj are explicitly asserted disequal, a single term cannot equal both values. Raw clauses are delayed until after the destructive simplification loop and are deduplicated against the post-simplification recognizer before they are added to the assertion vector. The raw scan is counted by :preprocessing.finite-domain.raw-choices and :preprocessing.finite-domain.raw-amo-clauses; post-simplification clauses are counted by :preprocessing.finite-domain.post-amo-clauses; duplicates removed between raw, post, and already-present assertions are counted by :preprocessing.finite-domain.deduped-amo-clauses.

For QF_LIA and QF_UFLIA only, explicit strong also recognizes the same choice shape when every candidate value is a distinct, integer-valued Rational term of sort Int. No explicit pairwise disequalities are required in that case: the SMT-LIB Ints theory interprets each numeral as its corresponding integer. The implementation checks the term kind, Int sort, integral rational value, and distinct hash-consed TermIds; mixed value lists, arbitrary Int terms, and Real-sorted numerals remain outside this deliberately narrow subset and still require the older explicit-disequality proof. The same recognized numeral domains can feed equality-definition channeling between already-observed term equalities.

Numeral domains never feed UfSymmetryBreaker: arithmetic numeral meanings are fixed by the theory and cannot be permuted as uninterpreted constants. Recognition reports :preprocessing.finite-domain.integer-numeral-choices, .explicit-disequality-choices, and .rejected-missing-distinctness. The recognizer and clauses remain owned by smt/preprocessing; terms are only created through TermManager, and the SAT/theory boundary continues to see ordinary equality atoms. This is a semantic specialization of the existing finite-domain encoding, not a new integer solving algorithm. Its tests cover AMO generation, equality channeling, symmetry exclusion, and rejection of an otherwise identical Real domain.

The second source repeats explicit-choice recognition after the ordinary preprocessing loop. This keeps AMO generation useful on formulas whose choices are exposed by earlier passes. Use --no-finite-domain-post-amo for same-binary ablations that keep the raw choice AMO clauses but suppress this post-simplification scan.

The third source scans equality atoms already present in the assertion DAG. If the formula mentions both s = u and s = v, and u and v are explicit top-level disequal non-Boolean terms, the pass may append the same AMO clause even when there is no choice disjunction for s. This generalizes the common constant-value case to arbitrary disequality endpoints, but it is still only a theory-lemma strengthening over existing equality atoms. It does not add one-of-domain constraints, fresh finite-domain variables, or finite-model search.

If two recognized finite-domain terms s and t are explicitly asserted disequal, or are forced disequal by the top-level forced-atom pass, and share the same value set, the pass also appends distinct-endpoint AMO clauses:

(or (not (= s ci)) (not (= t ci)))

for every domain value ci. Forced disequalities are carried with the forced equalities from the same preprocessing snapshot, so the endpoint check is modulo those equalities. This is still an asserted-fact strengthening: it does not infer disequalities hidden under arbitrary Boolean structure and it does not perform finite-model search. Symmetry breaking remains narrower than AMO generation: the current symmetry pass still uses the original assertion vector and requires explicit choice disjunctions before it accepts a finite-domain value set.

When an equality atom between two recognized finite-domain terms occurs in the assertion DAG, strong preprocessing also appends equality-definition clauses over that existing equality atom. For the observed pair s, t and every value ci, the generated clauses state that:

• if s = ci and t = ci, then s = t;

• if s = t and s = ci, then t = ci;

• if s = t and t = ci, then s = ci.

Together with the explicit choice disjunctions and at-most-one clauses, these clauses expose finite-domain equality structure to SAT without fresh Boolean variables or SAT/theory shortcuts. The pass deliberately does not define every pair of terms in a finite-domain group: it only strengthens equality atoms the formula already mentions, which keeps the expansion bounded on NEQ/PEQ/SEQ families. They are counted by :preprocessing.equality-definitions; :preprocessing.equality-definitions.candidate-pairs counts observed same-domain term equalities.

A July 20, 2026 local probe on the NEQ/PEQ gap confirmed the limits of this observed-pair design. Forced finite-domain equality definitions generated no clauses on NEQ016_size7 or NEQ016_size8, because the observed equality pairs were not pairs of terms with explicit recognized finite-domain choices. On PEQ002_size8, unbounded forced equality definitions generated 10,752 clauses but made the 50,000-theory-conflict capped run slower. The pass therefore remains guarded and is not a default solution for the NEQ/PEQ operation-table slowdown.

--ground-congruence emits a bounded subset of ordinary ground-EUF congruence clauses over applications already present in the formula:

(or (not (= a0 b0)) ... (not (= an bn)) (= (f a0 ... an) (f b0 ... bn)))

No fresh applications or propositional variables are introduced. Clauses are deduplicated structurally, capped per preprocessing call, and counted by :preprocessing.ground-congruence-clauses; skipped groups are counted by :preprocessing.ground-congruence-skipped-groups.

Choice disjunctions may be nested or trees. The recognizer flattens the or node before checking that every branch is an equality between the same candidate term and one explicit value.

UF Symmetry Breaking

The recognizer looks for finite-domain choice formulas:

(or (= t c0) (= t c1) ... (= t cn))

where c0 ... cn are constants and every pair of values is asserted distinct at top level. In SMT-LIB this usually appears as assertions such as:

(assert (not (= c0 c1)))
(assert (not (= c0 c2)))
(assert (not (= c1 c2)))
(assert (or (= x c0) (= x c1) (= x c2)))

Terms with the same value set form a candidate symmetry group. A group is accepted only if:

• all values are constants of an uninterpreted sort, not Bool-valued propositions;

• the accumulated assertion multiset is syntactically invariant under the value cycle and under swapping the first two values.

For an accepted group, candidate terms are annotated with the group values that occur syntactically inside the term. If the group contains fixed terms, meaning recognized finite-domain terms that contain none of the permuted values, Primo orders those fixed terms by TermId and emits value-precedence restrictions for that fixed sequence. The first fixed term may use only the first value, the second may use only the first two values, and so on; when a later term uses value v_j, an earlier fixed term must have used v_{j-1}. These restrictions are emitted as ordinary SMT assertions over the existing equality atoms.

If a candidate group has no fixed terms after dropping terms that contain the permuted values, the pass rejects the group. A QG-style table term such as (op c0 c1) moves when the values c0, c1, ... are permuted, so it is not a stable ordered representative for value-precedence clauses. This conservative guard prevents benchmark-provided symmetry constraints from being strengthened with restrictions that are not justified by the implemented subset.

Some QG-derived formulas also contain fixed Skolem-style constants with explicit finite-domain choices over the same value set. Those fixed terms do not contain the permuted values, so they remain eligible even when the operation-table terms are dropped. The pass should then report one accepted symmetry set, count only the fixed terms, and emit value-precedence clauses for that fixed sequence. benchmarks/seeds/qf_uf/qg_symmetry_fixed_terms.smt2 keeps this behavior in the seed corpus; qg_symmetry_residual_domain.smt2 covers the rejecting side.

--finite-domain-value-precedence is default-on. Disabling it keeps the same fixed-term eligibility guard, but emits the weaker Déharbe-style unit exclusions only for the fixed terms. Primo does not currently implement a moving-term symmetry restriction.

These assertions remove value-renaming representatives from the search space. They do not replace EUF reasoning and they do not create a finite model finder by themselves.

UF symmetry breaking is emitted after the fixed-point simplification loop, but the recognizer checks the source assertion snapshot from before that loop. The ordering matters: preprocessing can turn a full finite-domain choice into a residual partial-domain disjunction after propagating forced negative equality units, and such residual domains are not independent evidence of a source-level value symmetry. AMO/equality-definition clauses are generated after symmetry breaking and are treated as derived strengthening lemmas, not symmetry evidence.

Activation is reported with :preprocessing.uf-symmetry.accepted-sets, :preprocessing.uf-symmetry.values, :preprocessing.uf-symmetry.terms, :preprocessing.uf-symmetry.constraints, :preprocessing.uf-symmetry.value-precedence-terms, :preprocessing.uf-symmetry.value-precedence-constraints, and :preprocessing.uf-symmetry.rejected-noninvariant.

Implementation Notes

The preprocessing passes operate on hash-consed core::TermId values after SMT-LIB parsing.

Equality bridging builds a small local union-find per disjunction branch. It intersects the terms that occur in equality atoms in every branch, then checks pairs of shared terms for equivalence in every branch closure.

Unit equality propagation builds one local union-find from top-level equality facts and rewrites equality atoms whose endpoints are already in the same class to true. Negated equalities then simplify through mk_not, and enclosing Boolean structure simplifies through the existing TermManager constructors. It does not inspect equalities hidden under or, implication, negation, or predicate applications.

Finite-domain equality definitions are owned by smt::FiniteDomainEqualityDefinitions in src/smt/preprocessing.*. The pass collects explicit finite-domain choice disjunctions and top-level value disequalities, records equality atoms that occur in the assertion DAG, and emits ordinary SMT assertions relating an observed (= s t) to the already-visible atoms (= s c_i) and (= t c_i) when both endpoints have the same recognized finite-domain value list. It does not create fresh Boolean variables, inspect SAT backend state, or define unmentioned term pairs. In auto, CheckSatOptions::auto_finite_domain_equality_definitions must be set before this pass runs. Then CheckSatOptions::finite_domain_eqdefs_auto_domain_limit and CheckSatOptions::finite_domain_eqdefs_auto_clause_limit bound the expansion; the clause limit applies to the single post-loop equality-definition expansion. CheckSatOptions::finite_domain_eqdefs_auto_term_limit blocks this expansion on large single-assertion formulas. Zero means unlimited for each of these guards. Guard decisions are reported with :preprocessing.equality-definitions.candidate-pairs, :preprocessing.equality-definitions.accepted-pairs, :preprocessing.equality-definitions.predicted-clauses, :preprocessing.equality-definitions.rejected-domain-size, and :preprocessing.equality-definitions.rejected-clause-limit.

Ground unit-equality substitution uses a second local union-find over the endpoints of the same visible non-Boolean unit equalities. Each equivalence class is represented by a deterministic existing term, preferring constants and then the smallest TermId. Recursive rebuilding rewrites child terms first, then rewrites the rebuilt application if it is itself a known unit-equality endpoint. The original unit equalities are emitted before the rewritten assertions, so replacing a term by its representative is justified by facts still present in the formula. This is not a full congruence-closure preprocessor: it substitutes endpoints already connected by visible unit equalities and relies on repeated passes plus hash-consing to expose additional exact endpoint matches.

Boolean unit propagation collects top-level user Bool constants and rewrites Boolean structure with those constants while preserving the unit assertions. It does not rewrite inside UF applications, so SAT/EUF still receives the facts needed for Boolean terms used as first-order arguments.

If there are no top-level Boolean-unit facts, the pass returns the input assertion vector unchanged and reports zero rewrites. This avoids constructing temporary equality/query structures for formulas whose Boolean simplification cannot use the pass.

After preprocessing, solver_strategy.cpp uses the formula-analysis module to classify the final assertion DAG with a memoized per-term feature summary. The summary preserves the existing dispatch rules: plain Real equalities are arithmetic atoms, Real equalities containing UF applications are mixed EUF/LRA atoms, and Bool-sorted UF constants or applications are EUF predicate atoms. Model-producing formulas with declared Real or Int constants retain typed model reconstruction even when preprocessing has eliminated all arithmetic atoms. Their values come from the shared model adapter and reverse conversion replay, not an abstract UF-only string builder.

For QF_UFLRA, the SMT layer also runs a memoized pre-scan before mixed purification. If there are no Real-valued UF applications in arithmetic atoms and no non-constant Real terms inside EUF atoms, the purification pass returns the assertions unchanged and reports :no.purification.skipped-no-sites. The Boolean mixed-purification rewrite itself also memoizes formula, arithmetic, and EUF rewrites by TermId for that pass. Repeated hash-consed subterms therefore reuse their rewritten result and do not rebuild the same proxy definitions or child vectors. Formula-level purification uses an explicit post-order worklist; the theory-specific arithmetic and EUF leaf rewriters remain responsible for their own term kinds. The Boolean clausifier records theory-atom polarity by (TermId, polarity), so repeated hash-consed subformulas are traversed at most once per polarity while preserving positive/negative occurrence flags.

All preprocessing walks that can receive expanded Boolean structure are stack-safe. Forced-atom simplification, Boolean-unit simplification, unit-equality consequence rebuilding, solved-constant substitution, Real-equality lowering, equality-node counting, and candidate-variable subtree summaries use explicit work vectors. Memoized passes process children before reconstructing a parent. subtree_occurrences still has work proportional to the candidate-variable summaries it merges; replacing recursion does not claim an asymptotic improvement to that map union. Boolean-unit cache hits retain the existing rewrite-accounting semantics, including replay of the cached subtree’s rewrite count. These are traversal changes only: they do not add facts, alter the congruence relation, or change Real-equality lowering rules.

UF symmetry breaking traverses top-level conjunctions to collect explicit disequalities, then scans or nodes for choice disjunctions. The invariance check builds canonical string keys for formulas after applying a value permutation. Equality, and, and or children are sorted in the key because those operators are commutative for this syntactic check.

Generated assertions are ordinary TermId formulas using mk_not, mk_implies, mk_or, and mk_eq. They are appended before QF_UF solving, so they reuse the same SAT abstraction and congruence-closure code as user assertions.

QF_UFLRA Preprocessing Opportunities

The 2026-08-04 full-corpus QF_UFLRA mining run at commit 77599f4 found 582 files where Z3 solved in at most one second while default Primo timed out at five seconds. The committed follow-up manifest benchmarks/qf_uflra-z3-fast-primo-timeout-100.txt is the current optimization sample. The first model-equality/NO pass did not explain these gaps: the default-off model-equality branch solved only five more files, worsened PAR2, and learned no forced model-equality clauses on the full run because every mutation-forced candidate was already true at the SAT level.

That conclusion applies to the former per-pair strict-separation proxy, which has since been replaced by one Section 5.2 scratch diversification sweep per mixed round. Fresh evaluation of that integration is tracked in docs/qf-uflra-model-guided-performance.md. The remaining high-value opportunities still include preprocessing and SAT-visible arithmetic strengthening:

• the first adjacent Nelson-Oppen pruning step is implemented as opt-in --qf-uflra-candidate-final-scan: it reduces the final LRA-to-EUF equality scan to EUF care pairs, EUF-atom co-occurrence pairs, and true paired LRA bounds, with a broad-scan fallback that routes discovered equalities back through SAT before accepting the arrangement;

• recognize MathSAT-style pseudo-Boolean-over-Real encodings as LRA-local finite-domain shapes, not only as UF finite-domain choice disjunctions;

• add guarded SAT-visible at-most-one/exactly-one structure for repeated Real domain choices such as x = c0, x = c1, …, when the disequality/order facts make the strengthening sound;

• simplify large mixed Boolean/LRA disjunctions using top-level LRA unit facts and solved Real definitions before SAT search;

• reuse equality and bound definitions aggressively for repeated linear terms and Real-valued UF proxies introduced by mixed purification;

• profile representative files from the committed top-100 gap manifest before choosing between LRA-domain preprocessing, stronger arithmetic propagation, or Boolean encoding changes.

Except for the opt-in candidate final scan noted above, these are planned opportunities, not implemented behavior. Any accepted preprocessing pass must emit ordinary TermId assertions, preserve the preprocessing reconstruction trail for model-producing runs, include counters showing the recognizer and generated clauses are active, and be evaluated against the current SLURM QF_UFLRA baseline.

Nullary define-fun compilation is implemented in the frontend rather than as a preprocessing pass. The motivating Problem05_60 profile attributed about 55 percent of a 6.28-second instrumented run to term dispatch and definition instantiation over 109,849 nullary definitions. The implementation compiles each such body at declaration time and makes later references direct TermId lookups. At implementation revision cef5165, three repeated runs fell from the recorded 5.37-second baseline to 2.71–2.74 seconds, and frontend time in the stats run fell from 2.783 to 0.125 seconds. SAT variables, clauses, conflicts, decisions, and propagations were unchanged on that target. This remains local microbenchmark evidence. The first 1,284-file corpus run of the eager compiler was rejected after five deep CPAchecker definition DAGs exited with SIGSEGV. ASAN identified recursive preprocessing, dispatch, purification, and clausification walks rather than a theory conflict or CaDiCaL defect. Those walks now use explicit worklists, and the five witnesses complete in an optimized local smoke check. At stack-safe revision 1f3d81c, a fresh SLURM gate passed 3,000/3,000 mixed generated cases, 1,000/1,000 finite-domain cases, 11/11 tracked seeds, and 43,978 YinYang differential solver calls with no bug trigger. The exact-commit 1,284-file, 30-second SLURM comparison then completed with zero errors, wrong answers, unsupported rows, or decisive-answer disagreements. It solved 1,238 files against the 9b9a035 baseline’s 1,234, reduced timeouts from 50 to 46, and reduced PAR2 from 3,588.44 to 3,307.00. Seven files were gained and three lost. On the 1,231 files solved by both, aggregate time fell from 526.98 to 423.16 seconds. All five former SIGSEGV rows now terminate normally: four solve inside the corpus limit and Problem08_60 times out normally. The gain is concentrated in CPAchecker induction; MathSAT remains 900/900 solved but its aggregate time increased from 62.95 to 74.30 seconds in this run.

Current Status

Implemented:

• preset CLI option --preprocessing-mode=off|basic|strong|auto;

• CLI-default auto preprocessing dispatcher;

• goal-owned typed model-conversion records, with reverse simultaneous replay;

• first-class ITE/div/mod/abs terms and mandatory extended-term lowering even when optional preprocessing is off; later generated ground formulas require their own lowering call, with auxiliary definitions included in the returned assertions (the lifecycle audit is in Boolean Arguments in EUF);

• default-on bounded constant-ITE simplification and equality-ITE distribution;

• default-off arithmetic-atom canonicalization and monotone Real elimination;

• equality bridging under disjunctions;

• unit equality propagation from top-level equalities;

• opt-in ground unit-equality substitution over non-Bool terms;

• guarded opt-in ground unit-equality substitution for campaign evaluation;

• Boolean unit propagation from top-level user Bool constants, preserving the unit facts for EUF;

• configurable repeated preprocessing loop with --preprocessing-passes;

• targeted equality-ITE lowering for (= x (ite c a b)) without a fresh non-Boolean auxiliary;

• finite-domain choice recognition from explicit disjunctions;

• opt-in strong recognition of distinct Int numeral domains for QF_LIA and QF_UFLIA, excluded from UF symmetry breaking;

• finite-domain at-most-one clauses in the strong preset and auto path, from explicit choices and from observed equality atoms to explicitly disequal constants;

• finite-domain equality-definition clauses in the strong preset and guarded finite-domain equality-definition clauses in the auto preset;

• opt-in bounded ground-congruence clauses;

• top-level pairwise disequality requirement;

• syntactic constant-permutation invariance check;

• Algorithm 1 symmetry restrictions that preserve constants occurring in moving terms;

• CLI flag --eq-bridge;

• CLI flag --uf-symmetry-breaking;

• CLI flag --no-uf-symmetry-breaking, which disables symmetry breaking even for the strong preprocessing preset;

• CLI flags --finite-domain-value-precedence and --no-finite-domain-value-precedence;

• CLI flags --finite-domain-equality-definitions and --no-finite-domain-equality-definitions;

• unit tests for equality bridging and for accepted, asymmetric, and moving-term symmetry-breaking cases.

Deferred:

• proof support for generated preprocessing lemmas;

• unconstrained-value simplification as a global formula transformation;

• unrestricted term-ITE distribution or the full CITE algorithm beyond the bounded rules described above; lowering itself is implemented in preprocessing, not the frontend;

• minimum-transitivity-constraint generation and selective Ackermannization for equality logic;

• SyGuS-derived rewrite-rule enumeration for preprocessing;

• finite-domain equality evaluation in the strong preset. A prototype evaluator exists as an internal utility, but it remains disabled because unguarded equality simplification can be unsound on PEQ-like cases;

• a semantic finite-model profile selector. The current auto dispatcher uses assertion shape only and must be judged by full-archive SLURM results, not by individual local timings;

• enabling --ground-congruence in the tuned profile. Exact-set evaluation regressed from 2 solved rows to 1 solved row on SLURM job 108936, so the clause generator remains explicit opt-in pending a better filter;

• SyMT-style graph automorphism detection;

• full-archive symmetry-only A/B reports with activation counts.

Paper Traceability

This pass is a clean Primo implementation of the idea that was successful in LLM2SMT lra; no LLM2SMT code was copied.

• Ofer Strichman and Mirron Rozanov, Generating minimum transitivity constraints in P-time for deciding Equality Logic, SMT Workshop 2005, is the source named by the SMT-LIB equality-diamond benchmarks. Primo does not implement a full minimum-transitivity-constraint generator; --eq-bridge is a narrow disjunction-consequence pass for that benchmark shape.

• Déharbe, Fontaine, Merz, and Woltzenlogel Paleo, Exploiting symmetry in SMT problems, is the source for SMT symmetry breaking by invariance under permutations of uninterpreted constants.

• Reger and Suda, Using SAT and SMT Solvers for Finite Model Finding with Sorts, remains background for finite-model value ordering; Primo’s current SMT symmetry pass uses the Déharbe et al. restriction algorithm instead.

• Bradley and Manna, The Calculus of Computation, Chapter 9, is the background reference for ground EUF reasoning used by the finite-domain at-most-one lemmas.

• Barrett et al., CVC4, CAV 2011, is the architecture reference for treating nonclausal simplification as a preprocessing stage. Primo implements only the visible unit-equality substitution subset described above.

See Exploiting Symmetry In SMT Problems and Using SAT And SMT Solvers For Finite Model Finding With Sorts.