import { type TCorePropositionalExpression, type TCorePropositionalVariable } from "../../schemata/index.js";
import { type TCoreArgumentEvaluationOptions, type TCoreArgumentEvaluationResult, type TCoreExpressionAssignment, type TCoreQuadrivalentValue, type TCoreResolvedAssignment, type TCoreResolvedVariableValues, type TCoreValidityCheckOptions, type TCoreValidityCheckResult, type TCorePremiseEvaluationResult, type TCoreValidationResult } from "../../types/evaluation.js";
import { closeUnderAcceptedOperators, propagateOperatorConstraints } from "./propagation.js";
export { closeUnderAcceptedOperators, propagateOperatorConstraints };
/**
 * 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;
    /**
     * Whether the argument is a response. A response has no conclusion and is
     * not evaluated against one, so evaluation and the validity check refuse
     * it with `ARGUMENT_IS_RESPONSE`. Absent means a standard argument.
     */
    isResponse?: boolean;
    /** 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;
/**
 * 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