Class PremiseEngine<TArg, TPremise, TExpr, TVar>

Adds an expression to this premise's tree.

If the expression has parentId: null it becomes the root; only one root is permitted per premise. All Structural rules (implies/iff root-only, child limits, position uniqueness, derivation root operator) are enforced at mutation time.

As of v1.0 P-1 (non-not operator under operator) is not enforced at mutation time — the AN-1 post-hook in assistive behavior inserts the formula buffer; in permissive behavior the un-buffered state stays and surfaces via engine.validate('presentable').

Adds an expression immediately before or after an existing sibling, with position computed automatically.

Composite-mutation behavior (spec §8 / S-9): sibling positions are always shifted as part of the bundled op when the computed midpoint position would collide with an existing sibling. Only the minimal set of nodes is repositioned. Repositioned siblings appear in changes.expressions.modified.

Adds an expression as the last child of the given parent, with position computed automatically. If parentId is null, the expression becomes the root.

Composite-mutation behavior (spec §8 / S-9): sibling positions are always shifted as part of the bundled op when the computed position would collide with an existing sibling. Repositioned siblings appear in changes.expressions.modified.

Changes the operator type of an existing operator expression.

Handles three structural cases automatically:

• Simple change: The operator has exactly 2 children and no merge condition. Updates the operator type in-place.
• Merge: The operator has exactly 2 children and its parent is the same type as newOperator. Dissolves the current operator and reparents its children under the parent.
• Split: The operator has >2 children. Extracts sourceChildId and targetChildId into a new sub-operator of type newOperator, inserting a formula buffer between the parent and the new sub-operator (the buffer is part of the bundled composite mutation so the resulting tree satisfies P-1 regardless of the engine's behavior setting).

Deletes all expressions that reference the given variable ID, including their subtrees. As of v1.0 the pre-mutation operator collapse cascade is gone — AN-3 (post-mutation hook in assistive behavior) handles 0/1-child operator/formula collapse on the surviving parents.

Evaluates the premise under a three-valued expression assignment.

Variable values are looked up using Kleene three-valued logic (null = unknown). Missing variables default to null. For inference premises (implies/iff), an inferenceDiagnostic is computed with three-valued fields unless the root is rejected.

Forces recomputation of all dirty checksums in the hierarchy.

Returns the child expressions of the given parent, sorted by position.

Returns the checksum for a named descendant collection. Null if collection is empty.

Returns the operator expressions a reviewer can accept or reject, in pre-order depth-first tree order.

Excludes "not" operators (NOT is flipped via a render-time flag, not voted on) and skips formula nodes (they are traversed but never emitted). Returns [] for empty premises and premises with no operators.

Order is stable across calls on the same PremiseEngine instance; callers typically rely on index for step-queue construction.

Returns an expression by ID, or undefined if not found in this premise.

Returns all expressions in this premise.

Returns the premise's extra metadata record.

Returns the premise ID.

Returns the set of variable IDs referenced by expressions in this premise. Only variables that appear in type: "variable" expression nodes are included.

Returns the root expression, or undefined if the premise is empty.

Returns the ID of the root expression, or undefined if the premise is empty.

Returns all argument-level variables (from the shared VariableManager) sorted by ID. Since the VariableManager is shared across all premises, this returns every registered variable — not just those referenced by expressions in this premise.

Splices a new expression between existing nodes in the tree. The new expression inherits the tree slot of the anchor node (leftNodeId ?? rightNodeId).

As of v1.0 P-1 (non-not operator under operator) is not enforced at mutation time — the AN-1 post-hook in assistive behavior inserts the formula buffer; in permissive behavior the un-buffered state stays and surfaces via engine.validate('presentable').

Returns true if this premise does not have an inference operator at its root. Equivalent to !isInference().

Returns true if the root expression is an implies or iff operator, meaning this premise expresses a logical inference relationship.

Loads expressions in BFS order with the nesting check bypassed. Bypasses all PremiseEngine validation (ownership, variable existence, circularity) since restoration paths trust existing data completely.

Invalidates the cached checksum so the next call recomputes it.

Removes an expression and optionally its entire descendant subtree.

As of v1.0 the pre-mutation 0/1-child collapse cascade is gone — AN-3 (post-mutation hook in assistive mode) handles 0/1-child operator/formula collapse on the surviving parent.

Reparent an existing expression onto a new parent at the given position. Bundled-composite mutation per spec §8 — the parent reference, position field, and checksum-dirty propagation update atomically in a single call. No transient orphan state is externally observable.

Enforces Structural rules only (S-1 FK soundness, S-4 no-cycles, entity-not-found, and S-9 logical sibling-position uniqueness at the bundled-composite level — same-position collisions with the moved expression's own prior slot are tolerated as transient, since the move atomically frees that slot). Higher-tier violations never throw here — Evaluable/Derivable/Presentable issues surface through validate(tier) per spec §7.1.

Used by the native AN-1 (formula-buffer insertion) and AN-4 (same-operator absorption) passes in src/lib/grammar/an-rules.ts, and available to repair primitives and future composite ops that need a public reparent surface (e.g. removeOrphanOperators).

Sets a callback that runs full argument-level invariant validation. Injected by ArgumentEngine so the premise can delegate to the argument-level validator.

Sets a callback that checks whether adding a variable-expression to a premise would create a circular binding. Injected by ArgumentEngine to enable cross-premise cycle detection. If not set, only the direct check (within the premise itself) runs.

Sets a callback that checks whether a premise-bound variable's target premise has an empty expression tree. Injected by ArgumentEngine to enable cross-premise validation. Used during validateEvaluability.

Replaces the premise's extra metadata record.

Sets a callback invoked after every mutation, or undefined to clear.

Sets a callback that returns the full set of variable IDs registered in the argument. Injected by ArgumentEngine.

Returns a serializable snapshot of the premise's owned state.

Renders the entity as a human-readable string.

Toggles negation on an expression. If the expression's parent is a NOT operator, removes the NOT (promoting the expression). Otherwise, wraps the expression with a new NOT operator.

As of v1.0 P-1 (non-not operator under operator) and P-2 (NOT(NOT(x)) double-negation) are not enforced at mutation time. The post-mutation AN hook handles them in assistive behavior: AN-1 inserts the formula buffer between NOT and a non-not operator child; AN-2 collapses NOT(NOT(x)) → x. In permissive behavior both states stay and surface via engine.validate('presentable').

Returns a serializable premise representation containing only identity/metadata and checksum. Use getRootExpressionId(), getExpressions(), getReferencedVariableIds() for runtime state.

Updates mutable fields of an existing expression. Only position, variableId, and operator may be updated.

Shallow-merges updates into the premise's existing extras.

Run invariant validation on this premise and its expression tree.

Validates that this premise is structurally ready for evaluation.

Walks the premise's expression tree, invoking the visitor for each node, and returns the visitor's result for the root. Returns the result of visitor.empty() when the premise has no root expression.

Wraps an existing expression with a new operator and a new sibling in a single atomic operation.

The operator takes the existing node's slot in the tree. Both the existing node and the new sibling become children of the operator. Exactly one of leftNodeId / rightNodeId must be provided — it identifies the existing node and which child slot it occupies.

As of v1.0 P-1 (non-not operator under operator) is not enforced at mutation time — the AN-1 post-hook in assistive behavior inserts the formula buffer; in permissive behavior the un-buffered state stays and surfaces via engine.validate('presentable').

Wrap an existing expression in a freshly-minted formula node atomically. The formula takes the child's original parent slot (parentId + position); the child becomes the formula's sole child at position 0. Bundled-composite mutation per spec §8.

Used by the native AN-1 (formula-buffer insertion) pass in src/lib/grammar/an-rules.ts. Composing this from addExpression + reparentExpression is not possible: the intermediate state would either (a) violate S-9 with the child still occupying the formula's target slot, or (b) trip the parent's assertChildLimit (unary not, binary implies/iff) even though the net child count of the parent is unchanged after the wrap.

The new formula's id is minted via the engine's idGenerator accessor and returned in the mutation result. Argument fields (argumentId, argumentVersion, premiseId) are inherited from the source child.

Creates a new PremiseEngine from a previously captured snapshot.