Terms, symbols, and ownership

Primo stores formulas as a shared graph of typed terms. A symbol table owns the signature, a term manager owns the graph, and other layers refer to nodes by numeric IDs. The architecture overview shows where these owners fit into a solving session; this chapter explains their storage and lifetime contracts.

Continue with tactics and preprocessing for query composition and transformations, then Boolean abstraction and SAT integration to see how Boolean terms become clauses while their meanings remain in the SMT layer.

Representation

Type and code	Stored data	Ownership contract
Sort	Name and kind: Bool, Real, Int, or uninterpreted	Stored in the symbol table’s sort vector.
Symbol	Name, argument sorts, result sort, kind, and internal-symbol flag	Stored in the symbol table’s symbol vector; sort references are IDs.
Term	Kind, result sort, child IDs, and kind-specific payload	Stored in the term manager’s term vector; children are shared through IDs.
SymbolTable	Sorts, symbols, name lookup maps, and scope trails	Owns the signature storage and controls which names are visible.
TermManager	Terms, structural interning table, and binder metadata	Owns term storage and borrows its symbol table.

SortId, SymbolId, and TermId are aliases of std::uint32_t. Each is an index interpreted by its owner. They contain no owner identity or generation, and the aliases do not enforce distinct C++ types. An in-range ID from another manager can therefore identify an unrelated object without failing a bounds check. Callers must preserve the association between an ID and its owner.

Sorts, declarations, and visibility

SymbolTable’s constructor installs the three built-in sorts. declare_sort adds an uninterpreted sort. Declarations record signatures: constants have no argument sorts; functions and predicates have argument lists, with predicates returning Bool. add_symbol checks that the referenced sorts exist and rejects a name already visible in the symbol table.

push_scope and pop_scope scope name lookup. Pop removes bindings introduced since the matching push, while the sort and symbol vectors retain their entries. Redeclaring a popped name allocates a new ID. This keeps old terms interpretable within the same manager without making a popped declaration available to new name resolution.

Generated auxiliaries have an explicit Symbol::internal flag. visible_symbols checks that flag and the current binding; it does not classify symbols by a spelling convention.

Node shapes

The TermKind declarations determine how to read each node’s payload. Every node has an explicit result sort, including Boolean formulas. A Term record has fields for all payload categories rather than a separate C++ subclass for each kind.

Kinds	Representation
BoolValue, Rational	A Boolean value or exact rational payload. An Int literal must have an integral value.
Constant	A symbol ID and no children.
Application	A function or predicate symbol ID and ordered argument IDs. Constants have their own node kind.
Equality, Not, And, Or, Implies	Boolean result and ordered operand IDs.
Plus, Times, Le, Lt	Arithmetic operands; Times has one child and a scalar payload, so it does not represent arbitrary multiplication. Comparisons return Bool.
Ite	Condition, then-branch, and else-branch IDs; the result has the common branch sort.
IntDiv, IntMod, Abs	One Int operand; division and modulo also store a normalized positive literal divisor.
BoundVariable	Sort and de Bruijn index, stored in the symbol field as an integer rather than a symbol-table entry.
Forall, Exists, Pattern	Binder declaration leaves, body, and optional pattern nodes; patterns hold their term IDs. These node kinds have sort Bool.

The core stores no SMT-LIB let node. Name binding and expansion belong to Frontend; the resulting graph uses ordinary term IDs. Parsing, printing, and the detailed frontend binding rules belong to their own chapters.

Construction, sharing, and equality

Create terms through TermManager::mk_*. These operations return IDs and can reuse a node or simplify an expression instead of allocating the requested node shape. Consumers read stored nodes through const accessors.

TermManager::Key contains kind, sort, symbol/payload index, the ordered child list, Boolean value, and rational value. intern looks up that structural key. A hit returns the existing ID; a miss appends a term, records its binder metadata, and inserts the key-to-ID mapping.

Children already exist when a parent is interned. Together with read-only access to stored nodes, this keeps the graph built through these constructors acyclic while allowing many parents to share one child.

Hash-consing shares equal constructed representations. Within one manager, mk_app(f, {a}) repeated with the same arguments returns the same ID. Asserting a = b does not change those IDs or make f(a) and f(b) the same stored node. Theory reasoning and model evaluation establish semantic equality separately. Constructors also preserve operand order: mk_eq(a, b) and mk_eq(b, a) can be distinct terms.

