/** Factory for creating integer constants and values. */
export interface IntSortFactory {
    const(name: string): any;
    val(n: number): any;
    sort(): any;
}
/** Factory for creating boolean constants and values. */
export interface BoolSortFactory {
    const(name: string): any;
    val(v: boolean): any;
}
/** Factory for creating real constants and values. */
export interface RealSortFactory {
    const(name: string): any;
    val(n: number): any;
}
/** SMT solver instance. */
export interface SmtSolver {
    /** Set solver option (e.g., timeout). */
    set(key: string, value: number): void;
    /** Add a constraint. */
    add(expr: any): void;
    /** Check satisfiability. */
    check(): Promise<"sat" | "unsat" | "unknown">;
    /** Synchronous check — only available on the built-in solver. */
    checkSync?(): "sat" | "unsat" | "unknown";
    /** Get model (only valid after check() returns "sat"). */
    model(): SmtModel;
}
/** Model from a satisfying assignment. */
export interface SmtModel {
    /** Evaluate an expression in the model. */
    eval(expr: any, completion: boolean): any;
}
/**
 * Abstract SMT solver context.
 *
 * Provides factories for creating expressions and solvers.
 * Both the Z3 adapter and the built-in QF-LIA solver implement this.
 *
 * Optional members (ForAll, Exists, Array, Function) are only implemented
 * by the Z3 adapter for semantic assertion support. The built-in solver
 * omits them — translate-semantic.ts checks for their presence.
 */
export interface SolverContext {
    readonly Int: IntSortFactory;
    readonly Bool: BoolSortFactory;
    readonly Real: RealSortFactory;
    And(...args: any[]): any;
    Or(...args: any[]): any;
    Not(expr: any): any;
    Implies(a: any, b: any): any;
    If(cond: any, thenExpr: any, elseExpr: any): any;
    Solver: {
        new (): SmtSolver;
    };
    /** Quantifier: ∀ vars. body (Z3 only). */
    ForAll?(vars: any[], body: any): any;
    /** Quantifier: ∃ vars. body (Z3 only). */
    Exists?(vars: any[], body: any): any;
    /** Array sort factory (Z3 only). */
    readonly Array?: {
        const(name: string, keySort: any, valueSort: any): any;
    };
    /** Uninterpreted function factory (Z3 only). */
    readonly Function?: {
        declare(name: string, ...sorts: any[]): any;
    };
}
//# sourceMappingURL=solver-context.d.ts.map