de Moura-Bjorner Model-Based Theory Combination

de Moura-Bjorner Model-Based Theory Combination#

Status reviewed 2026-09-09 on modular-theory-combination. QF_UFLIA now uses the collection driver described in N-component combination migration, while QF_UFLRA retains its dedicated coordinator. The model foundation is the shared immutable interpretation in Finalized model interpretations. Historical gates below qualify their named revisions; latest acceptance is indexed in Current implementation and qualification.

Reference:

Leonardo de Moura and Nikolaj Bjorner, “Model-based Theory Combination”, Electronic Notes in Theoretical Computer Science 198(2), 2008, pp. 37-49, DOI: https://doi.org/10.1016/j.entcs.2008.04.079.

This note records what the paper says, section by section, and whether Primo currently implements it. The checklist below is deliberately conservative: Primo implements a complete convex equality-sharing path for its documented QF_UFLRA subset and a default non-convex QF_UFLIA model-guided path with a complete fallback, but not the paper’s full model-based theory-combination procedure.

Overall Status#

Primo does not yet implement full DPLL(T^M) or full model-based Nelson-Oppen combination. It has these related pieces:

typed owning get-model interpretations for Boolean and all five supported logic routes, with reverse conversion replay and shared evaluation/printing;
a production theory::TheoryComponent collection protocol with immutable ownership, scope, stable-infiniteness, convexity and capability descriptors, validated projections and owned model exports. The older TheorySolver projection protocol remains inside adapters and the experimental QF_UFLRA coordinator; it is not the new scheduler boundary;
TheoryCombinationManager ownership of the shared equality ledger for interface terms, equality atoms, SAT assignment snapshots, trailed arrangement values, and per-round equality classifications;
a convex equality-sharing fixpoint for the documented mixed QF_UFLRA interface, with an exact unresolved-pair fallback;
lazy SAT-visible equality atoms for shared Real terms;
guarded equality clauses when EUF or LRA implies a shared Real equality;
default convex QF_UFLRA model reconciliation, disableable with --no-qf-uflra-model-reconciliation, where TheoryCombinationManager owns a round-scoped shared-interface model projection, explained-equality worklist, and lazy equality-decision state; the coordinator mutates a scratch LRA model, satisfies active shared disequalities, checks whether EUF can absorb each LRA value-class spanning edge and its congruence consequences, and exposes the canonical frontier of rejected edges as one lazy positive-first SAT-assumption batch;
bounded shared-Real separation for the documented model-printing subset;
default-off --model-equality-branching, which keeps surviving LRA-model-equal shared Real equality guesses on an active SAT-assumption trail;
the Section 5.2 LRA freedom-interval and greedy diversification operations, with one scratch mutation sweep per feasible mixed round when either model reconciliation or model-equality branching is enabled; its post-mutation classes feed both consumers and the exact convex candidate filter;
an opt-in --nelson-oppen-prop=online paired-bound LRA-to-EUF propagation experiment that avoids all-pairs equality precreation. The mixed dispatcher now creates and observes a fresh SAT equality variable from cb_propagate() only for a selected paired-bound candidate published by OnlineLraPropagator. The exact fallback uses the checked Simplex model partition to reject cross-value pairs before exact probes. Successful default reconciliation validates arrangement compatibility and can avoid that broad scan. A previous candidate-only experiment reran it only after separation failure, but that validation condition missed congruence conflicts caused by EUF-mergeable pairs. Omitting the scan requires the implemented shared-model compatibility invariant, not only a successful pair-separation search.

The generic coordinator implements a transition subset, not the paper’s full generic state machine. TheoryCombinationManager owns the shared projection and equality-decision lifecycle, while EUF and arithmetic retain their theory-local closure/tableau objects.

The default modular QF_UFLIA coordinator projects the checked EUF closure and final integer tableau, using coincident integer values only as reversible SAT choices. Such a choice is not an entailed equality. Because integer linear arithmetic is non-convex, bounded exhaustion or an inconclusive component restarts the complete shared-Int delayed-combination arrangement. The convex QF_UFLRA argument is therefore never applied to integers.