Local simplification

Constructor and code	Behavior relevant to representation
mk_app	Checks arity and argument sorts against the symbol signature; constant symbols use mk_constant.
mk_eq	Requires matching operand sorts; equal IDs fold to the Boolean constant true.
mk_not	Folds Boolean constants and removes double negation.
mk_and and mk_or	Fold Boolean constants, remove duplicate direct operands, and collapse empty/singleton results. Preserve the order of surviving operands and nested same-kind nodes.
mk_implies	Folds equal operands and constant antecedents/consequents.
mk_ite	Checks the Boolean condition and matching branch sorts; a literal condition selects a branch. Equal branches alone do not trigger a constructor rewrite.

Preserving nested And and Or nodes is a memory decision. A shared prefix such as and(and(p, q), r) keeps the inner node as a child. Expanding every prefix into a fresh flat operand list can turn a small shared graph into large retained child arrays. Optional bounded flattening belongs to SMT preprocessing; the original Boolean-DAG design note records that boundary and its motivating failure.

The arithmetic constructors perform their own limited normalization and exact constant folding. For example, mk_plus and mk_times can flatten arithmetic shapes, whereas mk_and and mk_or preserve nested connectives. Int division/modulo validation requires a nonzero integral literal divisor. These constructors are not a complete arithmetic normalizer or theory solver.

get reports an out-of-range term ID with std::out_of_range; checked arity, sort, and operator-precondition failures use std::invalid_argument. Callers must supply valid IDs and satisfy constructor preconditions. Checks protect the constructed representation; short-circuit simplifications do not promise to inspect every later argument after the result is already determined. The generic Rewriter and Substitution classes are still empty scaffolds. Their names do not describe a working general rewrite API.

Binders and cached facts

mk_quantifier stores the number of bound variables in symbol. Its children are declaration leaves in source order, followed by the body and any patterns. With two declarations, the first has index 1 and the second index 0 in the body. Keeping declaration sorts in the key distinguishes quantifiers even when some variables are unused; source variable names do not enter that key.

record_binder_facts maintains loose_index and contains_quantifier arrays indexed by TermId. The former is zero for a closed term, and otherwise one past its largest index left free by the term’s own binders. The arrays are allocated when the first binder-related node is interned; earlier entries are initialized as closed and quantifier-free. Each later new node derives its metadata from older children. Interning an already existing node does not increment the quantifier or extended-term counts.

Local constructor checks do not establish that every bound occurrence refers to an enclosing variable of the right sort. The separate check_bound_variables interface checks that whole-term condition. The same module exposes shifting, instantiation, and operator rebuilding; those can create terms and require the lifetime discipline below. The quantifier chapter explains their algorithms and the instantiation loop that uses them.

Allocation and borrowed references

The signature must outlive its term manager. The frontend’s member order makes that relationship concrete: it constructs the symbol table before the manager, and destroys the manager first.

An ID remains usable across insertions into its original owner. A reference returned by TermManager::get points into a vector and can be invalidated by term creation. The same concern applies to references into the symbol and sort vectors when declarations are appended. Copying an ID does not keep any of these owners alive.

Before a direct or indirect term-creating call, copy the child IDs and payloads needed by the operation. After the call, reacquire nodes by ID. This includes helpers that appear to be reads but invoke constructors internally, and sibling function arguments whose evaluation order must not be assumed. A const Term& does not prevent another call from growing its backing vector.

Operation	Allocation and lifetime effect
get, size, symbols, binder-fact queries	Read existing storage; do not intern terms. Returned references remain borrowed.
mk_*, binder transformations, preprocessing	May create nodes and grow term/key/metadata storage, even if some calls simplify or hit the interning table.
Sort/symbol declaration	Appends signature entries and lookup state; may invalidate borrowed sort/symbol references.
visible_symbols	Allocates a result vector of IDs; owning that vector does not own the signature.
Scope pop	Removes active bindings/state according to the owner; does not imply term reclamation.

For a node with k direct children, building and hashing its key visits those children; ordinary interning does not recursively inspect the descendants. Expected hash-table behavior is not a worst-case constant-time guarantee, and vector growth, rehashing, and exact-number operations add costs. Boolean deduplication uses a bounded small scan or a hash set. The first binder metadata allocation also initializes entries for the terms already present.

