// THIS FILE IS AUTOMATICALLY GENERATED BY make-ts-wrapper.ts // DO NOT EDIT IT BY HAND interface Pointer extends Number { readonly __typeName: T; } interface Subpointer extends Pointer { readonly __typeName2: T; } export type Z3_error_handler = Pointer<'Z3_error_handler'>; export type Z3_push_eh = Pointer<'Z3_push_eh'>; export type Z3_pop_eh = Pointer<'Z3_pop_eh'>; export type Z3_fresh_eh = Pointer<'Z3_fresh_eh'>; export type Z3_fixed_eh = Pointer<'Z3_fixed_eh'>; export type Z3_eq_eh = Pointer<'Z3_eq_eh'>; export type Z3_final_eh = Pointer<'Z3_final_eh'>; export type Z3_created_eh = Pointer<'Z3_created_eh'>; export type Z3_decide_eh = Pointer<'Z3_decide_eh'>; export type Z3_on_binding_eh = Pointer<'Z3_on_binding_eh'>; export type Z3_on_clause_eh = Pointer<'Z3_on_clause_eh'>; export type Z3_symbol = Pointer<'Z3_symbol'>; export type Z3_config = Pointer<'Z3_config'>; export type Z3_context = Pointer<'Z3_context'>; export type Z3_sort = Subpointer<'Z3_sort', 'Z3_ast'>; export type Z3_func_decl = Subpointer<'Z3_func_decl', 'Z3_ast'>; export type Z3_ast = Pointer<'Z3_ast'>; export type Z3_app = Pointer<'Z3_app'>; export type Z3_pattern = Pointer<'Z3_pattern'>; export type Z3_model = Pointer<'Z3_model'>; export type Z3_constructor = Pointer<'Z3_constructor'>; export type Z3_constructor_list = Pointer<'Z3_constructor_list'>; export type Z3_params = Pointer<'Z3_params'>; export type Z3_param_descrs = Pointer<'Z3_param_descrs'>; export type Z3_parser_context = Pointer<'Z3_parser_context'>; export type Z3_goal = Pointer<'Z3_goal'>; export type Z3_tactic = Pointer<'Z3_tactic'>; export type Z3_simplifier = Pointer<'Z3_simplifier'>; export type Z3_probe = Pointer<'Z3_probe'>; export type Z3_stats = Pointer<'Z3_stats'>; export type Z3_solver = Pointer<'Z3_solver'>; export type Z3_solver_callback = Pointer<'Z3_solver_callback'>; export type Z3_ast_vector = Pointer<'Z3_ast_vector'>; export type Z3_ast_map = Pointer<'Z3_ast_map'>; export type Z3_apply_result = Pointer<'Z3_apply_result'>; export type Z3_func_interp = Pointer<'Z3_func_interp'>; export type Z3_func_entry = Pointer<'Z3_func_entry'>; export type Z3_fixedpoint = Pointer<'Z3_fixedpoint'>; export type Z3_optimize = Pointer<'Z3_optimize'>; export type Z3_rcf_num = Pointer<'Z3_rcf_num'>; export enum Z3_lbool { Z3_L_FALSE = -1, Z3_L_UNDEF, Z3_L_TRUE, } export enum Z3_symbol_kind { Z3_INT_SYMBOL, Z3_STRING_SYMBOL, } export enum Z3_parameter_kind { Z3_PARAMETER_INT, Z3_PARAMETER_DOUBLE, Z3_PARAMETER_RATIONAL, Z3_PARAMETER_SYMBOL, Z3_PARAMETER_SORT, Z3_PARAMETER_AST, Z3_PARAMETER_FUNC_DECL, Z3_PARAMETER_INTERNAL, Z3_PARAMETER_ZSTRING, } export enum Z3_sort_kind { Z3_UNINTERPRETED_SORT, Z3_BOOL_SORT, Z3_INT_SORT, Z3_REAL_SORT, Z3_BV_SORT, Z3_ARRAY_SORT, Z3_DATATYPE_SORT, Z3_RELATION_SORT, Z3_FINITE_DOMAIN_SORT, Z3_FLOATING_POINT_SORT, Z3_ROUNDING_MODE_SORT, Z3_SEQ_SORT, Z3_RE_SORT, Z3_CHAR_SORT, Z3_TYPE_VAR, Z3_UNKNOWN_SORT = 1000, } export enum Z3_ast_kind { Z3_NUMERAL_AST, Z3_APP_AST, Z3_VAR_AST, Z3_QUANTIFIER_AST, Z3_SORT_AST, Z3_FUNC_DECL_AST, Z3_UNKNOWN_AST = 1000, } export enum Z3_decl_kind { Z3_OP_TRUE = 256, Z3_OP_FALSE, Z3_OP_EQ, Z3_OP_DISTINCT, Z3_OP_ITE, Z3_OP_AND, Z3_OP_OR, Z3_OP_IFF, Z3_OP_XOR, Z3_OP_NOT, Z3_OP_IMPLIES, Z3_OP_OEQ, Z3_OP_ANUM = 512, Z3_OP_AGNUM, Z3_OP_LE, Z3_OP_GE, Z3_OP_LT, Z3_OP_GT, Z3_OP_ADD, Z3_OP_SUB, Z3_OP_UMINUS, Z3_OP_MUL, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_REM, Z3_OP_MOD, Z3_OP_TO_REAL, Z3_OP_TO_INT, Z3_OP_IS_INT, Z3_OP_POWER, Z3_OP_ABS, Z3_OP_STORE = 768, Z3_OP_SELECT, Z3_OP_CONST_ARRAY, Z3_OP_ARRAY_MAP, Z3_OP_ARRAY_DEFAULT, Z3_OP_SET_UNION, Z3_OP_SET_INTERSECT, Z3_OP_SET_DIFFERENCE, Z3_OP_SET_COMPLEMENT, Z3_OP_SET_SUBSET, Z3_OP_AS_ARRAY, Z3_OP_ARRAY_EXT, Z3_OP_BNUM = 1024, Z3_OP_BIT1, Z3_OP_BIT0, Z3_OP_BNEG, Z3_OP_BADD, Z3_OP_BSUB, Z3_OP_BMUL, Z3_OP_BSDIV, Z3_OP_BUDIV, Z3_OP_BSREM, Z3_OP_BUREM, Z3_OP_BSMOD, Z3_OP_BSDIV0, Z3_OP_BUDIV0, Z3_OP_BSREM0, Z3_OP_BUREM0, Z3_OP_BSMOD0, Z3_OP_ULEQ, Z3_OP_SLEQ, Z3_OP_UGEQ, Z3_OP_SGEQ, Z3_OP_ULT, Z3_OP_SLT, Z3_OP_UGT, Z3_OP_SGT, Z3_OP_BAND, Z3_OP_BOR, Z3_OP_BNOT, Z3_OP_BXOR, Z3_OP_BNAND, Z3_OP_BNOR, Z3_OP_BXNOR, Z3_OP_CONCAT, Z3_OP_SIGN_EXT, Z3_OP_ZERO_EXT, Z3_OP_EXTRACT, Z3_OP_REPEAT, Z3_OP_BREDOR, Z3_OP_BREDAND, Z3_OP_BCOMP, Z3_OP_BSHL, Z3_OP_BLSHR, Z3_OP_BASHR, Z3_OP_ROTATE_LEFT, Z3_OP_ROTATE_RIGHT, Z3_OP_EXT_ROTATE_LEFT, Z3_OP_EXT_ROTATE_RIGHT, Z3_OP_BIT2BOOL, Z3_OP_INT2BV, Z3_OP_BV2INT, Z3_OP_SBV2INT, Z3_OP_CARRY, Z3_OP_XOR3, Z3_OP_BSMUL_NO_OVFL, Z3_OP_BUMUL_NO_OVFL, Z3_OP_BSMUL_NO_UDFL, Z3_OP_BSDIV_I, Z3_OP_BUDIV_I, Z3_OP_BSREM_I, Z3_OP_BUREM_I, Z3_OP_BSMOD_I, Z3_OP_PR_UNDEF = 1280, Z3_OP_PR_TRUE, Z3_OP_PR_ASSERTED, Z3_OP_PR_GOAL, Z3_OP_PR_MODUS_PONENS, Z3_OP_PR_REFLEXIVITY, Z3_OP_PR_SYMMETRY, Z3_OP_PR_TRANSITIVITY, Z3_OP_PR_TRANSITIVITY_STAR, Z3_OP_PR_MONOTONICITY, Z3_OP_PR_QUANT_INTRO, Z3_OP_PR_BIND, Z3_OP_PR_DISTRIBUTIVITY, Z3_OP_PR_AND_ELIM, Z3_OP_PR_NOT_OR_ELIM, Z3_OP_PR_REWRITE, Z3_OP_PR_REWRITE_STAR, Z3_OP_PR_PULL_QUANT, Z3_OP_PR_PUSH_QUANT, Z3_OP_PR_ELIM_UNUSED_VARS, Z3_OP_PR_DER, Z3_OP_PR_QUANT_INST, Z3_OP_PR_HYPOTHESIS, Z3_OP_PR_LEMMA, Z3_OP_PR_UNIT_RESOLUTION, Z3_OP_PR_IFF_TRUE, Z3_OP_PR_IFF_FALSE, Z3_OP_PR_COMMUTATIVITY, Z3_OP_PR_DEF_AXIOM, Z3_OP_PR_ASSUMPTION_ADD, Z3_OP_PR_LEMMA_ADD, Z3_OP_PR_REDUNDANT_DEL, Z3_OP_PR_CLAUSE_TRAIL, Z3_OP_PR_DEF_INTRO, Z3_OP_PR_APPLY_DEF, Z3_OP_PR_IFF_OEQ, Z3_OP_PR_NNF_POS, Z3_OP_PR_NNF_NEG, Z3_OP_PR_SKOLEMIZE, Z3_OP_PR_MODUS_PONENS_OEQ, Z3_OP_PR_TH_LEMMA, Z3_OP_PR_HYPER_RESOLVE, Z3_OP_RA_STORE = 1536, Z3_OP_RA_EMPTY, Z3_OP_RA_IS_EMPTY, Z3_OP_RA_JOIN, Z3_OP_RA_UNION, Z3_OP_RA_WIDEN, Z3_OP_RA_PROJECT, Z3_OP_RA_FILTER, Z3_OP_RA_NEGATION_FILTER, Z3_OP_RA_RENAME, Z3_OP_RA_COMPLEMENT, Z3_OP_RA_SELECT, Z3_OP_RA_CLONE, Z3_OP_FD_CONSTANT, Z3_OP_FD_LT, Z3_OP_SEQ_UNIT, Z3_OP_SEQ_EMPTY, Z3_OP_SEQ_CONCAT, Z3_OP_SEQ_PREFIX, Z3_OP_SEQ_SUFFIX, Z3_OP_SEQ_CONTAINS, Z3_OP_SEQ_EXTRACT, Z3_OP_SEQ_REPLACE, Z3_OP_SEQ_REPLACE_RE, Z3_OP_SEQ_REPLACE_RE_ALL, Z3_OP_SEQ_REPLACE_ALL, Z3_OP_SEQ_AT, Z3_OP_SEQ_NTH, Z3_OP_SEQ_LENGTH, Z3_OP_SEQ_INDEX, Z3_OP_SEQ_LAST_INDEX, Z3_OP_SEQ_TO_RE, Z3_OP_SEQ_IN_RE, Z3_OP_SEQ_MAP, Z3_OP_SEQ_MAPI, Z3_OP_SEQ_FOLDL, Z3_OP_SEQ_FOLDLI, Z3_OP_STR_TO_INT, Z3_OP_INT_TO_STR, Z3_OP_UBV_TO_STR, Z3_OP_SBV_TO_STR, Z3_OP_STR_TO_CODE, Z3_OP_STR_FROM_CODE, Z3_OP_STRING_LT, Z3_OP_STRING_LE, Z3_OP_RE_PLUS, Z3_OP_RE_STAR, Z3_OP_RE_OPTION, Z3_OP_RE_CONCAT, Z3_OP_RE_UNION, Z3_OP_RE_RANGE, Z3_OP_RE_DIFF, Z3_OP_RE_INTERSECT, Z3_OP_RE_LOOP, Z3_OP_RE_POWER, Z3_OP_RE_COMPLEMENT, Z3_OP_RE_EMPTY_SET, Z3_OP_RE_FULL_SET, Z3_OP_RE_FULL_CHAR_SET, Z3_OP_RE_OF_PRED, Z3_OP_RE_REVERSE, Z3_OP_RE_DERIVATIVE, Z3_OP_CHAR_CONST, Z3_OP_CHAR_LE, Z3_OP_CHAR_TO_INT, Z3_OP_CHAR_TO_BV, Z3_OP_CHAR_FROM_BV, Z3_OP_CHAR_IS_DIGIT, Z3_OP_LABEL = 1792, Z3_OP_LABEL_LIT, Z3_OP_DT_CONSTRUCTOR = 2048, Z3_OP_DT_RECOGNISER, Z3_OP_DT_IS, Z3_OP_DT_ACCESSOR, Z3_OP_DT_UPDATE_FIELD, Z3_OP_PB_AT_MOST = 2304, Z3_OP_PB_AT_LEAST, Z3_OP_PB_LE, Z3_OP_PB_GE, Z3_OP_PB_EQ, Z3_OP_SPECIAL_RELATION_LO = 40960, Z3_OP_SPECIAL_RELATION_PO, Z3_OP_SPECIAL_RELATION_PLO, Z3_OP_SPECIAL_RELATION_TO, Z3_OP_SPECIAL_RELATION_TC, Z3_OP_SPECIAL_RELATION_TRC, Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 45056, Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, Z3_OP_FPA_RM_TOWARD_POSITIVE, Z3_OP_FPA_RM_TOWARD_NEGATIVE, Z3_OP_FPA_RM_TOWARD_ZERO, Z3_OP_FPA_NUM, Z3_OP_FPA_PLUS_INF, Z3_OP_FPA_MINUS_INF, Z3_OP_FPA_NAN, Z3_OP_FPA_PLUS_ZERO, Z3_OP_FPA_MINUS_ZERO, Z3_OP_FPA_ADD, Z3_OP_FPA_SUB, Z3_OP_FPA_NEG, Z3_OP_FPA_MUL, Z3_OP_FPA_DIV, Z3_OP_FPA_REM, Z3_OP_FPA_ABS, Z3_OP_FPA_MIN, Z3_OP_FPA_MAX, Z3_OP_FPA_FMA, Z3_OP_FPA_SQRT, Z3_OP_FPA_ROUND_TO_INTEGRAL, Z3_OP_FPA_EQ, Z3_OP_FPA_LT, Z3_OP_FPA_GT, Z3_OP_FPA_LE, Z3_OP_FPA_GE, Z3_OP_FPA_IS_NAN, Z3_OP_FPA_IS_INF, Z3_OP_FPA_IS_ZERO, Z3_OP_FPA_IS_NORMAL, Z3_OP_FPA_IS_SUBNORMAL, Z3_OP_FPA_IS_NEGATIVE, Z3_OP_FPA_IS_POSITIVE, Z3_OP_FPA_FP, Z3_OP_FPA_TO_FP, Z3_OP_FPA_TO_FP_UNSIGNED, Z3_OP_FPA_TO_UBV, Z3_OP_FPA_TO_SBV, Z3_OP_FPA_TO_REAL, Z3_OP_FPA_TO_IEEE_BV, Z3_OP_FPA_BVWRAP, Z3_OP_FPA_BV2RM, Z3_OP_INTERNAL, Z3_OP_RECURSIVE, Z3_OP_UNINTERPRETED, } export enum Z3_param_kind { Z3_PK_UINT, Z3_PK_BOOL, Z3_PK_DOUBLE, Z3_PK_SYMBOL, Z3_PK_STRING, Z3_PK_OTHER, Z3_PK_INVALID, } export enum Z3_ast_print_mode { Z3_PRINT_SMTLIB_FULL, Z3_PRINT_LOW_LEVEL, Z3_PRINT_SMTLIB2_COMPLIANT, } export enum Z3_error_code { Z3_OK, Z3_SORT_ERROR, Z3_IOB, Z3_INVALID_ARG, Z3_PARSER_ERROR, Z3_NO_PARSER, Z3_INVALID_PATTERN, Z3_MEMOUT_FAIL, Z3_FILE_ACCESS_ERROR, Z3_INTERNAL_FATAL, Z3_INVALID_USAGE, Z3_DEC_REF_ERROR, Z3_EXCEPTION, } export enum Z3_goal_prec { Z3_GOAL_PRECISE, Z3_GOAL_UNDER, Z3_GOAL_OVER, Z3_GOAL_UNDER_OVER, }