|
Z3
|
|
|
Z3
|
|
00001 // Automatically generated file 00002 00003 using System; 00004 00005 #pragma warning disable 1591 00006 00007 namespace Microsoft.Z3 00008 { 00010 public enum Z3_lbool { 00011 Z3_L_TRUE = 1, 00012 Z3_L_UNDEF = 0, 00013 Z3_L_FALSE = -1, 00014 } 00015 00017 public enum Z3_symbol_kind { 00018 Z3_INT_SYMBOL = 0, 00019 Z3_STRING_SYMBOL = 1, 00020 } 00021 00023 public enum Z3_parameter_kind { 00024 Z3_PARAMETER_FUNC_DECL = 6, 00025 Z3_PARAMETER_DOUBLE = 1, 00026 Z3_PARAMETER_SYMBOL = 3, 00027 Z3_PARAMETER_INT = 0, 00028 Z3_PARAMETER_AST = 5, 00029 Z3_PARAMETER_SORT = 4, 00030 Z3_PARAMETER_RATIONAL = 2, 00031 } 00032 00034 public enum Z3_sort_kind { 00035 Z3_BV_SORT = 4, 00036 Z3_FINITE_DOMAIN_SORT = 8, 00037 Z3_ARRAY_SORT = 5, 00038 Z3_UNKNOWN_SORT = 1000, 00039 Z3_RELATION_SORT = 7, 00040 Z3_REAL_SORT = 3, 00041 Z3_INT_SORT = 2, 00042 Z3_FLOATING_POINT_SORT = 9, 00043 Z3_ROUNDING_MODE_SORT = 10, 00044 Z3_UNINTERPRETED_SORT = 0, 00045 Z3_BOOL_SORT = 1, 00046 Z3_DATATYPE_SORT = 6, 00047 } 00048 00050 public enum Z3_ast_kind { 00051 Z3_VAR_AST = 2, 00052 Z3_SORT_AST = 4, 00053 Z3_QUANTIFIER_AST = 3, 00054 Z3_UNKNOWN_AST = 1000, 00055 Z3_FUNC_DECL_AST = 5, 00056 Z3_NUMERAL_AST = 0, 00057 Z3_APP_AST = 1, 00058 } 00059 00061 public enum Z3_decl_kind { 00062 Z3_OP_LABEL = 1792, 00063 Z3_OP_PR_REWRITE = 1294, 00064 Z3_OP_UNINTERPRETED = 2349, 00065 Z3_OP_SUB = 519, 00066 Z3_OP_ZERO_EXT = 1058, 00067 Z3_OP_ADD = 518, 00068 Z3_OP_FPA_ABS = 2324, 00069 Z3_OP_IS_INT = 528, 00070 Z3_OP_BREDOR = 1061, 00071 Z3_OP_FPA_IS_INF = 2336, 00072 Z3_OP_BNOT = 1051, 00073 Z3_OP_BNOR = 1054, 00074 Z3_OP_PR_CNF_STAR = 1315, 00075 Z3_OP_FPA_TO_UBV = 2345, 00076 Z3_OP_RA_JOIN = 1539, 00077 Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY = 2308, 00078 Z3_OP_LE = 514, 00079 Z3_OP_SET_UNION = 773, 00080 Z3_OP_PR_UNDEF = 1280, 00081 Z3_OP_BREDAND = 1062, 00082 Z3_OP_LT = 516, 00083 Z3_OP_RA_UNION = 1540, 00084 Z3_OP_FPA_IS_SUBNORMAL = 2339, 00085 Z3_OP_BADD = 1028, 00086 Z3_OP_BUREM0 = 1039, 00087 Z3_OP_OEQ = 267, 00088 Z3_OP_PR_MODUS_PONENS = 1284, 00089 Z3_OP_RA_CLONE = 1548, 00090 Z3_OP_REPEAT = 1060, 00091 Z3_OP_RA_NEGATION_FILTER = 1544, 00092 Z3_OP_FPA_NAN = 2315, 00093 Z3_OP_BSMOD0 = 1040, 00094 Z3_OP_FPA_GT = 2332, 00095 Z3_OP_BLSHR = 1065, 00096 Z3_OP_BASHR = 1066, 00097 Z3_OP_PR_UNIT_RESOLUTION = 1304, 00098 Z3_OP_ROTATE_RIGHT = 1068, 00099 Z3_OP_ARRAY_DEFAULT = 772, 00100 Z3_OP_PR_PULL_QUANT = 1296, 00101 Z3_OP_PR_APPLY_DEF = 1310, 00102 Z3_OP_PR_REWRITE_STAR = 1295, 00103 Z3_OP_IDIV = 523, 00104 Z3_OP_PR_GOAL = 1283, 00105 Z3_OP_FPA_RM_TOWARD_POSITIVE = 2309, 00106 Z3_OP_PR_IFF_TRUE = 1305, 00107 Z3_OP_FPA_LT = 2331, 00108 Z3_OP_FPA_IS_NORMAL = 2338, 00109 Z3_OP_LABEL_LIT = 1793, 00110 Z3_OP_FPA_TO_IEEE_BV = 2348, 00111 Z3_OP_FPA_LE = 2333, 00112 Z3_OP_BOR = 1050, 00113 Z3_OP_PR_SYMMETRY = 1286, 00114 Z3_OP_TRUE = 256, 00115 Z3_OP_SET_COMPLEMENT = 776, 00116 Z3_OP_CONCAT = 1056, 00117 Z3_OP_PR_NOT_OR_ELIM = 1293, 00118 Z3_OP_IFF = 263, 00119 Z3_OP_BSHL = 1064, 00120 Z3_OP_PR_TRANSITIVITY = 1287, 00121 Z3_OP_FPA_ROUND_TO_INTEGRAL = 2329, 00122 Z3_OP_SGT = 1048, 00123 Z3_OP_RA_WIDEN = 1541, 00124 Z3_OP_PR_DEF_INTRO = 1309, 00125 Z3_OP_NOT = 265, 00126 Z3_OP_PR_QUANT_INTRO = 1290, 00127 Z3_OP_FPA_PLUS_ZERO = 2316, 00128 Z3_OP_UGT = 1047, 00129 Z3_OP_FPA_NEG = 2320, 00130 Z3_OP_DT_RECOGNISER = 2049, 00131 Z3_OP_SET_INTERSECT = 774, 00132 Z3_OP_BSREM = 1033, 00133 Z3_OP_RA_STORE = 1536, 00134 Z3_OP_SLT = 1046, 00135 Z3_OP_ROTATE_LEFT = 1067, 00136 Z3_OP_PR_NNF_NEG = 1313, 00137 Z3_OP_FPA_EQ = 2330, 00138 Z3_OP_PR_REFLEXIVITY = 1285, 00139 Z3_OP_ULEQ = 1041, 00140 Z3_OP_BIT1 = 1025, 00141 Z3_OP_BIT0 = 1026, 00142 Z3_OP_FPA_MIN = 2325, 00143 Z3_OP_PB_AT_MOST = 2304, 00144 Z3_OP_EQ = 258, 00145 Z3_OP_FPA_SUB = 2319, 00146 Z3_OP_BMUL = 1030, 00147 Z3_OP_ARRAY_MAP = 771, 00148 Z3_OP_STORE = 768, 00149 Z3_OP_PR_HYPOTHESIS = 1302, 00150 Z3_OP_RA_RENAME = 1545, 00151 Z3_OP_AND = 261, 00152 Z3_OP_TO_REAL = 526, 00153 Z3_OP_DT_UPDATE_FIELD = 2051, 00154 Z3_OP_PR_NNF_POS = 1312, 00155 Z3_OP_PR_AND_ELIM = 1292, 00156 Z3_OP_FPA_TO_SBV = 2346, 00157 Z3_OP_MOD = 525, 00158 Z3_OP_BUDIV0 = 1037, 00159 Z3_OP_FPA_MAX = 2326, 00160 Z3_OP_PR_TRUE = 1281, 00161 Z3_OP_BNAND = 1053, 00162 Z3_OP_PR_ELIM_UNUSED_VARS = 1299, 00163 Z3_OP_RA_FILTER = 1543, 00164 Z3_OP_FPA_ADD = 2318, 00165 Z3_OP_FD_LT = 1549, 00166 Z3_OP_RA_EMPTY = 1537, 00167 Z3_OP_DIV = 522, 00168 Z3_OP_ANUM = 512, 00169 Z3_OP_MUL = 521, 00170 Z3_OP_UGEQ = 1043, 00171 Z3_OP_BSREM0 = 1038, 00172 Z3_OP_PR_TH_LEMMA = 1318, 00173 Z3_OP_FPA_MINUS_INF = 2314, 00174 Z3_OP_BXOR = 1052, 00175 Z3_OP_DISTINCT = 259, 00176 Z3_OP_PR_IFF_FALSE = 1306, 00177 Z3_OP_BV2INT = 1072, 00178 Z3_OP_EXT_ROTATE_LEFT = 1069, 00179 Z3_OP_PR_PULL_QUANT_STAR = 1297, 00180 Z3_OP_BSUB = 1029, 00181 Z3_OP_PR_ASSERTED = 1282, 00182 Z3_OP_BXNOR = 1055, 00183 Z3_OP_FPA_IS_ZERO = 2337, 00184 Z3_OP_EXTRACT = 1059, 00185 Z3_OP_PR_DER = 1300, 00186 Z3_OP_DT_CONSTRUCTOR = 2048, 00187 Z3_OP_GT = 517, 00188 Z3_OP_BUREM = 1034, 00189 Z3_OP_IMPLIES = 266, 00190 Z3_OP_SLEQ = 1042, 00191 Z3_OP_GE = 515, 00192 Z3_OP_PB_GE = 2306, 00193 Z3_OP_BAND = 1049, 00194 Z3_OP_ITE = 260, 00195 Z3_OP_AS_ARRAY = 778, 00196 Z3_OP_FPA_IS_POSITIVE = 2341, 00197 Z3_OP_RA_SELECT = 1547, 00198 Z3_OP_CONST_ARRAY = 770, 00199 Z3_OP_FPA_TO_REAL = 2347, 00200 Z3_OP_BSDIV = 1031, 00201 Z3_OP_FPA_IS_NEGATIVE = 2340, 00202 Z3_OP_OR = 262, 00203 Z3_OP_FPA_FP = 2342, 00204 Z3_OP_PR_HYPER_RESOLVE = 1319, 00205 Z3_OP_AGNUM = 513, 00206 Z3_OP_FPA_IS_NAN = 2335, 00207 Z3_OP_PR_PUSH_QUANT = 1298, 00208 Z3_OP_FPA_FMA = 2327, 00209 Z3_OP_BSMOD = 1035, 00210 Z3_OP_PR_IFF_OEQ = 1311, 00211 Z3_OP_INTERP = 268, 00212 Z3_OP_PR_LEMMA = 1303, 00213 Z3_OP_FPA_TO_FP_UNSIGNED = 2344, 00214 Z3_OP_SET_SUBSET = 777, 00215 Z3_OP_FPA_SQRT = 2328, 00216 Z3_OP_PB_LE = 2305, 00217 Z3_OP_FPA_GE = 2334, 00218 Z3_OP_FPA_DIV = 2322, 00219 Z3_OP_FPA_RM_TOWARD_ZERO = 2311, 00220 Z3_OP_SELECT = 769, 00221 Z3_OP_RA_PROJECT = 1542, 00222 Z3_OP_BNEG = 1027, 00223 Z3_OP_UMINUS = 520, 00224 Z3_OP_REM = 524, 00225 Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 2307, 00226 Z3_OP_TO_INT = 527, 00227 Z3_OP_PR_QUANT_INST = 1301, 00228 Z3_OP_SGEQ = 1044, 00229 Z3_OP_POWER = 529, 00230 Z3_OP_XOR3 = 1074, 00231 Z3_OP_RA_IS_EMPTY = 1538, 00232 Z3_OP_CARRY = 1073, 00233 Z3_OP_DT_ACCESSOR = 2050, 00234 Z3_OP_PR_TRANSITIVITY_STAR = 1288, 00235 Z3_OP_PR_NNF_STAR = 1314, 00236 Z3_OP_PR_COMMUTATIVITY = 1307, 00237 Z3_OP_ULT = 1045, 00238 Z3_OP_FPA_MUL = 2321, 00239 Z3_OP_BSDIV0 = 1036, 00240 Z3_OP_SET_DIFFERENCE = 775, 00241 Z3_OP_INT2BV = 1071, 00242 Z3_OP_FPA_NUM = 2312, 00243 Z3_OP_FPA_MINUS_ZERO = 2317, 00244 Z3_OP_FPA_REM = 2323, 00245 Z3_OP_XOR = 264, 00246 Z3_OP_FPA_TO_FP = 2343, 00247 Z3_OP_PR_MODUS_PONENS_OEQ = 1317, 00248 Z3_OP_FPA_RM_TOWARD_NEGATIVE = 2310, 00249 Z3_OP_BNUM = 1024, 00250 Z3_OP_BUDIV = 1032, 00251 Z3_OP_PR_MONOTONICITY = 1289, 00252 Z3_OP_PR_DEF_AXIOM = 1308, 00253 Z3_OP_FALSE = 257, 00254 Z3_OP_EXT_ROTATE_RIGHT = 1070, 00255 Z3_OP_PR_DISTRIBUTIVITY = 1291, 00256 Z3_OP_SIGN_EXT = 1057, 00257 Z3_OP_FPA_PLUS_INF = 2313, 00258 Z3_OP_PR_SKOLEMIZE = 1316, 00259 Z3_OP_BCOMP = 1063, 00260 Z3_OP_RA_COMPLEMENT = 1546, 00261 } 00262 00264 public enum Z3_param_kind { 00265 Z3_PK_BOOL = 1, 00266 Z3_PK_SYMBOL = 3, 00267 Z3_PK_OTHER = 5, 00268 Z3_PK_INVALID = 6, 00269 Z3_PK_UINT = 0, 00270 Z3_PK_STRING = 4, 00271 Z3_PK_DOUBLE = 2, 00272 } 00273 00275 public enum Z3_ast_print_mode { 00276 Z3_PRINT_SMTLIB2_COMPLIANT = 3, 00277 Z3_PRINT_SMTLIB_COMPLIANT = 2, 00278 Z3_PRINT_SMTLIB_FULL = 0, 00279 Z3_PRINT_LOW_LEVEL = 1, 00280 } 00281 00283 public enum Z3_error_code { 00284 Z3_INVALID_PATTERN = 6, 00285 Z3_MEMOUT_FAIL = 7, 00286 Z3_NO_PARSER = 5, 00287 Z3_OK = 0, 00288 Z3_INVALID_ARG = 3, 00289 Z3_EXCEPTION = 12, 00290 Z3_IOB = 2, 00291 Z3_INTERNAL_FATAL = 9, 00292 Z3_INVALID_USAGE = 10, 00293 Z3_FILE_ACCESS_ERROR = 8, 00294 Z3_SORT_ERROR = 1, 00295 Z3_PARSER_ERROR = 4, 00296 Z3_DEC_REF_ERROR = 11, 00297 } 00298 00300 public enum Z3_goal_prec { 00301 Z3_GOAL_UNDER = 1, 00302 Z3_GOAL_PRECISE = 0, 00303 Z3_GOAL_UNDER_OVER = 3, 00304 Z3_GOAL_OVER = 2, 00305 } 00306 00307 }
1.7.6.1