import type { Z3_lbool } from '../types.js';
import type { CallbackRegistry } from '../callback-registry.js';
import type { CallbackErrorChannel } from '../user-propagator.js';
import type { EmscriptenModule, UnsafeZ3Api } from '../types.js';
import { SolveContext } from './context.js';
import type { Z3Low } from './types.js';
export type SolveStatus = 'sat' | 'unsat' | 'unknown';
export interface SolveResult {
    status: SolveStatus;
    sat: boolean;
    unsat: boolean;
    unknown: boolean;
    model: Map<string, boolean | number | string>;
    unsatCore: string[];
    rawResult: Z3_lbool;
}
export type SolveBuilder = (ctx: SolveContext) => void;
export declare function createSolveFunction(em: EmscriptenModule, Z3: Z3Low, UnsafeZ3: UnsafeZ3Api, registry: CallbackRegistry, errorChannel: CallbackErrorChannel): (builder: SolveBuilder) => SolveResult;
//# sourceMappingURL=solve.d.ts.map