At bbd43b9, this exact profile passed 4,000 generated/finite differential cases, all 11 deterministic QF_UFLRA seeds, a complete 100-mutation-per-seed YinYang pass, and Dolmen validation of all 611 SAT models in a 1,000-case local sample. The 30-second 1,284-file run solved 1,257 files versus 1,238 for 1f3d81c, with 19 timeout recoveries, no losses or answer disagreements, and a PAR2 reduction from 3,306.995737 to 2,092.497309. This validated the specialized convex mechanism before the later retained component epoch and split-frontier work justified default promotion.

The later historical exact model gate at 4dca518 covers that revision after the live-EUF, care-scope, preprocessing, and model-composition changes. SLURM job 125327 passed 3,000 general and 1,000 finite-domain answer comparisons, then validated all 2,137 satisfiable generated models directly with Dolmen; the other 1,363 generated cases were unsatisfiable. Job 125328 validated all 17 satisfiable models in the deterministic 20-file real-corpus sample directly with Dolmen; the other three cases were unsatisfiable. No fallback, model error, wrong answer, crash, timeout, parser/type error, unsupported result, or saved bug remained. This validates the implemented convex QF_UFLRA model-composition subset. It does not turn the implementation into the generic Appendix A system.

no generic model object carried by the DPLL(T) state;
no theory-independent M-Propagate transition beyond the supported shared Real and Int interfaces in EUF+linear arithmetic;
no generic M-Mutate transition or mutable theory-model object; the implemented LRA sweep is scratch-only;
no production component family beyond EUF plus rational or integer linear arithmetic;
no completeness claim for general Nelson-Oppen combination.

The former per-pair theory::ModelEqualityEvaluation scaffold and LraTheoryModelView adapter have been removed. They rebuilt LRA twice per coincident pair and, more importantly, conflated failure to find a mutation with an entailment classification. The current ownership is narrower and sounder: the LRA tableau returns a valid diversified partition, the SMT coordinator uses it only to suppress model-equality candidates, and explained convex propagation remains a separate operation.

Section-by-Section Comparison#

