import type { Z3_context, Z3_solver, Z3_ast, EmscriptenModule } from '../types.js';
import { BoolExpr, IntExpr, RealExpr, ArithExpr, Expr, type Z3Low } from './types.js';
export interface PropagatorCallback {
    conflict(fixed: Expr[]): void;
    propagate(consequent: BoolExpr, fixed: Expr[], eqs?: [Expr, Expr][]): void;
}
export interface PropagatorConfig {
    variables: Expr[];
    onFixed?(cb: PropagatorCallback, term: Z3_ast, value: Z3_ast): void;
    onEq?(cb: PropagatorCallback, lhs: Z3_ast, rhs: Z3_ast): void;
    onDiseq?(cb: PropagatorCallback, lhs: Z3_ast, rhs: Z3_ast): void;
    onFinal?(cb: PropagatorCallback): boolean | void;
    onDecide?(cb: PropagatorCallback, term: Z3_ast, idx: number, phase: boolean): void;
    onCreated?(cb: PropagatorCallback, term: Z3_ast): void;
}
export declare class SolveContext {
    private readonly em;
    readonly ctx: Z3_context;
    readonly solver: Z3_solver;
    readonly Z3: Z3Low;
    private readonly vars;
    private readonly tracked;
    private readonly enumSorts;
    private propagatorConfig;
    private _objectives;
    constructor(Z3: Z3Low, em: EmscriptenModule);
    Bool(name: string): BoolExpr;
    Int(name: string): IntExpr;
    Real(name: string): RealExpr;
    Enum(sortName: string, values: readonly string[]): {
        val: (v: string) => IntExpr;
        var: (name: string) => IntExpr;
        values: readonly string[];
    };
    IntVal(n: number): IntExpr;
    RealVal(num: number, den?: number): RealExpr;
    BoolVal(v: boolean): BoolExpr;
    EnumVal(sortName: string, value: string): IntExpr;
    assert(...exprs: BoolExpr[]): void;
    track(name: string, expr: BoolExpr): void;
    distinct(...exprs: Expr[]): BoolExpr;
    ite<T extends Expr>(cond: BoolExpr, then_: T, else_: T): T;
    push(): void;
    pop(n?: number): void;
    check(): 'sat' | 'unsat' | 'unknown';
    setTimeout(ms: number): void;
    minimize(expr: ArithExpr): void;
    maximize(expr: ArithExpr): void;
    propagate(config: PropagatorConfig): void;
    debug(expr: Expr): string;
    /** @internal */ getPropagatorConfig(): PropagatorConfig | null;
    /** @internal */ getVars(): Map<string, {
        expr: Expr;
        ast: Z3_ast;
        sort: "bool" | "int" | "real" | "enum";
    }>;
    /** @internal */ hasTracked(): boolean;
    /** @internal */ getObjectives(): {
        kind: "min" | "max";
        expr: ArithExpr;
    }[];
    /** @internal */ getEnumSorts(): Map<string, {
        values: string[];
    }>;
    /** @internal */ destroy(): void;
}
//# sourceMappingURL=context.d.ts.map