import { type TCoreExpressionAssignment, type TCorePropagationOptions, type TCoreResolvedVariableValues, type TCoreVariableProvenance } from "../../types/evaluation.js";
import type { TArgumentEvaluationContext } from "./argument-evaluation.js";
/**
 * Run constraint propagation to a fixed point over the operators the reader
 * accepted, filling in variable values the granted steps force.
 *
 * Only acceptances propagate. A rejection is not a truth value: it strikes the
 * premise it lives in, and the caller excludes that premise here via
 * `options.excludedPremiseIds` — so nothing inside a struck premise
 * contributes, and no value is ever forced `false` by a refusal.
 *
 * Each step **merges** what it forces into the variable's current value rather
 * than overwriting it or declining to write, so two steps that force opposite
 * values leave the variable `CONTESTED` instead of letting whichever step ran
 * first decide. That merge is the join of the knowledge order, every rule's
 * trigger is monotone in that same order, and the state space is finite — so
 * the sweep converges to the least fixed point above the reader's assignment
 * and reaches it whatever order premises, expressions and rules are visited
 * in.
 *
 * Each rule moves **one truth component in one direction**, and that is not
 * decoration: an accepted `A → B` fires forward on `A` being told true and
 * merges told-true into `B`, and backward on `B` being told false merging
 * told-false into `A`. Transferring both components at once would read the
 * conditional as a biconditional and derive `B` false from `A` false. The
 * one-directional pairing is what a material implication licenses; only `iff`
 * carries both components both ways.
 *
 * Because only the told-true component travels forward, a contested variable
 * can produce an uncontested `true` downstream and leave every aggregate fact
 * reading clean. `evaluateArgument` reports `contestedVariableIds` so a
 * conflict is never inferred from the aggregates. Attribution's counterfactual depends on that: withholding an assertion
 * and re-closing must give one answer, and must not let mutually supporting
 * premises certify each other.
 *
 * A reader's own assertion takes part in the merge like any other source. If
 * the reader asserts a value that a granted step contradicts, the result is
 * `CONTESTED` — the conflict is reported, not silently resolved in either
 * direction.
 *
 * Axiomatic-bound variables are forced to `true` by `ArgumentEngine`'s
 * pre-pass before this function runs, and are merged on the same footing.
 */
export declare function propagateOperatorConstraints(ctx: TArgumentEvaluationContext, assignment: TCoreExpressionAssignment, options?: TCorePropagationOptions): TCoreResolvedVariableValues;
/**
 * `propagateOperatorConstraints` plus the provenance of every value it saw or
 * produced. The two share one closure, so a tag is recorded where the value is
 * actually set rather than reconstructed afterwards.
 */
export declare function closeUnderAcceptedOperators(ctx: TArgumentEvaluationContext, assignment: TCoreExpressionAssignment, options?: TCorePropagationOptions): {
    variables: TCoreResolvedVariableValues;
    provenance: Record<string, TCoreVariableProvenance>;
};
//# sourceMappingURL=propagation.d.ts.map