Paper section	Paper content	Primo status
Abstract	The paper proposes reconciling candidate models from component theories instead of eagerly propagating every implied equality or eagerly adding all shared equality literals.	Partial. Primo has model printing and partial QF_UFLRA reconciliation, but no full model-based combination engine.
1 Introduction	The motivating example is that a theory model can reveal that two shared variables have equal values. The solver can use such model equalities to guide equality sharing between theories.	Partial scaffold. `--model-equality-branching` can inspect the diversified LRA model and keep surviving equality guesses between shared Real terms on an active SAT-assumption trail. This is still not the paper’s full model-propagation transition.
2 Background	Defines signatures, formulas, theories, structures, satisfaction, equality, stable infiniteness, convexity, and combination terminology.	Implemented protocol subset. `theory::TheorySolver` and `TheoryProperties` explicitly record shared sorts, stable infiniteness, convexity, and model/equality/care capabilities. They do not yet provide the mutable component-model operations of Appendix A.
2.1 Nelson-Oppen Combination Method	Reviews purification, shared variables, arrangements, and equality propagation between disjoint theories. For convex theories, propagating implied equalities can avoid arrangement enumeration.	Implemented subset. The documented purified QF_UFLRA path performs explained bidirectional equality sharing to a fixpoint. EUF emits a spanning set; LRA emits all four Section 5.1 equality shapes and uses an exact fallback over unresolved pairs equal in the checked LRA model. This is complete for that convex interface, not generic multi-theory Nelson-Oppen.
3 Related Work	Places the approach against Shostak-style combination, delayed theory combination, Ackermannization, and dynamic Ackermannization. The paper’s point is that existing alternatives can add too many literals or too many lemmas.	Mostly not implemented as paper mechanisms. Primo has separate EUF/Ackermann diagnostics and separate QF_UF disequality-propagation work, but these are not the model-based combination algorithm.
3.1 Convex Theories	Describes equality propagation for convex theories and notes that complete enumeration of all theory-implied equalities can be expensive.	Implemented subset, different schedule. Primo’s final-check coordinator reaches a complete convex fixpoint for the supported shared Real interface. Cheap producers run first; exact strict-separation probes cover what they miss. It is not the paper’s model-guided schedule.
3.2 Delayed Theory Combination	DTC creates Boolean equality literals for shared variables and lets SAT search over arrangements. This avoids special theory-combination rules but may create a quadratic number of literals.	Implemented QF_UFLIA fallback; not used by default QF_UFLRA. The default EUF+LIA route starts sparse but restarts a complete same-sort shared-Int arrangement on exhaustion or an inconclusive component because LIA is non-convex. The established QF_UFLRA path instead creates shared Real equalities lazily.
3.3 Ackermannization	Ackermann reduction replaces UF reasoning with constraints over applications and congruence axioms. The paper treats it as useful in some cases but potentially expensive.	Separate from this work. Primo’s Ackermann and disequality-propagation options are EUF-side mechanisms. They are not integrated as the paper’s model-combination method.
3.3.1 Dynamic Ackermannization	Dynamic Ackermannization adds Ackermann constraints during search, especially when disequalities between applications make argument disequalities relevant.	Separate/partial. This belongs to the QF_UF disequality propagation line, not to current mixed QF_UFLRA model-based combination.
4 Model-Based Theory Combination	This is the core contribution. A theory solver maintains or exposes a candidate model. If two shared terms are equal in that model, the combination layer may propagate that equality. If the equality is bad for another theory, search backtracks or the model is mutated.	Implemented convex QF_UFLRA subset. The default reconciliation path postpones model choices until both theories are feasible, mutates the scratch LRA model, tests LRA class spanning edges in a checkpointed EUF closure, and sends the canonical rejected-edge frontier through one positive-first IPASIR assumption solve. The default-off live-EUF profile can borrow the trail-synchronized EUF closure under a rollback scope instead of rebuilding it. Failed assumptions produce blocking clauses. Frontier batching and callback deferral are Primo scheduling mechanisms, not separate paper transitions, and this is not generic `DPLL(T^M)`.
5 Simplex: An Example Model-Producing Theory Solver	The paper shows how Simplex naturally provides a model: the current assignment maps arithmetic variables to rational values. Equal-valued shared variables are equality candidates.	Implemented LRA subset. Primo hashes exact `DeltaRational` candidate values into classes, retains the complete diversified assignment, and uses that same assignment for accepted mixed model output.
5.1 Opportunistic Equality Propagation	The paper describes `FixedEq`, `EqRow`, `EqOffsetRows`, and `EqRows`, plus fixed-variable removal and supporting bound propagation.	Partial implementation. `LraTableau::entailed_equalities()` implements all four rules with exact explanations and spanning output; mixed QF_UFLRA removes fixed basic variables by default. Primo polls the rules after a feasible check rather than maintaining the first three eagerly during pivots. Row-bound propagation is wired into mixed solving but remains opt-in after a mixed full-corpus A/B exchanged one solve for one loss. The exact unresolved-pair fallback preserves convex completeness despite those deviations.
5.2 Model Mutation	The paper describes mutating arithmetic model values, using freedom intervals, to avoid unnecessary equalities before propagating them to other theories.	Implemented LRA subset. `LraTableau::diversify_shared_model()` performs the greedy nonbasic-variable sweep on a scratch assignment and returns the complete candidate assignment plus post-mutation classes. It accepts forbidden shared-variable pairs and never reintroduces one already separated. The coordinator applies targeted strict orientations to unresolved mandatory disequalities and rebuilds the scratch model; the live tableau remains unchanged.
6 Experimental Evaluation	The paper compares model-based theory combination against DTC, Ackermannization, Yices, and MathSAT on several UF+arithmetic benchmark families.	Not reproduced. Primo has local and SLURM benchmark evidence in `docs/run-log.json`, including QF_UFLRA CPAchecker and sample Z3 comparisons, but it has not reproduced the paper’s experiment suite.
7 Conclusions	The paper emphasizes that the approach requires theories to efficiently answer whether two shared terms have equal values in the current model.	Implemented protocol subset. `TheoryModelProjection` exposes per-sort equality classes; `TheoryComponent::mutate` requests a compatible variant by opaque epoch/revision token when the capability is supported. QF_UFLIA uses the collection protocol by default but its LIA adapter does not implement live mutation. The older generic QF_UFLRA scheduler remains experimental; three/four-component tests do not add a third production theory.
7.1 On the Significance of Ackermann’s Reduction	The paper argues that model-based combination can avoid some Ackermannization costs, while dynamic Ackermannization remains useful in UF-heavy cases.	Separate. Primo’s Ackermann-related work should stay documented as EUF-specific unless it is explicitly wired into mixed-theory model combination.
7.2 Are Theories Amenable to Model-Based Combinations?	The paper asks which theories can cheaply expose useful candidate models; Simplex is the main positive example.	Implemented two-arithmetic-sort subset. Experimental generic QF_UFLRA projects exact `DeltaRational` classes, while default QF_UFLIA projects the integer completion returned by patching/cuts/branch-and-bound. Both pair those classes with an EUF closure projection through the generic scheduler; no third production theory is adapted yet.
Acknowledgment	No algorithmic content.	No implementation relevance.
Appendix A: Presentation of `DPLL(T^M)`	Gives the abstract transition system where the SAT/theory search state includes model information and model-based propagation/mutation rules.	Implemented transition subset. `ModelBasedCombinationCoordinator` represents typed component checks, entailed facts, model choices, compatible variants, fixed points, and stops after a satisfying SAT assignment. CaDiCaL still owns ordinary DPLL/CDCL transitions. Experimental generic QF_UFLRA and default QF_UFLIA use the scheduler, but persistent multi-theory state, live model mutation, and theory registration remain incomplete.

