import type { EmscriptenModule, Z3_context, Z3_solver, Z3_solver_callback, Z3_ast, Z3_sort, Z3_symbol, Z3_model, Z3_optimize, Z3_lbool } from './types.js';
type Z3_ast_vector = number;
type Z3_params = number;
type Z3_stats = number;
/**
 * Z3 C API surface via ccall — every function the Possibility Engine needs.
 *
 * Array-taking functions (mk_and, mk_or, mk_add, …) marshal JS
 * number arrays to the WASM heap automatically.
 */
export interface Z3Api {
    mk_config(): number;
    del_config(cfg: number): void;
    mk_context(cfg: number): Z3_context;
    mk_context_rc(cfg: number): Z3_context;
    del_context(ctx: Z3_context): void;
    inc_ref(ctx: Z3_context, ast: Z3_ast): void;
    dec_ref(ctx: Z3_context, ast: Z3_ast): void;
    mk_bool_sort(ctx: Z3_context): Z3_sort;
    mk_int_sort(ctx: Z3_context): Z3_sort;
    mk_real_sort(ctx: Z3_context): Z3_sort;
    mk_bv_sort(ctx: Z3_context, sz: number): Z3_sort;
    mk_enumeration_sort(ctx: Z3_context, name: Z3_symbol, n: number, enumNames: number, enumConsts: number, enumTesters: number): Z3_sort;
    mk_finite_domain_sort(ctx: Z3_context, name: Z3_symbol, size: number): Z3_sort;
    mk_string_symbol(ctx: Z3_context, s: string): Z3_symbol;
    mk_int_symbol(ctx: Z3_context, i: number): Z3_symbol;
    mk_const(ctx: Z3_context, sym: Z3_symbol, sort: Z3_sort): Z3_ast;
    mk_true(ctx: Z3_context): Z3_ast;
    mk_false(ctx: Z3_context): Z3_ast;
    mk_int(ctx: Z3_context, n: number, sort: Z3_sort): Z3_ast;
    mk_int64(ctx: Z3_context, n: number, sort: Z3_sort): Z3_ast;
    mk_real(ctx: Z3_context, num: number, den: number): Z3_ast;
    mk_numeral(ctx: Z3_context, numStr: string, sort: Z3_sort): Z3_ast;
    mk_string(ctx: Z3_context, s: string): Z3_ast;
    mk_not(ctx: Z3_context, a: Z3_ast): Z3_ast;
    mk_and(ctx: Z3_context, args: Z3_ast[]): Z3_ast;
    mk_or(ctx: Z3_context, args: Z3_ast[]): Z3_ast;
    mk_implies(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_iff(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_xor(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_eq(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_distinct(ctx: Z3_context, args: Z3_ast[]): Z3_ast;
    mk_ite(ctx: Z3_context, cond: Z3_ast, then_: Z3_ast, else_: Z3_ast): Z3_ast;
    mk_add(ctx: Z3_context, args: Z3_ast[]): Z3_ast;
    mk_sub(ctx: Z3_context, args: Z3_ast[]): Z3_ast;
    mk_mul(ctx: Z3_context, args: Z3_ast[]): Z3_ast;
    mk_div(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_mod(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_rem(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_power(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_unary_minus(ctx: Z3_context, a: Z3_ast): Z3_ast;
    mk_le(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_lt(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_ge(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_gt(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_bvadd(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_bvsub(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_bvand(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_bvor(ctx: Z3_context, a: Z3_ast, b: Z3_ast): Z3_ast;
    mk_solver(ctx: Z3_context): Z3_solver;
    mk_simple_solver(ctx: Z3_context): Z3_solver;
    solver_inc_ref(ctx: Z3_context, solver: Z3_solver): void;
    solver_dec_ref(ctx: Z3_context, solver: Z3_solver): void;
    solver_assert(ctx: Z3_context, solver: Z3_solver, ast: Z3_ast): void;
    solver_assert_and_track(ctx: Z3_context, solver: Z3_solver, ast: Z3_ast, track: Z3_ast): void;
    solver_push(ctx: Z3_context, solver: Z3_solver): void;
    solver_pop(ctx: Z3_context, solver: Z3_solver, n: number): void;
    solver_reset(ctx: Z3_context, solver: Z3_solver): void;
    solver_get_num_scopes(ctx: Z3_context, solver: Z3_solver): number;
    solver_set_initial_value(ctx: Z3_context, solver: Z3_solver, variable: Z3_ast, value: Z3_ast): void;
    solver_set_params(ctx: Z3_context, solver: Z3_solver, params: Z3_params): void;
    solver_get_model(ctx: Z3_context, solver: Z3_solver): Z3_model;
    solver_get_unsat_core(ctx: Z3_context, solver: Z3_solver): Z3_ast_vector;
    solver_get_assertions(ctx: Z3_context, solver: Z3_solver): Z3_ast_vector;
    solver_get_statistics(ctx: Z3_context, solver: Z3_solver): Z3_stats;
    solver_to_string(ctx: Z3_context, solver: Z3_solver): string;
    solver_propagate_register(ctx: Z3_context, solver: Z3_solver, e: Z3_ast): void;
    solver_propagate_consequence(ctx: Z3_context, cb: Z3_solver_callback, fixed: Z3_ast[], eqLhs: Z3_ast[], eqRhs: Z3_ast[], consequent: Z3_ast): void;
    ast_vector_size(ctx: Z3_context, vec: Z3_ast_vector): number;
    ast_vector_get(ctx: Z3_context, vec: Z3_ast_vector, i: number): Z3_ast;
    ast_to_string(ctx: Z3_context, ast: Z3_ast): string;
    get_sort(ctx: Z3_context, ast: Z3_ast): Z3_sort;
    get_sort_kind(ctx: Z3_context, sort: Z3_sort): number;
    sort_to_string(ctx: Z3_context, sort: Z3_sort): string;
    get_ast_kind(ctx: Z3_context, ast: Z3_ast): number;
    is_eq_ast(ctx: Z3_context, a: Z3_ast, b: Z3_ast): boolean;
    mk_params(ctx: Z3_context): Z3_params;
    params_set_uint(ctx: Z3_context, p: Z3_params, k: Z3_symbol, v: number): void;
    params_set_bool(ctx: Z3_context, p: Z3_params, k: Z3_symbol, v: boolean): void;
    params_set_symbol(ctx: Z3_context, p: Z3_params, k: Z3_symbol, v: Z3_symbol): void;
    params_to_string(ctx: Z3_context, p: Z3_params): string;
    params_dec_ref(ctx: Z3_context, p: Z3_params): void;
    model_eval(ctx: Z3_context, model: Z3_model, t: Z3_ast, completion: boolean): Z3_ast | null;
    model_to_string(ctx: Z3_context, model: Z3_model): string;
    model_inc_ref(ctx: Z3_context, model: Z3_model): void;
    model_dec_ref(ctx: Z3_context, model: Z3_model): void;
    get_bool_value(ctx: Z3_context, ast: Z3_ast): number;
    get_numeral_string(ctx: Z3_context, ast: Z3_ast): string;
    mk_optimize(ctx: Z3_context): Z3_optimize;
    optimize_assert(ctx: Z3_context, opt: Z3_optimize, ast: Z3_ast): void;
    optimize_maximize(ctx: Z3_context, opt: Z3_optimize, ast: Z3_ast): number;
    optimize_minimize(ctx: Z3_context, opt: Z3_optimize, ast: Z3_ast): number;
    optimize_check(ctx: Z3_context, opt: Z3_optimize, numAssumptions: number, assumptions: number): Z3_lbool;
    optimize_get_model(ctx: Z3_context, opt: Z3_optimize): Z3_model;
    optimize_push(ctx: Z3_context, opt: Z3_optimize): void;
    optimize_pop(ctx: Z3_context, opt: Z3_optimize): void;
    mk_forall_const(ctx: Z3_context, weight: number, numBound: number, bound: number, numPatterns: number, patterns: number, body: Z3_ast): Z3_ast;
    mk_exists_const(ctx: Z3_context, weight: number, numBound: number, bound: number, numPatterns: number, patterns: number, body: Z3_ast): Z3_ast;
    get_error_code(ctx: Z3_context): number;
    get_error_msg(ctx: Z3_context, code: number): string;
}
export declare function createZ3Api(mod: EmscriptenModule): Z3Api;
export {};
//# sourceMappingURL=z3-api.d.ts.map