From commands to an answer

Primo separates the lifetime of an SMT-LIB session from the lifetime of a solving attempt. The session remembers declarations and assertions; a solving attempt translates that context into typed terms, transforms it, and asks the appropriate Boolean/theory engines for an answer.

This overview maps the implemented boundaries to their owning types and functions. Detailed algorithms belong in the component chapters.

Making these boundaries suitable for a public library API is an open lead. The internal interfaces still need review and testing for use as a public library API.

Fig. 1 The default rebuild route. Rounded boxes are processing stages; square boxes are data. Arrows show data flow, not ownership or a complete call graph. Preprocessing may answer without invoking an engine; early errors and admission checks are omitted. The numbered walkthrough below links each stage to code.

Follow one query through the code

1. Read a command. execute_stream owns a smtlib::Parser and an smt::SmtSession for an input stream. Parser::next_command() produces command syntax; the session interprets it.

2. Maintain the context. SmtSession::Implementation owns the command journal, scope depth, frontend, optional retained engine, and last query outcome. The journal is the replayable source of declarations and assertions.

3. Translate and solve. In the default rebuild mode, SmtSession::Implementation::execute transfers the frontend and assertion roots into check_sat_frontend_once. The Frontend resolves names and types and creates terms in its own manager. Solver and theory code consume core IDs rather than SMT-LIB syntax nodes.

4. Select a route. Quantified formulas take a separate quantified-UF route. Ground goals pass through preprocessing and make_solver_dispatch, using formula features, declared logic, and model requirements to choose a strategy leaf: a terminal strategy step that invokes a solver engine. make_session_solver_strategy connects these leaves to concrete engines.

5. Return an owning outcome. CheckSatOutcome carries the result, diagnostic, statistics, model text, and optional immutable typed model. The command loop prints responses and handles command errors separately from solver answers.

A declared logic determines which inputs are accepted and helps select an engine. Preprocessing can settle a goal or expose a simpler route.

Goals, tactics, and strategies explains composition, route selection, and the lifetime of reconstruction records. Preprocessing follows the actual pass order, including required translations with the loop disabled, automatic profiles, and integer-specific restrictions.

Representation and ownership

The core representation chapter details sorts, symbols, term shapes, construction, and what survives queries and scope changes.

Object and code	What it owns or borrows	Lifetime rule
Frontend::Implementation	Symbol table and term manager	The manager borrows the symbol table; the frontend keeps them together.
core::TermManager	Term vector and hash-cons table	A TermId identifies a term in this manager. It is not portable across frontend instances.
smt::Goal	Shared immutable goal data: assertion IDs, reconstruction records, optional typed model	Owning a vector of IDs does not own the term manager those IDs address.
smt::TacticContext	Borrowed manager/statistics; invocation callbacks and deadlines	Execution state must remain within the owning solve. Strategies obtain capabilities from the executing context.
smt::BooleanClausifier	Boolean abstraction and theory-atom registry; borrowed backend and terms	The SMT layer owns the term-to-SAT mapping; the SAT backend receives literals and clauses.
core::Model	Copied signature, typed values, and interpretation tables	The completed model can survive destruction of the query frontend; evaluation of terms still needs their live manager.

TermManager::intern looks up a structural key and appends a node only when that key is absent. Term identity is TermId identity within that manager. This is distinct from two different terms becoming equal under theory reasoning.

IDs remain stable when the term vector grows; borrowed references into that vector may not. A term-creating call can invalidate a reference returned by get(), including through a helper. Copy the IDs or scalar payloads needed before the call, then reacquire the node afterwards. Reserving capacity or observing a hash-cons hit does not establish a general lifetime guarantee.

Model ownership is a separate contract. Model::Model copies the signature, and construction validates the interpretation. The ModelEvaluator borrows a live term manager and caches values for that interpretation. The printer serializes the completed model; it must not repair inconsistent function rows. Model construction explains how the SMT layer establishes that consistency before freezing the model.

Where SAT and theories meet