Current Primo Anchors#

The relevant implemented pieces are documented and tested here:

docs/current-status.md and docs/architecture.md: current routes, qualification scope, ownership and non-goals.
docs/n-way-combination-migration.md: collection protocol, scope normalization, model-fragment obligations and accepted migration evidence.
docs/papers/nelson-oppen-closure-methods.md: historical design intake and detailed literature progression, not the current source map.
src/smt/theory_combination.hpp: TheoryCombinationManager, the current shared equality ledger and diagnostic scaffold.
src/theory/theory_component.hpp: production component descriptors, lifecycle, capabilities and owned model exports. theory_solver.hpp retains shared result/projection types and the older projection protocol.
src/smt/component_solver.cpp, component_dispatcher.cpp, and component_model_coordinator.cpp: collection solving, callback routing and candidate reconciliation; component_model_assembler.cpp validates and assembles final fragments.
src/smt/solver_engines.cpp: the QF_UFLRA scratch candidate construction, targeted mandatory separation, EUF compatibility checking, lazy generated equality assumptions, exact fallback, candidate-model output, and the production QF_UFLIA adapters/recipe that invoke the collection driver.
tests/unit/lra_tableau_tests.cpp: all four Section 5.1 equality rules, explanations, soundness oracle, and fixed-basis preparation.
tests/unit/qf_lra_solver_tests.cpp: QF_UFLRA convex fixpoint, model-printing, shared-Real equality propagation, exact fallback, separation, and model-equality-branching regressions.
tests/unit/theory_combination_tests.cpp and tests/unit/qf_uflia_solver_tests.cpp: component-protocol properties and the non-convex complete-arrangement invariant, reversible integer model choices, bounded fallback, agreeing projections, and mixed-model reconstruction.

2026-09-01 Modular Integration Record#

The component boundary and backend-neutral coordinator implement a typed subset of the paper’s model-guided transition system. The mapping is:

Paper operation	Current generic representation	Missing generic operation
Component candidate model	`TheoryCheckResult::model`, with an opaque component/assignment/revision token and per-sort shared equality classes	Persistent theory-private model ownership across SAT transitions
`M-Propagate`	`EntailedLiteral` for justified propagation and `TheoryDecisionRequest` for a model choice; the generic scheduler preserves the distinction	Additional production component adapters
`M-Mutate`	`TheorySolver::mutate`, accepting required relations and returning a changed compatible projection, fixed point, or typed stop	Persistent component implementations beyond the experimental generic QF_UFLRA adapter; QF_UFLIA currently relies on decisions and restart rather than live integer-model mutation
Care restriction	`TheorySolver::care_pairs`, prioritized without constructing all shared pairs	Invalidation rules for long-lived component models
Backtracking	Owned by SAT and the SMT coordinator; assignment epochs reject stale projections; QF_UFLIA EUF and rational-LIA components consume the SAT trail	Dynamic arithmetic-row registration without rebuilding the online QF_UFLIA components

The generic model-guided coordinator preserves three separate kinds of information:

An entailed clause is justified by a component explanation and may be learned permanently under its guards.
A candidate-model equality says only that two shared terms coincide in the current model. It is a search choice, not a lemma.
A mutated projection is valid only for the SAT assignment and required interface relations against which it was constructed.

For convex EUF+LRA, the specialized coordinator may use explained equality propagation plus model mutation and exact separation. For non-convex LIA, a model-guided implementation may prioritize, postpone, or compact arrangement search, but it may not discard the other equality disjuncts merely because one candidate model selects a particular partition. Until a complete paper-backed DPLL(T^M) argument is implemented, the complete SAT-visible arrangement remains the QF_UFLIA completeness backstop.

This makes the intended extension point explicit: model-guided operations belong on theory components, while model-choice scheduling, SAT assumptions, failed-assumption clauses, and lifecycle invalidation belong to the SMT coordinator. Theory components still receive no SAT-backend handle.

Full Appendix A integration checklist#

The production coordinator will implement the paper’s Appendix A transition system at the SMT/SAT boundary. CaDiCaL continues to realize ordinary propositional unit propagation, decisions, failure, backjumping, learning, forgetting, and restarts; Primo does not duplicate those CDCL operations.

The coordinator state consists of an assignment epoch, a monotonically changing model revision for each component, the current per-sort shared-term partition, the dynamically introduced interface literals \(L\), and a reversible trail of candidate-model choices. A theory model stays private to its component. The generic interface exposes only an opaque snapshot token and the projected shared equality classes. The SMT layer alone owns SAT literals and dynamic literal creation.

The transition contracts are:

Theory propagation returns an entailed literal or clause together with its theory explanation. Such facts may become SAT lemmas under their stated guards.
Model propagation chooses one canonical equality on which current component projections disagree, creates its SAT literal lazily, and appends a positive decision to \(L\). A candidate-model equality is never learned as a theorem merely because it appears in one model.
Model mutation receives required interface relations and a snapshot token. Figure 1 permits any compatible model variant; Section 4 recommends a model with no fewer equivalence classes as a diversity optimization, not as a correctness premise. The generic validator therefore requires a newer, changed projection compatible with the arrangement and requested relations, or a typed fixed point. A result with the wrong assignment epoch is stale; a mutation that merges a required disequality is invalid. One mutation call per component per reconciliation bounds round-local cycling.
Non-convex splitting lets a component request a fresh SAT-visible theory decision. LIA is never treated as convex: current integer model equalities are reversible search choices, and the unchanged complete arrangement is restarted after bounded choices or an inconclusive guided check.
Failed choices produce an explained blocking clause when one exists and invalidate snapshots affected by SAT backtracking. Cancellation and resource limits remain typed stop reasons rather than learned facts.

A satisfiable result is permitted only when every component is consistent and their projected partitions agree on every shared sort. Termination is measured by bounded model revisions within an assignment epoch, the finite number of shared equality pairs, and ordinary SAT progress. The implementation must not materialize the complete cross-product of partitions on the model-guided path.

The typed API must keep entailed facts, candidate choices, and fresh non-convex decisions distinct. Its tests must cover stale tokens, mutation monotonicity, rejected incompatible mutations, failed model choices, SAT backtracking, dynamic equality creation, incomplete projections, cancellation, and an LIA case whose complete explanation is a disjunction rather than one equality.

2026-08-09 LRA Model-Mutation Integration Checklist#

Bibliographic basis:

