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) are enforced.
When the wrapInsertFormula flag is enabled (either directly via
TAutoNormalizeConfig or via autoNormalize: true), operator nesting
violations are auto-corrected by inserting a formula buffer between
the parent operator and the non-not operator child, rather than
throwing. The same flag also controls auto-insertion in
insertExpression and wrapExpression.
The expression to add, including position and parent assignment.
The added expression (with checksum) and changeset.
Adds an expression immediately before or after an existing sibling, with position computed automatically.
When the repositionOnCollision auto-normalize flag is enabled,
sibling positions are automatically redistributed if 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.
The ID of the existing sibling expression.
Whether to insert "before" or "after"
the sibling.
The expression to add (position is auto-assigned).
The added expression (with checksum) and changeset.
Adds an expression as the last child of the given parent, with
position computed automatically. If parentId is null, the
expression becomes the root.
When the repositionOnCollision auto-normalize flag is enabled,
sibling positions are automatically redistributed if the computed
position would collide with an existing sibling. Repositioned
siblings appear in changes.expressions.modified.
The parent expression ID, or null for root.
The expression to add (position is auto-assigned).
The added expression (with checksum) and changeset.
Changes the operator type of an existing operator expression.
Handles three structural cases automatically:
newOperator. Dissolves the current operator and
reparents its children under the parent.sourceChildId and
targetChildId into a new sub-operator of type newOperator,
inserting a formula buffer if required by grammar enforcement.The operator expression to change.
The target operator type.
OptionalsourceChildId: stringFirst child to include in a split (required when >2 children).
OptionaltargetChildId: stringSecond child to include in a split (required when >2 children).
OptionalextraFields: Partial<TExpr>Optional partial expression fields merged into any newly created expressions (formula buffer, new sub-operator). Structural fields (id, type, operator, parentId, position, premiseId, argumentId, argumentVersion) cannot be overridden.
result — For simple change: the updated operator expression. For merge: null (operator was dissolved). For split: the newly created sub-operator expression. changes — Full changeset with correct hierarchical checksums.
Splices a new expression between existing nodes in the tree. The new
expression inherits the tree slot of the anchor node
(leftNodeId ?? rightNodeId).
The expression to insert, including position and parent assignment.
OptionalleftNodeId: stringThe existing node to become the left child of the new expression.
OptionalrightNodeId: stringThe existing node to become the right child of the new expression.
The inserted expression (with checksum) and changeset.
Performs a full normalization sweep on this premise's expression tree.
Collapses unjustified formulas, operators with 0/1 children, and inserts
formula buffers where needed. Works regardless of autoNormalize setting.
Removes an expression and optionally its entire descendant subtree, then collapses any ancestor operators with fewer than two children.
The ID of the expression to remove.
Whether to remove all descendants as well.
The removed root expression, or undefined if not found.
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.
When the target is already a NOT expression and collapseDoubleNegation
is enabled, removes the existing NOT (promoting its child) instead of
wrapping in another NOT — preventing NOT(NOT(x)).
When the target is a non-not operator and negationInsertFormula is
enabled, auto-inserts a formula buffer between the new NOT and the
target to satisfy the operator nesting restriction. Throws if the flag
is disabled and enforceFormulaBetweenOperators is true.
The ID of the expression to toggle negation on.
OptionalextraFields: Partial<TExpr>Optional additional fields to merge into newly created expressions (NOT and formula nodes). Structural fields (id, type, operator, parentId, position, premiseId, argumentId, argumentVersion) cannot be overridden.
The new NOT expression when adding negation, or null when
removing it, along with the changeset.
Updates mutable fields of an existing expression. Only position,
variableId, and operator may be updated.
The ID of the expression to update.
The fields to update.
The updated expression and changeset.
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.
The new operator expression to wrap with.
The new sibling expression to add alongside the existing node.
OptionalleftNodeId: stringThe existing node to place as the left child.
OptionalrightNodeId: stringThe existing node to place as the right child.
The inserted operator (with checksum) and changeset.
Single-premise expression tree mutations.