import type { EmscriptenModule, Z3_context, Z3_solver, Z3_ast, Z3_rcf_num, Z3_lbool, UnsafeZ3Api, UserPropagatorCallbacks, Disposer, RcfInterval } from './types.js';
import { CallbackRegistry } from './callback-registry.js';
import { type Z3Api } from './z3-api.js';
import { type ErrorMode } from './errors.js';
import { type SolveBuilder, type SolveResult } from './dsl/solve.js';
export interface UserPropagatorApi {
    attach<S>(ctx: Z3_context, solver: Z3_solver, initialState: S, callbacks: UserPropagatorCallbacks<S>): Disposer;
    register(ctx: Z3_context, solver: Z3_solver, expr: Z3_ast): void;
}
export interface InspectApi {
    getExactString(ctx: Z3_context, ast: Z3_ast): {
        str: string;
        length: number;
    };
    getFpaSign(ctx: Z3_context, ast: Z3_ast): {
        success: boolean;
        isNegative: boolean;
    };
    getRcfInterval(ctx: Z3_context, a: Z3_rcf_num): {
        result: number;
        interval: RcfInterval;
    };
}
export interface ErrorsApi {
    setMode(ctx: Z3_context, mode: ErrorMode): void;
    check(ctx: Z3_context): {
        code: number;
        message: string;
    } | null;
}
export interface Z3Full {
    em: EmscriptenModule;
    Z3: Z3Api;
    UnsafeZ3: UnsafeZ3Api;
    registry: CallbackRegistry;
    userPropagator: UserPropagatorApi;
    inspect: InspectApi;
    errors: ErrorsApi;
    solveSync(ctx: Z3_context, solver: Z3_solver): Z3_lbool;
    solve(builder: SolveBuilder): SolveResult;
    dispose(): void;
}
export declare function initZ3Full(): Promise<Z3Full>;
//# sourceMappingURL=init.d.ts.map