import { type TCorePropositionalExpression, type TCorePropositionalVariable } from "../../schemata/index.js";
import { type TCoreArgumentEvaluationOptions, type TCoreArgumentEvaluationResult, type TCoreExpressionAssignment, type TCorePropagationOptions, type TCoreQuadrivalentValue, type TCoreResolvedAssignment, type TCoreResolvedVariableValues, type TCoreValidityCheckOptions, type TCoreValidityCheckResult, type TCoreVariableProvenance, type TCorePremiseEvaluationResult, type TCoreValidationResult } from "../../types/evaluation.js";
/**
 * Read-only interface providing the data an evaluation needs from an
 * argument engine. This is intentionally narrow — evaluation should
 * not mutate anything.
 */
export interface TArgumentEvaluationContext {
    /** The argument's own ID. */
    argumentId: string;
    /** Returns the conclusion PremiseEngine, or undefined. */
    getConclusionPremise(): TEvaluablePremise | undefined;
    /** Returns supporting premises (inference premises minus conclusion). */
    listSupportingPremises(): TEvaluablePremise[];
    /** Returns all premises. */
    listPremises(): TEvaluablePremise[];
    /** The conclusion premise ID, if set. */
    conclusionPremiseId: string | undefined;
    /** Look up a variable by ID. */
    getVariable(variableId: string): TCorePropositionalVariable | undefined;
    /** Look up a premise by ID. */
    getPremise(premiseId: string): TEvaluablePremise | undefined;
    /** Pre-evaluation structural validation. */
    validateEvaluability(): TCoreValidationResult;
}
/**
 * Narrow view of a PremiseEngine needed for evaluation.
 */
export interface TEvaluablePremise {
    getId(): string;
    /**
     * The premise entity's `type`. Derivation premises are engine wiring
     * rather than a user-authored inferential step, so a rejection recorded
     * inside one never strikes it. Optional: an implementation that omits it
     * is treated as a freeform premise.
     */
    getPremiseType?(): string;
    getExpressions(): TCorePropositionalExpression[];
    getChildExpressions(parentId: string): TCorePropositionalExpression[];
    getVariables(): TCorePropositionalVariable[];
    /**
     * Evaluate this premise under an assignment.
     *
     * **The result must depend only on the variables this premise reaches** —
     * those named by `getExpressions()`, plus, transitively, those reached by
     * the premise behind any internally premise-bound variable among them.
     * Reading a variable outside that set is outside the contract even though
     * the whole assignment is in scope, and the type cannot express the
     * restriction.
     *
     * It is load-bearing rather than tidy: the satisfiability search splits the
     * premises into groups that share no reachable variable and walks each over
     * its own columns alone. A premise that consults a variable it does not
     * reach is walked without that variable varying, so it can report
     * satisfiable for a set that is not — which suppresses, or fails to
     * suppress, derivation across the whole argument.
     */
    evaluate(assignment: TCoreResolvedAssignment, options?: {
        strictUnknownKeys?: boolean;
        resolver?: (variableId: string) => TCoreQuadrivalentValue;
    }): TCorePremiseEvaluationResult;
    /**
     * Returns the operator expressions a reviewer can accept or reject,
     * in pre-order tree order. Excludes `"not"` operators and skips
     * formula nodes. See `TExpressionQueries.getDecidableOperatorExpressions`
     * on the full `PremiseEngine` for the authoritative contract.
     */
    getDecidableOperatorExpressions(): TCorePropositionalExpression[];
}
/**
 * Evaluate an expression subtree under a fixed variable assignment, using the
 * four-valued Belnap connectives.
 *
 * Total and side-effect free: unknown/missing variables and empty operators
 * yield `null`, and `formula` wrappers pass through to their single child.
 * Unlike `PremiseEngine.evaluate`, it never throws on a non-evaluable tree —
 * so callers deriving display-time defaults can evaluate a subtree of an
 * argument that is not yet fully evaluable.
 *
 * The operator base cases (`and` seeds `true`, `or` seeds `false`) match
 * `propagateOperatorConstraints`' internal resolver so the two agree.
 */
export declare function evaluateSubtree(rootExpressionId: string, getExpression: (id: string) => TCorePropositionalExpression | undefined, getChildren: (parentId: string) => TCorePropositionalExpression[], variables: TCoreResolvedVariableValues): TCoreQuadrivalentValue;
/**
 * 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>;
};
/**
 * Evaluates an argument under a three-valued expression assignment.
 */
export declare function evaluateArgument(ctx: TArgumentEvaluationContext, assignment: TCoreExpressionAssignment, options?: TCoreArgumentEvaluationOptions): TCoreArgumentEvaluationResult;
/**
 * Enumerates all 2^n variable assignments and checks for counterexamples.
 *
 * The optional `options.excludedVariableIds` set removes the listed IDs from
 * the enumeration — typically axiomatic-bound variables that the engine
 * forces to `true`. The optional `options.forcedTrueVariableIds` set fixes
 * the listed IDs to `true` in every generated assignment. Callers normally
 * pass the same set for both.
 */
export declare function checkArgumentValidity(ctx: TArgumentEvaluationContext, options?: TCoreValidityCheckOptions): TCoreValidityCheckResult;
//# sourceMappingURL=argument-evaluation.d.ts.map