Early LRA atom canonicalization

Algorithmic basis

The source is David Monniaux, “On using floating-point computations to help an exact linear arithmetic decision procedure,” CAV 2009, Section 2.1 (DOI). Before introducing tableau variables, that section scales every linear left-hand side to integer coefficients with no common factor and chooses its sign so the first coefficient in a fixed variable order is positive. The purpose is to give constraints in the same rational direction exactly the same left-hand side.

Primo’s implementation extends that normalization from tableau preparation to the hash-consed formula before clausification. This is still the paper’s canonicalization operation, not its floating-point basis-selection contribution; Primo does not implement that contribution.

Representation and invariants

For a Real predicate, normalize_atom first produces

[ \sum_i a_i x_i \mathrel{\sim} c, ]

where the \(x_i\) are opaque Real leaves and \(\sim\) is <=, <, or =. The canonicalizer then maintains these invariants:

1. Zero coefficients are absent and leaves are ordered by TermId.

2. The variable coefficients are integers whose absolute values have GCD one. Rational denominators are cleared before taking the GCD. The same positive scale is applied to \(c\); the right-hand side is not included when choosing the scale because different bounds on the same direction must keep the same canonical left-hand side.

3. The first variable coefficient is positive. Negating an ordered predicate reverses its orientation; negating an equality does not change equality.

4. Positive and negative monomials are reconstructed on opposite sides of the predicate, in TermId order. Thus 2a <= 2b becomes a <= b, preserving the endpoint shape used by Nelson-Oppen paired-bound publication.

5. A predicate with no variable coefficients is evaluated to a Boolean constant. A second application of the pass returns the same TermId.

The scale must be an explicit exact rational. A symbolic multiplier is an opaque leaf or unsupported nonlinear structure, not a factor that this pass may divide out. The implementation is for QF_LRA/QF_UFLRA; it does not claim validity for integer arithmetic.

Ownership and data flow

smt::canonicalize_arithmetic_atoms owns the iterative, memoized formula-DAG rewrite. It calls the arithmetic normalizer, rebuilds terms only through core::TermManager, and relies on existing hash-consing to merge canonical atoms and enclosing Boolean nodes. It traverses Boolean structure and UF arguments so a Real predicate used as a Boolean UF argument is normalized too. No model-reconstruction entry is needed because every replacement is equivalent over the Reals and no user symbol is removed.

Canonical equality orientation can change which side a later solve-eqs pass chooses to eliminate. This does not alter the canonicalizer’s model obligation, but it requires the existing directed preprocessing postsolve log to be replayed in reverse rather than treated as a set of symmetric equalities. The finite-domain model regression test covers that interaction explicitly.

When CheckSatOptions::arithmetic_atom_canonicalization is enabled, the first call runs immediately after frontend expansion and type checking, before Boolean flattening, automatic preprocessing selection, or optional preprocessing. Consequently unit propagation, solve-eqs, equality bridging, finite-domain analysis, and clausification all see canonical atoms. The final Real-equality-lowering traversal canonicalizes again to catch atoms generated by preprocessing before it replaces each Real equality with its two ordered bounds. If mixed purification rewrites arithmetic leaves or creates LRA definition bounds, a comparison-only catch-up call runs afterward. That call must leave the Real-sorted EUF definition equalities created by purification unchanged.

PreparedLraTheory retains its leading-coefficient normalization as a defensive theory-boundary invariant. Its coefficient representation can therefore differ from the primitive-integer core term, but both identify the same one-dimensional rational scale class.

Operations and complexity

• util::Rational::primitive_integer_scale computes the positive exact scale for one nonempty coefficient vector while keeping GMP representation details inside util/rational.cpp.

• Canonicalization visits each reachable DAG node once per invocation. For an arithmetic atom with \(m\) nonzero leaves it sorts in \(O(m\log m)\), computes one denominator LCM and numerator GCD, and constructs at most \(O(m)\) term references. Hash-consing reuses existing monomials, sums, predicates, and Boolean parents.

• Distinct top-level source assertions that canonicalize to the same term are deduplicated while preserving first occurrence order. Repeated occurrences of an already identical source assertion remain repeated, so the pass does not silently change assertion-count-based diagnostics or selectors.

The pass is exposed as --arithmetic-atom-canonicalization and defaults off. It remains independent of --preprocessing-mode; explicitly enabling it under --preprocessing-mode=off still runs the initial and required catch-up phases. This preserves the pre-pass default search while retaining the implementation for controlled QF_LRA and QF_UFLRA experiments. Statistics must expose visited and rewritten atoms, equalities and comparisons, constant folds, sign reversals, hash-cons aliases, removed duplicate assertions, created terms, and late catch-up rewrites.

Correctness obligations and tests

• Positive and negative integer and rational scales preserve <=, <, and equality, reversing only ordered predicates after a negative normalization.

• Scaled and side-swapped equalities canonicalize identically before lowering.

• Distinct right-hand sides remain distinct predicates even though their LRA bounds share a prepared tableau variable.

• Non-Real equalities and purification’s EUF definition equalities are unchanged.

