import type { ArgumentEngine } from "../core/argument-engine.js";
import type { TCoreArgument, TCorePremise, TCorePropositionalExpression, TCorePropositionalVariable, TCoreClaim } from "../schemata/index.js";
/**
 * Run AN-2 (collapse double negation) on every premise of `engine`.
 * Returns `true` iff any mutation occurred.
 *
 * Walks each premise's expression tree looking for NOT(NOT(x)) —
 * both the direct form (`NOT_outer → NOT_inner → x`) and the
 * buffered form (`NOT_outer → formula → NOT_inner → x`). For each
 * match issues two `pe.removeExpression(id, false)` calls that
 * promote the grandchild (and, in the buffered case, the residual
 * formula) through the two NOT layers.
 *
 * The buffered case leaves an unjustified `formula(x)` residue
 * which AN-3 cleans up in a subsequent iteration of
 * `applyANToFixedPoint`. AN-2 stays focused on the NOT-NOT
 * collapse itself — no formula bookkeeping.
 *
 * @since 1.0.0
 */
export declare function applyAN2<TArg extends TCoreArgument = TCoreArgument, TPremise extends TCorePremise = TCorePremise, TExpr extends TCorePropositionalExpression = TCorePropositionalExpression, TVar extends TCorePropositionalVariable = TCorePropositionalVariable, TClaim extends TCoreClaim = TCoreClaim>(engine: ArgumentEngine<TArg, TPremise, TExpr, TVar, TClaim>): boolean;
/**
 * Run AN-3 (collapse 0/1-child operator/formula) on every premise of
 * `engine`. Returns `true` iff any mutation occurred.
 *
 * Walks each premise's expression tree and collapses four sub-cases
 * via `pe.removeExpression(id, false)`:
 *
 *   1. Operator with 0 children → removed (leaf removal).
 *   2. Operator with 1 child (non-`not`) → child promoted into the
 *      operator's slot. `not` is unary so 1-child `not` is its
 *      Presentable form and is NOT collapsed by AN-3.
 *   3. Formula with 0 children → removed.
 *   4. Formula with 1 child whose bounded subtree contains no variadic
 *      connective (`and`/`or`/`xor`) → child promoted (the formula is
 *      unjustified per P-3, so it disappears).
 *
 * Bounded-subtree traversal stops at nested formulas (each formula
 * is a separate P-3 scope). The shared
 * `hasBinaryOperatorInBoundedSubtree` helper in
 * `src/lib/grammar/bounded-subtree.ts` is used by both this rule and
 * the P-3 validator; AN-3 binds its lookup function to
 * `pe.getChildExpressions(id)` so it sees live mid-mutation reads,
 * while the validator binds to a snapshot `TChildMap`. Sharing the
 * one helper keeps the rule and its validator in lockstep.
 *
 * Behavior is asserted by the regression-guard tests in
 * `test/grammar/an-rules.test.ts`.
 *
 * @since 1.0.0
 */
export declare function applyAN3<TArg extends TCoreArgument = TCoreArgument, TPremise extends TCorePremise = TCorePremise, TExpr extends TCorePropositionalExpression = TCorePropositionalExpression, TVar extends TCorePropositionalVariable = TCorePropositionalVariable, TClaim extends TCoreClaim = TCoreClaim>(engine: ArgumentEngine<TArg, TPremise, TExpr, TVar, TClaim>): boolean;
/**
 * Run AN-4 (absorb same-operator through formula) on every premise of
 * `engine`. Returns `true` iff any mutation occurred.
 *
 * Walks each premise's expression tree for the absorption shape
 * `OUTER_OP → (..., ) formula → INNER_OP (same
 * operator) → [c1, c2, …, cN]`, with both operators being one of the
 * variadic connectives `and`, `or`, `xor` (S-5 restricts `implies`/`iff`
 * to roots, so they never appear in AN-4-firing positions; `not` is unary
 * and has nothing to absorb). For each match:
 *
 *   1. Compute target positions for the N inner children under the
 *      outer operator using the legacy spacing algorithm from
 *      `ExpressionManager.absorbSameOperator` (em.ts:1240-1349):
 *      `leftPos + ((rightPos - leftPos) / (count + 1)) * (i + 1)`,
 *      truncated to integers. `leftPos` and `rightPos` are the
 *      formula's outer neighbors (or `positionConfig.min`/`max` at
 *      boundaries).
 *   2. If `gap = rightPos - leftPos <= count` (tight neighborhood
 *      where N evenly-spaced positions would collide), fall back to a
 *      **full redistribution**: renumber every existing sibling of the
 *      formula evenly across `positionConfig.min..max`, then redo the
 *      spacing on the refreshed boundaries before reparenting.
 *   3. Reparent each inner child to the outer operator at its computed
 *      target position via `pe.reparentExpression`.
 *   4. Remove the now-empty inner operator via
 *      `pe.removeExpression(inner.id, true)` (deleteSubtree is fine —
 *      it has zero children).
 *   5. Remove the now-empty formula wrapper via
 *      `pe.removeExpression(formula.id, false)`. Hits the 0-child
 *      leaf-removal branch of `removeAndPromote` so the inline P-1
 *      enforcement throw is not reached.
 *
 * Identity preservation: each absorbed child's expression id survives
 * the operation — `reparentExpression` mutates the position/parentId
 * fields atomically without minting new ids. Asserted by the contract
 * regression-guard tests in `test/grammar/an-rules.test.ts:559-893`.
 *
 * @since 1.0.0
 */