Storage includes both the Term and its retained hash key. In particular, intern’s copies retain child lists and rational payloads in both records. Memory estimates must include nodes, edges, keys, container capacity, and numeric payload storage. Counting only sizeof(Term) per node misses part of that cost.

Compact term storage tracks possible union or separate-payload representations, including the effect of future leaf types. The existing record layout remains in use; that redesign is deferred.

Queries, pop, and reset

The term manager has no per-term release, tracing collector, or scope-pop operation. The surrounding session decides when to destroy it.

Session operation	Effect on the term owner
Rebuild-mode check-sat	Transfers the frontend into one solving attempt. A later query recreates translation from the active journal; IDs from the old manager do not carry over.
Assumptions-mode check-sat	Reuses the frontend and engine across checks. Persistent IDs belong to that retained manager.
Assumptions-mode pop	Pops solver/frontend scopes and active assertion roots. Signature bindings are removed, but the retained manager still owns its previously created terms.
Nonzero rebuild-mode pop	Removes journal entries and discards translation; remaining commands are replayed when needed.
reset-assertions	Clears the journal and translation, including user declarations under Primo’s scoped-declaration policy; retains the selected logic and session option state.
reset	Also clears the selected logic and session model/print-success flags. Neither reset operation makes old term IDs usable in the new manager.

discard_translation destroys the engine before the frontend whose terms it borrows. The frontend pop implementation removes scoped definitions and lookup state without shrinking term storage.

An owning model has a different lifetime. Its constructor copies the signature and stores typed interpretations. A retained CheckSatOutcome::typed_model can therefore survive destruction of the frontend. Evaluating an old TermId still requires its live manager: ModelEvaluator borrows it, and the model-based constructor also borrows the model. Its memo belongs to that interpretation.

The copied signature includes the table’s stored declarations; the model’s visible-symbol list selects what is exposed, rather than shrinking those signature copies. Retaining an owning typed model can therefore retain more signature data than appears in its printed output. The serialized text does not retain that storage.

Retained terms, clauses, caches, and model snapshots all contribute to memory. The incremental-memory lead tracks profiling, reference counting, and possible collection policies. The library lead tracks public handle and lifetime guarantees.

Worked example

This complete program uses the internal core headers. It shows repeated construction sharing an ID, followed by name removal without term reclamation. These internal interfaces may change as the public library API is designed.

#include <cassert>

#include "core/symbol_table.hpp"
#include "core/term_manager.hpp"

int main() {
  primo::core::SymbolTable symbols;
  primo::core::TermManager terms(symbols);
  const auto u = symbols.declare_sort("U");
  const auto a = terms.mk_constant(symbols.declare_constant("a", u));
  const auto f = symbols.declare_function("f", {u}, u);
  const auto fa = terms.mk_app(f, {a});
  assert(terms.mk_app(f, {a}) == fa);
  const auto reflexive = terms.mk_eq(fa, fa);
  assert(reflexive == terms.mk_bool(true));

  symbols.push_scope();
  const auto old_symbol = symbols.declare_constant("temporary", u);
  const auto old_term = terms.mk_constant(old_symbol);
  const auto retained_count = terms.size();
  symbols.pop_scope();
  assert(!symbols.lookup_symbol("temporary"));
  assert(terms.size() == retained_count);
  assert(terms.get(old_term).symbol == old_symbol);

  const auto new_symbol = symbols.declare_constant("temporary", u);
  assert(new_symbol != old_symbol);
  assert(terms.mk_constant(new_symbol) != old_term);
}

The old term is still readable because its manager and signature remain alive. The second declaration has the same spelling but a different identity. Returning old_term to a caller after these local owners are destroyed would not transfer ownership or make the ID valid elsewhere.

Tests and sources

Existing regression entry points connect the explanation to executable checks:

• Hash-consing and sort checks; Boolean sharing; ITE constructor boundary.

• Binder construction and metadata.

• UF scope growth and LRA scope growth; models retained across rebuilds.

• Model ownership and printing.

The original Primo notes on Boolean DAG storage, binder representation, and model ownership record the design decisions behind these boundaries. Those notes also contain historical plans and evaluations. The quantifier chapter covers binder algorithms; model construction covers interpretation and replay. Detailed preprocessing algorithms remain outside this chapter’s scope.