import type { Z3_ast, Z3_context } from '../types.js';
export type Z3Low = Record<string, any>;
export declare class Expr {
    readonly ctx: Z3_context;
    readonly Z3: Z3Low;
    readonly ast: Z3_ast;
    readonly name?: string | undefined;
    constructor(ctx: Z3_context, Z3: Z3Low, ast: Z3_ast, name?: string | undefined);
    eq(other: Expr): BoolExpr;
    neq(other: Expr): BoolExpr;
    toString(): string;
}
export declare class BoolExpr extends Expr {
    and(...others: BoolExpr[]): BoolExpr;
    or(...others: BoolExpr[]): BoolExpr;
    not(): BoolExpr;
    implies(other: BoolExpr): BoolExpr;
    iff(other: BoolExpr): BoolExpr;
    xor(other: BoolExpr): BoolExpr;
    ite<T extends Expr>(then_: T, else_: T): T;
}
export declare class ArithExpr extends Expr {
    add(...others: ArithExpr[]): ArithExpr;
    sub(...others: ArithExpr[]): ArithExpr;
    mul(...others: ArithExpr[]): ArithExpr;
    div(other: ArithExpr): ArithExpr;
    mod(other: ArithExpr): IntExpr;
    rem(other: ArithExpr): IntExpr;
    power(exp: ArithExpr): ArithExpr;
    neg(): ArithExpr;
    le(other: ArithExpr): BoolExpr;
    lt(other: ArithExpr): BoolExpr;
    ge(other: ArithExpr): BoolExpr;
    gt(other: ArithExpr): BoolExpr;
}
export declare class IntExpr extends ArithExpr {
}
export declare class RealExpr extends ArithExpr {
}
//# sourceMappingURL=types.d.ts.map