• Boolean nesting, UF Boolean arguments, constant predicates, and a second canonicalization pass are covered directly.

• Scaled a <= b and b <= a forms still exercise the online paired-bound Nelson-Oppen path.

• The default profile reports zero canonicalization activity.

• Pure QF_UF reports zero activity even when the option is enabled.

Evaluation

The exact candidate b08a5a5 passed the 2026-08-17 SLURM merge gate: 3,000 generated mixed differential cases, 1,000 finite-domain cases, and 3,500 model rows completed without a wrong answer, crash, unsupported result, or saved bug. Dolmen directly accepted all 1,989 SAT models; the remaining 1,511 rows were UNSAT. The first gate attempt exposed and led to the repair of an independent model-postsolve termination bug before this accepted rerun.

The mandatory-pass parent/candidate comparison used exact Release binaries, CaDiCaL 3.0.0, a 60-second per-file limit, and statistics enabled:

corpus	parent	canonicalized	parent PAR2	canonicalized PAR2
QF_LRA stratified, 237 files	202	201	4922.3	5031.9
QF_UFLRA broader, 100 files	92	92	1064.9	1064.5

There were no wrong answers, errors, unsupported rows, or decisive-answer disagreements. On the 199 QF_LRA files solved by both binaries, aggregate time improved from 661.21 to 648.86 seconds, while the median candidate/parent ratio over the 61 parent runs of at least one second was 1.014. The 60-second solve set had two candidate recoveries and three losses. A three-repetition, 180-second follow-up on those five files was deterministic: each binary solved three, but different, files. Thus early canonicalization changes preprocessing and LRA search trajectories; it is a compilation invariant and an enabling simplification, not a uniform performance improvement. In particular, these results do not justify attributing a QF_LRA speedup to the pass. Consequently, the implementation is now default-off; the candidate column is the option-on profile and the parent column represents the restored default behavior.

The exact job identifiers, family summaries, mechanism counters, rejected first gate, and artifact locations are recorded in docs/run-log.json.

Additional pure-QF_LRA coverage used 3,000 generated cases and the established 14-file real benchmark seed set. The generated run produced 2,990 decisive agreements and 10 classified solver timeouts; model checking accepted 2,609 models, classified 386 rows as UNSAT, and timed out on five model-producing runs. There were no wrong answers, crashes, invalid models, or reference disagreements. OpFuzz and two typefuzz shards completed 5,600 mutations of the real seeds without a bug trigger. A separate mixed typefuzz run completed 6,000 mutations without a bug trigger. These timeout-only results do not establish completeness on arbitrary generated instances, but they do satisfy the fresh campaign requirement for retaining this experimental preprocessing pass.

Full-corpus evaluation, 2026-08-18: a materially different picture

The sample comparison above (237/1,753 QF_LRA, 100/1,284 QF_UFLRA) was never re-run at full-corpus scale. It was, as part of a broader re-evaluation campaign covering two unrelated check_sat.cpp branches landing around the same time (docs/run-log.json, entries 2026-08-18-arithmetic-canonicalization-*), run over the complete corpora: 1,753 QF_LRA files and 1,284 QF_UFLRA files, 120-second per-file limit, exact Release candidate binary (git 8cd7181, main f628dbb plus two unrelated Nelson-Oppen branches) with and without --arithmetic-atom-canonicalization:

corpus	files	default solved	canon solved	default PAR2	canon PAR2
QF_LRA, full	1,753	1,597	1,617 (+20)	49,891.78	44,394.62 (-11.0%)
QF_UFLRA, full	1,284	1,272	1,272 (+0)	3,682.91	3,685.73 (+0.08%, noise)

Zero wrong answers on either corpus, either configuration. QF_LRA complementarity: 34 files gained (canonicalization solves, default times out), 14 lost (default solves, canonicalization times out) – net +20, but still not a uniform win, exactly the “enabling simplification, not a uniform performance improvement” shape the sample already found. What changed is the sign and size of the net effect: the 237-file stratified sample evidently under-weighted the LassoRanker family (419 of the 1,753 QF_LRA files) relative to its true size, and that family accounts for most of the gains.

Three of the largest swings were verified by direct re-run outside SLURM (130-second cap, no shard contention), confirming they are genuine and reproducible rather than measurement noise: firewire.t2.c (default: timeout; canon: sat in 4.02s), disj_nightmare.t2.c (default: unsat in 108.44s; canon: unsat in 4.08s), and ecoliMILPglycerolYices3-70000 (default: sat in 12.69s; canon: timeout) – the last one confirming the losses are equally genuine, not just the gains.

QF_UFLRA remains flat, consistent with the sample. The mechanism – early canonicalization changes preprocessing and LRA search trajectories – is unchanged from the original finding; what this full run adds is that at full-corpus scale, on QF_LRA specifically, the net effect is a clear win rather than a wash. This is recorded as new evidence rather than as a decision: whether it justifies promoting --arithmetic-atom-canonicalization toward default (for QF_LRA, for QF_UFLRA, or not at all) has not been decided here.