export declare function applyAN4<TArg extends TCoreArgument = TCoreArgument, TPremise extends TCorePremise = TCorePremise, TExpr extends TCorePropositionalExpression = TCorePropositionalExpression, TVar extends TCorePropositionalVariable = TCorePropositionalVariable, TClaim extends TCoreClaim = TCoreClaim>(engine: ArgumentEngine<TArg, TPremise, TExpr, TVar, TClaim>): boolean;
/**
 * Run AN-1 (insert formula buffer between operators) on every premise
 * of `engine`. Returns `true` iff any mutation occurred.
 *
 * Walks each premise's expression tree looking for non-`not`
 * operators whose parent is also an operator — i.e., the P-1
 * violation shape `parent-op → child-op (non-not)`. For
 * each match, calls `pe.wrapInFormula(childOpId, formulaId)` which
 * atomically inserts a freshly-minted `formula` between parent and
 * child. The formula takes the child's original slot; the child
 * becomes the formula's sole child at position 0. Per spec §5.1 the
 * result preserves P-1.
 *
 * Why a dedicated `wrapInFormula` primitive rather than composing
 * `addExpression(formula)` + `reparentExpression(child)`:
 *
 *   - `addExpression(formula, parent, childPosition)` would throw S-9
 *     because the child still occupies that slot.
 *   - For unary `not` parents and binary `implies`/`iff` parents,
 *     `assertChildLimit` would reject the formula even transiently —
 *     even though the *net* child count of the parent is unchanged
 *     after the wrap (the formula displaces the child).
 *
 * `pe.wrapInFormula` sidesteps both by performing the insertion +
 * reparent as one bundled-composite mutation per spec §8 (see the PE
 * method's JSDoc for the atomicity contract).
 *
 * The new formula's id is minted via `engine.idGenerator` so id
 * provenance stays at the engine boundary (matches the
 * `populateFromGrounding` factory pattern in `populate-from.ts`).
 *
 * @since 1.0.0
 */
export declare function applyAN1<TArg extends TCoreArgument = TCoreArgument, TPremise extends TCorePremise = TCorePremise, TExpr extends TCorePropositionalExpression = TCorePropositionalExpression, TVar extends TCorePropositionalVariable = TCorePropositionalVariable, TClaim extends TCoreClaim = TCoreClaim>(engine: ArgumentEngine<TArg, TPremise, TExpr, TVar, TClaim>): boolean;
/**
 * Run AN-1..AN-4 to fixed point on every premise of `engine`.
 *
 * All four rules are native. The driver issues single-rule passes in
 * order — AN-2, AN-3, AN-4, AN-1 — so buffer insertion sees the
 * post-collapse tree (avoids inserting a buffer that would then need
 * to be collapsed by AN-3).
 *
 * The driver uses a reduce-or accumulator rather than a `||`
 * short-circuit chain: every outer iteration fires all four rules
 * and records whether ANY produced a mutation. This reduces outer
 * iterations by ~4x in the worst case versus the short-circuit
 * pattern, and pulls the iteration count back well within
 * MAX_AN_ITERATIONS for borderline inputs.
 *
 * Convergence cap: `MAX_AN_ITERATIONS = 10`. Typical convergence is ≤ 3
 * iterations (spec §5.1); the cap protects against pathological inputs
 * (e.g. malformed Structural state that would otherwise oscillate).
 *
 * @since 1.0.0
 */
export declare function applyANToFixedPoint<TArg extends TCoreArgument = TCoreArgument, TPremise extends TCorePremise = TCorePremise, TExpr extends TCorePropositionalExpression = TCorePropositionalExpression, TVar extends TCorePropositionalVariable = TCorePropositionalVariable, TClaim extends TCoreClaim = TCoreClaim>(engine: ArgumentEngine<TArg, TPremise, TExpr, TVar, TClaim>): void;
//# sourceMappingURL=an-rules.d.ts.map