Models: values, function tables, and reconstruction

A model must satisfy the assertions the user supplied, including expressions that preprocessing removed. A consistent EUF closure supplies equalities; arithmetic supplies numeric values. Neither alone is the complete interpretation that get-model prints. The SMT layer combines those facts, gives values to unconstrained symbols, and restores eliminated constants before returning an owning core::Model.

For example, eliminating x from x = f(y + 1) leaves a reconstruction obligation. Once the reduced problem has chosen y = 2 and f(3) = 7, the restored value must be x = 7. Giving x an arbitrary value, or treating f(y + 1) and f(3) as different function entries, would produce an invalid model. The worked replay below traces this example through the actual representation.

This chapter covers models for the supported ground fragments. The quantified UF route does not export models. The combination chapter explains how candidate theory models are reconciled before construction starts.

Representation and ownership

Object	Representation and lifetime
ModelValue	A SortId and a Boolean, exact rational, or DomainValue index. The sort is part of equality: an Int value is not a Real value with the same numeral, and indices from different uninterpreted sorts are not equal.
ModelInterpretation	One symbol’s default value and finite vector of argument/result rows. For a constant, the default is its value and there are no rows.
core::Model	Owns copies of sorts and symbols, the interpretations, visible symbol IDs, and tuple lookup tables. Its public operations are read-only. It owns no SAT state or term-manager references.
ModelEvaluator	Borrows a live TermManager and a model or construction resolver. Its memo belongs to that interpretation and manager; neither may change beneath it.
ModelConversionChain	A persistent list of typed preprocessing steps. Appending creates a new shared tail; replay visits the newest step first. Stored term IDs still require their original manager.
Construction adapters	smt/ owns temporary classes, authoritative values, mutable interpretation slots, and evaluation epochs. Those construction objects are discarded after the model is frozen.

The Model constructor checks symbol IDs, value sorts and payloads, argument counts, and function rows. An Int payload must be integral. Repeating a tuple with the same result is consistent; repeating it with a different result raises ModelError. Explicit visible symbol lists reject duplicates, missing interpretations, and internal symbols.

Because the signature is copied, printing a saved model does not need the original frontend. Evaluating a TermId still does: the ID names syntax in one particular live manager. Neither a domain index nor an EUF representative is a portable identifier across models.

Constructing the interpretation of the reduced problem

There are two adapters, with the same frozen representation and replay rules:

Route	Construction entry point
Boolean, QF_UF, standalone QF_LRA, the dedicated mixed-Real route, and preprocessing-only solutions	build_typed_model uses its private ComponentModelBuilder. Inputs include active reduced assertions, retained theory assignments, exact numeric values, and conversion records.
General component route used by QF_LIA and QF_UFLIA	assemble_component_model validates and combines exported fragments, then uses its private FragmentModelBuilder. It also accepts authoritative symbol interpretations from components.

For standalone QF_LIA, LiaTheoryComponent exports integer bindings from the winning completion tableau. The shared driver adds facts for Boolean constants that no component owns, using their final SAT values. An unassigned naming SAT variable is completed as false, with literal polarity applied. These facts are passed as a separate propositional_facts span to assemble_component_model, not as a component fragment with a synthetic token. The span is consumed during the call; only Boolean constants are accepted, and contradictory retained facts still raise ModelError. They need no EUF solving component. The shared assembler still uses its construction closure, completes unconstrained declarations, and replays eliminated definitions and model conversions. Model assembly is skipped when no model is requested.

Despite its name, ComponentModelBuilder is the first adapter above, not the general component collection driver. Both builders use a separate, direct-TermId IncrementalCongruenceClosure; they do not modify the FlatCongruenceClosure used during EUF search.

Retained facts, authoritative values, and completion choices

Construction begins from the reduced problem. The base-building code walks active assertion roots and unfiltered theory assignments, installs their equalities and disequalities, and keeps true distinct from false. Numeric component values and literal constants provide anchors: values the builder must preserve. Purification records also link each application to its proxy, so an arithmetic value assigned to the proxy reaches the application.

