// THIS FILE IS AUTOMATICALLY GENERATED BY make-ts-wrapper.ts // DO NOT EDIT IT BY HAND import { Z3_error_handler, Z3_push_eh, Z3_pop_eh, Z3_fresh_eh, Z3_fixed_eh, Z3_eq_eh, Z3_final_eh, Z3_created_eh, Z3_decide_eh, Z3_on_binding_eh, Z3_on_clause_eh, Z3_symbol, Z3_config, Z3_context, Z3_sort, Z3_func_decl, Z3_ast, Z3_app, Z3_pattern, Z3_model, Z3_constructor, Z3_constructor_list, Z3_params, Z3_param_descrs, Z3_parser_context, Z3_goal, Z3_tactic, Z3_simplifier, Z3_probe, Z3_stats, Z3_solver, Z3_solver_callback, Z3_ast_vector, Z3_ast_map, Z3_apply_result, Z3_func_interp, Z3_func_entry, Z3_fixedpoint, Z3_optimize, Z3_rcf_num, Z3_lbool, Z3_symbol_kind, Z3_parameter_kind, Z3_sort_kind, Z3_ast_kind, Z3_decl_kind, Z3_param_kind, Z3_ast_print_mode, Z3_error_code, Z3_goal_prec, } from './types.__GENERATED__'; type Z3_char_ptr = string; type unsigned = number; type int = number; type uint64_t = bigint; type int64_t = bigint; type double = number; type float = number; export async function init(initModule: any) { let Mod = await initModule(); // this works for both signed and unsigned, because JS will wrap for you when constructing the Uint32Array function intArrayToByteArr(ints: number[]) { return new Uint8Array(new Uint32Array(ints).buffer); } function boolArrayToByteArr(bools: boolean[]) { return bools.map((b) => (b ? 1 : 0)); } function readUintArray(address: number, count: number) { return Array.from(new Uint32Array(Mod.HEAPU32.buffer, address, count)); } let outAddress = Mod._malloc(24); let outUintArray = new Uint32Array(Mod.HEAPU32.buffer, outAddress, 4); let getOutUint = (i: 0 | 1 | 2 | 3 | 4 | 5) => outUintArray[i]; let outIntArray = new Int32Array(Mod.HEAPU32.buffer, outAddress, 4); let getOutInt = (i: 0 | 1 | 2 | 3 | 4 | 5) => outIntArray[i]; let outUint64Array = new BigUint64Array(Mod.HEAPU32.buffer, outAddress, 2); let getOutUint64 = (i: 0 | 1 | 2) => outUint64Array[i]; let outInt64Array = new BigInt64Array(Mod.HEAPU32.buffer, outAddress, 2); let getOutInt64 = (i: 0 | 1 | 2) => outInt64Array[i]; return { em: Mod, Z3: { mk_context: function (c: Z3_config): Z3_context { let ctx = Mod._Z3_mk_context(c); Mod._set_noop_error_handler(ctx); return ctx; }, mk_context_rc: function (c: Z3_config): Z3_context { let ctx = Mod._Z3_mk_context_rc(c); Mod._set_noop_error_handler(ctx); return ctx; }, global_param_set: function (param_id: string, param_value: string): void { return Mod.ccall( 'Z3_global_param_set', 'void', ['string', 'string'], [param_id, param_value], ); }, global_param_reset_all: Mod._Z3_global_param_reset_all as () => void, global_param_get: function (param_id: string): string | null { let ret = Mod.ccall( 'Z3_global_param_get', 'boolean', ['string', 'number'], [param_id, outAddress], ); if (!ret) { return null; } return Mod.UTF8ToString(getOutUint(0)); }, mk_config: Mod._Z3_mk_config as () => Z3_config, del_config: Mod._Z3_del_config as (c: Z3_config) => void, set_param_value: function ( c: Z3_config, param_id: string, param_value: string, ): void { return Mod.ccall( 'Z3_set_param_value', 'void', ['number', 'string', 'string'], [c, param_id, param_value], ); }, del_context: Mod._Z3_del_context as (c: Z3_context) => void, inc_ref: Mod._Z3_inc_ref as (c: Z3_context, a: Z3_ast) => void, dec_ref: Mod._Z3_dec_ref as (c: Z3_context, a: Z3_ast) => void, update_param_value: function ( c: Z3_context, param_id: string, param_value: string, ): void { return Mod.ccall( 'Z3_update_param_value', 'void', ['number', 'string', 'string'], [c, param_id, param_value], ); }, get_global_param_descrs: Mod._Z3_get_global_param_descrs as ( c: Z3_context, ) => Z3_param_descrs, interrupt: Mod._Z3_interrupt as (c: Z3_context) => void, enable_concurrent_dec_ref: Mod._Z3_enable_concurrent_dec_ref as ( c: Z3_context, ) => void, mk_params: Mod._Z3_mk_params as (c: Z3_context) => Z3_params, params_inc_ref: Mod._Z3_params_inc_ref as ( c: Z3_context, p: Z3_params, ) => void, params_dec_ref: Mod._Z3_params_dec_ref as ( c: Z3_context, p: Z3_params, ) => void, params_set_bool: Mod._Z3_params_set_bool as ( c: Z3_context, p: Z3_params, k: Z3_symbol, v: boolean, ) => void, params_set_uint: Mod._Z3_params_set_uint as ( c: Z3_context, p: Z3_params, k: Z3_symbol, v: unsigned, ) => void, params_set_double: Mod._Z3_params_set_double as ( c: Z3_context, p: Z3_params, k: Z3_symbol, v: double, ) => void, params_set_symbol: Mod._Z3_params_set_symbol as ( c: Z3_context, p: Z3_params, k: Z3_symbol, v: Z3_symbol, ) => void, params_to_string: function (c: Z3_context, p: Z3_params): string { return Mod.ccall( 'Z3_params_to_string', 'string', ['number', 'number'], [c, p], ); }, params_validate: Mod._Z3_params_validate as ( c: Z3_context, p: Z3_params, d: Z3_param_descrs, ) => void, param_descrs_inc_ref: Mod._Z3_param_descrs_inc_ref as ( c: Z3_context, p: Z3_param_descrs, ) => void, param_descrs_dec_ref: Mod._Z3_param_descrs_dec_ref as ( c: Z3_context, p: Z3_param_descrs, ) => void, param_descrs_get_kind: Mod._Z3_param_descrs_get_kind as ( c: Z3_context, p: Z3_param_descrs, n: Z3_symbol, ) => Z3_param_kind, param_descrs_size: function ( c: Z3_context, p: Z3_param_descrs, ): unsigned { let ret = Mod.ccall( 'Z3_param_descrs_size', 'number', ['number', 'number'], [c, p], ); ret = new Uint32Array([ret])[0]; return ret; }, param_descrs_get_name: Mod._Z3_param_descrs_get_name as ( c: Z3_context, p: Z3_param_descrs, i: unsigned, ) => Z3_symbol, param_descrs_get_documentation: function ( c: Z3_context, p: Z3_param_descrs, s: Z3_symbol, ): string { return Mod.ccall( 'Z3_param_descrs_get_documentation', 'string', ['number', 'number', 'number'], [c, p, s], ); }, param_descrs_to_string: function ( c: Z3_context, p: Z3_param_descrs, ): string { return Mod.ccall( 'Z3_param_descrs_to_string', 'string', ['number', 'number'], [c, p], ); }, mk_int_symbol: Mod._Z3_mk_int_symbol as ( c: Z3_context, i: int, ) => Z3_symbol, mk_string_symbol: function (c: Z3_context, s: string): Z3_symbol { return Mod.ccall( 'Z3_mk_string_symbol', 'number', ['number', 'string'], [c, s], ); }, mk_uninterpreted_sort: Mod._Z3_mk_uninterpreted_sort as ( c: Z3_context, s: Z3_symbol, ) => Z3_sort, mk_type_variable: Mod._Z3_mk_type_variable as ( c: Z3_context, s: Z3_symbol, ) => Z3_sort, mk_bool_sort: Mod._Z3_mk_bool_sort as (c: Z3_context) => Z3_sort, mk_int_sort: Mod._Z3_mk_int_sort as (c: Z3_context) => Z3_sort, mk_real_sort: Mod._Z3_mk_real_sort as (c: Z3_context) => Z3_sort, mk_bv_sort: Mod._Z3_mk_bv_sort as ( c: Z3_context, sz: unsigned, ) => Z3_sort, mk_finite_domain_sort: Mod._Z3_mk_finite_domain_sort as ( c: Z3_context, name: Z3_symbol, size: uint64_t, ) => Z3_sort, mk_array_sort: Mod._Z3_mk_array_sort as ( c: Z3_context, domain: Z3_sort, range: Z3_sort, ) => Z3_sort, mk_array_sort_n: function ( c: Z3_context, domain: Z3_sort[], range: Z3_sort, ): Z3_sort { return Mod.ccall( 'Z3_mk_array_sort_n', 'number', ['number', 'number', 'array', 'number'], [ c, domain.length, intArrayToByteArr(domain as unknown as number[]), range, ], ); }, mk_tuple_sort: function ( c: Z3_context, mk_tuple_name: Z3_symbol, field_names: Z3_symbol[], field_sorts: Z3_sort[], ): { rv: Z3_sort; mk_tuple_decl: Z3_func_decl; proj_decl: Z3_func_decl[]; } { if (field_names.length !== field_sorts.length) { throw new TypeError( `field_names and field_sorts must be the same length (got ${field_names.length} and {field_sorts.length})`, ); } let outArray_proj_decl = Mod._malloc(4 * field_names.length); try { let ret = Mod.ccall( 'Z3_mk_tuple_sort', 'number', [ 'number', 'number', 'number', 'array', 'array', 'number', 'number', ], [ c, mk_tuple_name, field_names.length, intArrayToByteArr(field_names as unknown as number[]), intArrayToByteArr(field_sorts as unknown as number[]), outAddress, outArray_proj_decl, ], ); return { rv: ret, mk_tuple_decl: getOutUint(0) as unknown as Z3_func_decl, proj_decl: readUintArray( outArray_proj_decl, field_names.length, ) as unknown as Z3_func_decl[], }; } finally { Mod._free(outArray_proj_decl); } }, mk_enumeration_sort: function ( c: Z3_context, name: Z3_symbol, enum_names: Z3_symbol[], ): { rv: Z3_sort; enum_consts: Z3_func_decl[]; enum_testers: Z3_func_decl[]; } { let outArray_enum_consts = Mod._malloc(4 * enum_names.length); try { let outArray_enum_testers = Mod._malloc(4 * enum_names.length); try { let ret = Mod.ccall( 'Z3_mk_enumeration_sort', 'number', ['number', 'number', 'number', 'array', 'number', 'number'], [ c, name, enum_names.length, intArrayToByteArr(enum_names as unknown as number[]), outArray_enum_consts, outArray_enum_testers, ], ); return { rv: ret, enum_consts: readUintArray( outArray_enum_consts, enum_names.length, ) as unknown as Z3_func_decl[], enum_testers: readUintArray( outArray_enum_testers, enum_names.length, ) as unknown as Z3_func_decl[], }; } finally { Mod._free(outArray_enum_testers); } } finally { Mod._free(outArray_enum_consts); } }, mk_list_sort: function ( c: Z3_context, name: Z3_symbol, elem_sort: Z3_sort, ): { rv: Z3_sort; nil_decl: Z3_func_decl; is_nil_decl: Z3_func_decl; cons_decl: Z3_func_decl; is_cons_decl: Z3_func_decl; head_decl: Z3_func_decl; tail_decl: Z3_func_decl; } { let ret = Mod.ccall( 'Z3_mk_list_sort', 'number', [ 'number', 'number', 'number', 'number', 'number', 'number', 'number', 'number', 'number', ], [ c, name, elem_sort, outAddress, outAddress + 4, outAddress + 8, outAddress + 12, outAddress + 16, outAddress + 20, ], ); return { rv: ret, nil_decl: getOutUint(0) as unknown as Z3_func_decl, is_nil_decl: getOutUint(1) as unknown as Z3_func_decl, cons_decl: getOutUint(2) as unknown as Z3_func_decl, is_cons_decl: getOutUint(3) as unknown as Z3_func_decl, head_decl: getOutUint(4) as unknown as Z3_func_decl, tail_decl: getOutUint(5) as unknown as Z3_func_decl, }; }, mk_constructor: function ( c: Z3_context, name: Z3_symbol, recognizer: Z3_symbol, field_names: Z3_symbol[], sorts: Z3_sort[], sort_refs: unsigned[], ): Z3_constructor { if (field_names.length !== sorts.length) { throw new TypeError( `field_names and sorts must be the same length (got ${field_names.length} and {sorts.length})`, ); } if (field_names.length !== sort_refs.length) { throw new TypeError( `field_names and sort_refs must be the same length (got ${field_names.length} and {sort_refs.length})`, ); } return Mod.ccall( 'Z3_mk_constructor', 'number', ['number', 'number', 'number', 'number', 'array', 'array', 'array'], [ c, name, recognizer, field_names.length, intArrayToByteArr(field_names as unknown as number[]), intArrayToByteArr(sorts as unknown as number[]), intArrayToByteArr(sort_refs as unknown as number[]), ], ); }, constructor_num_fields: function ( c: Z3_context, constr: Z3_constructor, ): unsigned { let ret = Mod.ccall( 'Z3_constructor_num_fields', 'number', ['number', 'number'], [c, constr], ); ret = new Uint32Array([ret])[0]; return ret; }, del_constructor: Mod._Z3_del_constructor as ( c: Z3_context, constr: Z3_constructor, ) => void, mk_datatype: function ( c: Z3_context, name: Z3_symbol, constructors: Z3_constructor[], ): Z3_sort { return Mod.ccall( 'Z3_mk_datatype', 'number', ['number', 'number', 'number', 'array'], [ c, name, constructors.length, intArrayToByteArr(constructors as unknown as number[]), ], ); }, mk_polymorphic_datatype: function ( c: Z3_context, name: Z3_symbol, parameters: Z3_sort[], constructors: Z3_constructor[], ): Z3_sort { return Mod.ccall( 'Z3_mk_polymorphic_datatype', 'number', ['number', 'number', 'number', 'array', 'number', 'array'], [ c, name, parameters.length, intArrayToByteArr(parameters as unknown as number[]), constructors.length, intArrayToByteArr(constructors as unknown as number[]), ], ); }, mk_datatype_sort: function ( c: Z3_context, name: Z3_symbol, params: Z3_sort[], ): Z3_sort { return Mod.ccall( 'Z3_mk_datatype_sort', 'number', ['number', 'number', 'number', 'array'], [ c, name, params.length, intArrayToByteArr(params as unknown as number[]), ], ); }, mk_constructor_list: function ( c: Z3_context, constructors: Z3_constructor[], ): Z3_constructor_list { return Mod.ccall( 'Z3_mk_constructor_list', 'number', ['number', 'number', 'array'], [ c, constructors.length, intArrayToByteArr(constructors as unknown as number[]), ], ); }, del_constructor_list: Mod._Z3_del_constructor_list as ( c: Z3_context, clist: Z3_constructor_list, ) => void, mk_datatypes: function ( c: Z3_context, sort_names: Z3_symbol[], constructor_lists: Z3_constructor_list[], ): Z3_sort[] { if (sort_names.length !== constructor_lists.length) { throw new TypeError( `sort_names and constructor_lists must be the same length (got ${sort_names.length} and {constructor_lists.length})`, ); } let outArray_sorts = Mod._malloc(4 * sort_names.length); try { let ret = Mod.ccall( 'Z3_mk_datatypes', 'void', ['number', 'number', 'array', 'number', 'array'], [ c, sort_names.length, intArrayToByteArr(sort_names as unknown as number[]), outArray_sorts, intArrayToByteArr(constructor_lists as unknown as number[]), ], ); return readUintArray( outArray_sorts, sort_names.length, ) as unknown as Z3_sort[]; } finally { Mod._free(outArray_sorts); } }, query_constructor: function ( c: Z3_context, constr: Z3_constructor, num_fields: unsigned, ): { constructor: Z3_func_decl; tester: Z3_func_decl; accessors: Z3_func_decl[]; } { let outArray_accessors = Mod._malloc(4 * num_fields); try { let ret = Mod.ccall( 'Z3_query_constructor', 'void', ['number', 'number', 'number', 'number', 'number', 'number'], [ c, constr, num_fields, outAddress, outAddress + 4, outArray_accessors, ], ); return { constructor: getOutUint(0) as unknown as Z3_func_decl, tester: getOutUint(1) as unknown as Z3_func_decl, accessors: readUintArray( outArray_accessors, num_fields, ) as unknown as Z3_func_decl[], }; } finally { Mod._free(outArray_accessors); } }, mk_func_decl: function ( c: Z3_context, s: Z3_symbol, domain: Z3_sort[], range: Z3_sort, ): Z3_func_decl { return Mod.ccall( 'Z3_mk_func_decl', 'number', ['number', 'number', 'number', 'array', 'number'], [ c, s, domain.length, intArrayToByteArr(domain as unknown as number[]), range, ], ); }, mk_app: function ( c: Z3_context, d: Z3_func_decl, args: Z3_ast[], ): Z3_ast { return Mod.ccall( 'Z3_mk_app', 'number', ['number', 'number', 'number', 'array'], [c, d, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_const: Mod._Z3_mk_const as ( c: Z3_context, s: Z3_symbol, ty: Z3_sort, ) => Z3_ast, mk_fresh_func_decl: function ( c: Z3_context, prefix: string, domain: Z3_sort[], range: Z3_sort, ): Z3_func_decl { return Mod.ccall( 'Z3_mk_fresh_func_decl', 'number', ['number', 'string', 'number', 'array', 'number'], [ c, prefix, domain.length, intArrayToByteArr(domain as unknown as number[]), range, ], ); }, mk_fresh_const: function ( c: Z3_context, prefix: string, ty: Z3_sort, ): Z3_ast { return Mod.ccall( 'Z3_mk_fresh_const', 'number', ['number', 'string', 'number'], [c, prefix, ty], ); }, mk_rec_func_decl: function ( c: Z3_context, s: Z3_symbol, domain: Z3_sort[], range: Z3_sort, ): Z3_func_decl { return Mod.ccall( 'Z3_mk_rec_func_decl', 'number', ['number', 'number', 'number', 'array', 'number'], [ c, s, domain.length, intArrayToByteArr(domain as unknown as number[]), range, ], ); }, add_rec_def: function ( c: Z3_context, f: Z3_func_decl, args: Z3_ast[], body: Z3_ast, ): void { return Mod.ccall( 'Z3_add_rec_def', 'void', ['number', 'number', 'number', 'array', 'number'], [ c, f, args.length, intArrayToByteArr(args as unknown as number[]), body, ], ); }, mk_true: Mod._Z3_mk_true as (c: Z3_context) => Z3_ast, mk_false: Mod._Z3_mk_false as (c: Z3_context) => Z3_ast, mk_eq: Mod._Z3_mk_eq as (c: Z3_context, l: Z3_ast, r: Z3_ast) => Z3_ast, mk_distinct: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_distinct', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_not: Mod._Z3_mk_not as (c: Z3_context, a: Z3_ast) => Z3_ast, mk_ite: Mod._Z3_mk_ite as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, t3: Z3_ast, ) => Z3_ast, mk_iff: Mod._Z3_mk_iff as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_implies: Mod._Z3_mk_implies as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_xor: Mod._Z3_mk_xor as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_and: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_and', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_or: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_or', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_add: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_add', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_mul: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_mul', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_sub: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_sub', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_unary_minus: Mod._Z3_mk_unary_minus as ( c: Z3_context, arg: Z3_ast, ) => Z3_ast, mk_div: Mod._Z3_mk_div as ( c: Z3_context, arg1: Z3_ast, arg2: Z3_ast, ) => Z3_ast, mk_mod: Mod._Z3_mk_mod as ( c: Z3_context, arg1: Z3_ast, arg2: Z3_ast, ) => Z3_ast, mk_rem: Mod._Z3_mk_rem as ( c: Z3_context, arg1: Z3_ast, arg2: Z3_ast, ) => Z3_ast, mk_power: Mod._Z3_mk_power as ( c: Z3_context, arg1: Z3_ast, arg2: Z3_ast, ) => Z3_ast, mk_abs: Mod._Z3_mk_abs as (c: Z3_context, arg: Z3_ast) => Z3_ast, mk_lt: Mod._Z3_mk_lt as (c: Z3_context, t1: Z3_ast, t2: Z3_ast) => Z3_ast, mk_le: Mod._Z3_mk_le as (c: Z3_context, t1: Z3_ast, t2: Z3_ast) => Z3_ast, mk_gt: Mod._Z3_mk_gt as (c: Z3_context, t1: Z3_ast, t2: Z3_ast) => Z3_ast, mk_ge: Mod._Z3_mk_ge as (c: Z3_context, t1: Z3_ast, t2: Z3_ast) => Z3_ast, mk_divides: Mod._Z3_mk_divides as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_int2real: Mod._Z3_mk_int2real as (c: Z3_context, t1: Z3_ast) => Z3_ast, mk_real2int: Mod._Z3_mk_real2int as (c: Z3_context, t1: Z3_ast) => Z3_ast, mk_is_int: Mod._Z3_mk_is_int as (c: Z3_context, t1: Z3_ast) => Z3_ast, mk_bvnot: Mod._Z3_mk_bvnot as (c: Z3_context, t1: Z3_ast) => Z3_ast, mk_bvredand: Mod._Z3_mk_bvredand as (c: Z3_context, t1: Z3_ast) => Z3_ast, mk_bvredor: Mod._Z3_mk_bvredor as (c: Z3_context, t1: Z3_ast) => Z3_ast, mk_bvand: Mod._Z3_mk_bvand as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvor: Mod._Z3_mk_bvor as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvxor: Mod._Z3_mk_bvxor as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvnand: Mod._Z3_mk_bvnand as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvnor: Mod._Z3_mk_bvnor as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvxnor: Mod._Z3_mk_bvxnor as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvneg: Mod._Z3_mk_bvneg as (c: Z3_context, t1: Z3_ast) => Z3_ast, mk_bvadd: Mod._Z3_mk_bvadd as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvsub: Mod._Z3_mk_bvsub as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvmul: Mod._Z3_mk_bvmul as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvudiv: Mod._Z3_mk_bvudiv as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvsdiv: Mod._Z3_mk_bvsdiv as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvurem: Mod._Z3_mk_bvurem as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvsrem: Mod._Z3_mk_bvsrem as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvsmod: Mod._Z3_mk_bvsmod as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvult: Mod._Z3_mk_bvult as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvslt: Mod._Z3_mk_bvslt as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvule: Mod._Z3_mk_bvule as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvsle: Mod._Z3_mk_bvsle as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvuge: Mod._Z3_mk_bvuge as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvsge: Mod._Z3_mk_bvsge as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvugt: Mod._Z3_mk_bvugt as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvsgt: Mod._Z3_mk_bvsgt as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_concat: Mod._Z3_mk_concat as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_extract: Mod._Z3_mk_extract as ( c: Z3_context, high: unsigned, low: unsigned, t1: Z3_ast, ) => Z3_ast, mk_sign_ext: Mod._Z3_mk_sign_ext as ( c: Z3_context, i: unsigned, t1: Z3_ast, ) => Z3_ast, mk_zero_ext: Mod._Z3_mk_zero_ext as ( c: Z3_context, i: unsigned, t1: Z3_ast, ) => Z3_ast, mk_repeat: Mod._Z3_mk_repeat as ( c: Z3_context, i: unsigned, t1: Z3_ast, ) => Z3_ast, mk_bit2bool: Mod._Z3_mk_bit2bool as ( c: Z3_context, i: unsigned, t1: Z3_ast, ) => Z3_ast, mk_bvshl: Mod._Z3_mk_bvshl as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvlshr: Mod._Z3_mk_bvlshr as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvashr: Mod._Z3_mk_bvashr as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_rotate_left: Mod._Z3_mk_rotate_left as ( c: Z3_context, i: unsigned, t1: Z3_ast, ) => Z3_ast, mk_rotate_right: Mod._Z3_mk_rotate_right as ( c: Z3_context, i: unsigned, t1: Z3_ast, ) => Z3_ast, mk_ext_rotate_left: Mod._Z3_mk_ext_rotate_left as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_ext_rotate_right: Mod._Z3_mk_ext_rotate_right as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_int2bv: Mod._Z3_mk_int2bv as ( c: Z3_context, n: unsigned, t1: Z3_ast, ) => Z3_ast, mk_bv2int: Mod._Z3_mk_bv2int as ( c: Z3_context, t1: Z3_ast, is_signed: boolean, ) => Z3_ast, mk_bvadd_no_overflow: Mod._Z3_mk_bvadd_no_overflow as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, is_signed: boolean, ) => Z3_ast, mk_bvadd_no_underflow: Mod._Z3_mk_bvadd_no_underflow as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvsub_no_overflow: Mod._Z3_mk_bvsub_no_overflow as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvsub_no_underflow: Mod._Z3_mk_bvsub_no_underflow as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, is_signed: boolean, ) => Z3_ast, mk_bvsdiv_no_overflow: Mod._Z3_mk_bvsdiv_no_overflow as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_bvneg_no_overflow: Mod._Z3_mk_bvneg_no_overflow as ( c: Z3_context, t1: Z3_ast, ) => Z3_ast, mk_bvmul_no_overflow: Mod._Z3_mk_bvmul_no_overflow as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, is_signed: boolean, ) => Z3_ast, mk_bvmul_no_underflow: Mod._Z3_mk_bvmul_no_underflow as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_select: Mod._Z3_mk_select as ( c: Z3_context, a: Z3_ast, i: Z3_ast, ) => Z3_ast, mk_select_n: function (c: Z3_context, a: Z3_ast, idxs: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_select_n', 'number', ['number', 'number', 'number', 'array'], [c, a, idxs.length, intArrayToByteArr(idxs as unknown as number[])], ); }, mk_store: Mod._Z3_mk_store as ( c: Z3_context, a: Z3_ast, i: Z3_ast, v: Z3_ast, ) => Z3_ast, mk_store_n: function ( c: Z3_context, a: Z3_ast, idxs: Z3_ast[], v: Z3_ast, ): Z3_ast { return Mod.ccall( 'Z3_mk_store_n', 'number', ['number', 'number', 'number', 'array', 'number'], [ c, a, idxs.length, intArrayToByteArr(idxs as unknown as number[]), v, ], ); }, mk_const_array: Mod._Z3_mk_const_array as ( c: Z3_context, domain: Z3_sort, v: Z3_ast, ) => Z3_ast, mk_map: function ( c: Z3_context, f: Z3_func_decl, args: Z3_ast[], ): Z3_ast { return Mod.ccall( 'Z3_mk_map', 'number', ['number', 'number', 'number', 'array'], [c, f, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_array_default: Mod._Z3_mk_array_default as ( c: Z3_context, array: Z3_ast, ) => Z3_ast, mk_as_array: Mod._Z3_mk_as_array as ( c: Z3_context, f: Z3_func_decl, ) => Z3_ast, mk_set_sort: Mod._Z3_mk_set_sort as ( c: Z3_context, ty: Z3_sort, ) => Z3_sort, mk_empty_set: Mod._Z3_mk_empty_set as ( c: Z3_context, domain: Z3_sort, ) => Z3_ast, mk_full_set: Mod._Z3_mk_full_set as ( c: Z3_context, domain: Z3_sort, ) => Z3_ast, mk_set_add: Mod._Z3_mk_set_add as ( c: Z3_context, set: Z3_ast, elem: Z3_ast, ) => Z3_ast, mk_set_del: Mod._Z3_mk_set_del as ( c: Z3_context, set: Z3_ast, elem: Z3_ast, ) => Z3_ast, mk_set_union: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_set_union', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_set_intersect: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_set_intersect', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_set_difference: Mod._Z3_mk_set_difference as ( c: Z3_context, arg1: Z3_ast, arg2: Z3_ast, ) => Z3_ast, mk_set_complement: Mod._Z3_mk_set_complement as ( c: Z3_context, arg: Z3_ast, ) => Z3_ast, mk_set_member: Mod._Z3_mk_set_member as ( c: Z3_context, elem: Z3_ast, set: Z3_ast, ) => Z3_ast, mk_set_subset: Mod._Z3_mk_set_subset as ( c: Z3_context, arg1: Z3_ast, arg2: Z3_ast, ) => Z3_ast, mk_array_ext: Mod._Z3_mk_array_ext as ( c: Z3_context, arg1: Z3_ast, arg2: Z3_ast, ) => Z3_ast, mk_numeral: function ( c: Z3_context, numeral: string, ty: Z3_sort, ): Z3_ast { return Mod.ccall( 'Z3_mk_numeral', 'number', ['number', 'string', 'number'], [c, numeral, ty], ); }, mk_real: Mod._Z3_mk_real as (c: Z3_context, num: int, den: int) => Z3_ast, mk_real_int64: Mod._Z3_mk_real_int64 as ( c: Z3_context, num: int64_t, den: int64_t, ) => Z3_ast, mk_int: Mod._Z3_mk_int as (c: Z3_context, v: int, ty: Z3_sort) => Z3_ast, mk_unsigned_int: Mod._Z3_mk_unsigned_int as ( c: Z3_context, v: unsigned, ty: Z3_sort, ) => Z3_ast, mk_int64: Mod._Z3_mk_int64 as ( c: Z3_context, v: int64_t, ty: Z3_sort, ) => Z3_ast, mk_unsigned_int64: Mod._Z3_mk_unsigned_int64 as ( c: Z3_context, v: uint64_t, ty: Z3_sort, ) => Z3_ast, mk_bv_numeral: function (c: Z3_context, bits: boolean[]): Z3_ast { return Mod.ccall( 'Z3_mk_bv_numeral', 'number', ['number', 'number', 'array'], [c, bits.length, boolArrayToByteArr(bits)], ); }, mk_seq_sort: Mod._Z3_mk_seq_sort as ( c: Z3_context, s: Z3_sort, ) => Z3_sort, is_seq_sort: function (c: Z3_context, s: Z3_sort): boolean { return Mod.ccall( 'Z3_is_seq_sort', 'boolean', ['number', 'number'], [c, s], ); }, get_seq_sort_basis: Mod._Z3_get_seq_sort_basis as ( c: Z3_context, s: Z3_sort, ) => Z3_sort, mk_re_sort: Mod._Z3_mk_re_sort as ( c: Z3_context, seq: Z3_sort, ) => Z3_sort, is_re_sort: function (c: Z3_context, s: Z3_sort): boolean { return Mod.ccall( 'Z3_is_re_sort', 'boolean', ['number', 'number'], [c, s], ); }, get_re_sort_basis: Mod._Z3_get_re_sort_basis as ( c: Z3_context, s: Z3_sort, ) => Z3_sort, mk_string_sort: Mod._Z3_mk_string_sort as (c: Z3_context) => Z3_sort, mk_char_sort: Mod._Z3_mk_char_sort as (c: Z3_context) => Z3_sort, is_string_sort: function (c: Z3_context, s: Z3_sort): boolean { return Mod.ccall( 'Z3_is_string_sort', 'boolean', ['number', 'number'], [c, s], ); }, is_char_sort: function (c: Z3_context, s: Z3_sort): boolean { return Mod.ccall( 'Z3_is_char_sort', 'boolean', ['number', 'number'], [c, s], ); }, mk_string: function (c: Z3_context, s: string): Z3_ast { return Mod.ccall( 'Z3_mk_string', 'number', ['number', 'string'], [c, s], ); }, mk_lstring: function (c: Z3_context, len: unsigned, s: string): Z3_ast { return Mod.ccall( 'Z3_mk_lstring', 'number', ['number', 'number', 'string'], [c, len, s], ); }, mk_u32string: function (c: Z3_context, chars: unsigned[]): Z3_ast { return Mod.ccall( 'Z3_mk_u32string', 'number', ['number', 'number', 'array'], [c, chars.length, intArrayToByteArr(chars as unknown as number[])], ); }, is_string: function (c: Z3_context, s: Z3_ast): boolean { return Mod.ccall( 'Z3_is_string', 'boolean', ['number', 'number'], [c, s], ); }, get_string: function (c: Z3_context, s: Z3_ast): string { return Mod.ccall( 'Z3_get_string', 'string', ['number', 'number'], [c, s], ); }, get_string_length: function (c: Z3_context, s: Z3_ast): unsigned { let ret = Mod.ccall( 'Z3_get_string_length', 'number', ['number', 'number'], [c, s], ); ret = new Uint32Array([ret])[0]; return ret; }, get_string_contents: function ( c: Z3_context, s: Z3_ast, length: unsigned, ): unsigned[] { let outArray_contents = Mod._malloc(4 * length); try { let ret = Mod.ccall( 'Z3_get_string_contents', 'void', ['number', 'number', 'number', 'number'], [c, s, length, outArray_contents], ); return readUintArray(outArray_contents, length); } finally { Mod._free(outArray_contents); } }, mk_seq_empty: Mod._Z3_mk_seq_empty as ( c: Z3_context, seq: Z3_sort, ) => Z3_ast, mk_seq_unit: Mod._Z3_mk_seq_unit as (c: Z3_context, a: Z3_ast) => Z3_ast, mk_seq_concat: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_seq_concat', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_seq_prefix: Mod._Z3_mk_seq_prefix as ( c: Z3_context, prefix: Z3_ast, s: Z3_ast, ) => Z3_ast, mk_seq_suffix: Mod._Z3_mk_seq_suffix as ( c: Z3_context, suffix: Z3_ast, s: Z3_ast, ) => Z3_ast, mk_seq_contains: Mod._Z3_mk_seq_contains as ( c: Z3_context, container: Z3_ast, containee: Z3_ast, ) => Z3_ast, mk_str_lt: Mod._Z3_mk_str_lt as ( c: Z3_context, prefix: Z3_ast, s: Z3_ast, ) => Z3_ast, mk_str_le: Mod._Z3_mk_str_le as ( c: Z3_context, prefix: Z3_ast, s: Z3_ast, ) => Z3_ast, mk_seq_extract: Mod._Z3_mk_seq_extract as ( c: Z3_context, s: Z3_ast, offset: Z3_ast, length: Z3_ast, ) => Z3_ast, mk_seq_replace: Mod._Z3_mk_seq_replace as ( c: Z3_context, s: Z3_ast, src: Z3_ast, dst: Z3_ast, ) => Z3_ast, mk_seq_replace_all: Mod._Z3_mk_seq_replace_all as ( c: Z3_context, s: Z3_ast, src: Z3_ast, dst: Z3_ast, ) => Z3_ast, mk_seq_replace_re: Mod._Z3_mk_seq_replace_re as ( c: Z3_context, s: Z3_ast, re: Z3_ast, dst: Z3_ast, ) => Z3_ast, mk_seq_replace_re_all: Mod._Z3_mk_seq_replace_re_all as ( c: Z3_context, s: Z3_ast, re: Z3_ast, dst: Z3_ast, ) => Z3_ast, mk_seq_at: Mod._Z3_mk_seq_at as ( c: Z3_context, s: Z3_ast, index: Z3_ast, ) => Z3_ast, mk_seq_nth: Mod._Z3_mk_seq_nth as ( c: Z3_context, s: Z3_ast, index: Z3_ast, ) => Z3_ast, mk_seq_length: Mod._Z3_mk_seq_length as ( c: Z3_context, s: Z3_ast, ) => Z3_ast, mk_seq_index: Mod._Z3_mk_seq_index as ( c: Z3_context, s: Z3_ast, substr: Z3_ast, offset: Z3_ast, ) => Z3_ast, mk_seq_last_index: Mod._Z3_mk_seq_last_index as ( c: Z3_context, s: Z3_ast, substr: Z3_ast, ) => Z3_ast, mk_seq_map: Mod._Z3_mk_seq_map as ( c: Z3_context, f: Z3_ast, s: Z3_ast, ) => Z3_ast, mk_seq_mapi: Mod._Z3_mk_seq_mapi as ( c: Z3_context, f: Z3_ast, i: Z3_ast, s: Z3_ast, ) => Z3_ast, mk_seq_foldl: Mod._Z3_mk_seq_foldl as ( c: Z3_context, f: Z3_ast, a: Z3_ast, s: Z3_ast, ) => Z3_ast, mk_seq_foldli: Mod._Z3_mk_seq_foldli as ( c: Z3_context, f: Z3_ast, i: Z3_ast, a: Z3_ast, s: Z3_ast, ) => Z3_ast, mk_str_to_int: Mod._Z3_mk_str_to_int as ( c: Z3_context, s: Z3_ast, ) => Z3_ast, mk_int_to_str: Mod._Z3_mk_int_to_str as ( c: Z3_context, s: Z3_ast, ) => Z3_ast, mk_string_to_code: Mod._Z3_mk_string_to_code as ( c: Z3_context, a: Z3_ast, ) => Z3_ast, mk_string_from_code: Mod._Z3_mk_string_from_code as ( c: Z3_context, a: Z3_ast, ) => Z3_ast, mk_ubv_to_str: Mod._Z3_mk_ubv_to_str as ( c: Z3_context, s: Z3_ast, ) => Z3_ast, mk_sbv_to_str: Mod._Z3_mk_sbv_to_str as ( c: Z3_context, s: Z3_ast, ) => Z3_ast, mk_seq_to_re: Mod._Z3_mk_seq_to_re as ( c: Z3_context, seq: Z3_ast, ) => Z3_ast, mk_seq_in_re: Mod._Z3_mk_seq_in_re as ( c: Z3_context, seq: Z3_ast, re: Z3_ast, ) => Z3_ast, mk_re_plus: Mod._Z3_mk_re_plus as (c: Z3_context, re: Z3_ast) => Z3_ast, mk_re_star: Mod._Z3_mk_re_star as (c: Z3_context, re: Z3_ast) => Z3_ast, mk_re_option: Mod._Z3_mk_re_option as ( c: Z3_context, re: Z3_ast, ) => Z3_ast, mk_re_union: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_re_union', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_re_concat: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_re_concat', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_re_range: Mod._Z3_mk_re_range as ( c: Z3_context, lo: Z3_ast, hi: Z3_ast, ) => Z3_ast, mk_re_allchar: Mod._Z3_mk_re_allchar as ( c: Z3_context, regex_sort: Z3_sort, ) => Z3_ast, mk_re_loop: Mod._Z3_mk_re_loop as ( c: Z3_context, r: Z3_ast, lo: unsigned, hi: unsigned, ) => Z3_ast, mk_re_power: Mod._Z3_mk_re_power as ( c: Z3_context, re: Z3_ast, n: unsigned, ) => Z3_ast, mk_re_intersect: function (c: Z3_context, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_mk_re_intersect', 'number', ['number', 'number', 'array'], [c, args.length, intArrayToByteArr(args as unknown as number[])], ); }, mk_re_complement: Mod._Z3_mk_re_complement as ( c: Z3_context, re: Z3_ast, ) => Z3_ast, mk_re_diff: Mod._Z3_mk_re_diff as ( c: Z3_context, re1: Z3_ast, re2: Z3_ast, ) => Z3_ast, mk_re_empty: Mod._Z3_mk_re_empty as ( c: Z3_context, re: Z3_sort, ) => Z3_ast, mk_re_full: Mod._Z3_mk_re_full as (c: Z3_context, re: Z3_sort) => Z3_ast, mk_char: Mod._Z3_mk_char as (c: Z3_context, ch: unsigned) => Z3_ast, mk_char_le: Mod._Z3_mk_char_le as ( c: Z3_context, ch1: Z3_ast, ch2: Z3_ast, ) => Z3_ast, mk_char_to_int: Mod._Z3_mk_char_to_int as ( c: Z3_context, ch: Z3_ast, ) => Z3_ast, mk_char_to_bv: Mod._Z3_mk_char_to_bv as ( c: Z3_context, ch: Z3_ast, ) => Z3_ast, mk_char_from_bv: Mod._Z3_mk_char_from_bv as ( c: Z3_context, bv: Z3_ast, ) => Z3_ast, mk_char_is_digit: Mod._Z3_mk_char_is_digit as ( c: Z3_context, ch: Z3_ast, ) => Z3_ast, mk_linear_order: Mod._Z3_mk_linear_order as ( c: Z3_context, a: Z3_sort, id: unsigned, ) => Z3_func_decl, mk_partial_order: Mod._Z3_mk_partial_order as ( c: Z3_context, a: Z3_sort, id: unsigned, ) => Z3_func_decl, mk_piecewise_linear_order: Mod._Z3_mk_piecewise_linear_order as ( c: Z3_context, a: Z3_sort, id: unsigned, ) => Z3_func_decl, mk_tree_order: Mod._Z3_mk_tree_order as ( c: Z3_context, a: Z3_sort, id: unsigned, ) => Z3_func_decl, mk_transitive_closure: Mod._Z3_mk_transitive_closure as ( c: Z3_context, f: Z3_func_decl, ) => Z3_func_decl, mk_pattern: function (c: Z3_context, terms: Z3_ast[]): Z3_pattern { return Mod.ccall( 'Z3_mk_pattern', 'number', ['number', 'number', 'array'], [c, terms.length, intArrayToByteArr(terms as unknown as number[])], ); }, mk_bound: Mod._Z3_mk_bound as ( c: Z3_context, index: unsigned, ty: Z3_sort, ) => Z3_ast, mk_forall: function ( c: Z3_context, weight: unsigned, patterns: Z3_pattern[], sorts: Z3_sort[], decl_names: Z3_symbol[], body: Z3_ast, ): Z3_ast { if (sorts.length !== decl_names.length) { throw new TypeError( `sorts and decl_names must be the same length (got ${sorts.length} and {decl_names.length})`, ); } return Mod.ccall( 'Z3_mk_forall', 'number', [ 'number', 'number', 'number', 'array', 'number', 'array', 'array', 'number', ], [ c, weight, patterns.length, intArrayToByteArr(patterns as unknown as number[]), sorts.length, intArrayToByteArr(sorts as unknown as number[]), intArrayToByteArr(decl_names as unknown as number[]), body, ], ); }, mk_exists: function ( c: Z3_context, weight: unsigned, patterns: Z3_pattern[], sorts: Z3_sort[], decl_names: Z3_symbol[], body: Z3_ast, ): Z3_ast { if (sorts.length !== decl_names.length) { throw new TypeError( `sorts and decl_names must be the same length (got ${sorts.length} and {decl_names.length})`, ); } return Mod.ccall( 'Z3_mk_exists', 'number', [ 'number', 'number', 'number', 'array', 'number', 'array', 'array', 'number', ], [ c, weight, patterns.length, intArrayToByteArr(patterns as unknown as number[]), sorts.length, intArrayToByteArr(sorts as unknown as number[]), intArrayToByteArr(decl_names as unknown as number[]), body, ], ); }, mk_quantifier: function ( c: Z3_context, is_forall: boolean, weight: unsigned, patterns: Z3_pattern[], sorts: Z3_sort[], decl_names: Z3_symbol[], body: Z3_ast, ): Z3_ast { if (sorts.length !== decl_names.length) { throw new TypeError( `sorts and decl_names must be the same length (got ${sorts.length} and {decl_names.length})`, ); } return Mod.ccall( 'Z3_mk_quantifier', 'number', [ 'number', 'boolean', 'number', 'number', 'array', 'number', 'array', 'array', 'number', ], [ c, is_forall, weight, patterns.length, intArrayToByteArr(patterns as unknown as number[]), sorts.length, intArrayToByteArr(sorts as unknown as number[]), intArrayToByteArr(decl_names as unknown as number[]), body, ], ); }, mk_quantifier_ex: function ( c: Z3_context, is_forall: boolean, weight: unsigned, quantifier_id: Z3_symbol, skolem_id: Z3_symbol, patterns: Z3_pattern[], no_patterns: Z3_ast[], sorts: Z3_sort[], decl_names: Z3_symbol[], body: Z3_ast, ): Z3_ast { if (sorts.length !== decl_names.length) { throw new TypeError( `sorts and decl_names must be the same length (got ${sorts.length} and {decl_names.length})`, ); } return Mod.ccall( 'Z3_mk_quantifier_ex', 'number', [ 'number', 'boolean', 'number', 'number', 'number', 'number', 'array', 'number', 'array', 'number', 'array', 'array', 'number', ], [ c, is_forall, weight, quantifier_id, skolem_id, patterns.length, intArrayToByteArr(patterns as unknown as number[]), no_patterns.length, intArrayToByteArr(no_patterns as unknown as number[]), sorts.length, intArrayToByteArr(sorts as unknown as number[]), intArrayToByteArr(decl_names as unknown as number[]), body, ], ); }, mk_forall_const: function ( c: Z3_context, weight: unsigned, bound: Z3_app[], patterns: Z3_pattern[], body: Z3_ast, ): Z3_ast { return Mod.ccall( 'Z3_mk_forall_const', 'number', ['number', 'number', 'number', 'array', 'number', 'array', 'number'], [ c, weight, bound.length, intArrayToByteArr(bound as unknown as number[]), patterns.length, intArrayToByteArr(patterns as unknown as number[]), body, ], ); }, mk_exists_const: function ( c: Z3_context, weight: unsigned, bound: Z3_app[], patterns: Z3_pattern[], body: Z3_ast, ): Z3_ast { return Mod.ccall( 'Z3_mk_exists_const', 'number', ['number', 'number', 'number', 'array', 'number', 'array', 'number'], [ c, weight, bound.length, intArrayToByteArr(bound as unknown as number[]), patterns.length, intArrayToByteArr(patterns as unknown as number[]), body, ], ); }, mk_quantifier_const: function ( c: Z3_context, is_forall: boolean, weight: unsigned, bound: Z3_app[], patterns: Z3_pattern[], body: Z3_ast, ): Z3_ast { return Mod.ccall( 'Z3_mk_quantifier_const', 'number', [ 'number', 'boolean', 'number', 'number', 'array', 'number', 'array', 'number', ], [ c, is_forall, weight, bound.length, intArrayToByteArr(bound as unknown as number[]), patterns.length, intArrayToByteArr(patterns as unknown as number[]), body, ], ); }, mk_quantifier_const_ex: function ( c: Z3_context, is_forall: boolean, weight: unsigned, quantifier_id: Z3_symbol, skolem_id: Z3_symbol, bound: Z3_app[], patterns: Z3_pattern[], no_patterns: Z3_ast[], body: Z3_ast, ): Z3_ast { return Mod.ccall( 'Z3_mk_quantifier_const_ex', 'number', [ 'number', 'boolean', 'number', 'number', 'number', 'number', 'array', 'number', 'array', 'number', 'array', 'number', ], [ c, is_forall, weight, quantifier_id, skolem_id, bound.length, intArrayToByteArr(bound as unknown as number[]), patterns.length, intArrayToByteArr(patterns as unknown as number[]), no_patterns.length, intArrayToByteArr(no_patterns as unknown as number[]), body, ], ); }, mk_lambda: function ( c: Z3_context, sorts: Z3_sort[], decl_names: Z3_symbol[], body: Z3_ast, ): Z3_ast { if (sorts.length !== decl_names.length) { throw new TypeError( `sorts and decl_names must be the same length (got ${sorts.length} and {decl_names.length})`, ); } return Mod.ccall( 'Z3_mk_lambda', 'number', ['number', 'number', 'array', 'array', 'number'], [ c, sorts.length, intArrayToByteArr(sorts as unknown as number[]), intArrayToByteArr(decl_names as unknown as number[]), body, ], ); }, mk_lambda_const: function ( c: Z3_context, bound: Z3_app[], body: Z3_ast, ): Z3_ast { return Mod.ccall( 'Z3_mk_lambda_const', 'number', ['number', 'number', 'array', 'number'], [ c, bound.length, intArrayToByteArr(bound as unknown as number[]), body, ], ); }, get_symbol_kind: Mod._Z3_get_symbol_kind as ( c: Z3_context, s: Z3_symbol, ) => Z3_symbol_kind, get_symbol_int: Mod._Z3_get_symbol_int as ( c: Z3_context, s: Z3_symbol, ) => int, get_symbol_string: function (c: Z3_context, s: Z3_symbol): string { return Mod.ccall( 'Z3_get_symbol_string', 'string', ['number', 'number'], [c, s], ); }, get_sort_name: Mod._Z3_get_sort_name as ( c: Z3_context, d: Z3_sort, ) => Z3_symbol, get_sort_id: function (c: Z3_context, s: Z3_sort): unsigned { let ret = Mod.ccall( 'Z3_get_sort_id', 'number', ['number', 'number'], [c, s], ); ret = new Uint32Array([ret])[0]; return ret; }, sort_to_ast: Mod._Z3_sort_to_ast as (c: Z3_context, s: Z3_sort) => Z3_ast, is_eq_sort: function (c: Z3_context, s1: Z3_sort, s2: Z3_sort): boolean { return Mod.ccall( 'Z3_is_eq_sort', 'boolean', ['number', 'number', 'number'], [c, s1, s2], ); }, get_sort_kind: Mod._Z3_get_sort_kind as ( c: Z3_context, t: Z3_sort, ) => Z3_sort_kind, get_bv_sort_size: function (c: Z3_context, t: Z3_sort): unsigned { let ret = Mod.ccall( 'Z3_get_bv_sort_size', 'number', ['number', 'number'], [c, t], ); ret = new Uint32Array([ret])[0]; return ret; }, get_finite_domain_sort_size: function ( c: Z3_context, s: Z3_sort, ): uint64_t | null { let ret = Mod.ccall( 'Z3_get_finite_domain_sort_size', 'boolean', ['number', 'number', 'number'], [c, s, outAddress], ); if (!ret) { return null; } return getOutUint64(0); }, get_array_arity: function (c: Z3_context, s: Z3_sort): unsigned { let ret = Mod.ccall( 'Z3_get_array_arity', 'number', ['number', 'number'], [c, s], ); ret = new Uint32Array([ret])[0]; return ret; }, get_array_sort_domain: Mod._Z3_get_array_sort_domain as ( c: Z3_context, t: Z3_sort, ) => Z3_sort, get_array_sort_domain_n: Mod._Z3_get_array_sort_domain_n as ( c: Z3_context, t: Z3_sort, idx: unsigned, ) => Z3_sort, get_array_sort_range: Mod._Z3_get_array_sort_range as ( c: Z3_context, t: Z3_sort, ) => Z3_sort, get_tuple_sort_mk_decl: Mod._Z3_get_tuple_sort_mk_decl as ( c: Z3_context, t: Z3_sort, ) => Z3_func_decl, get_tuple_sort_num_fields: function ( c: Z3_context, t: Z3_sort, ): unsigned { let ret = Mod.ccall( 'Z3_get_tuple_sort_num_fields', 'number', ['number', 'number'], [c, t], ); ret = new Uint32Array([ret])[0]; return ret; }, get_tuple_sort_field_decl: Mod._Z3_get_tuple_sort_field_decl as ( c: Z3_context, t: Z3_sort, i: unsigned, ) => Z3_func_decl, is_recursive_datatype_sort: function ( c: Z3_context, s: Z3_sort, ): boolean { return Mod.ccall( 'Z3_is_recursive_datatype_sort', 'boolean', ['number', 'number'], [c, s], ); }, get_datatype_sort_num_constructors: function ( c: Z3_context, t: Z3_sort, ): unsigned { let ret = Mod.ccall( 'Z3_get_datatype_sort_num_constructors', 'number', ['number', 'number'], [c, t], ); ret = new Uint32Array([ret])[0]; return ret; }, get_datatype_sort_constructor: Mod._Z3_get_datatype_sort_constructor as ( c: Z3_context, t: Z3_sort, idx: unsigned, ) => Z3_func_decl, get_datatype_sort_recognizer: Mod._Z3_get_datatype_sort_recognizer as ( c: Z3_context, t: Z3_sort, idx: unsigned, ) => Z3_func_decl, get_datatype_sort_constructor_accessor: Mod._Z3_get_datatype_sort_constructor_accessor as ( c: Z3_context, t: Z3_sort, idx_c: unsigned, idx_a: unsigned, ) => Z3_func_decl, datatype_update_field: Mod._Z3_datatype_update_field as ( c: Z3_context, field_access: Z3_func_decl, t: Z3_ast, value: Z3_ast, ) => Z3_ast, get_relation_arity: function (c: Z3_context, s: Z3_sort): unsigned { let ret = Mod.ccall( 'Z3_get_relation_arity', 'number', ['number', 'number'], [c, s], ); ret = new Uint32Array([ret])[0]; return ret; }, get_relation_column: Mod._Z3_get_relation_column as ( c: Z3_context, s: Z3_sort, col: unsigned, ) => Z3_sort, mk_atmost: function (c: Z3_context, args: Z3_ast[], k: unsigned): Z3_ast { return Mod.ccall( 'Z3_mk_atmost', 'number', ['number', 'number', 'array', 'number'], [c, args.length, intArrayToByteArr(args as unknown as number[]), k], ); }, mk_atleast: function ( c: Z3_context, args: Z3_ast[], k: unsigned, ): Z3_ast { return Mod.ccall( 'Z3_mk_atleast', 'number', ['number', 'number', 'array', 'number'], [c, args.length, intArrayToByteArr(args as unknown as number[]), k], ); }, mk_pble: function ( c: Z3_context, args: Z3_ast[], coeffs: int[], k: int, ): Z3_ast { if (args.length !== coeffs.length) { throw new TypeError( `args and coeffs must be the same length (got ${args.length} and {coeffs.length})`, ); } return Mod.ccall( 'Z3_mk_pble', 'number', ['number', 'number', 'array', 'array', 'number'], [ c, args.length, intArrayToByteArr(args as unknown as number[]), intArrayToByteArr(coeffs as unknown as number[]), k, ], ); }, mk_pbge: function ( c: Z3_context, args: Z3_ast[], coeffs: int[], k: int, ): Z3_ast { if (args.length !== coeffs.length) { throw new TypeError( `args and coeffs must be the same length (got ${args.length} and {coeffs.length})`, ); } return Mod.ccall( 'Z3_mk_pbge', 'number', ['number', 'number', 'array', 'array', 'number'], [ c, args.length, intArrayToByteArr(args as unknown as number[]), intArrayToByteArr(coeffs as unknown as number[]), k, ], ); }, mk_pbeq: function ( c: Z3_context, args: Z3_ast[], coeffs: int[], k: int, ): Z3_ast { if (args.length !== coeffs.length) { throw new TypeError( `args and coeffs must be the same length (got ${args.length} and {coeffs.length})`, ); } return Mod.ccall( 'Z3_mk_pbeq', 'number', ['number', 'number', 'array', 'array', 'number'], [ c, args.length, intArrayToByteArr(args as unknown as number[]), intArrayToByteArr(coeffs as unknown as number[]), k, ], ); }, func_decl_to_ast: Mod._Z3_func_decl_to_ast as ( c: Z3_context, f: Z3_func_decl, ) => Z3_ast, is_eq_func_decl: function ( c: Z3_context, f1: Z3_func_decl, f2: Z3_func_decl, ): boolean { return Mod.ccall( 'Z3_is_eq_func_decl', 'boolean', ['number', 'number', 'number'], [c, f1, f2], ); }, get_func_decl_id: function (c: Z3_context, f: Z3_func_decl): unsigned { let ret = Mod.ccall( 'Z3_get_func_decl_id', 'number', ['number', 'number'], [c, f], ); ret = new Uint32Array([ret])[0]; return ret; }, get_decl_name: Mod._Z3_get_decl_name as ( c: Z3_context, d: Z3_func_decl, ) => Z3_symbol, get_decl_kind: Mod._Z3_get_decl_kind as ( c: Z3_context, d: Z3_func_decl, ) => Z3_decl_kind, get_domain_size: function (c: Z3_context, d: Z3_func_decl): unsigned { let ret = Mod.ccall( 'Z3_get_domain_size', 'number', ['number', 'number'], [c, d], ); ret = new Uint32Array([ret])[0]; return ret; }, get_arity: function (c: Z3_context, d: Z3_func_decl): unsigned { let ret = Mod.ccall( 'Z3_get_arity', 'number', ['number', 'number'], [c, d], ); ret = new Uint32Array([ret])[0]; return ret; }, get_domain: Mod._Z3_get_domain as ( c: Z3_context, d: Z3_func_decl, i: unsigned, ) => Z3_sort, get_range: Mod._Z3_get_range as ( c: Z3_context, d: Z3_func_decl, ) => Z3_sort, get_decl_num_parameters: function ( c: Z3_context, d: Z3_func_decl, ): unsigned { let ret = Mod.ccall( 'Z3_get_decl_num_parameters', 'number', ['number', 'number'], [c, d], ); ret = new Uint32Array([ret])[0]; return ret; }, get_decl_parameter_kind: Mod._Z3_get_decl_parameter_kind as ( c: Z3_context, d: Z3_func_decl, idx: unsigned, ) => Z3_parameter_kind, get_decl_int_parameter: Mod._Z3_get_decl_int_parameter as ( c: Z3_context, d: Z3_func_decl, idx: unsigned, ) => int, get_decl_double_parameter: Mod._Z3_get_decl_double_parameter as ( c: Z3_context, d: Z3_func_decl, idx: unsigned, ) => double, get_decl_symbol_parameter: Mod._Z3_get_decl_symbol_parameter as ( c: Z3_context, d: Z3_func_decl, idx: unsigned, ) => Z3_symbol, get_decl_sort_parameter: Mod._Z3_get_decl_sort_parameter as ( c: Z3_context, d: Z3_func_decl, idx: unsigned, ) => Z3_sort, get_decl_ast_parameter: Mod._Z3_get_decl_ast_parameter as ( c: Z3_context, d: Z3_func_decl, idx: unsigned, ) => Z3_ast, get_decl_func_decl_parameter: Mod._Z3_get_decl_func_decl_parameter as ( c: Z3_context, d: Z3_func_decl, idx: unsigned, ) => Z3_func_decl, get_decl_rational_parameter: function ( c: Z3_context, d: Z3_func_decl, idx: unsigned, ): string { return Mod.ccall( 'Z3_get_decl_rational_parameter', 'string', ['number', 'number', 'number'], [c, d, idx], ); }, app_to_ast: Mod._Z3_app_to_ast as (c: Z3_context, a: Z3_app) => Z3_ast, get_app_decl: Mod._Z3_get_app_decl as ( c: Z3_context, a: Z3_app, ) => Z3_func_decl, get_app_num_args: function (c: Z3_context, a: Z3_app): unsigned { let ret = Mod.ccall( 'Z3_get_app_num_args', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, get_app_arg: Mod._Z3_get_app_arg as ( c: Z3_context, a: Z3_app, i: unsigned, ) => Z3_ast, is_eq_ast: function (c: Z3_context, t1: Z3_ast, t2: Z3_ast): boolean { return Mod.ccall( 'Z3_is_eq_ast', 'boolean', ['number', 'number', 'number'], [c, t1, t2], ); }, get_ast_id: function (c: Z3_context, t: Z3_ast): unsigned { let ret = Mod.ccall( 'Z3_get_ast_id', 'number', ['number', 'number'], [c, t], ); ret = new Uint32Array([ret])[0]; return ret; }, get_ast_hash: function (c: Z3_context, a: Z3_ast): unsigned { let ret = Mod.ccall( 'Z3_get_ast_hash', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, get_sort: Mod._Z3_get_sort as (c: Z3_context, a: Z3_ast) => Z3_sort, is_well_sorted: function (c: Z3_context, t: Z3_ast): boolean { return Mod.ccall( 'Z3_is_well_sorted', 'boolean', ['number', 'number'], [c, t], ); }, get_bool_value: Mod._Z3_get_bool_value as ( c: Z3_context, a: Z3_ast, ) => Z3_lbool, get_ast_kind: Mod._Z3_get_ast_kind as ( c: Z3_context, a: Z3_ast, ) => Z3_ast_kind, is_app: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall('Z3_is_app', 'boolean', ['number', 'number'], [c, a]); }, is_ground: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_is_ground', 'boolean', ['number', 'number'], [c, a], ); }, get_depth: function (c: Z3_context, a: Z3_ast): unsigned { let ret = Mod.ccall( 'Z3_get_depth', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, is_numeral_ast: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_is_numeral_ast', 'boolean', ['number', 'number'], [c, a], ); }, is_algebraic_number: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_is_algebraic_number', 'boolean', ['number', 'number'], [c, a], ); }, to_app: Mod._Z3_to_app as (c: Z3_context, a: Z3_ast) => Z3_app, to_func_decl: Mod._Z3_to_func_decl as ( c: Z3_context, a: Z3_ast, ) => Z3_func_decl, get_numeral_string: function (c: Z3_context, a: Z3_ast): string { return Mod.ccall( 'Z3_get_numeral_string', 'string', ['number', 'number'], [c, a], ); }, get_numeral_binary_string: function (c: Z3_context, a: Z3_ast): string { return Mod.ccall( 'Z3_get_numeral_binary_string', 'string', ['number', 'number'], [c, a], ); }, get_numeral_decimal_string: function ( c: Z3_context, a: Z3_ast, precision: unsigned, ): string { return Mod.ccall( 'Z3_get_numeral_decimal_string', 'string', ['number', 'number', 'number'], [c, a, precision], ); }, get_numeral_double: Mod._Z3_get_numeral_double as ( c: Z3_context, a: Z3_ast, ) => double, get_numerator: Mod._Z3_get_numerator as ( c: Z3_context, a: Z3_ast, ) => Z3_ast, get_denominator: Mod._Z3_get_denominator as ( c: Z3_context, a: Z3_ast, ) => Z3_ast, get_numeral_small: function ( c: Z3_context, a: Z3_ast, ): { num: int64_t; den: int64_t } | null { let ret = Mod.ccall( 'Z3_get_numeral_small', 'boolean', ['number', 'number', 'number', 'number'], [c, a, outAddress, outAddress + 8], ); if (!ret) { return null; } return { num: getOutInt64(0), den: getOutInt64(1) }; }, get_numeral_int: function (c: Z3_context, v: Z3_ast): int | null { let ret = Mod.ccall( 'Z3_get_numeral_int', 'boolean', ['number', 'number', 'number'], [c, v, outAddress], ); if (!ret) { return null; } return getOutInt(0); }, get_numeral_uint: function (c: Z3_context, v: Z3_ast): unsigned | null { let ret = Mod.ccall( 'Z3_get_numeral_uint', 'boolean', ['number', 'number', 'number'], [c, v, outAddress], ); if (!ret) { return null; } return getOutUint(0); }, get_numeral_uint64: function (c: Z3_context, v: Z3_ast): uint64_t | null { let ret = Mod.ccall( 'Z3_get_numeral_uint64', 'boolean', ['number', 'number', 'number'], [c, v, outAddress], ); if (!ret) { return null; } return getOutUint64(0); }, get_numeral_int64: function (c: Z3_context, v: Z3_ast): int64_t | null { let ret = Mod.ccall( 'Z3_get_numeral_int64', 'boolean', ['number', 'number', 'number'], [c, v, outAddress], ); if (!ret) { return null; } return getOutInt64(0); }, get_numeral_rational_int64: function ( c: Z3_context, v: Z3_ast, ): { num: int64_t; den: int64_t } | null { let ret = Mod.ccall( 'Z3_get_numeral_rational_int64', 'boolean', ['number', 'number', 'number', 'number'], [c, v, outAddress, outAddress + 8], ); if (!ret) { return null; } return { num: getOutInt64(0), den: getOutInt64(1) }; }, get_algebraic_number_lower: Mod._Z3_get_algebraic_number_lower as ( c: Z3_context, a: Z3_ast, precision: unsigned, ) => Z3_ast, get_algebraic_number_upper: Mod._Z3_get_algebraic_number_upper as ( c: Z3_context, a: Z3_ast, precision: unsigned, ) => Z3_ast, pattern_to_ast: Mod._Z3_pattern_to_ast as ( c: Z3_context, p: Z3_pattern, ) => Z3_ast, get_pattern_num_terms: function (c: Z3_context, p: Z3_pattern): unsigned { let ret = Mod.ccall( 'Z3_get_pattern_num_terms', 'number', ['number', 'number'], [c, p], ); ret = new Uint32Array([ret])[0]; return ret; }, get_pattern: Mod._Z3_get_pattern as ( c: Z3_context, p: Z3_pattern, idx: unsigned, ) => Z3_ast, get_index_value: function (c: Z3_context, a: Z3_ast): unsigned { let ret = Mod.ccall( 'Z3_get_index_value', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, is_quantifier_forall: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_is_quantifier_forall', 'boolean', ['number', 'number'], [c, a], ); }, is_quantifier_exists: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_is_quantifier_exists', 'boolean', ['number', 'number'], [c, a], ); }, is_lambda: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_is_lambda', 'boolean', ['number', 'number'], [c, a], ); }, get_quantifier_weight: function (c: Z3_context, a: Z3_ast): unsigned { let ret = Mod.ccall( 'Z3_get_quantifier_weight', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, get_quantifier_skolem_id: Mod._Z3_get_quantifier_skolem_id as ( c: Z3_context, a: Z3_ast, ) => Z3_symbol, get_quantifier_id: Mod._Z3_get_quantifier_id as ( c: Z3_context, a: Z3_ast, ) => Z3_symbol, get_quantifier_num_patterns: function ( c: Z3_context, a: Z3_ast, ): unsigned { let ret = Mod.ccall( 'Z3_get_quantifier_num_patterns', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, get_quantifier_pattern_ast: Mod._Z3_get_quantifier_pattern_ast as ( c: Z3_context, a: Z3_ast, i: unsigned, ) => Z3_pattern, get_quantifier_num_no_patterns: function ( c: Z3_context, a: Z3_ast, ): unsigned { let ret = Mod.ccall( 'Z3_get_quantifier_num_no_patterns', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, get_quantifier_no_pattern_ast: Mod._Z3_get_quantifier_no_pattern_ast as ( c: Z3_context, a: Z3_ast, i: unsigned, ) => Z3_ast, get_quantifier_num_bound: function (c: Z3_context, a: Z3_ast): unsigned { let ret = Mod.ccall( 'Z3_get_quantifier_num_bound', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, get_quantifier_bound_name: Mod._Z3_get_quantifier_bound_name as ( c: Z3_context, a: Z3_ast, i: unsigned, ) => Z3_symbol, get_quantifier_bound_sort: Mod._Z3_get_quantifier_bound_sort as ( c: Z3_context, a: Z3_ast, i: unsigned, ) => Z3_sort, get_quantifier_body: Mod._Z3_get_quantifier_body as ( c: Z3_context, a: Z3_ast, ) => Z3_ast, simplify: function (c: Z3_context, a: Z3_ast): Promise { return Mod.async_call(Mod._async_Z3_simplify, c, a); }, simplify_ex: function ( c: Z3_context, a: Z3_ast, p: Z3_params, ): Promise { return Mod.async_call(Mod._async_Z3_simplify_ex, c, a, p); }, simplify_get_help: function (c: Z3_context): string { return Mod.ccall('Z3_simplify_get_help', 'string', ['number'], [c]); }, simplify_get_param_descrs: Mod._Z3_simplify_get_param_descrs as ( c: Z3_context, ) => Z3_param_descrs, update_term: function (c: Z3_context, a: Z3_ast, args: Z3_ast[]): Z3_ast { return Mod.ccall( 'Z3_update_term', 'number', ['number', 'number', 'number', 'array'], [c, a, args.length, intArrayToByteArr(args as unknown as number[])], ); }, substitute: function ( c: Z3_context, a: Z3_ast, from: Z3_ast[], to: Z3_ast[], ): Z3_ast { if (from.length !== to.length) { throw new TypeError( `from and to must be the same length (got ${from.length} and {to.length})`, ); } return Mod.ccall( 'Z3_substitute', 'number', ['number', 'number', 'number', 'array', 'array'], [ c, a, from.length, intArrayToByteArr(from as unknown as number[]), intArrayToByteArr(to as unknown as number[]), ], ); }, substitute_vars: function ( c: Z3_context, a: Z3_ast, to: Z3_ast[], ): Z3_ast { return Mod.ccall( 'Z3_substitute_vars', 'number', ['number', 'number', 'number', 'array'], [c, a, to.length, intArrayToByteArr(to as unknown as number[])], ); }, substitute_funs: function ( c: Z3_context, a: Z3_ast, from: Z3_func_decl[], to: Z3_ast[], ): Z3_ast { if (from.length !== to.length) { throw new TypeError( `from and to must be the same length (got ${from.length} and {to.length})`, ); } return Mod.ccall( 'Z3_substitute_funs', 'number', ['number', 'number', 'number', 'array', 'array'], [ c, a, from.length, intArrayToByteArr(from as unknown as number[]), intArrayToByteArr(to as unknown as number[]), ], ); }, translate: Mod._Z3_translate as ( source: Z3_context, a: Z3_ast, target: Z3_context, ) => Z3_ast, mk_model: Mod._Z3_mk_model as (c: Z3_context) => Z3_model, model_inc_ref: Mod._Z3_model_inc_ref as ( c: Z3_context, m: Z3_model, ) => void, model_dec_ref: Mod._Z3_model_dec_ref as ( c: Z3_context, m: Z3_model, ) => void, model_eval: function ( c: Z3_context, m: Z3_model, t: Z3_ast, model_completion: boolean, ): Z3_ast | null { let ret = Mod.ccall( 'Z3_model_eval', 'boolean', ['number', 'number', 'number', 'boolean', 'number'], [c, m, t, model_completion, outAddress], ); if (!ret) { return null; } return getOutUint(0) as unknown as Z3_ast; }, model_get_const_interp: Mod._Z3_model_get_const_interp as ( c: Z3_context, m: Z3_model, a: Z3_func_decl, ) => Z3_ast, model_has_interp: function ( c: Z3_context, m: Z3_model, a: Z3_func_decl, ): boolean { return Mod.ccall( 'Z3_model_has_interp', 'boolean', ['number', 'number', 'number'], [c, m, a], ); }, model_get_func_interp: Mod._Z3_model_get_func_interp as ( c: Z3_context, m: Z3_model, f: Z3_func_decl, ) => Z3_func_interp, model_get_num_consts: function (c: Z3_context, m: Z3_model): unsigned { let ret = Mod.ccall( 'Z3_model_get_num_consts', 'number', ['number', 'number'], [c, m], ); ret = new Uint32Array([ret])[0]; return ret; }, model_get_const_decl: Mod._Z3_model_get_const_decl as ( c: Z3_context, m: Z3_model, i: unsigned, ) => Z3_func_decl, model_get_num_funcs: function (c: Z3_context, m: Z3_model): unsigned { let ret = Mod.ccall( 'Z3_model_get_num_funcs', 'number', ['number', 'number'], [c, m], ); ret = new Uint32Array([ret])[0]; return ret; }, model_get_func_decl: Mod._Z3_model_get_func_decl as ( c: Z3_context, m: Z3_model, i: unsigned, ) => Z3_func_decl, model_get_num_sorts: function (c: Z3_context, m: Z3_model): unsigned { let ret = Mod.ccall( 'Z3_model_get_num_sorts', 'number', ['number', 'number'], [c, m], ); ret = new Uint32Array([ret])[0]; return ret; }, model_get_sort: Mod._Z3_model_get_sort as ( c: Z3_context, m: Z3_model, i: unsigned, ) => Z3_sort, model_get_sort_universe: Mod._Z3_model_get_sort_universe as ( c: Z3_context, m: Z3_model, s: Z3_sort, ) => Z3_ast_vector, model_translate: Mod._Z3_model_translate as ( c: Z3_context, m: Z3_model, dst: Z3_context, ) => Z3_model, is_as_array: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_is_as_array', 'boolean', ['number', 'number'], [c, a], ); }, get_as_array_func_decl: Mod._Z3_get_as_array_func_decl as ( c: Z3_context, a: Z3_ast, ) => Z3_func_decl, add_func_interp: Mod._Z3_add_func_interp as ( c: Z3_context, m: Z3_model, f: Z3_func_decl, default_value: Z3_ast, ) => Z3_func_interp, add_const_interp: Mod._Z3_add_const_interp as ( c: Z3_context, m: Z3_model, f: Z3_func_decl, a: Z3_ast, ) => void, func_interp_inc_ref: Mod._Z3_func_interp_inc_ref as ( c: Z3_context, f: Z3_func_interp, ) => void, func_interp_dec_ref: Mod._Z3_func_interp_dec_ref as ( c: Z3_context, f: Z3_func_interp, ) => void, func_interp_get_num_entries: function ( c: Z3_context, f: Z3_func_interp, ): unsigned { let ret = Mod.ccall( 'Z3_func_interp_get_num_entries', 'number', ['number', 'number'], [c, f], ); ret = new Uint32Array([ret])[0]; return ret; }, func_interp_get_entry: Mod._Z3_func_interp_get_entry as ( c: Z3_context, f: Z3_func_interp, i: unsigned, ) => Z3_func_entry, func_interp_get_else: Mod._Z3_func_interp_get_else as ( c: Z3_context, f: Z3_func_interp, ) => Z3_ast, func_interp_set_else: Mod._Z3_func_interp_set_else as ( c: Z3_context, f: Z3_func_interp, else_value: Z3_ast, ) => void, func_interp_get_arity: function ( c: Z3_context, f: Z3_func_interp, ): unsigned { let ret = Mod.ccall( 'Z3_func_interp_get_arity', 'number', ['number', 'number'], [c, f], ); ret = new Uint32Array([ret])[0]; return ret; }, func_interp_add_entry: Mod._Z3_func_interp_add_entry as ( c: Z3_context, fi: Z3_func_interp, args: Z3_ast_vector, value: Z3_ast, ) => void, func_entry_inc_ref: Mod._Z3_func_entry_inc_ref as ( c: Z3_context, e: Z3_func_entry, ) => void, func_entry_dec_ref: Mod._Z3_func_entry_dec_ref as ( c: Z3_context, e: Z3_func_entry, ) => void, func_entry_get_value: Mod._Z3_func_entry_get_value as ( c: Z3_context, e: Z3_func_entry, ) => Z3_ast, func_entry_get_num_args: function ( c: Z3_context, e: Z3_func_entry, ): unsigned { let ret = Mod.ccall( 'Z3_func_entry_get_num_args', 'number', ['number', 'number'], [c, e], ); ret = new Uint32Array([ret])[0]; return ret; }, func_entry_get_arg: Mod._Z3_func_entry_get_arg as ( c: Z3_context, e: Z3_func_entry, i: unsigned, ) => Z3_ast, open_log: function (filename: string): boolean { return Mod.ccall('Z3_open_log', 'boolean', ['string'], [filename]); }, append_log: function (string: string): void { return Mod.ccall('Z3_append_log', 'void', ['string'], [string]); }, close_log: Mod._Z3_close_log as () => void, toggle_warning_messages: Mod._Z3_toggle_warning_messages as ( enabled: boolean, ) => void, set_ast_print_mode: Mod._Z3_set_ast_print_mode as ( c: Z3_context, mode: Z3_ast_print_mode, ) => void, ast_to_string: function (c: Z3_context, a: Z3_ast): string { return Mod.ccall( 'Z3_ast_to_string', 'string', ['number', 'number'], [c, a], ); }, pattern_to_string: function (c: Z3_context, p: Z3_pattern): string { return Mod.ccall( 'Z3_pattern_to_string', 'string', ['number', 'number'], [c, p], ); }, sort_to_string: function (c: Z3_context, s: Z3_sort): string { return Mod.ccall( 'Z3_sort_to_string', 'string', ['number', 'number'], [c, s], ); }, func_decl_to_string: function (c: Z3_context, d: Z3_func_decl): string { return Mod.ccall( 'Z3_func_decl_to_string', 'string', ['number', 'number'], [c, d], ); }, model_to_string: function (c: Z3_context, m: Z3_model): string { return Mod.ccall( 'Z3_model_to_string', 'string', ['number', 'number'], [c, m], ); }, benchmark_to_smtlib_string: function ( c: Z3_context, name: string, logic: string, status: string, attributes: string, assumptions: Z3_ast[], formula: Z3_ast, ): string { return Mod.ccall( 'Z3_benchmark_to_smtlib_string', 'string', [ 'number', 'string', 'string', 'string', 'string', 'number', 'array', 'number', ], [ c, name, logic, status, attributes, assumptions.length, intArrayToByteArr(assumptions as unknown as number[]), formula, ], ); }, parse_smtlib2_string: function ( c: Z3_context, str: string, sort_names: Z3_symbol[], sorts: Z3_sort[], decl_names: Z3_symbol[], decls: Z3_func_decl[], ): Z3_ast_vector { if (sort_names.length !== sorts.length) { throw new TypeError( `sort_names and sorts must be the same length (got ${sort_names.length} and {sorts.length})`, ); } if (decl_names.length !== decls.length) { throw new TypeError( `decl_names and decls must be the same length (got ${decl_names.length} and {decls.length})`, ); } return Mod.ccall( 'Z3_parse_smtlib2_string', 'number', [ 'number', 'string', 'number', 'array', 'array', 'number', 'array', 'array', ], [ c, str, sort_names.length, intArrayToByteArr(sort_names as unknown as number[]), intArrayToByteArr(sorts as unknown as number[]), decl_names.length, intArrayToByteArr(decl_names as unknown as number[]), intArrayToByteArr(decls as unknown as number[]), ], ); }, parse_smtlib2_file: function ( c: Z3_context, file_name: string, sort_names: Z3_symbol[], sorts: Z3_sort[], decl_names: Z3_symbol[], decls: Z3_func_decl[], ): Z3_ast_vector { if (sort_names.length !== sorts.length) { throw new TypeError( `sort_names and sorts must be the same length (got ${sort_names.length} and {sorts.length})`, ); } if (decl_names.length !== decls.length) { throw new TypeError( `decl_names and decls must be the same length (got ${decl_names.length} and {decls.length})`, ); } return Mod.ccall( 'Z3_parse_smtlib2_file', 'number', [ 'number', 'string', 'number', 'array', 'array', 'number', 'array', 'array', ], [ c, file_name, sort_names.length, intArrayToByteArr(sort_names as unknown as number[]), intArrayToByteArr(sorts as unknown as number[]), decl_names.length, intArrayToByteArr(decl_names as unknown as number[]), intArrayToByteArr(decls as unknown as number[]), ], ); }, eval_smtlib2_string: async function ( c: Z3_context, str: string, ): Promise { return await Mod.async_call(() => Mod.ccall( 'async_Z3_eval_smtlib2_string', 'void', ['number', 'string'], [c, str], ), ); }, mk_parser_context: Mod._Z3_mk_parser_context as ( c: Z3_context, ) => Z3_parser_context, parser_context_inc_ref: Mod._Z3_parser_context_inc_ref as ( c: Z3_context, pc: Z3_parser_context, ) => void, parser_context_dec_ref: Mod._Z3_parser_context_dec_ref as ( c: Z3_context, pc: Z3_parser_context, ) => void, parser_context_add_sort: Mod._Z3_parser_context_add_sort as ( c: Z3_context, pc: Z3_parser_context, s: Z3_sort, ) => void, parser_context_add_decl: Mod._Z3_parser_context_add_decl as ( c: Z3_context, pc: Z3_parser_context, f: Z3_func_decl, ) => void, parser_context_from_string: function ( c: Z3_context, pc: Z3_parser_context, s: string, ): Z3_ast_vector { return Mod.ccall( 'Z3_parser_context_from_string', 'number', ['number', 'number', 'string'], [c, pc, s], ); }, get_error_code: Mod._Z3_get_error_code as ( c: Z3_context, ) => Z3_error_code, set_error: Mod._Z3_set_error as (c: Z3_context, e: Z3_error_code) => void, get_error_msg: function (c: Z3_context, err: Z3_error_code): string { return Mod.ccall( 'Z3_get_error_msg', 'string', ['number', 'number'], [c, err], ); }, get_version: function (): { major: unsigned; minor: unsigned; build_number: unsigned; revision_number: unsigned; } { let ret = Mod.ccall( 'Z3_get_version', 'void', ['number', 'number', 'number', 'number'], [outAddress, outAddress + 4, outAddress + 8, outAddress + 12], ); return { major: getOutUint(0), minor: getOutUint(1), build_number: getOutUint(2), revision_number: getOutUint(3), }; }, get_full_version: function (): string { return Mod.ccall('Z3_get_full_version', 'string', [], []); }, enable_trace: function (tag: string): void { return Mod.ccall('Z3_enable_trace', 'void', ['string'], [tag]); }, disable_trace: function (tag: string): void { return Mod.ccall('Z3_disable_trace', 'void', ['string'], [tag]); }, reset_memory: Mod._Z3_reset_memory as () => void, finalize_memory: Mod._Z3_finalize_memory as () => void, mk_goal: Mod._Z3_mk_goal as ( c: Z3_context, models: boolean, unsat_cores: boolean, proofs: boolean, ) => Z3_goal, goal_inc_ref: Mod._Z3_goal_inc_ref as (c: Z3_context, g: Z3_goal) => void, goal_dec_ref: Mod._Z3_goal_dec_ref as (c: Z3_context, g: Z3_goal) => void, goal_precision: Mod._Z3_goal_precision as ( c: Z3_context, g: Z3_goal, ) => Z3_goal_prec, goal_assert: Mod._Z3_goal_assert as ( c: Z3_context, g: Z3_goal, a: Z3_ast, ) => void, goal_inconsistent: function (c: Z3_context, g: Z3_goal): boolean { return Mod.ccall( 'Z3_goal_inconsistent', 'boolean', ['number', 'number'], [c, g], ); }, goal_depth: function (c: Z3_context, g: Z3_goal): unsigned { let ret = Mod.ccall( 'Z3_goal_depth', 'number', ['number', 'number'], [c, g], ); ret = new Uint32Array([ret])[0]; return ret; }, goal_reset: Mod._Z3_goal_reset as (c: Z3_context, g: Z3_goal) => void, goal_size: function (c: Z3_context, g: Z3_goal): unsigned { let ret = Mod.ccall( 'Z3_goal_size', 'number', ['number', 'number'], [c, g], ); ret = new Uint32Array([ret])[0]; return ret; }, goal_formula: Mod._Z3_goal_formula as ( c: Z3_context, g: Z3_goal, idx: unsigned, ) => Z3_ast, goal_num_exprs: function (c: Z3_context, g: Z3_goal): unsigned { let ret = Mod.ccall( 'Z3_goal_num_exprs', 'number', ['number', 'number'], [c, g], ); ret = new Uint32Array([ret])[0]; return ret; }, goal_is_decided_sat: function (c: Z3_context, g: Z3_goal): boolean { return Mod.ccall( 'Z3_goal_is_decided_sat', 'boolean', ['number', 'number'], [c, g], ); }, goal_is_decided_unsat: function (c: Z3_context, g: Z3_goal): boolean { return Mod.ccall( 'Z3_goal_is_decided_unsat', 'boolean', ['number', 'number'], [c, g], ); }, goal_translate: Mod._Z3_goal_translate as ( source: Z3_context, g: Z3_goal, target: Z3_context, ) => Z3_goal, goal_convert_model: Mod._Z3_goal_convert_model as ( c: Z3_context, g: Z3_goal, m: Z3_model, ) => Z3_model, goal_to_string: function (c: Z3_context, g: Z3_goal): string { return Mod.ccall( 'Z3_goal_to_string', 'string', ['number', 'number'], [c, g], ); }, goal_to_dimacs_string: function ( c: Z3_context, g: Z3_goal, include_names: boolean, ): string { return Mod.ccall( 'Z3_goal_to_dimacs_string', 'string', ['number', 'number', 'boolean'], [c, g, include_names], ); }, mk_tactic: function (c: Z3_context, name: string): Z3_tactic { return Mod.ccall( 'Z3_mk_tactic', 'number', ['number', 'string'], [c, name], ); }, tactic_inc_ref: Mod._Z3_tactic_inc_ref as ( c: Z3_context, t: Z3_tactic, ) => void, tactic_dec_ref: Mod._Z3_tactic_dec_ref as ( c: Z3_context, g: Z3_tactic, ) => void, mk_probe: function (c: Z3_context, name: string): Z3_probe { return Mod.ccall( 'Z3_mk_probe', 'number', ['number', 'string'], [c, name], ); }, probe_inc_ref: Mod._Z3_probe_inc_ref as ( c: Z3_context, p: Z3_probe, ) => void, probe_dec_ref: Mod._Z3_probe_dec_ref as ( c: Z3_context, p: Z3_probe, ) => void, tactic_and_then: Mod._Z3_tactic_and_then as ( c: Z3_context, t1: Z3_tactic, t2: Z3_tactic, ) => Z3_tactic, tactic_or_else: Mod._Z3_tactic_or_else as ( c: Z3_context, t1: Z3_tactic, t2: Z3_tactic, ) => Z3_tactic, tactic_par_or: function (c: Z3_context, ts: Z3_tactic[]): Z3_tactic { return Mod.ccall( 'Z3_tactic_par_or', 'number', ['number', 'number', 'array'], [c, ts.length, intArrayToByteArr(ts as unknown as number[])], ); }, tactic_par_and_then: Mod._Z3_tactic_par_and_then as ( c: Z3_context, t1: Z3_tactic, t2: Z3_tactic, ) => Z3_tactic, tactic_try_for: Mod._Z3_tactic_try_for as ( c: Z3_context, t: Z3_tactic, ms: unsigned, ) => Z3_tactic, tactic_when: Mod._Z3_tactic_when as ( c: Z3_context, p: Z3_probe, t: Z3_tactic, ) => Z3_tactic, tactic_cond: Mod._Z3_tactic_cond as ( c: Z3_context, p: Z3_probe, t1: Z3_tactic, t2: Z3_tactic, ) => Z3_tactic, tactic_repeat: Mod._Z3_tactic_repeat as ( c: Z3_context, t: Z3_tactic, max: unsigned, ) => Z3_tactic, tactic_skip: Mod._Z3_tactic_skip as (c: Z3_context) => Z3_tactic, tactic_fail: Mod._Z3_tactic_fail as (c: Z3_context) => Z3_tactic, tactic_fail_if: Mod._Z3_tactic_fail_if as ( c: Z3_context, p: Z3_probe, ) => Z3_tactic, tactic_fail_if_not_decided: Mod._Z3_tactic_fail_if_not_decided as ( c: Z3_context, ) => Z3_tactic, tactic_using_params: Mod._Z3_tactic_using_params as ( c: Z3_context, t: Z3_tactic, p: Z3_params, ) => Z3_tactic, mk_simplifier: function (c: Z3_context, name: string): Z3_simplifier { return Mod.ccall( 'Z3_mk_simplifier', 'number', ['number', 'string'], [c, name], ); }, simplifier_inc_ref: Mod._Z3_simplifier_inc_ref as ( c: Z3_context, t: Z3_simplifier, ) => void, simplifier_dec_ref: Mod._Z3_simplifier_dec_ref as ( c: Z3_context, g: Z3_simplifier, ) => void, solver_add_simplifier: Mod._Z3_solver_add_simplifier as ( c: Z3_context, solver: Z3_solver, simplifier: Z3_simplifier, ) => Z3_solver, simplifier_and_then: Mod._Z3_simplifier_and_then as ( c: Z3_context, t1: Z3_simplifier, t2: Z3_simplifier, ) => Z3_simplifier, simplifier_using_params: Mod._Z3_simplifier_using_params as ( c: Z3_context, t: Z3_simplifier, p: Z3_params, ) => Z3_simplifier, get_num_simplifiers: function (c: Z3_context): unsigned { let ret = Mod.ccall( 'Z3_get_num_simplifiers', 'number', ['number'], [c], ); ret = new Uint32Array([ret])[0]; return ret; }, get_simplifier_name: function (c: Z3_context, i: unsigned): string { return Mod.ccall( 'Z3_get_simplifier_name', 'string', ['number', 'number'], [c, i], ); }, simplifier_get_help: function (c: Z3_context, t: Z3_simplifier): string { return Mod.ccall( 'Z3_simplifier_get_help', 'string', ['number', 'number'], [c, t], ); }, simplifier_get_param_descrs: Mod._Z3_simplifier_get_param_descrs as ( c: Z3_context, t: Z3_simplifier, ) => Z3_param_descrs, simplifier_get_descr: function (c: Z3_context, name: string): string { return Mod.ccall( 'Z3_simplifier_get_descr', 'string', ['number', 'string'], [c, name], ); }, probe_const: Mod._Z3_probe_const as ( x: Z3_context, val: double, ) => Z3_probe, probe_lt: Mod._Z3_probe_lt as ( x: Z3_context, p1: Z3_probe, p2: Z3_probe, ) => Z3_probe, probe_gt: Mod._Z3_probe_gt as ( x: Z3_context, p1: Z3_probe, p2: Z3_probe, ) => Z3_probe, probe_le: Mod._Z3_probe_le as ( x: Z3_context, p1: Z3_probe, p2: Z3_probe, ) => Z3_probe, probe_ge: Mod._Z3_probe_ge as ( x: Z3_context, p1: Z3_probe, p2: Z3_probe, ) => Z3_probe, probe_eq: Mod._Z3_probe_eq as ( x: Z3_context, p1: Z3_probe, p2: Z3_probe, ) => Z3_probe, probe_and: Mod._Z3_probe_and as ( x: Z3_context, p1: Z3_probe, p2: Z3_probe, ) => Z3_probe, probe_or: Mod._Z3_probe_or as ( x: Z3_context, p1: Z3_probe, p2: Z3_probe, ) => Z3_probe, probe_not: Mod._Z3_probe_not as (x: Z3_context, p: Z3_probe) => Z3_probe, get_num_tactics: function (c: Z3_context): unsigned { let ret = Mod.ccall('Z3_get_num_tactics', 'number', ['number'], [c]); ret = new Uint32Array([ret])[0]; return ret; }, get_tactic_name: function (c: Z3_context, i: unsigned): string { return Mod.ccall( 'Z3_get_tactic_name', 'string', ['number', 'number'], [c, i], ); }, get_num_probes: function (c: Z3_context): unsigned { let ret = Mod.ccall('Z3_get_num_probes', 'number', ['number'], [c]); ret = new Uint32Array([ret])[0]; return ret; }, get_probe_name: function (c: Z3_context, i: unsigned): string { return Mod.ccall( 'Z3_get_probe_name', 'string', ['number', 'number'], [c, i], ); }, tactic_get_help: function (c: Z3_context, t: Z3_tactic): string { return Mod.ccall( 'Z3_tactic_get_help', 'string', ['number', 'number'], [c, t], ); }, tactic_get_param_descrs: Mod._Z3_tactic_get_param_descrs as ( c: Z3_context, t: Z3_tactic, ) => Z3_param_descrs, tactic_get_descr: function (c: Z3_context, name: string): string { return Mod.ccall( 'Z3_tactic_get_descr', 'string', ['number', 'string'], [c, name], ); }, probe_get_descr: function (c: Z3_context, name: string): string { return Mod.ccall( 'Z3_probe_get_descr', 'string', ['number', 'string'], [c, name], ); }, probe_apply: Mod._Z3_probe_apply as ( c: Z3_context, p: Z3_probe, g: Z3_goal, ) => double, tactic_apply: function ( c: Z3_context, t: Z3_tactic, g: Z3_goal, ): Promise { return Mod.async_call(Mod._async_Z3_tactic_apply, c, t, g); }, tactic_apply_ex: function ( c: Z3_context, t: Z3_tactic, g: Z3_goal, p: Z3_params, ): Promise { return Mod.async_call(Mod._async_Z3_tactic_apply_ex, c, t, g, p); }, apply_result_inc_ref: Mod._Z3_apply_result_inc_ref as ( c: Z3_context, r: Z3_apply_result, ) => void, apply_result_dec_ref: Mod._Z3_apply_result_dec_ref as ( c: Z3_context, r: Z3_apply_result, ) => void, apply_result_to_string: function ( c: Z3_context, r: Z3_apply_result, ): string { return Mod.ccall( 'Z3_apply_result_to_string', 'string', ['number', 'number'], [c, r], ); }, apply_result_get_num_subgoals: function ( c: Z3_context, r: Z3_apply_result, ): unsigned { let ret = Mod.ccall( 'Z3_apply_result_get_num_subgoals', 'number', ['number', 'number'], [c, r], ); ret = new Uint32Array([ret])[0]; return ret; }, apply_result_get_subgoal: Mod._Z3_apply_result_get_subgoal as ( c: Z3_context, r: Z3_apply_result, i: unsigned, ) => Z3_goal, mk_solver: Mod._Z3_mk_solver as (c: Z3_context) => Z3_solver, mk_simple_solver: Mod._Z3_mk_simple_solver as ( c: Z3_context, ) => Z3_solver, mk_solver_for_logic: Mod._Z3_mk_solver_for_logic as ( c: Z3_context, logic: Z3_symbol, ) => Z3_solver, mk_solver_from_tactic: Mod._Z3_mk_solver_from_tactic as ( c: Z3_context, t: Z3_tactic, ) => Z3_solver, solver_translate: Mod._Z3_solver_translate as ( source: Z3_context, s: Z3_solver, target: Z3_context, ) => Z3_solver, solver_import_model_converter: Mod._Z3_solver_import_model_converter as ( ctx: Z3_context, src: Z3_solver, dst: Z3_solver, ) => void, solver_get_help: function (c: Z3_context, s: Z3_solver): string { return Mod.ccall( 'Z3_solver_get_help', 'string', ['number', 'number'], [c, s], ); }, solver_get_param_descrs: Mod._Z3_solver_get_param_descrs as ( c: Z3_context, s: Z3_solver, ) => Z3_param_descrs, solver_set_params: Mod._Z3_solver_set_params as ( c: Z3_context, s: Z3_solver, p: Z3_params, ) => void, solver_inc_ref: Mod._Z3_solver_inc_ref as ( c: Z3_context, s: Z3_solver, ) => void, solver_dec_ref: Mod._Z3_solver_dec_ref as ( c: Z3_context, s: Z3_solver, ) => void, solver_interrupt: Mod._Z3_solver_interrupt as ( c: Z3_context, s: Z3_solver, ) => void, solver_push: Mod._Z3_solver_push as (c: Z3_context, s: Z3_solver) => void, solver_pop: Mod._Z3_solver_pop as ( c: Z3_context, s: Z3_solver, n: unsigned, ) => void, solver_reset: Mod._Z3_solver_reset as ( c: Z3_context, s: Z3_solver, ) => void, solver_get_num_scopes: function (c: Z3_context, s: Z3_solver): unsigned { let ret = Mod.ccall( 'Z3_solver_get_num_scopes', 'number', ['number', 'number'], [c, s], ); ret = new Uint32Array([ret])[0]; return ret; }, solver_assert: Mod._Z3_solver_assert as ( c: Z3_context, s: Z3_solver, a: Z3_ast, ) => void, solver_assert_and_track: Mod._Z3_solver_assert_and_track as ( c: Z3_context, s: Z3_solver, a: Z3_ast, p: Z3_ast, ) => void, solver_from_file: function ( c: Z3_context, s: Z3_solver, file_name: string, ): void { return Mod.ccall( 'Z3_solver_from_file', 'void', ['number', 'number', 'string'], [c, s, file_name], ); }, solver_from_string: function ( c: Z3_context, s: Z3_solver, str: string, ): void { return Mod.ccall( 'Z3_solver_from_string', 'void', ['number', 'number', 'string'], [c, s, str], ); }, solver_get_assertions: Mod._Z3_solver_get_assertions as ( c: Z3_context, s: Z3_solver, ) => Z3_ast_vector, solver_get_units: Mod._Z3_solver_get_units as ( c: Z3_context, s: Z3_solver, ) => Z3_ast_vector, solver_get_trail: Mod._Z3_solver_get_trail as ( c: Z3_context, s: Z3_solver, ) => Z3_ast_vector, solver_get_non_units: Mod._Z3_solver_get_non_units as ( c: Z3_context, s: Z3_solver, ) => Z3_ast_vector, solver_get_levels: function ( c: Z3_context, s: Z3_solver, literals: Z3_ast_vector, sz: unsigned, ): unsigned[] { let outArray_levels = Mod._malloc(4 * sz); try { let ret = Mod.ccall( 'Z3_solver_get_levels', 'void', ['number', 'number', 'number', 'number', 'number'], [c, s, literals, sz, outArray_levels], ); return readUintArray(outArray_levels, sz); } finally { Mod._free(outArray_levels); } }, solver_congruence_root: Mod._Z3_solver_congruence_root as ( c: Z3_context, s: Z3_solver, a: Z3_ast, ) => Z3_ast, solver_congruence_next: Mod._Z3_solver_congruence_next as ( c: Z3_context, s: Z3_solver, a: Z3_ast, ) => Z3_ast, solver_congruence_explain: Mod._Z3_solver_congruence_explain as ( c: Z3_context, s: Z3_solver, a: Z3_ast, b: Z3_ast, ) => Z3_ast, solver_solve_for: Mod._Z3_solver_solve_for as ( c: Z3_context, s: Z3_solver, variables: Z3_ast_vector, terms: Z3_ast_vector, guards: Z3_ast_vector, ) => void, solver_next_split: function ( c: Z3_context, cb: Z3_solver_callback, t: Z3_ast, idx: unsigned, phase: Z3_lbool, ): boolean { return Mod.ccall( 'Z3_solver_next_split', 'boolean', ['number', 'number', 'number', 'number', 'number'], [c, cb, t, idx, phase], ); }, solver_propagate_declare: function ( c: Z3_context, name: Z3_symbol, domain: Z3_sort[], range: Z3_sort, ): Z3_func_decl { return Mod.ccall( 'Z3_solver_propagate_declare', 'number', ['number', 'number', 'number', 'array', 'number'], [ c, name, domain.length, intArrayToByteArr(domain as unknown as number[]), range, ], ); }, solver_propagate_register: Mod._Z3_solver_propagate_register as ( c: Z3_context, s: Z3_solver, e: Z3_ast, ) => void, solver_propagate_register_cb: Mod._Z3_solver_propagate_register_cb as ( c: Z3_context, cb: Z3_solver_callback, e: Z3_ast, ) => void, solver_propagate_consequence: function ( c: Z3_context, cb: Z3_solver_callback, fixed: Z3_ast[], eq_lhs: Z3_ast[], eq_rhs: Z3_ast[], conseq: Z3_ast, ): boolean { if (eq_lhs.length !== eq_rhs.length) { throw new TypeError( `eq_lhs and eq_rhs must be the same length (got ${eq_lhs.length} and {eq_rhs.length})`, ); } return Mod.ccall( 'Z3_solver_propagate_consequence', 'boolean', [ 'number', 'number', 'number', 'array', 'number', 'array', 'array', 'number', ], [ c, cb, fixed.length, intArrayToByteArr(fixed as unknown as number[]), eq_lhs.length, intArrayToByteArr(eq_lhs as unknown as number[]), intArrayToByteArr(eq_rhs as unknown as number[]), conseq, ], ); }, solver_set_initial_value: Mod._Z3_solver_set_initial_value as ( c: Z3_context, s: Z3_solver, v: Z3_ast, val: Z3_ast, ) => void, solver_check: function (c: Z3_context, s: Z3_solver): Promise { return Mod.async_call(Mod._async_Z3_solver_check, c, s); }, solver_check_assumptions: async function ( c: Z3_context, s: Z3_solver, assumptions: Z3_ast[], ): Promise { const assumptions_ptr = Mod._malloc(assumptions.length * 4); Mod.HEAPU32.set( assumptions as unknown as number[], assumptions_ptr / 4, ); try { let ret = await Mod.async_call(() => Mod.ccall( 'async_Z3_solver_check_assumptions', 'void', ['number', 'number', 'number', 'number'], [c, s, assumptions.length, assumptions_ptr], ), ); return ret; } finally { Mod._free(assumptions_ptr); } }, get_implied_equalities: function ( c: Z3_context, s: Z3_solver, terms: Z3_ast[], ): { rv: Z3_lbool; class_ids: unsigned[] } { let outArray_class_ids = Mod._malloc(4 * terms.length); try { let ret = Mod.ccall( 'Z3_get_implied_equalities', 'number', ['number', 'number', 'number', 'array', 'number'], [ c, s, terms.length, intArrayToByteArr(terms as unknown as number[]), outArray_class_ids, ], ); return { rv: ret, class_ids: readUintArray(outArray_class_ids, terms.length), }; } finally { Mod._free(outArray_class_ids); } }, solver_get_consequences: function ( c: Z3_context, s: Z3_solver, assumptions: Z3_ast_vector, variables: Z3_ast_vector, consequences: Z3_ast_vector, ): Promise { return Mod.async_call( Mod._async_Z3_solver_get_consequences, c, s, assumptions, variables, consequences, ); }, solver_cube: function ( c: Z3_context, s: Z3_solver, vars: Z3_ast_vector, backtrack_level: unsigned, ): Promise { return Mod.async_call( Mod._async_Z3_solver_cube, c, s, vars, backtrack_level, ); }, solver_get_model: Mod._Z3_solver_get_model as ( c: Z3_context, s: Z3_solver, ) => Z3_model, solver_get_proof: Mod._Z3_solver_get_proof as ( c: Z3_context, s: Z3_solver, ) => Z3_ast, solver_get_unsat_core: Mod._Z3_solver_get_unsat_core as ( c: Z3_context, s: Z3_solver, ) => Z3_ast_vector, solver_get_reason_unknown: function ( c: Z3_context, s: Z3_solver, ): string { return Mod.ccall( 'Z3_solver_get_reason_unknown', 'string', ['number', 'number'], [c, s], ); }, solver_get_statistics: Mod._Z3_solver_get_statistics as ( c: Z3_context, s: Z3_solver, ) => Z3_stats, solver_to_string: function (c: Z3_context, s: Z3_solver): string { return Mod.ccall( 'Z3_solver_to_string', 'string', ['number', 'number'], [c, s], ); }, solver_to_dimacs_string: function ( c: Z3_context, s: Z3_solver, include_names: boolean, ): string { return Mod.ccall( 'Z3_solver_to_dimacs_string', 'string', ['number', 'number', 'boolean'], [c, s, include_names], ); }, stats_to_string: function (c: Z3_context, s: Z3_stats): string { return Mod.ccall( 'Z3_stats_to_string', 'string', ['number', 'number'], [c, s], ); }, stats_inc_ref: Mod._Z3_stats_inc_ref as ( c: Z3_context, s: Z3_stats, ) => void, stats_dec_ref: Mod._Z3_stats_dec_ref as ( c: Z3_context, s: Z3_stats, ) => void, stats_size: function (c: Z3_context, s: Z3_stats): unsigned { let ret = Mod.ccall( 'Z3_stats_size', 'number', ['number', 'number'], [c, s], ); ret = new Uint32Array([ret])[0]; return ret; }, stats_get_key: function ( c: Z3_context, s: Z3_stats, idx: unsigned, ): string { return Mod.ccall( 'Z3_stats_get_key', 'string', ['number', 'number', 'number'], [c, s, idx], ); }, stats_is_uint: function ( c: Z3_context, s: Z3_stats, idx: unsigned, ): boolean { return Mod.ccall( 'Z3_stats_is_uint', 'boolean', ['number', 'number', 'number'], [c, s, idx], ); }, stats_is_double: function ( c: Z3_context, s: Z3_stats, idx: unsigned, ): boolean { return Mod.ccall( 'Z3_stats_is_double', 'boolean', ['number', 'number', 'number'], [c, s, idx], ); }, stats_get_uint_value: function ( c: Z3_context, s: Z3_stats, idx: unsigned, ): unsigned { let ret = Mod.ccall( 'Z3_stats_get_uint_value', 'number', ['number', 'number', 'number'], [c, s, idx], ); ret = new Uint32Array([ret])[0]; return ret; }, stats_get_double_value: Mod._Z3_stats_get_double_value as ( c: Z3_context, s: Z3_stats, idx: unsigned, ) => double, get_estimated_alloc_size: Mod._Z3_get_estimated_alloc_size as () => uint64_t, algebraic_is_value: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_algebraic_is_value', 'boolean', ['number', 'number'], [c, a], ); }, algebraic_is_pos: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_algebraic_is_pos', 'boolean', ['number', 'number'], [c, a], ); }, algebraic_is_neg: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_algebraic_is_neg', 'boolean', ['number', 'number'], [c, a], ); }, algebraic_is_zero: function (c: Z3_context, a: Z3_ast): boolean { return Mod.ccall( 'Z3_algebraic_is_zero', 'boolean', ['number', 'number'], [c, a], ); }, algebraic_sign: Mod._Z3_algebraic_sign as ( c: Z3_context, a: Z3_ast, ) => int, algebraic_add: Mod._Z3_algebraic_add as ( c: Z3_context, a: Z3_ast, b: Z3_ast, ) => Z3_ast, algebraic_sub: Mod._Z3_algebraic_sub as ( c: Z3_context, a: Z3_ast, b: Z3_ast, ) => Z3_ast, algebraic_mul: Mod._Z3_algebraic_mul as ( c: Z3_context, a: Z3_ast, b: Z3_ast, ) => Z3_ast, algebraic_div: Mod._Z3_algebraic_div as ( c: Z3_context, a: Z3_ast, b: Z3_ast, ) => Z3_ast, algebraic_root: Mod._Z3_algebraic_root as ( c: Z3_context, a: Z3_ast, k: unsigned, ) => Z3_ast, algebraic_power: Mod._Z3_algebraic_power as ( c: Z3_context, a: Z3_ast, k: unsigned, ) => Z3_ast, algebraic_lt: function (c: Z3_context, a: Z3_ast, b: Z3_ast): boolean { return Mod.ccall( 'Z3_algebraic_lt', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, algebraic_gt: function (c: Z3_context, a: Z3_ast, b: Z3_ast): boolean { return Mod.ccall( 'Z3_algebraic_gt', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, algebraic_le: function (c: Z3_context, a: Z3_ast, b: Z3_ast): boolean { return Mod.ccall( 'Z3_algebraic_le', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, algebraic_ge: function (c: Z3_context, a: Z3_ast, b: Z3_ast): boolean { return Mod.ccall( 'Z3_algebraic_ge', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, algebraic_eq: function (c: Z3_context, a: Z3_ast, b: Z3_ast): boolean { return Mod.ccall( 'Z3_algebraic_eq', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, algebraic_neq: function (c: Z3_context, a: Z3_ast, b: Z3_ast): boolean { return Mod.ccall( 'Z3_algebraic_neq', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, algebraic_roots: async function ( c: Z3_context, p: Z3_ast, a: Z3_ast[], ): Promise { const a_ptr = Mod._malloc(a.length * 4); Mod.HEAPU32.set(a as unknown as number[], a_ptr / 4); try { let ret = await Mod.async_call(() => Mod.ccall( 'async_Z3_algebraic_roots', 'void', ['number', 'number', 'number', 'number'], [c, p, a.length, a_ptr], ), ); return ret; } finally { Mod._free(a_ptr); } }, algebraic_eval: async function ( c: Z3_context, p: Z3_ast, a: Z3_ast[], ): Promise { const a_ptr = Mod._malloc(a.length * 4); Mod.HEAPU32.set(a as unknown as number[], a_ptr / 4); try { let ret = await Mod.async_call(() => Mod.ccall( 'async_Z3_algebraic_eval', 'void', ['number', 'number', 'number', 'number'], [c, p, a.length, a_ptr], ), ); return ret; } finally { Mod._free(a_ptr); } }, algebraic_get_poly: Mod._Z3_algebraic_get_poly as ( c: Z3_context, a: Z3_ast, ) => Z3_ast_vector, algebraic_get_i: function (c: Z3_context, a: Z3_ast): unsigned { let ret = Mod.ccall( 'Z3_algebraic_get_i', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, mk_ast_vector: Mod._Z3_mk_ast_vector as (c: Z3_context) => Z3_ast_vector, ast_vector_inc_ref: Mod._Z3_ast_vector_inc_ref as ( c: Z3_context, v: Z3_ast_vector, ) => void, ast_vector_dec_ref: Mod._Z3_ast_vector_dec_ref as ( c: Z3_context, v: Z3_ast_vector, ) => void, ast_vector_size: function (c: Z3_context, v: Z3_ast_vector): unsigned { let ret = Mod.ccall( 'Z3_ast_vector_size', 'number', ['number', 'number'], [c, v], ); ret = new Uint32Array([ret])[0]; return ret; }, ast_vector_get: Mod._Z3_ast_vector_get as ( c: Z3_context, v: Z3_ast_vector, i: unsigned, ) => Z3_ast, ast_vector_set: Mod._Z3_ast_vector_set as ( c: Z3_context, v: Z3_ast_vector, i: unsigned, a: Z3_ast, ) => void, ast_vector_resize: Mod._Z3_ast_vector_resize as ( c: Z3_context, v: Z3_ast_vector, n: unsigned, ) => void, ast_vector_push: Mod._Z3_ast_vector_push as ( c: Z3_context, v: Z3_ast_vector, a: Z3_ast, ) => void, ast_vector_translate: Mod._Z3_ast_vector_translate as ( s: Z3_context, v: Z3_ast_vector, t: Z3_context, ) => Z3_ast_vector, ast_vector_to_string: function (c: Z3_context, v: Z3_ast_vector): string { return Mod.ccall( 'Z3_ast_vector_to_string', 'string', ['number', 'number'], [c, v], ); }, mk_ast_map: Mod._Z3_mk_ast_map as (c: Z3_context) => Z3_ast_map, ast_map_inc_ref: Mod._Z3_ast_map_inc_ref as ( c: Z3_context, m: Z3_ast_map, ) => void, ast_map_dec_ref: Mod._Z3_ast_map_dec_ref as ( c: Z3_context, m: Z3_ast_map, ) => void, ast_map_contains: function ( c: Z3_context, m: Z3_ast_map, k: Z3_ast, ): boolean { return Mod.ccall( 'Z3_ast_map_contains', 'boolean', ['number', 'number', 'number'], [c, m, k], ); }, ast_map_find: Mod._Z3_ast_map_find as ( c: Z3_context, m: Z3_ast_map, k: Z3_ast, ) => Z3_ast, ast_map_insert: Mod._Z3_ast_map_insert as ( c: Z3_context, m: Z3_ast_map, k: Z3_ast, v: Z3_ast, ) => void, ast_map_erase: Mod._Z3_ast_map_erase as ( c: Z3_context, m: Z3_ast_map, k: Z3_ast, ) => void, ast_map_reset: Mod._Z3_ast_map_reset as ( c: Z3_context, m: Z3_ast_map, ) => void, ast_map_size: function (c: Z3_context, m: Z3_ast_map): unsigned { let ret = Mod.ccall( 'Z3_ast_map_size', 'number', ['number', 'number'], [c, m], ); ret = new Uint32Array([ret])[0]; return ret; }, ast_map_keys: Mod._Z3_ast_map_keys as ( c: Z3_context, m: Z3_ast_map, ) => Z3_ast_vector, ast_map_to_string: function (c: Z3_context, m: Z3_ast_map): string { return Mod.ccall( 'Z3_ast_map_to_string', 'string', ['number', 'number'], [c, m], ); }, mk_fixedpoint: Mod._Z3_mk_fixedpoint as (c: Z3_context) => Z3_fixedpoint, fixedpoint_inc_ref: Mod._Z3_fixedpoint_inc_ref as ( c: Z3_context, d: Z3_fixedpoint, ) => void, fixedpoint_dec_ref: Mod._Z3_fixedpoint_dec_ref as ( c: Z3_context, d: Z3_fixedpoint, ) => void, fixedpoint_add_rule: Mod._Z3_fixedpoint_add_rule as ( c: Z3_context, d: Z3_fixedpoint, rule: Z3_ast, name: Z3_symbol, ) => void, fixedpoint_add_fact: function ( c: Z3_context, d: Z3_fixedpoint, r: Z3_func_decl, args: unsigned[], ): void { return Mod.ccall( 'Z3_fixedpoint_add_fact', 'void', ['number', 'number', 'number', 'number', 'array'], [ c, d, r, args.length, intArrayToByteArr(args as unknown as number[]), ], ); }, fixedpoint_assert: Mod._Z3_fixedpoint_assert as ( c: Z3_context, d: Z3_fixedpoint, axiom: Z3_ast, ) => void, fixedpoint_query: function ( c: Z3_context, d: Z3_fixedpoint, query: Z3_ast, ): Promise { return Mod.async_call(Mod._async_Z3_fixedpoint_query, c, d, query); }, fixedpoint_query_relations: async function ( c: Z3_context, d: Z3_fixedpoint, relations: Z3_func_decl[], ): Promise { const relations_ptr = Mod._malloc(relations.length * 4); Mod.HEAPU32.set(relations as unknown as number[], relations_ptr / 4); try { let ret = await Mod.async_call(() => Mod.ccall( 'async_Z3_fixedpoint_query_relations', 'void', ['number', 'number', 'number', 'number'], [c, d, relations.length, relations_ptr], ), ); return ret; } finally { Mod._free(relations_ptr); } }, fixedpoint_get_answer: Mod._Z3_fixedpoint_get_answer as ( c: Z3_context, d: Z3_fixedpoint, ) => Z3_ast, fixedpoint_get_reason_unknown: function ( c: Z3_context, d: Z3_fixedpoint, ): string { return Mod.ccall( 'Z3_fixedpoint_get_reason_unknown', 'string', ['number', 'number'], [c, d], ); }, fixedpoint_update_rule: Mod._Z3_fixedpoint_update_rule as ( c: Z3_context, d: Z3_fixedpoint, a: Z3_ast, name: Z3_symbol, ) => void, fixedpoint_get_num_levels: function ( c: Z3_context, d: Z3_fixedpoint, pred: Z3_func_decl, ): unsigned { let ret = Mod.ccall( 'Z3_fixedpoint_get_num_levels', 'number', ['number', 'number', 'number'], [c, d, pred], ); ret = new Uint32Array([ret])[0]; return ret; }, fixedpoint_get_cover_delta: Mod._Z3_fixedpoint_get_cover_delta as ( c: Z3_context, d: Z3_fixedpoint, level: int, pred: Z3_func_decl, ) => Z3_ast, fixedpoint_add_cover: Mod._Z3_fixedpoint_add_cover as ( c: Z3_context, d: Z3_fixedpoint, level: int, pred: Z3_func_decl, property: Z3_ast, ) => void, fixedpoint_get_statistics: Mod._Z3_fixedpoint_get_statistics as ( c: Z3_context, d: Z3_fixedpoint, ) => Z3_stats, fixedpoint_register_relation: Mod._Z3_fixedpoint_register_relation as ( c: Z3_context, d: Z3_fixedpoint, f: Z3_func_decl, ) => void, fixedpoint_set_predicate_representation: function ( c: Z3_context, d: Z3_fixedpoint, f: Z3_func_decl, relation_kinds: Z3_symbol[], ): void { return Mod.ccall( 'Z3_fixedpoint_set_predicate_representation', 'void', ['number', 'number', 'number', 'number', 'array'], [ c, d, f, relation_kinds.length, intArrayToByteArr(relation_kinds as unknown as number[]), ], ); }, fixedpoint_get_rules: Mod._Z3_fixedpoint_get_rules as ( c: Z3_context, f: Z3_fixedpoint, ) => Z3_ast_vector, fixedpoint_get_assertions: Mod._Z3_fixedpoint_get_assertions as ( c: Z3_context, f: Z3_fixedpoint, ) => Z3_ast_vector, fixedpoint_set_params: Mod._Z3_fixedpoint_set_params as ( c: Z3_context, f: Z3_fixedpoint, p: Z3_params, ) => void, fixedpoint_get_help: function (c: Z3_context, f: Z3_fixedpoint): string { return Mod.ccall( 'Z3_fixedpoint_get_help', 'string', ['number', 'number'], [c, f], ); }, fixedpoint_get_param_descrs: Mod._Z3_fixedpoint_get_param_descrs as ( c: Z3_context, f: Z3_fixedpoint, ) => Z3_param_descrs, fixedpoint_to_string: function ( c: Z3_context, f: Z3_fixedpoint, queries: Z3_ast[], ): string { return Mod.ccall( 'Z3_fixedpoint_to_string', 'string', ['number', 'number', 'number', 'array'], [ c, f, queries.length, intArrayToByteArr(queries as unknown as number[]), ], ); }, fixedpoint_from_string: function ( c: Z3_context, f: Z3_fixedpoint, s: string, ): Z3_ast_vector { return Mod.ccall( 'Z3_fixedpoint_from_string', 'number', ['number', 'number', 'string'], [c, f, s], ); }, fixedpoint_from_file: function ( c: Z3_context, f: Z3_fixedpoint, s: string, ): Z3_ast_vector { return Mod.ccall( 'Z3_fixedpoint_from_file', 'number', ['number', 'number', 'string'], [c, f, s], ); }, mk_fpa_rounding_mode_sort: Mod._Z3_mk_fpa_rounding_mode_sort as ( c: Z3_context, ) => Z3_sort, mk_fpa_round_nearest_ties_to_even: Mod._Z3_mk_fpa_round_nearest_ties_to_even as (c: Z3_context) => Z3_ast, mk_fpa_rne: Mod._Z3_mk_fpa_rne as (c: Z3_context) => Z3_ast, mk_fpa_round_nearest_ties_to_away: Mod._Z3_mk_fpa_round_nearest_ties_to_away as (c: Z3_context) => Z3_ast, mk_fpa_rna: Mod._Z3_mk_fpa_rna as (c: Z3_context) => Z3_ast, mk_fpa_round_toward_positive: Mod._Z3_mk_fpa_round_toward_positive as ( c: Z3_context, ) => Z3_ast, mk_fpa_rtp: Mod._Z3_mk_fpa_rtp as (c: Z3_context) => Z3_ast, mk_fpa_round_toward_negative: Mod._Z3_mk_fpa_round_toward_negative as ( c: Z3_context, ) => Z3_ast, mk_fpa_rtn: Mod._Z3_mk_fpa_rtn as (c: Z3_context) => Z3_ast, mk_fpa_round_toward_zero: Mod._Z3_mk_fpa_round_toward_zero as ( c: Z3_context, ) => Z3_ast, mk_fpa_rtz: Mod._Z3_mk_fpa_rtz as (c: Z3_context) => Z3_ast, mk_fpa_sort: Mod._Z3_mk_fpa_sort as ( c: Z3_context, ebits: unsigned, sbits: unsigned, ) => Z3_sort, mk_fpa_sort_half: Mod._Z3_mk_fpa_sort_half as (c: Z3_context) => Z3_sort, mk_fpa_sort_16: Mod._Z3_mk_fpa_sort_16 as (c: Z3_context) => Z3_sort, mk_fpa_sort_single: Mod._Z3_mk_fpa_sort_single as ( c: Z3_context, ) => Z3_sort, mk_fpa_sort_32: Mod._Z3_mk_fpa_sort_32 as (c: Z3_context) => Z3_sort, mk_fpa_sort_double: Mod._Z3_mk_fpa_sort_double as ( c: Z3_context, ) => Z3_sort, mk_fpa_sort_64: Mod._Z3_mk_fpa_sort_64 as (c: Z3_context) => Z3_sort, mk_fpa_sort_quadruple: Mod._Z3_mk_fpa_sort_quadruple as ( c: Z3_context, ) => Z3_sort, mk_fpa_sort_128: Mod._Z3_mk_fpa_sort_128 as (c: Z3_context) => Z3_sort, mk_fpa_nan: Mod._Z3_mk_fpa_nan as (c: Z3_context, s: Z3_sort) => Z3_ast, mk_fpa_inf: Mod._Z3_mk_fpa_inf as ( c: Z3_context, s: Z3_sort, negative: boolean, ) => Z3_ast, mk_fpa_zero: Mod._Z3_mk_fpa_zero as ( c: Z3_context, s: Z3_sort, negative: boolean, ) => Z3_ast, mk_fpa_fp: Mod._Z3_mk_fpa_fp as ( c: Z3_context, sgn: Z3_ast, exp: Z3_ast, sig: Z3_ast, ) => Z3_ast, mk_fpa_numeral_float: Mod._Z3_mk_fpa_numeral_float as ( c: Z3_context, v: float, ty: Z3_sort, ) => Z3_ast, mk_fpa_numeral_double: Mod._Z3_mk_fpa_numeral_double as ( c: Z3_context, v: double, ty: Z3_sort, ) => Z3_ast, mk_fpa_numeral_int: Mod._Z3_mk_fpa_numeral_int as ( c: Z3_context, v: int, ty: Z3_sort, ) => Z3_ast, mk_fpa_numeral_int_uint: Mod._Z3_mk_fpa_numeral_int_uint as ( c: Z3_context, sgn: boolean, exp: int, sig: unsigned, ty: Z3_sort, ) => Z3_ast, mk_fpa_numeral_int64_uint64: Mod._Z3_mk_fpa_numeral_int64_uint64 as ( c: Z3_context, sgn: boolean, exp: int64_t, sig: uint64_t, ty: Z3_sort, ) => Z3_ast, mk_fpa_abs: Mod._Z3_mk_fpa_abs as (c: Z3_context, t: Z3_ast) => Z3_ast, mk_fpa_neg: Mod._Z3_mk_fpa_neg as (c: Z3_context, t: Z3_ast) => Z3_ast, mk_fpa_add: Mod._Z3_mk_fpa_add as ( c: Z3_context, rm: Z3_ast, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_sub: Mod._Z3_mk_fpa_sub as ( c: Z3_context, rm: Z3_ast, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_mul: Mod._Z3_mk_fpa_mul as ( c: Z3_context, rm: Z3_ast, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_div: Mod._Z3_mk_fpa_div as ( c: Z3_context, rm: Z3_ast, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_fma: Mod._Z3_mk_fpa_fma as ( c: Z3_context, rm: Z3_ast, t1: Z3_ast, t2: Z3_ast, t3: Z3_ast, ) => Z3_ast, mk_fpa_sqrt: Mod._Z3_mk_fpa_sqrt as ( c: Z3_context, rm: Z3_ast, t: Z3_ast, ) => Z3_ast, mk_fpa_rem: Mod._Z3_mk_fpa_rem as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_round_to_integral: Mod._Z3_mk_fpa_round_to_integral as ( c: Z3_context, rm: Z3_ast, t: Z3_ast, ) => Z3_ast, mk_fpa_min: Mod._Z3_mk_fpa_min as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_max: Mod._Z3_mk_fpa_max as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_leq: Mod._Z3_mk_fpa_leq as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_lt: Mod._Z3_mk_fpa_lt as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_geq: Mod._Z3_mk_fpa_geq as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_gt: Mod._Z3_mk_fpa_gt as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_eq: Mod._Z3_mk_fpa_eq as ( c: Z3_context, t1: Z3_ast, t2: Z3_ast, ) => Z3_ast, mk_fpa_is_normal: Mod._Z3_mk_fpa_is_normal as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, mk_fpa_is_subnormal: Mod._Z3_mk_fpa_is_subnormal as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, mk_fpa_is_zero: Mod._Z3_mk_fpa_is_zero as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, mk_fpa_is_infinite: Mod._Z3_mk_fpa_is_infinite as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, mk_fpa_is_nan: Mod._Z3_mk_fpa_is_nan as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, mk_fpa_is_negative: Mod._Z3_mk_fpa_is_negative as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, mk_fpa_is_positive: Mod._Z3_mk_fpa_is_positive as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, mk_fpa_to_fp_bv: Mod._Z3_mk_fpa_to_fp_bv as ( c: Z3_context, bv: Z3_ast, s: Z3_sort, ) => Z3_ast, mk_fpa_to_fp_float: Mod._Z3_mk_fpa_to_fp_float as ( c: Z3_context, rm: Z3_ast, t: Z3_ast, s: Z3_sort, ) => Z3_ast, mk_fpa_to_fp_real: Mod._Z3_mk_fpa_to_fp_real as ( c: Z3_context, rm: Z3_ast, t: Z3_ast, s: Z3_sort, ) => Z3_ast, mk_fpa_to_fp_signed: Mod._Z3_mk_fpa_to_fp_signed as ( c: Z3_context, rm: Z3_ast, t: Z3_ast, s: Z3_sort, ) => Z3_ast, mk_fpa_to_fp_unsigned: Mod._Z3_mk_fpa_to_fp_unsigned as ( c: Z3_context, rm: Z3_ast, t: Z3_ast, s: Z3_sort, ) => Z3_ast, mk_fpa_to_ubv: Mod._Z3_mk_fpa_to_ubv as ( c: Z3_context, rm: Z3_ast, t: Z3_ast, sz: unsigned, ) => Z3_ast, mk_fpa_to_sbv: Mod._Z3_mk_fpa_to_sbv as ( c: Z3_context, rm: Z3_ast, t: Z3_ast, sz: unsigned, ) => Z3_ast, mk_fpa_to_real: Mod._Z3_mk_fpa_to_real as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, fpa_get_ebits: function (c: Z3_context, s: Z3_sort): unsigned { let ret = Mod.ccall( 'Z3_fpa_get_ebits', 'number', ['number', 'number'], [c, s], ); ret = new Uint32Array([ret])[0]; return ret; }, fpa_get_sbits: function (c: Z3_context, s: Z3_sort): unsigned { let ret = Mod.ccall( 'Z3_fpa_get_sbits', 'number', ['number', 'number'], [c, s], ); ret = new Uint32Array([ret])[0]; return ret; }, fpa_is_numeral: function (c: Z3_context, t: Z3_ast): boolean { return Mod.ccall( 'Z3_fpa_is_numeral', 'boolean', ['number', 'number'], [c, t], ); }, fpa_is_numeral_nan: function (c: Z3_context, t: Z3_ast): boolean { return Mod.ccall( 'Z3_fpa_is_numeral_nan', 'boolean', ['number', 'number'], [c, t], ); }, fpa_is_numeral_inf: function (c: Z3_context, t: Z3_ast): boolean { return Mod.ccall( 'Z3_fpa_is_numeral_inf', 'boolean', ['number', 'number'], [c, t], ); }, fpa_is_numeral_zero: function (c: Z3_context, t: Z3_ast): boolean { return Mod.ccall( 'Z3_fpa_is_numeral_zero', 'boolean', ['number', 'number'], [c, t], ); }, fpa_is_numeral_normal: function (c: Z3_context, t: Z3_ast): boolean { return Mod.ccall( 'Z3_fpa_is_numeral_normal', 'boolean', ['number', 'number'], [c, t], ); }, fpa_is_numeral_subnormal: function (c: Z3_context, t: Z3_ast): boolean { return Mod.ccall( 'Z3_fpa_is_numeral_subnormal', 'boolean', ['number', 'number'], [c, t], ); }, fpa_is_numeral_positive: function (c: Z3_context, t: Z3_ast): boolean { return Mod.ccall( 'Z3_fpa_is_numeral_positive', 'boolean', ['number', 'number'], [c, t], ); }, fpa_is_numeral_negative: function (c: Z3_context, t: Z3_ast): boolean { return Mod.ccall( 'Z3_fpa_is_numeral_negative', 'boolean', ['number', 'number'], [c, t], ); }, fpa_get_numeral_sign_bv: Mod._Z3_fpa_get_numeral_sign_bv as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, fpa_get_numeral_significand_bv: Mod._Z3_fpa_get_numeral_significand_bv as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, fpa_get_numeral_significand_string: function ( c: Z3_context, t: Z3_ast, ): string { return Mod.ccall( 'Z3_fpa_get_numeral_significand_string', 'string', ['number', 'number'], [c, t], ); }, fpa_get_numeral_significand_uint64: function ( c: Z3_context, t: Z3_ast, ): uint64_t | null { let ret = Mod.ccall( 'Z3_fpa_get_numeral_significand_uint64', 'boolean', ['number', 'number', 'number'], [c, t, outAddress], ); if (!ret) { return null; } return getOutUint64(0); }, fpa_get_numeral_exponent_string: function ( c: Z3_context, t: Z3_ast, biased: boolean, ): string { return Mod.ccall( 'Z3_fpa_get_numeral_exponent_string', 'string', ['number', 'number', 'boolean'], [c, t, biased], ); }, fpa_get_numeral_exponent_int64: function ( c: Z3_context, t: Z3_ast, biased: boolean, ): int64_t | null { let ret = Mod.ccall( 'Z3_fpa_get_numeral_exponent_int64', 'boolean', ['number', 'number', 'number', 'boolean'], [c, t, outAddress, biased], ); if (!ret) { return null; } return getOutInt64(0); }, fpa_get_numeral_exponent_bv: Mod._Z3_fpa_get_numeral_exponent_bv as ( c: Z3_context, t: Z3_ast, biased: boolean, ) => Z3_ast, mk_fpa_to_ieee_bv: Mod._Z3_mk_fpa_to_ieee_bv as ( c: Z3_context, t: Z3_ast, ) => Z3_ast, mk_fpa_to_fp_int_real: Mod._Z3_mk_fpa_to_fp_int_real as ( c: Z3_context, rm: Z3_ast, exp: Z3_ast, sig: Z3_ast, s: Z3_sort, ) => Z3_ast, mk_optimize: Mod._Z3_mk_optimize as (c: Z3_context) => Z3_optimize, optimize_inc_ref: Mod._Z3_optimize_inc_ref as ( c: Z3_context, d: Z3_optimize, ) => void, optimize_dec_ref: Mod._Z3_optimize_dec_ref as ( c: Z3_context, d: Z3_optimize, ) => void, optimize_assert: Mod._Z3_optimize_assert as ( c: Z3_context, o: Z3_optimize, a: Z3_ast, ) => void, optimize_assert_and_track: Mod._Z3_optimize_assert_and_track as ( c: Z3_context, o: Z3_optimize, a: Z3_ast, t: Z3_ast, ) => void, optimize_assert_soft: function ( c: Z3_context, o: Z3_optimize, a: Z3_ast, weight: string, id: Z3_symbol, ): unsigned { let ret = Mod.ccall( 'Z3_optimize_assert_soft', 'number', ['number', 'number', 'number', 'string', 'number'], [c, o, a, weight, id], ); ret = new Uint32Array([ret])[0]; return ret; }, optimize_maximize: function ( c: Z3_context, o: Z3_optimize, t: Z3_ast, ): unsigned { let ret = Mod.ccall( 'Z3_optimize_maximize', 'number', ['number', 'number', 'number'], [c, o, t], ); ret = new Uint32Array([ret])[0]; return ret; }, optimize_minimize: function ( c: Z3_context, o: Z3_optimize, t: Z3_ast, ): unsigned { let ret = Mod.ccall( 'Z3_optimize_minimize', 'number', ['number', 'number', 'number'], [c, o, t], ); ret = new Uint32Array([ret])[0]; return ret; }, optimize_push: Mod._Z3_optimize_push as ( c: Z3_context, d: Z3_optimize, ) => void, optimize_pop: Mod._Z3_optimize_pop as ( c: Z3_context, d: Z3_optimize, ) => void, optimize_set_initial_value: Mod._Z3_optimize_set_initial_value as ( c: Z3_context, o: Z3_optimize, v: Z3_ast, val: Z3_ast, ) => void, optimize_check: async function ( c: Z3_context, o: Z3_optimize, assumptions: Z3_ast[], ): Promise { const assumptions_ptr = Mod._malloc(assumptions.length * 4); Mod.HEAPU32.set( assumptions as unknown as number[], assumptions_ptr / 4, ); try { let ret = await Mod.async_call(() => Mod.ccall( 'async_Z3_optimize_check', 'void', ['number', 'number', 'number', 'number'], [c, o, assumptions.length, assumptions_ptr], ), ); return ret; } finally { Mod._free(assumptions_ptr); } }, optimize_get_reason_unknown: function ( c: Z3_context, d: Z3_optimize, ): string { return Mod.ccall( 'Z3_optimize_get_reason_unknown', 'string', ['number', 'number'], [c, d], ); }, optimize_get_model: Mod._Z3_optimize_get_model as ( c: Z3_context, o: Z3_optimize, ) => Z3_model, optimize_get_unsat_core: Mod._Z3_optimize_get_unsat_core as ( c: Z3_context, o: Z3_optimize, ) => Z3_ast_vector, optimize_set_params: Mod._Z3_optimize_set_params as ( c: Z3_context, o: Z3_optimize, p: Z3_params, ) => void, optimize_get_param_descrs: Mod._Z3_optimize_get_param_descrs as ( c: Z3_context, o: Z3_optimize, ) => Z3_param_descrs, optimize_get_lower: Mod._Z3_optimize_get_lower as ( c: Z3_context, o: Z3_optimize, idx: unsigned, ) => Z3_ast, optimize_get_upper: Mod._Z3_optimize_get_upper as ( c: Z3_context, o: Z3_optimize, idx: unsigned, ) => Z3_ast, optimize_get_lower_as_vector: Mod._Z3_optimize_get_lower_as_vector as ( c: Z3_context, o: Z3_optimize, idx: unsigned, ) => Z3_ast_vector, optimize_get_upper_as_vector: Mod._Z3_optimize_get_upper_as_vector as ( c: Z3_context, o: Z3_optimize, idx: unsigned, ) => Z3_ast_vector, optimize_to_string: function (c: Z3_context, o: Z3_optimize): string { return Mod.ccall( 'Z3_optimize_to_string', 'string', ['number', 'number'], [c, o], ); }, optimize_from_string: function ( c: Z3_context, o: Z3_optimize, s: string, ): void { return Mod.ccall( 'Z3_optimize_from_string', 'void', ['number', 'number', 'string'], [c, o, s], ); }, optimize_from_file: function ( c: Z3_context, o: Z3_optimize, s: string, ): void { return Mod.ccall( 'Z3_optimize_from_file', 'void', ['number', 'number', 'string'], [c, o, s], ); }, optimize_get_help: function (c: Z3_context, t: Z3_optimize): string { return Mod.ccall( 'Z3_optimize_get_help', 'string', ['number', 'number'], [c, t], ); }, optimize_get_statistics: Mod._Z3_optimize_get_statistics as ( c: Z3_context, d: Z3_optimize, ) => Z3_stats, optimize_get_assertions: Mod._Z3_optimize_get_assertions as ( c: Z3_context, o: Z3_optimize, ) => Z3_ast_vector, optimize_get_objectives: Mod._Z3_optimize_get_objectives as ( c: Z3_context, o: Z3_optimize, ) => Z3_ast_vector, optimize_translate: Mod._Z3_optimize_translate as ( c: Z3_context, o: Z3_optimize, target: Z3_context, ) => Z3_optimize, polynomial_subresultants: function ( c: Z3_context, p: Z3_ast, q: Z3_ast, x: Z3_ast, ): Promise { return Mod.async_call( Mod._async_Z3_polynomial_subresultants, c, p, q, x, ); }, rcf_del: Mod._Z3_rcf_del as (c: Z3_context, a: Z3_rcf_num) => void, rcf_mk_rational: function (c: Z3_context, val: string): Z3_rcf_num { return Mod.ccall( 'Z3_rcf_mk_rational', 'number', ['number', 'string'], [c, val], ); }, rcf_mk_small_int: Mod._Z3_rcf_mk_small_int as ( c: Z3_context, val: int, ) => Z3_rcf_num, rcf_mk_pi: Mod._Z3_rcf_mk_pi as (c: Z3_context) => Z3_rcf_num, rcf_mk_e: Mod._Z3_rcf_mk_e as (c: Z3_context) => Z3_rcf_num, rcf_mk_infinitesimal: Mod._Z3_rcf_mk_infinitesimal as ( c: Z3_context, ) => Z3_rcf_num, rcf_mk_roots: function ( c: Z3_context, a: Z3_rcf_num[], ): { rv: unsigned; roots: Z3_rcf_num[] } { let outArray_roots = Mod._malloc(4 * a.length); try { let ret = Mod.ccall( 'Z3_rcf_mk_roots', 'number', ['number', 'number', 'array', 'number'], [ c, a.length, intArrayToByteArr(a as unknown as number[]), outArray_roots, ], ); ret = new Uint32Array([ret])[0]; return { rv: ret, roots: readUintArray( outArray_roots, a.length, ) as unknown as Z3_rcf_num[], }; } finally { Mod._free(outArray_roots); } }, rcf_add: Mod._Z3_rcf_add as ( c: Z3_context, a: Z3_rcf_num, b: Z3_rcf_num, ) => Z3_rcf_num, rcf_sub: Mod._Z3_rcf_sub as ( c: Z3_context, a: Z3_rcf_num, b: Z3_rcf_num, ) => Z3_rcf_num, rcf_mul: Mod._Z3_rcf_mul as ( c: Z3_context, a: Z3_rcf_num, b: Z3_rcf_num, ) => Z3_rcf_num, rcf_div: Mod._Z3_rcf_div as ( c: Z3_context, a: Z3_rcf_num, b: Z3_rcf_num, ) => Z3_rcf_num, rcf_neg: Mod._Z3_rcf_neg as (c: Z3_context, a: Z3_rcf_num) => Z3_rcf_num, rcf_inv: Mod._Z3_rcf_inv as (c: Z3_context, a: Z3_rcf_num) => Z3_rcf_num, rcf_power: Mod._Z3_rcf_power as ( c: Z3_context, a: Z3_rcf_num, k: unsigned, ) => Z3_rcf_num, rcf_lt: function (c: Z3_context, a: Z3_rcf_num, b: Z3_rcf_num): boolean { return Mod.ccall( 'Z3_rcf_lt', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, rcf_gt: function (c: Z3_context, a: Z3_rcf_num, b: Z3_rcf_num): boolean { return Mod.ccall( 'Z3_rcf_gt', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, rcf_le: function (c: Z3_context, a: Z3_rcf_num, b: Z3_rcf_num): boolean { return Mod.ccall( 'Z3_rcf_le', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, rcf_ge: function (c: Z3_context, a: Z3_rcf_num, b: Z3_rcf_num): boolean { return Mod.ccall( 'Z3_rcf_ge', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, rcf_eq: function (c: Z3_context, a: Z3_rcf_num, b: Z3_rcf_num): boolean { return Mod.ccall( 'Z3_rcf_eq', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, rcf_neq: function (c: Z3_context, a: Z3_rcf_num, b: Z3_rcf_num): boolean { return Mod.ccall( 'Z3_rcf_neq', 'boolean', ['number', 'number', 'number'], [c, a, b], ); }, rcf_num_to_string: function ( c: Z3_context, a: Z3_rcf_num, compact: boolean, html: boolean, ): string { return Mod.ccall( 'Z3_rcf_num_to_string', 'string', ['number', 'number', 'boolean', 'boolean'], [c, a, compact, html], ); }, rcf_num_to_decimal_string: function ( c: Z3_context, a: Z3_rcf_num, prec: unsigned, ): string { return Mod.ccall( 'Z3_rcf_num_to_decimal_string', 'string', ['number', 'number', 'number'], [c, a, prec], ); }, rcf_get_numerator_denominator: function ( c: Z3_context, a: Z3_rcf_num, ): { n: Z3_rcf_num; d: Z3_rcf_num } { let ret = Mod.ccall( 'Z3_rcf_get_numerator_denominator', 'void', ['number', 'number', 'number', 'number'], [c, a, outAddress, outAddress + 4], ); return { n: getOutUint(0) as unknown as Z3_rcf_num, d: getOutUint(1) as unknown as Z3_rcf_num, }; }, rcf_is_rational: function (c: Z3_context, a: Z3_rcf_num): boolean { return Mod.ccall( 'Z3_rcf_is_rational', 'boolean', ['number', 'number'], [c, a], ); }, rcf_is_algebraic: function (c: Z3_context, a: Z3_rcf_num): boolean { return Mod.ccall( 'Z3_rcf_is_algebraic', 'boolean', ['number', 'number'], [c, a], ); }, rcf_is_infinitesimal: function (c: Z3_context, a: Z3_rcf_num): boolean { return Mod.ccall( 'Z3_rcf_is_infinitesimal', 'boolean', ['number', 'number'], [c, a], ); }, rcf_is_transcendental: function (c: Z3_context, a: Z3_rcf_num): boolean { return Mod.ccall( 'Z3_rcf_is_transcendental', 'boolean', ['number', 'number'], [c, a], ); }, rcf_extension_index: function (c: Z3_context, a: Z3_rcf_num): unsigned { let ret = Mod.ccall( 'Z3_rcf_extension_index', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, rcf_transcendental_name: Mod._Z3_rcf_transcendental_name as ( c: Z3_context, a: Z3_rcf_num, ) => Z3_symbol, rcf_infinitesimal_name: Mod._Z3_rcf_infinitesimal_name as ( c: Z3_context, a: Z3_rcf_num, ) => Z3_symbol, rcf_num_coefficients: function (c: Z3_context, a: Z3_rcf_num): unsigned { let ret = Mod.ccall( 'Z3_rcf_num_coefficients', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, rcf_coefficient: Mod._Z3_rcf_coefficient as ( c: Z3_context, a: Z3_rcf_num, i: unsigned, ) => Z3_rcf_num, rcf_num_sign_conditions: function ( c: Z3_context, a: Z3_rcf_num, ): unsigned { let ret = Mod.ccall( 'Z3_rcf_num_sign_conditions', 'number', ['number', 'number'], [c, a], ); ret = new Uint32Array([ret])[0]; return ret; }, rcf_sign_condition_sign: Mod._Z3_rcf_sign_condition_sign as ( c: Z3_context, a: Z3_rcf_num, i: unsigned, ) => int, rcf_num_sign_condition_coefficients: function ( c: Z3_context, a: Z3_rcf_num, i: unsigned, ): unsigned { let ret = Mod.ccall( 'Z3_rcf_num_sign_condition_coefficients', 'number', ['number', 'number', 'number'], [c, a, i], ); ret = new Uint32Array([ret])[0]; return ret; }, rcf_sign_condition_coefficient: Mod._Z3_rcf_sign_condition_coefficient as ( c: Z3_context, a: Z3_rcf_num, i: unsigned, j: unsigned, ) => Z3_rcf_num, fixedpoint_query_from_lvl: function ( c: Z3_context, d: Z3_fixedpoint, query: Z3_ast, lvl: unsigned, ): Promise { return Mod.async_call( Mod._async_Z3_fixedpoint_query_from_lvl, c, d, query, lvl, ); }, fixedpoint_get_ground_sat_answer: Mod._Z3_fixedpoint_get_ground_sat_answer as ( c: Z3_context, d: Z3_fixedpoint, ) => Z3_ast, fixedpoint_get_rules_along_trace: Mod._Z3_fixedpoint_get_rules_along_trace as ( c: Z3_context, d: Z3_fixedpoint, ) => Z3_ast_vector, fixedpoint_get_rule_names_along_trace: Mod._Z3_fixedpoint_get_rule_names_along_trace as ( c: Z3_context, d: Z3_fixedpoint, ) => Z3_symbol, fixedpoint_add_invariant: Mod._Z3_fixedpoint_add_invariant as ( c: Z3_context, d: Z3_fixedpoint, pred: Z3_func_decl, property: Z3_ast, ) => void, fixedpoint_get_reachable: Mod._Z3_fixedpoint_get_reachable as ( c: Z3_context, d: Z3_fixedpoint, pred: Z3_func_decl, ) => Z3_ast, qe_model_project: function ( c: Z3_context, m: Z3_model, bound: Z3_app[], body: Z3_ast, ): Z3_ast { return Mod.ccall( 'Z3_qe_model_project', 'number', ['number', 'number', 'number', 'array', 'number'], [ c, m, bound.length, intArrayToByteArr(bound as unknown as number[]), body, ], ); }, qe_model_project_skolem: function ( c: Z3_context, m: Z3_model, bound: Z3_app[], body: Z3_ast, map: Z3_ast_map, ): Z3_ast { return Mod.ccall( 'Z3_qe_model_project_skolem', 'number', ['number', 'number', 'number', 'array', 'number', 'number'], [ c, m, bound.length, intArrayToByteArr(bound as unknown as number[]), body, map, ], ); }, qe_model_project_with_witness: function ( c: Z3_context, m: Z3_model, bound: Z3_app[], body: Z3_ast, map: Z3_ast_map, ): Z3_ast { return Mod.ccall( 'Z3_qe_model_project_with_witness', 'number', ['number', 'number', 'number', 'array', 'number', 'number'], [ c, m, bound.length, intArrayToByteArr(bound as unknown as number[]), body, map, ], ); }, model_extrapolate: Mod._Z3_model_extrapolate as ( c: Z3_context, m: Z3_model, fml: Z3_ast, ) => Z3_ast, qe_lite: Mod._Z3_qe_lite as ( c: Z3_context, vars: Z3_ast_vector, body: Z3_ast, ) => Z3_ast, }, }; }