de Moura and Bjorner, “Model-based Theory Combination”, Section 4 for the model-based equality-sharing trigger and M-Propagate/M-Mutate transition shape;
Section 5 for the Simplex assignment as the arithmetic model;
Section 5.2 for the idea that a theory may mutate or diversify its model to avoid unnecessary equalities before sharing them.

Implemented subset:

LraTableau::freedom_interval() implements the four Section 5.2 endpoint cases for a nonbasic variable without pivoting.
LraTableau::diversify_shared_model() runs the greedy update sequence on a scratch assignment, accepts an update only when the number of distinct shared values grows, and returns post-mutation non-singleton classes plus an update audit trail.
solve_qf_uflra_engine_impl() invokes the sweep once per feasible mixed round when --qf-uflra-model-reconciliation or --model-equality-branching is active. It projects classes through PreparedLraTheory::variables_by_term and reuses the result for shared-model reconciliation, exact convex candidate filtering, and model-equality branch selection.
choose_lra_model_equality_branch() receives only post-mutation candidates. The care-queued policy intersects those candidates with current EUF care pairs before queue construction. Surviving unexplained equalities remain SAT assumption guesses stored by TheoryCombinationManager; the local arrangement coordinator performs IPASIR-UP calls and failed-assumption learning.

Data structures and invariants:

LraTableau::ModelMutationResult owns the complete scratch assignment, variable classes, accepted updates, distinct-class counts, and forbidden-equality violation counts. It contains no SAT literals or SMT-LIB nodes.
LraModelEqualPartition is a round-local SMT-coordinator projection over TermIds and canonical TermPairKeys. It does not own the tableau.
The live tableau is unchanged. This preserves its trail/backtrack invariants. Targeted strict atoms create a second scratch model only for unresolved mandatory disequalities.
A post-mutation equality is a model fact, not an entailment. Failure of the greedy sweep to separate a pair cannot force an equality. Explained propagation remains owned by entailed_equalities() and the exact convex strict-orientation scan.
Unmapped shared terms are paired conservatively with all other shared terms, so missing mapping metadata cannot prune a required exact probe.
EUF-only Real terms are not interface variables and never enter the transition system. Model printing separately assigns one fresh rational to each unanchored EUF equivalence class, while a class containing a shared term keeps that term’s LRA value. The assignment is copied to every Real constant and Real-valued application in the class. When preprocessing leaves an older application in the term arena with the same concrete arguments as an active purified application, the exact class assignment for the active application wins table-row deduplication. This reconstruction step repairs the concrete combined interpretation without adding LRA atoms or SAT arrangements.

Counters and tests:

:no.interface.lra-model-mutation-* reports enablement, calls, accepted updates, distinct value classes before/after, candidate pairs before/after, and pruned pairs.
:no.interface.model-equality-filtered-pairs reports the surviving branch candidates. The pre-mutation count is computed from class cardinalities; the coordinator materializes only the surviving pair set.
Unit regressions in tests/unit/qf_lra_solver_tests.cpp cover mutation disabled, accidental equality removal, an entailed equality retained with no accepted update, care filtering before queue/atom creation, and final model reconstruction after scratch-only mutation.

Deviations and limitations:

The generic state carries opaque per-theory snapshot identities and projected equality classes, not the private theory model objects themselves.
Explained M-Propagate remains limited to the convex EUF+rational-LRA shared-Real subset. QF_UFLIA exposes model equalities only as reversible SAT choices, never as entailed propagation.
The experimental QF_UFLRA adapter exposes its checked projections through the generic transition contract. Its EUF mutation callback reuses the established checkpointed compatibility merge rather than implementing a new EUF model generator.
No non-LRA arithmetic theory model implements a production mutator yet.
No completeness claim changes. The supported behavior remains the documented convex QF_UFLRA path plus opt-in model-guided profiles.

2026-08-09 Class Projection and Reconciliation Checklist#

Bibliographic basis:

de Moura and Bjorner, Sections 4 and 5.2, for model-value equivalence classes, model mutation before equality sharing, and model-based propagation;
Nieuwenhuis and Oliveras, “Proof-Producing Congruence Closure”, for eager representative maintenance and expected-linear projection of a finite term set into congruence classes. Primo uses only that ordinary projection property here, not the paper’s proof-producing union-find implementation.

