import { type Context } from "z3-solver";
import type { SolverContext } from "./solver-context.js";
type Z3Context = Context<"main">;
/**
 * Get or initialize the Z3 context (lazy singleton).
 * Z3 WASM initialization is expensive (~1s), so we cache the context.
 *
 * The returned Context has the high-level API: Int, Bool, Real, Solver,
 * and operations like Not, And, Or, Implies.
 */
export declare function getZ3(): Promise<Z3Context>;
/**
 * Get a solver context — the abstract interface for SMT solving.
 *
 * @param options.useZ3 - Use Z3 solver (default: false — uses built-in QF-LIA solver)
 * @returns SolverContext instance
 */
export declare function getSolver(options?: {
    useZ3?: boolean;
}): Promise<SolverContext>;
/** Reset the Z3 context (used by tests). */
export declare function resetZ3(): void;
export {};
//# sourceMappingURL=z3-context.d.ts.map