import { type TCorePropositionalExpression, type TCorePropositionalVariable } from "../../schemata/index.js";
import type { TCorePremiseEvaluationResult, TCoreQuadrivalentValue, TCoreResolvedAssignment } from "../../types/evaluation.js";
import type { TColumnReference } from "../../types/response.js";
import type { TArgumentEngineSnapshot } from "../argument-engine.js";
import type { TEvaluablePremise } from "../evaluation/argument-evaluation.js";
/**
 * A formula of the combined premise set: a column, or an operator over
 * formulas. Formula (parenthesis) nodes are dropped when copying, since they
 * change nothing a formula means.
 */
export type TCombinedNode = {
    kind: "column";
    key: string;
} | {
    kind: "op";
    operator: string;
    kids: TCombinedNode[];
};
/** One premise of the response as it enters the combined set. */
export interface TCombinedSourcePremise {
    id: string;
    expressions: readonly TCorePropositionalExpression[];
}
export interface TCombinedSetInput {
    responseArgumentId: string;
    responseArgumentVersion: number;
    /** The response's premises, leaving out unpopulated derivation stubs. */
    premises: readonly TCombinedSourcePremise[];
    getVariable: (id: string) => TCorePropositionalVariable | undefined;
    /** The response's own citation- and axiom-bound variables. */
    groundedVariableIds: ReadonlySet<string>;
    /** The argument the response answers, at the version it answers. */
    target: TArgumentEngineSnapshot;
}
/** A link of the response, read in terms of the combined set. */
export interface TCombinedLink {
    premiseId: string;
    negated: boolean;
    /** What the link says is true or false, expanded into the target. */
    referent: TCombinedNode;
    /** Equal for two links exactly when their referents are the same formula. */
    referentKey: string;
}
/**
 * The in-memory premise set every check of a response searches. It is built
 * for one check and never stored.
 *
 * Every premise reads only columns of this set: a statement binding is
 * replaced by a copy of the target expression it names, and a binding between
 * premises is replaced by a copy of the bound premise's formula. So nothing in
 * it reaches into another argument, and grouping by shared columns is exact.
 */
export interface TCombinedSet {
    premises: CombinedPremise[];
    links: TCombinedLink[];
    columns: Map<string, TColumnReference>;
    /** Columns from the response's own grounded variables, held true. */
    forcedTrueColumns: Set<string>;
}
/** The canonical text of a formula; equal texts mean equal formulas. */
export declare function formulaKey(node: TCombinedNode): string;
/**
 * Expands expressions of the argument a response answers into formulas over
 * columns, the way every check reads them. Every column it creates is
 * recorded in `columns`, shared by all expansions it makes.
 *
 * It records nothing about the response: a column one of the response's own
 * grounded variables also names is a plain column here, free to take either
 * value.
 */
export interface TTargetExpander {
    /** The formula an expression of the target stands for. */
    expand: (expressionId: string) => TCombinedNode;
    columns: Map<string, TColumnReference>;
    claimColumn: (claimId: string) => TCombinedNode;
    premiseColumn: (argumentId: string, argumentVersion: number, premiseId: string) => TCombinedNode;
    expressionColumn: (argumentId: string, expressionId: string, aspect: "statement" | "inference") => TCombinedNode;
}
export declare function createTargetExpander(target: TArgumentEngineSnapshot): TTargetExpander;
export declare function buildCombinedSet(input: TCombinedSetInput): TCombinedSet;
/** Evaluates a formula of the combined set with the library's own operator rules. */
export declare function evaluateCombinedNode(node: TCombinedNode, read: (key: string) => TCoreQuadrivalentValue): TCoreQuadrivalentValue;
/**
 * A premise of the combined set, in the shape the satisfiability search
 * reads. Its expressions are generated from its formula; only their types and
 * column ids are meaningful, so that the search can group premises by the
 * columns they share.
 */
export declare class CombinedPremise implements TEvaluablePremise {
    private readonly id;
    readonly tree: TCombinedNode;
    private readonly expressions;
    constructor(id: string, tree: TCombinedNode);
    getId(): string;
    getExpressions(): TCorePropositionalExpression[];
    getChildExpressions(parentId: string): TCorePropositionalExpression[];
    getVariables(): TCorePropositionalVariable[];
    getDecidableOperatorExpressions(): TCorePropositionalExpression[];
    evaluate(assignment: TCoreResolvedAssignment, options?: {
        resolver?: (variableId: string) => TCoreQuadrivalentValue;
    }): TCorePremiseEvaluationResult;
}
//# sourceMappingURL=combined-premise-set.d.ts.map