The Boolean abstraction and SAT integration chapter follows terms into clauses, explains scope guards, and details the callback ownership contract. The DPLL(T) chapter follows assignments, explanations, backtracking, and the final checks through the concrete SMT drivers.

The IpasirUpBackend interface exposes SAT variables, clauses, assumptions, solving, and result queries. The concrete CadicalBackend contains backend-specific integration. Primo does not implement its own SAT search engine.

ExternalPropagator is the callback boundary for assignment notifications, backtracking, explained propagation, external clauses, and checking a candidate assignment. Theory interaction can happen during Boolean search as well as when a complete assignment is found. SAT literals themselves do not contain terms; the SMT-owned atom registry connects them to the corresponding theory obligations.

Fig. 2 The simplified lazy SMT loop explains why theory lemmas feed back into Boolean search. In Primo, assignment notifications, backtracking, and explained propagation can also occur during search. This picture omits those callbacks, model construction, and unknown/unsupported exits.

In this picture, clauses cross the IpasirUpBackend::add_clause boundary; the assignment and lemma arrows stand for interactions mediated by the SMT-owned abstraction and atom registry. They do not give the SAT backend access to core terms. A candidate Boolean assignment is not yet the typed model returned to the user.

Quantified solving adds further obligations. The quantified UF entry point uses instantiation with limited SAT completion; a ground candidate alone does not establish that all quantified assertions hold. The route can return SAT only when every assigned quantifier is covered by a Skolem lemma; otherwise an unrefuted candidate may still yield unknown. Quantified models are not produced. The detailed instantiation and completion rules belong in the quantifier chapter.

The shared SMT driver, solve_component_recipe, owns the SAT loop and theory solver lifecycle. The standalone QF_LIA recipe supplies one integer-arithmetic component; the QF_UFLIA recipe supplies EUF and integer arithmetic; the quantified-UF recipe supplies EUF and quantifier instantiation. All three use the theory solver interface, called TheoryComponent in C++. That chapter describes registration, assignment changes, checks, explanations, and model contributions. QF_UFLRA retains a dedicated engine. Migrating that Real route to the existing general driver remains open. The theory-combination chapter explains shared equality obligations, candidate models, and final acceptance.

Sessions and result validity

The default is IncrementalMode::Rebuild. Rebuilding solving state does not prevent the user from making repeated queries or using scopes. In this mode, replay constructs a frontend from the current journal after the previous one has been consumed.

The opt-in assumptions mode retains additional frontend/engine state and is admitted only for QF_UF and QF_LRA. Its option validation excludes transformations and modes that are unsafe or unsupported in that setting. SAT decision-level backtracking and SMT-LIB push/pop are different lifetimes.

Scope changes and get-model show the user-facing boundary: changing the active context invalidates the last answer, and get-model requires both model production and a current SAT model. An old owning model may still exist in memory without being valid for the session’s new context.

unknown, unsupported, and command errors are distinct from unsat. CheckSatResult and CommandResponse keep those layers separate. For requested ground models, the finalization path optionally checks the original assertions and then serializes the model. An internal model inconsistency is not a logical UNSAT result.

The frontend chapter explains lexical categories, let bindings, definition expansion and typed term construction. Sessions traces command scope, journal replay, retained engines and model invalidation, including the option restrictions needed for sound incremental preprocessing.

Worked example and tests

In the first example, the session records declarations for a, b, and f, followed by a = b and f(a) != f(b). The frontend creates typed core terms. The conjunction is unsatisfiable because function congruence requires f(a) = f(b).

Preprocessing may expose that contradiction before a full SAT/theory exchange. The BooleanClausifier maps Boolean structure and atoms to SAT literals while theory code reasons about terms.

Useful entry points for checking these contracts are:

• core identity and construction tests;

• unary congruence and lookup tests;

• session scope and reuse tests;

• model representation tests;

• SAT backend protocol tests;

• strategy lifetime tests.

Sources and implementation status

Primo’s design notes provide the detailed session replay contract, model ownership contract, and tactic contract.

The existing IPASIR-UP paper map and combination implementation notes record algorithm sources and implemented subsets. Component chapters explain the corresponding algorithms and their limitations.