Terms with identical typed anchors are merged before saturation. If one class then contains incompatible anchors, construction fails. This is essential for arithmetic arguments: independently supplied x = 2 and y = 2 require f(x) and f(y) to agree, even if the input contained no equality x = y.

After saturation, Boolean constants and applications not yet anchored to true or false are completed as false. The EUF coverage argument explains why protected Boolean arguments and congruence make that safe on the prepared ground path. The fragment adapter preserves component-owned interpretations instead of overwriting them with this choice.

For the remaining classes, class_value uses a domain index for an uninterpreted sort or a fresh integer-valued rational for a numeric sort, avoiding numbers already used. Distinct unanchored EUF classes therefore receive distinct values within their sort. These choices complete a particular model; they are not values entailed by the input. Symbols outside the relevant roots receive a sort-correct default: false, zero, or an uninterpreted-domain value.

Only relevant syntax contributes application rows. Terms left in the arena from earlier preprocessing stages do not become independent constraints merely because their IDs still exist. In particular, an application appearing only in an eliminated definition is evaluated later against the established table. It does not acquire a new arbitrary result.

Function rows use evaluated arguments

For an interpretation I, a row for f(t1, …, tn) has key

(SymbolId(f), [value_I(t1), …, value_I(tn)])

The builder evaluates the children before inserting the result of the application’s class. The table is indexed by semantic values, not by child TermIds or by printed expressions. The insertion check rejects different results for one key. Thus if x and y both evaluate to 2, rows f(x) = 7 and f(y) = 8 are inconsistent; choosing whichever row was printed last cannot repair them.

Each function also has a default result for every tuple absent from its finite table. This makes the function total, including at arguments never encountered during solving. Model::apply returns the explicit row when present and otherwise the default, without inserting anything or changing the model.

Combining exported fragments

On the collection route, an accepted component token identifies the component, assignment epoch, and model revision. Before assembly, validate_component_fragment checks that the export has that exact token, contains required shared bindings, preserves the accepted equality partition or arrangement, and only supplies interpretations of owned symbols.

Uninterpreted-domain labels remain local to each component until shared terms identify them. Component A’s value 0 and component B’s value 0 need not be the same element. Conversely, if both components give a value to shared term x, those two local values must be identified even when their indices differ. FragmentDomains performs that identification before translating bindings and function rows to one model. Numeric and Boolean bindings already have concrete meanings; conflicting values cannot be repaired by renaming.

The fragment builder then applies the same class, evaluated-tuple, and replay checks. Component-owned tables remain authoritative. Assembly checks the supplied final assertions against the resulting model before returning it. Choosing an arrangement and establishing component consistency remain the responsibility of the combination driver.

Following a model back through preprocessing

The preprocessing chapter follows the forward pass order; the tactic contract explains why each goal carries its own conversion history. This section follows that history backwards after solving.

Write F0 → F1 → … → Fn for successive preprocessing stages. A conversion record for Fi → Fi+1 describes how to turn a model of Fi+1 into one of Fi. Construction starts from a model of Fn, so records must be replayed in reverse execution order. Keeping only the last definition of each symbol would lose the intermediate interpretations needed by earlier stages.

Consider the assertions

x = f(y + 1)       y = 2       f(3) = 7       p ∨ q

with Int constants x, y, Boolean constants p, q, and f : Int → Int. For a log that first eliminates x, then y, the forward and reverse steps are:

Stage	Assertions or interpretation	Saved or replayed operation
Original F0	The four assertions above	—
Eliminate x	y = 2, f(3) = 7, p ∨ q	Save x ← f(y + 1).
Eliminate y	f(3) = 7, p ∨ q	Save y ← 2.
Build a base model	Table f: [3] ↦ 7, with default 0; p = false, q = true	Preserve the numeric anchor and retained Boolean assignment; complete unanchored p. Eliminated constants may still have provisional defaults.
Replay the newest record	Set y = 2.	Evaluate 2 in the base interpretation, then update y.
Replay the older record	y + 1 evaluates to 3, so f(y + 1) reads the existing row 7. Set x = 7.	Use a fresh evaluator after the change to y. No row is inserted during replay.
Freeze and check	x = 7, y = 2, f(3) = 7, p ∨ q = true	All four original assertions evaluate to true.

