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 declare enum Z3_lbool { Z3_L_FALSE = -1, Z3_L_UNDEF = 0, Z3_L_TRUE = 1 } export declare enum Z3_symbol_kind { Z3_INT_SYMBOL = 0, Z3_STRING_SYMBOL = 1 } export declare enum Z3_parameter_kind { Z3_PARAMETER_INT = 0, Z3_PARAMETER_DOUBLE = 1, Z3_PARAMETER_RATIONAL = 2, Z3_PARAMETER_SYMBOL = 3, Z3_PARAMETER_SORT = 4, Z3_PARAMETER_AST = 5, Z3_PARAMETER_FUNC_DECL = 6, Z3_PARAMETER_INTERNAL = 7, Z3_PARAMETER_ZSTRING = 8 } export declare enum Z3_sort_kind { Z3_UNINTERPRETED_SORT = 0, Z3_BOOL_SORT = 1, Z3_INT_SORT = 2, Z3_REAL_SORT = 3, Z3_BV_SORT = 4, Z3_ARRAY_SORT = 5, Z3_DATATYPE_SORT = 6, Z3_RELATION_SORT = 7, Z3_FINITE_DOMAIN_SORT = 8, Z3_FLOATING_POINT_SORT = 9, Z3_ROUNDING_MODE_SORT = 10, Z3_SEQ_SORT = 11, Z3_RE_SORT = 12, Z3_CHAR_SORT = 13, Z3_TYPE_VAR = 14, Z3_UNKNOWN_SORT = 1000 } export declare enum Z3_ast_kind { Z3_NUMERAL_AST = 0, Z3_APP_AST = 1, Z3_VAR_AST = 2, Z3_QUANTIFIER_AST = 3, Z3_SORT_AST = 4, Z3_FUNC_DECL_AST = 5, Z3_UNKNOWN_AST = 1000 } export declare enum Z3_decl_kind { Z3_OP_TRUE = 256, Z3_OP_FALSE = 257, Z3_OP_EQ = 258, Z3_OP_DISTINCT = 259, Z3_OP_ITE = 260, Z3_OP_AND = 261, Z3_OP_OR = 262, Z3_OP_IFF = 263, Z3_OP_XOR = 264, Z3_OP_NOT = 265, Z3_OP_IMPLIES = 266, Z3_OP_OEQ = 267, Z3_OP_ANUM = 512, Z3_OP_AGNUM = 513, Z3_OP_LE = 514, Z3_OP_GE = 515, Z3_OP_LT = 516, Z3_OP_GT = 517, Z3_OP_ADD = 518, Z3_OP_SUB = 519, Z3_OP_UMINUS = 520, Z3_OP_MUL = 521, Z3_OP_DIV = 522, Z3_OP_IDIV = 523, Z3_OP_REM = 524, Z3_OP_MOD = 525, Z3_OP_TO_REAL = 526, Z3_OP_TO_INT = 527, Z3_OP_IS_INT = 528, Z3_OP_POWER = 529, Z3_OP_ABS = 530, Z3_OP_STORE = 768, Z3_OP_SELECT = 769, Z3_OP_CONST_ARRAY = 770, Z3_OP_ARRAY_MAP = 771, Z3_OP_ARRAY_DEFAULT = 772, Z3_OP_SET_UNION = 773, Z3_OP_SET_INTERSECT = 774, Z3_OP_SET_DIFFERENCE = 775, Z3_OP_SET_COMPLEMENT = 776, Z3_OP_SET_SUBSET = 777, Z3_OP_AS_ARRAY = 778, Z3_OP_ARRAY_EXT = 779, Z3_OP_BNUM = 1024, Z3_OP_BIT1 = 1025, Z3_OP_BIT0 = 1026, Z3_OP_BNEG = 1027, Z3_OP_BADD = 1028, Z3_OP_BSUB = 1029, Z3_OP_BMUL = 1030, Z3_OP_BSDIV = 1031, Z3_OP_BUDIV = 1032, Z3_OP_BSREM = 1033, Z3_OP_BUREM = 1034, Z3_OP_BSMOD = 1035, Z3_OP_BSDIV0 = 1036, Z3_OP_BUDIV0 = 1037, Z3_OP_BSREM0 = 1038, Z3_OP_BUREM0 = 1039, Z3_OP_BSMOD0 = 1040, Z3_OP_ULEQ = 1041, Z3_OP_SLEQ = 1042, Z3_OP_UGEQ = 1043, Z3_OP_SGEQ = 1044, Z3_OP_ULT = 1045, Z3_OP_SLT = 1046, Z3_OP_UGT = 1047, Z3_OP_SGT = 1048, Z3_OP_BAND = 1049, Z3_OP_BOR = 1050, Z3_OP_BNOT = 1051, Z3_OP_BXOR = 1052, Z3_OP_BNAND = 1053, Z3_OP_BNOR = 1054, Z3_OP_BXNOR = 1055, Z3_OP_CONCAT = 1056, Z3_OP_SIGN_EXT = 1057, Z3_OP_ZERO_EXT = 1058, Z3_OP_EXTRACT = 1059, Z3_OP_REPEAT = 1060, Z3_OP_BREDOR = 1061, Z3_OP_BREDAND = 1062, Z3_OP_BCOMP = 1063, Z3_OP_BSHL = 1064, Z3_OP_BLSHR = 1065, Z3_OP_BASHR = 1066, Z3_OP_ROTATE_LEFT = 1067, Z3_OP_ROTATE_RIGHT = 1068, Z3_OP_EXT_ROTATE_LEFT = 1069, Z3_OP_EXT_ROTATE_RIGHT = 1070, Z3_OP_BIT2BOOL = 1071, Z3_OP_INT2BV = 1072, Z3_OP_BV2INT = 1073, Z3_OP_SBV2INT = 1074, Z3_OP_CARRY = 1075, Z3_OP_XOR3 = 1076, Z3_OP_BSMUL_NO_OVFL = 1077, Z3_OP_BUMUL_NO_OVFL = 1078, Z3_OP_BSMUL_NO_UDFL = 1079, Z3_OP_BSDIV_I = 1080, Z3_OP_BUDIV_I = 1081, Z3_OP_BSREM_I = 1082, Z3_OP_BUREM_I = 1083, Z3_OP_BSMOD_I = 1084, Z3_OP_PR_UNDEF = 1280, Z3_OP_PR_TRUE = 1281, Z3_OP_PR_ASSERTED = 1282, Z3_OP_PR_GOAL = 1283, Z3_OP_PR_MODUS_PONENS = 1284, Z3_OP_PR_REFLEXIVITY = 1285, Z3_OP_PR_SYMMETRY = 1286, Z3_OP_PR_TRANSITIVITY = 1287, Z3_OP_PR_TRANSITIVITY_STAR = 1288, Z3_OP_PR_MONOTONICITY = 1289, Z3_OP_PR_QUANT_INTRO = 1290, Z3_OP_PR_BIND = 1291, Z3_OP_PR_DISTRIBUTIVITY = 1292, Z3_OP_PR_AND_ELIM = 1293, Z3_OP_PR_NOT_OR_ELIM = 1294, Z3_OP_PR_REWRITE = 1295, Z3_OP_PR_REWRITE_STAR = 1296, Z3_OP_PR_PULL_QUANT = 1297, Z3_OP_PR_PUSH_QUANT = 1298, Z3_OP_PR_ELIM_UNUSED_VARS = 1299, Z3_OP_PR_DER = 1300, Z3_OP_PR_QUANT_INST = 1301, Z3_OP_PR_HYPOTHESIS = 1302, Z3_OP_PR_LEMMA = 1303, Z3_OP_PR_UNIT_RESOLUTION = 1304, Z3_OP_PR_IFF_TRUE = 1305, Z3_OP_PR_IFF_FALSE = 1306, Z3_OP_PR_COMMUTATIVITY = 1307, Z3_OP_PR_DEF_AXIOM = 1308, Z3_OP_PR_ASSUMPTION_ADD = 1309, Z3_OP_PR_LEMMA_ADD = 1310, Z3_OP_PR_REDUNDANT_DEL = 1311, Z3_OP_PR_CLAUSE_TRAIL = 1312, Z3_OP_PR_DEF_INTRO = 1313, Z3_OP_PR_APPLY_DEF = 1314, Z3_OP_PR_IFF_OEQ = 1315, Z3_OP_PR_NNF_POS = 1316, Z3_OP_PR_NNF_NEG = 1317, Z3_OP_PR_SKOLEMIZE = 1318, Z3_OP_PR_MODUS_PONENS_OEQ = 1319, Z3_OP_PR_TH_LEMMA = 1320, Z3_OP_PR_HYPER_RESOLVE = 1321, Z3_OP_RA_STORE = 1536, Z3_OP_RA_EMPTY = 1537, Z3_OP_RA_IS_EMPTY = 1538, Z3_OP_RA_JOIN = 1539, Z3_OP_RA_UNION = 1540, Z3_OP_RA_WIDEN = 1541, Z3_OP_RA_PROJECT = 1542, Z3_OP_RA_FILTER = 1543, Z3_OP_RA_NEGATION_FILTER = 1544, Z3_OP_RA_RENAME = 1545, Z3_OP_RA_COMPLEMENT = 1546, Z3_OP_RA_SELECT = 1547, Z3_OP_RA_CLONE = 1548, Z3_OP_FD_CONSTANT = 1549, Z3_OP_FD_LT = 1550, Z3_OP_SEQ_UNIT = 1551, Z3_OP_SEQ_EMPTY = 1552, Z3_OP_SEQ_CONCAT = 1553, Z3_OP_SEQ_PREFIX = 1554, Z3_OP_SEQ_SUFFIX = 1555, Z3_OP_SEQ_CONTAINS = 1556, Z3_OP_SEQ_EXTRACT = 1557, Z3_OP_SEQ_REPLACE = 1558, Z3_OP_SEQ_REPLACE_RE = 1559, Z3_OP_SEQ_REPLACE_RE_ALL = 1560, Z3_OP_SEQ_REPLACE_ALL = 1561, Z3_OP_SEQ_AT = 1562, Z3_OP_SEQ_NTH = 1563, Z3_OP_SEQ_LENGTH = 1564, Z3_OP_SEQ_INDEX = 1565, Z3_OP_SEQ_LAST_INDEX = 1566, Z3_OP_SEQ_TO_RE = 1567, Z3_OP_SEQ_IN_RE = 1568, Z3_OP_SEQ_MAP = 1569, Z3_OP_SEQ_MAPI = 1570, Z3_OP_SEQ_FOLDL = 1571, Z3_OP_SEQ_FOLDLI = 1572, Z3_OP_STR_TO_INT = 1573, Z3_OP_INT_TO_STR = 1574, Z3_OP_UBV_TO_STR = 1575, Z3_OP_SBV_TO_STR = 1576, Z3_OP_STR_TO_CODE = 1577, Z3_OP_STR_FROM_CODE = 1578, Z3_OP_STRING_LT = 1579, Z3_OP_STRING_LE = 1580, Z3_OP_RE_PLUS = 1581, Z3_OP_RE_STAR = 1582, Z3_OP_RE_OPTION = 1583, Z3_OP_RE_CONCAT = 1584, Z3_OP_RE_UNION = 1585, Z3_OP_RE_RANGE = 1586, Z3_OP_RE_DIFF = 1587, Z3_OP_RE_INTERSECT = 1588, Z3_OP_RE_LOOP = 1589, Z3_OP_RE_POWER = 1590, Z3_OP_RE_COMPLEMENT = 1591, Z3_OP_RE_EMPTY_SET = 1592, Z3_OP_RE_FULL_SET = 1593, Z3_OP_RE_FULL_CHAR_SET = 1594, Z3_OP_RE_OF_PRED = 1595, Z3_OP_RE_REVERSE = 1596, Z3_OP_RE_DERIVATIVE = 1597, Z3_OP_CHAR_CONST = 1598, Z3_OP_CHAR_LE = 1599, Z3_OP_CHAR_TO_INT = 1600, Z3_OP_CHAR_TO_BV = 1601, Z3_OP_CHAR_FROM_BV = 1602, Z3_OP_CHAR_IS_DIGIT = 1603, Z3_OP_LABEL = 1792, Z3_OP_LABEL_LIT = 1793, Z3_OP_DT_CONSTRUCTOR = 2048, Z3_OP_DT_RECOGNISER = 2049, Z3_OP_DT_IS = 2050, Z3_OP_DT_ACCESSOR = 2051, Z3_OP_DT_UPDATE_FIELD = 2052, Z3_OP_PB_AT_MOST = 2304, Z3_OP_PB_AT_LEAST = 2305, Z3_OP_PB_LE = 2306, Z3_OP_PB_GE = 2307, Z3_OP_PB_EQ = 2308, Z3_OP_SPECIAL_RELATION_LO = 40960, Z3_OP_SPECIAL_RELATION_PO = 40961, Z3_OP_SPECIAL_RELATION_PLO = 40962, Z3_OP_SPECIAL_RELATION_TO = 40963, Z3_OP_SPECIAL_RELATION_TC = 40964, Z3_OP_SPECIAL_RELATION_TRC = 40965, Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 45056, Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY = 45057, Z3_OP_FPA_RM_TOWARD_POSITIVE = 45058, Z3_OP_FPA_RM_TOWARD_NEGATIVE = 45059, Z3_OP_FPA_RM_TOWARD_ZERO = 45060, Z3_OP_FPA_NUM = 45061, Z3_OP_FPA_PLUS_INF = 45062, Z3_OP_FPA_MINUS_INF = 45063, Z3_OP_FPA_NAN = 45064, Z3_OP_FPA_PLUS_ZERO = 45065, Z3_OP_FPA_MINUS_ZERO = 45066, Z3_OP_FPA_ADD = 45067, Z3_OP_FPA_SUB = 45068, Z3_OP_FPA_NEG = 45069, Z3_OP_FPA_MUL = 45070, Z3_OP_FPA_DIV = 45071, Z3_OP_FPA_REM = 45072, Z3_OP_FPA_ABS = 45073, Z3_OP_FPA_MIN = 45074, Z3_OP_FPA_MAX = 45075, Z3_OP_FPA_FMA = 45076, Z3_OP_FPA_SQRT = 45077, Z3_OP_FPA_ROUND_TO_INTEGRAL = 45078, Z3_OP_FPA_EQ = 45079, Z3_OP_FPA_LT = 45080, Z3_OP_FPA_GT = 45081, Z3_OP_FPA_LE = 45082, Z3_OP_FPA_GE = 45083, Z3_OP_FPA_IS_NAN = 45084, Z3_OP_FPA_IS_INF = 45085, Z3_OP_FPA_IS_ZERO = 45086, Z3_OP_FPA_IS_NORMAL = 45087, Z3_OP_FPA_IS_SUBNORMAL = 45088, Z3_OP_FPA_IS_NEGATIVE = 45089, Z3_OP_FPA_IS_POSITIVE = 45090, Z3_OP_FPA_FP = 45091, Z3_OP_FPA_TO_FP = 45092, Z3_OP_FPA_TO_FP_UNSIGNED = 45093, Z3_OP_FPA_TO_UBV = 45094, Z3_OP_FPA_TO_SBV = 45095, Z3_OP_FPA_TO_REAL = 45096, Z3_OP_FPA_TO_IEEE_BV = 45097, Z3_OP_FPA_BVWRAP = 45098, Z3_OP_FPA_BV2RM = 45099, Z3_OP_INTERNAL = 45100, Z3_OP_RECURSIVE = 45101, Z3_OP_UNINTERPRETED = 45102 } export declare enum Z3_param_kind { Z3_PK_UINT = 0, Z3_PK_BOOL = 1, Z3_PK_DOUBLE = 2, Z3_PK_SYMBOL = 3, Z3_PK_STRING = 4, Z3_PK_OTHER = 5, Z3_PK_INVALID = 6 } export declare enum Z3_ast_print_mode { Z3_PRINT_SMTLIB_FULL = 0, Z3_PRINT_LOW_LEVEL = 1, Z3_PRINT_SMTLIB2_COMPLIANT = 2 } export declare enum Z3_error_code { Z3_OK = 0, Z3_SORT_ERROR = 1, Z3_IOB = 2, Z3_INVALID_ARG = 3, Z3_PARSER_ERROR = 4, Z3_NO_PARSER = 5, Z3_INVALID_PATTERN = 6, Z3_MEMOUT_FAIL = 7, Z3_FILE_ACCESS_ERROR = 8, Z3_INTERNAL_FATAL = 9, Z3_INVALID_USAGE = 10, Z3_DEC_REF_ERROR = 11, Z3_EXCEPTION = 12 } export declare enum Z3_goal_prec { Z3_GOAL_PRECISE = 0, Z3_GOAL_UNDER = 1, Z3_GOAL_OVER = 2, Z3_GOAL_UNDER_OVER = 3 } export {};