export type Sort = "Int" | "Bool" | "Real";
export interface SortDescriptor {
    name(): string;
}
export declare function makeSortDescriptor(sort: Sort): SortDescriptor;
export type Expr = IntConst | IntVar | BoolConst | BoolVar | RealConst | RealVar | BinOp | UnOp | CompOp | BoolBinOp | BoolNot | IteExpr | EqExpr | NeqExpr;
export interface IntConst {
    readonly tag: "int_const";
    readonly value: number;
}
export interface IntVar {
    readonly tag: "int_var";
    readonly name: string;
}
export interface BoolConst {
    readonly tag: "bool_const";
    readonly value: boolean;
}
export interface BoolVar {
    readonly tag: "bool_var";
    readonly name: string;
}
export interface RealConst {
    readonly tag: "real_const";
    readonly value: number;
}
export interface RealVar {
    readonly tag: "real_var";
    readonly name: string;
}
export type ArithOp = "add" | "sub" | "mul" | "div" | "mod" | "neg";
export interface BinOp {
    readonly tag: "binop";
    readonly op: "add" | "sub" | "mul" | "div" | "mod";
    readonly left: Expr;
    readonly right: Expr;
    readonly sort: Sort;
}
export interface UnOp {
    readonly tag: "unop";
    readonly op: "neg";
    readonly operand: Expr;
    readonly sort: Sort;
}
export type CmpOp = "lt" | "gt" | "le" | "ge";
export interface CompOp {
    readonly tag: "cmp";
    readonly op: CmpOp;
    readonly left: Expr;
    readonly right: Expr;
}
export interface EqExpr {
    readonly tag: "eq";
    readonly left: Expr;
    readonly right: Expr;
}
export interface NeqExpr {
    readonly tag: "neq";
    readonly left: Expr;
    readonly right: Expr;
}
export interface BoolBinOp {
    readonly tag: "bool_binop";
    readonly op: "and" | "or" | "implies";
    readonly args: Expr[];
}
export interface BoolNot {
    readonly tag: "bool_not";
    readonly operand: Expr;
}
export interface IteExpr {
    readonly tag: "ite";
    readonly cond: Expr;
    readonly thenExpr: Expr;
    readonly elseExpr: Expr;
}
/**
 * Wrap an internal Expr as a Z3-API-compatible expression object.
 * These objects have methods like .add(), .sub(), .eq(), etc.,
 * matching the Z3 Context API surface used by translate.ts.
 */
export declare function wrapExpr(e: Expr, sort: Sort): any;
/** Unwrap a fluent expression object back to the internal Expr. */
export declare function unwrap(e: any): Expr;
/** Collect all variable names and their sorts from an expression tree. */
export declare function collectVariables(e: Expr): Map<string, Sort>;
//# sourceMappingURL=types.d.ts.map