Implemented target subset:

Store each LRA model-value class once, with a term-to-class index and a separate set of unmapped shared terms. Keep the quadratic number of possible pairs as a diagnostic integer, not a vector or hash set.
Filter sparse EUF care and candidate-final pairs by class membership in expected linear time in the sparse input size.
Enumerate complete fallback and branch pairs through a deterministic, resumable class cursor. Consumers stop the cursor at their own budget; the complete exact fallback consumes it to exhaustion.
Let TheoryCombinationManager own a round-scoped, canonical worklist of explained shared equalities. The manager owns terms and SAT explanations but neither the EUF closure nor the LRA tableau.
Batch explained LRA equalities into the assignment-local EUF closure, preserving every LRA reason literal. Return a direct conflict if congruence closure contradicts an asserted EUF disequality.
Project shared EUF classes once after each batch. Keep an EUF consequence internal only when both endpoints are mapped into the same diversified LRA model class; otherwise lazily expose that consequence to SAT with its EUF explanation.

Data structures and ownership:

LraModelEqualPartition is an SMT-layer, round-local view. It stores sorted classes, a term-to-class index, sorted unmapped terms, and logical pair counts. It never owns or changes LraTableau state.
The pair cursor is a local consumer over an immutable partition. It yields canonical pairs in deterministic order and never materializes the remaining sequence.
TheoryCombinationManager::SharedModelState owns the model-class projection, internal shared equalities, and explained-worklist deduplication for one SAT assignment generation. Theory operations remain in solver_engines.cpp and FlatCongruenceClosure.
FlatCongruenceClosure exposes a read-only projection of selected flat terms into classes. It remains the owner of representatives and explanations.

Invariants and proof obligations:

A mapped pair is a model-equality candidate exactly when both terms have the same post-mutation class. Any pair containing an unmapped term remains a conservative candidate for the complete exact entailment fallback, but it is never treated as model agreement for internal reconciliation.
A model-equal pair is not an entailed equality. Only LRA equalities carrying independently checkable reasons may enter the EUF reconciliation worklist.
Every internal LRA-to-EUF merge keeps its LRA blocking literals in the EUF proof forest. A resulting EUF conflict or propagated consequence must include those literals in its explanation.
Internal EUF consequences are accepted only as agreement between the current EUF closure and the valid diversified LRA model. Final arrangement checking and model reconstruction remain completeness and soundness backstops.
Canonical worklist deduplication and monotone EUF class merging guarantee termination within a round. A SAT-visible consequence starts a new SAT round.

Complexity expectations and measurements:

Projection is linear in the shared terms plus hash-table cost. Sparse filtering is linear in the supplied sparse pairs. Physical pair enumeration is proportional only to what a consumer actually requests.
Counters distinguish logical candidate pairs, physically enumerated pairs, materialized SAT equality atoms, worklist operations, direct conflicts, and EUF consequences retained internally or exposed to SAT.
Focused tests must cover deterministic streaming, unmapped-term conservativeness, explanation composition through congruence, direct conflicts, transitive/nested EUF consequences, and lazy SAT exposure on LRA model disagreement.
At commit 4a93256, the 746,510-candidate-pair CPAchecker profile case physically enumerated zero complete-fallback pairs. Across the full corpus, sparse filters inspected 1,365,471 pairs and retained 778,460 without constructing a full candidate-pair container.

Deviations and limitations:

This is a convex EUF plus rational-LRA coordinator subset, not the Appendix A DPLL(T^M) transition system.
It does not install the scratch mutation into the live LRA tableau and does not change LRA freedom intervals, pivoting, or reason storage.
Non-convex theories and finite shared sorts remain out of scope.