For the Boolean part, take a SAT candidate with p = false, q = true. If pure-theory filtering is enabled, p’s false assignment is omitted and q’s true assignment is retained. Here p has no role as a function argument, so completing its unanchored class as false is safe. For the arithmetic part, purification can supply a proxy for f(3): its authoritative value 7 and its recorded equality to f(3) give that application its result. The numeric value must survive both construction and replay.

The numeric replay in this log is exercised by the staged reconstruction regression; it illustrates the replay contract rather than prescribing the order selected by preprocessing heuristics. One corresponding serialized interpretation is:

(model
  (define-fun x () Int 7)
  (define-fun y () Int 2)
  (define-fun p () Bool false)
  (define-fun q () Bool true)
  (define-fun f ((u Int)) Int (ite (= u 3) 7 0)))

What each conversion does

The conversion variants distinguish elimination from retained facts. The replay visitor handles them in the recorded order, not in batches grouped by variant.

Record	Reconstruction obligation
DirectedEqualitySubstitutionConversion, retained_facts = false	Evaluate all right-hand sides in the interpretation of the following stage, then update the eliminated same-sort constants simultaneously.
LiaSubstitutionConversion	The same staged constant restoration for recorded integer substitutions.
DirectedEqualitySubstitutionConversion, retained_facts = true	Ground-unit rewriting kept the facts in the reduced problem. Check the equalities at this replay stage; do not use them to overwrite constants.
BooleanTheoryAssignmentConversion	Check the retained Boolean facts at this stage. These records are not instructions to assign arbitrary truth values after solving.
PurificationProxyConversion	Application/proxy equalities constrain base construction. Replay does not change their public function interpretations.
MonotoneEliminationConversion	Restore each eliminated Real constant beyond its tightest one-sided bound, then check the discharged facts together.

For a simultaneous substitution step, every right-hand side is evaluated before any target changes. For different steps, the later step’s updates must be visible to the earlier one. Both requirements are enforced by creating an evaluator for the step, collecting updates, and only then applying them.

For monotone Real elimination, fix the current values of the other variables. A constraint a*x + r ≤ b with a > 0 gives an upper bound x ≤ (b - r)/a; a negative coefficient reverses the direction. Preprocessing records whether all required literals push x upward or downward, accounting for their polarity. The reconstruction loop evaluates these thresholds and chooses one unit below the smallest upper threshold or above the largest lower threshold. The strict margin also satisfies strict inequalities. It starts a new evaluation epoch after each variable and checks shared discharged constraints after the batch, because a later variable can finish repairing them. This is the one-sided baseline rule documented in Primo’s elimination design note; it is not a general quantifier-elimination procedure.

Dependencies and evaluation epochs

An authoritative value comes from accepted component facts or an interpreted literal. A completion choice gives an otherwise unconstrained class or symbol a value. An eliminated constant’s initial default is provisional: its reconstruction record will replace it. A derived value, such as the result of evaluating f(y + 1), depends on the interpretation used for that evaluation. These are semantic roles; the implementation does not attach a four-way tag to every value.

Changing y invalidates cached evaluations of y + 1 and f(y + 1). Primo handles that dependency by discarding the evaluator between changed stages. Within one epoch, the resolver must never revise a value already returned. Base construction may add a previously absent function row; replay only reads those tables and changes eliminated constants between epochs. There is no selective dependency graph or incremental invalidation algorithm in these builders.

This also explains why the old application f(y + 1) is not given a row before y is restored: such a row could be keyed by a provisional argument value. Evaluating it during replay instead uses the fixed function at the newly evaluated tuple. If that tuple has no explicit row, the function’s default supplies its value.

A cyclic equality such as x = f(x) is a different matter. It can be satisfied by choosing a value v for their common class and installing f(v) = v; evaluating the argument x does not recursively expand a definition of x. The solved-constant elimination guard rejects self-dependent substitution candidates. Model construction can therefore preserve a cyclic EUF equation without treating it as a cyclic conversion to replay.