Fresh validation at commit 4a93256 passed 3,000 generated mixed cases, 1,000 finite-domain cases, all 11 tracked seeds, and a 2,000-iteration-per-seed YinYang campaign without a wrong answer or bug trigger. On the 1,284-file five-second QF_UFLRA corpus, the new implementation preserved 1,156 solved files and 128 timeouts with no status or answer change relative to 4937d3c. PAR2 improved from 1412.285 to 1407.514 seconds. On the 241 rows that had used the old congruence fallback, SAT equality atoms fell from 1,139 to 728, solve calls from 1,220 to 845, decisions from 582,833 to 506,065, and propagations from 7,827,815 to 6,775,357. At that milestone the profile remained opt-in; later split-frontier, retained-epoch, exact-commit fuzz, and 30-second corpus evidence justified promoting the convex path without claiming the paper’s generic transition system.

Next Implementation Direction#

The implemented convex path now follows the paper’s candidate-first principle: it gets equality candidates from a current theory model, a cheap theory implication, or a care-ranked relevance filter before creating SAT equality atoms. It does not materialize the full same-sort shared-pair cross product. The next paper-level step is SAT-trail-synchronized component-model state and explicit generic M-Propagate/M-Mutate transitions, not another pair container. Primo’s one-entry augmented LRA epoch is a measured QF_UFLRA ownership subset, not that generic state.

The concrete post-2026-08-05 performance plan is tracked in docs/qf-uflra-model-guided-performance.md. That note records the Z3-stat diagnosis from the current SLURM artifact and turns the paper mechanisms into a QF_UFLRA implementation checklist. Its first consumer-aware target and the later guarded per-merge experiment are historical milestones. The rejected shortcut carried an LRA-implied equality internally without reconciling all EUF congruence consequences. The current worklist path instead asserts the explained equality into EUF, composes conflicts from the retained reason, and keeps only consequences accepted by the diversified LRA model. Its focused tests and the bbd43b9 fuzz/model-validation gates provide the separate proof and regression coverage that the earlier shortcut lacked.

For the current CaDiCaL backend, the concrete rule is:

Keep the online producer’s paired-bound candidates separate from the full shared-pair cross product.
For CaDiCaL-backed online search, use the backend-neutral sat::ExternalPropagator and IpasirUpBackend::new_observed_var() path to test selected fresh equality atoms at controlled callback boundaries before relying on them in the mixed dispatcher.
Stream the theory-owned explanation if the equality is entailed; use SAT assumptions or guarded clauses for model-equality guesses.
Record the full shared-pair count, selected candidate count, lazy-created/observed atom count, delivered propagation count, disagreement conflicts, and pairs removed by model diversification.

The dispatcher follow-up has landed for the paired-bound source only: --nelson-oppen-prop=online no longer precreates equality atoms before search, but it still does not turn arbitrary LRA model equalities into entailed theory propagations.

The next narrow step after the paired-bound dispatcher has also landed: the Section 5.2 LRA mutator now filters shared-model and branch candidates once per feasible mixed round. It never treats an unseparated pair as forced. This is still not a full DPLL(T^M) implementation until the solver has a generic mutable theory-model object and theory implementations that can participate in the paper’s transitions.

Documentation Claim To Use#

Use this wording when summarizing the current state:

Primo implements a convex experimental QF_UFLRA subset of de Moura and Bjorner’s model-based theory combination. Its LRA component diversifies a scratch model, mandatory disequalities receive targeted separation, and a checkpointed EUF closure tests LRA value-class spanning edges and their congruence consequences. Rejected edges become lazy positive-first assumptions owned by TheoryCombinationManager; successful model choices never become entailed propagations. The opt-in online paired-bound producer exercises the SAT callback path without all-pairs equality precreation and lazily creates only the selected equality atom it is about to propagate. Primo does not yet implement the full DPLL(T^M) procedure, a mutable generic theory-model object, or complete Nelson-Oppen model-equality propagation.

Avoid saying that Primo implements “the de Moura-Bjorner algorithm” without the qualification above.

de Moura-Bjorner Model-Based Theory Combination

Contents

de Moura-Bjorner Model-Based Theory Combination#

Overall Status#

Implementation Checklist#

Convex combination foundation#

Section 4: model-based combination#

Sections 5 and 5.1: Simplex equality production#

Structural boundary for fresh equality probes#

Section 5.2: freedom-interval mutation#

Evaluation and generality#