Freezing, checking, and printing

After replay, the builders construct shared_ptr<const core::Model>. Construction checks its structure; subsequent evaluation and printing cannot complete or repair it. This prevents output order from changing the meaning of constants or function rows.

The core evaluator uses an explicit stack and a memo over demanded terms. It computes interpreted operators from their children using exact arithmetic and consults the model only for constants and uninterpreted applications. For an ite, it evaluates the condition and selected branch. A component cache cannot override the arithmetic meaning of an expression. Bound variables and quantified terms are outside its supported ground evaluation contract.

In the rebuilding solver path, finalize_model checks the original, pre-preprocessing assertions whenever model checking is requested, and also in debug builds when a model is produced. The retained-session path checks active assertions when check_model is enabled. The component assembler additionally checks its supplied final assertions. These checks use Primo’s own evaluator; independent printed-model validation is still required by the correctness guide.

smtlib::print_model emits visible symbols, using nested ite expressions for finite rows and the default as the final branch. It can omit rows equal to the default without changing the function. It quotes names and chooses parameter names that avoid capture. Internal auxiliaries are identified by symbol metadata and are not printed; a user’s similar-looking name is not evidence that it is internal.

Retained sessions supply the active visible signature while preserving interpretations needed for checking. Popping a declaration or reusing its name does not mutate an earlier model snapshot. The session nevertheless invalidates its current model after relevant state changes: get-model requires both :produce-models true and a current SAT result containing a model.

Contradictory anchors, false retained facts, incompatible tuple rows, and failed assertion checks raise ModelError. They are internal correctness failures, not an unsat proof or an ordinary unknown result. Resource limits in earlier solving or model reconciliation can still yield unknown before construction. Model-free solving avoids postsolve reconstruction and printing.

Cost and limitations

Within one evaluation epoch, each demanded DAG node is evaluated once; work is linear in the visited nodes and edges apart from exact arithmetic and tuple hashing. The explicit stack and memo also require space. A new epoch can revisit the same DAG, so this is not a linear bound for the whole conversion chain. Base construction additionally performs congruence closure and stores the relevant terms, classes, function rows, and signature snapshot.

The two construction adapters currently duplicate much of the replay logic. Neither provides dependency-directed reevaluation, minimal models, or a proof certificate. A valid model may use arbitrary defaults and different domain indices in different runs. :time.model.reconstruction-us measures the builder; the rebuilding path records assertion checking and serialization separately, while retained sessions report :time.model.check-and-print-us for those two operations together. Independent model-checking time must stay separate from solver benchmark timing.

Sources and implementation status

The algorithm and ownership basis is Primo’s original model-interpretation design contract, together with the typed conversion contract. The implemented design uses staged reverse replay and stable evaluation epochs. The older contract’s dependency-invalidation requirements are satisfied by fresh evaluators; they do not imply an implemented dependency worklist. Congruence closure and theory reconciliation have their paper mappings in EUF and combination. No additional optimized model-construction algorithm from another solver is claimed here.

Obligation	Existing regression coverage
Typed values, total defaults, and conflicting tuple rejection	Model table tests.
Interpreted syntax uses semantic values, exact arithmetic, and the selected ITE branch	Evaluator tests.
Deep application DAGs do not require recursive evaluation	Deep application test.
Printing survives signature destruction and avoids capture	Printer lifetime and name tests.
Reverse replay preserves intermediate versions, fixed tables, and cyclic EUF equations	Reconstruction tests and conversion order test.
Fragment labels are component-local; exports preserve tokens and shared classes	Fragment validation and assembly tests.
Restored Real values satisfy eliminated one-sided constraints	Monotone reconstruction test.
Saved models remain independent across session scopes	Session lifetime tests.

These are tests to maintain, not new execution results. The earlier model redesign’s qualification remains in its dated evidence record; subsequent component assembly has its own migration evidence. The review ledger records the documentation checks separately from those historical solver runs.