Z3
Enumerations.cs
Go to the documentation of this file.
1 // Automatically generated file
2 
3 using System;
4 
5 #pragma warning disable 1591
6 
7 namespace Microsoft.Z3
8 {
10  public enum Z3_lbool {
11  Z3_L_TRUE = 1,
12  Z3_L_UNDEF = 0,
13  Z3_L_FALSE = -1,
14  }
15 
17  public enum Z3_symbol_kind {
18  Z3_INT_SYMBOL = 0,
19  Z3_STRING_SYMBOL = 1,
20  }
21 
23  public enum Z3_parameter_kind {
27  Z3_PARAMETER_INT = 0,
28  Z3_PARAMETER_AST = 5,
31  }
32 
34  public enum Z3_sort_kind {
35  Z3_BV_SORT = 4,
37  Z3_ARRAY_SORT = 5,
38  Z3_UNKNOWN_SORT = 1000,
39  Z3_RELATION_SORT = 7,
40  Z3_REAL_SORT = 3,
41  Z3_INT_SORT = 2,
45  Z3_BOOL_SORT = 1,
46  Z3_DATATYPE_SORT = 6,
47  }
48 
50  public enum Z3_ast_kind {
51  Z3_VAR_AST = 2,
52  Z3_SORT_AST = 4,
54  Z3_UNKNOWN_AST = 1000,
55  Z3_FUNC_DECL_AST = 5,
56  Z3_NUMERAL_AST = 0,
57  Z3_APP_AST = 1,
58  }
59 
61  public enum Z3_decl_kind {
62  Z3_OP_LABEL = 1792,
63  Z3_OP_PR_REWRITE = 1294,
64  Z3_OP_UNINTERPRETED = 2349,
65  Z3_OP_SUB = 519,
66  Z3_OP_ZERO_EXT = 1058,
67  Z3_OP_ADD = 518,
68  Z3_OP_FPA_ABS = 2324,
69  Z3_OP_IS_INT = 528,
70  Z3_OP_BREDOR = 1061,
71  Z3_OP_FPA_IS_INF = 2336,
72  Z3_OP_BNOT = 1051,
73  Z3_OP_BNOR = 1054,
74  Z3_OP_PR_CNF_STAR = 1315,
75  Z3_OP_FPA_TO_UBV = 2345,
76  Z3_OP_RA_JOIN = 1539,
78  Z3_OP_LE = 514,
79  Z3_OP_SET_UNION = 773,
80  Z3_OP_PR_UNDEF = 1280,
81  Z3_OP_BREDAND = 1062,
82  Z3_OP_LT = 516,
83  Z3_OP_RA_UNION = 1540,
85  Z3_OP_BADD = 1028,
86  Z3_OP_BUREM0 = 1039,
87  Z3_OP_OEQ = 267,
88  Z3_OP_PR_MODUS_PONENS = 1284,
89  Z3_OP_RA_CLONE = 1548,
90  Z3_OP_REPEAT = 1060,
92  Z3_OP_FPA_NAN = 2315,
93  Z3_OP_BSMOD0 = 1040,
94  Z3_OP_FPA_GT = 2332,
95  Z3_OP_BLSHR = 1065,
96  Z3_OP_BASHR = 1066,
98  Z3_OP_ROTATE_RIGHT = 1068,
99  Z3_OP_ARRAY_DEFAULT = 772,
100  Z3_OP_PR_PULL_QUANT = 1296,
101  Z3_OP_PR_APPLY_DEF = 1310,
102  Z3_OP_PR_REWRITE_STAR = 1295,
103  Z3_OP_IDIV = 523,
104  Z3_OP_PR_GOAL = 1283,
106  Z3_OP_PR_IFF_TRUE = 1305,
107  Z3_OP_FPA_LT = 2331,
108  Z3_OP_FPA_IS_NORMAL = 2338,
109  Z3_OP_LABEL_LIT = 1793,
110  Z3_OP_FPA_TO_IEEE_BV = 2348,
111  Z3_OP_FPA_LE = 2333,
112  Z3_OP_BOR = 1050,
113  Z3_OP_PR_SYMMETRY = 1286,
114  Z3_OP_TRUE = 256,
115  Z3_OP_SET_COMPLEMENT = 776,
116  Z3_OP_CONCAT = 1056,
117  Z3_OP_PR_NOT_OR_ELIM = 1293,
118  Z3_OP_IFF = 263,
119  Z3_OP_BSHL = 1064,
120  Z3_OP_PR_TRANSITIVITY = 1287,
122  Z3_OP_SGT = 1048,
123  Z3_OP_RA_WIDEN = 1541,
124  Z3_OP_PR_DEF_INTRO = 1309,
125  Z3_OP_NOT = 265,
126  Z3_OP_PR_QUANT_INTRO = 1290,
127  Z3_OP_FPA_PLUS_ZERO = 2316,
128  Z3_OP_UGT = 1047,
129  Z3_OP_FPA_NEG = 2320,
130  Z3_OP_DT_RECOGNISER = 2049,
131  Z3_OP_SET_INTERSECT = 774,
132  Z3_OP_BSREM = 1033,
133  Z3_OP_RA_STORE = 1536,
134  Z3_OP_SLT = 1046,
135  Z3_OP_ROTATE_LEFT = 1067,
136  Z3_OP_PR_NNF_NEG = 1313,
137  Z3_OP_FPA_EQ = 2330,
138  Z3_OP_PR_REFLEXIVITY = 1285,
139  Z3_OP_ULEQ = 1041,
140  Z3_OP_BIT1 = 1025,
141  Z3_OP_BIT0 = 1026,
142  Z3_OP_FPA_MIN = 2325,
143  Z3_OP_PB_AT_MOST = 2304,
144  Z3_OP_EQ = 258,
145  Z3_OP_FPA_SUB = 2319,
146  Z3_OP_BMUL = 1030,
147  Z3_OP_ARRAY_MAP = 771,
148  Z3_OP_STORE = 768,
149  Z3_OP_PR_HYPOTHESIS = 1302,
150  Z3_OP_RA_RENAME = 1545,
151  Z3_OP_AND = 261,
152  Z3_OP_TO_REAL = 526,
153  Z3_OP_DT_UPDATE_FIELD = 2051,
154  Z3_OP_PR_NNF_POS = 1312,
155  Z3_OP_PR_AND_ELIM = 1292,
156  Z3_OP_FPA_TO_SBV = 2346,
157  Z3_OP_MOD = 525,
158  Z3_OP_BUDIV0 = 1037,
159  Z3_OP_FPA_MAX = 2326,
160  Z3_OP_PR_TRUE = 1281,
161  Z3_OP_BNAND = 1053,
163  Z3_OP_RA_FILTER = 1543,
164  Z3_OP_FPA_ADD = 2318,
165  Z3_OP_FD_LT = 1549,
166  Z3_OP_RA_EMPTY = 1537,
167  Z3_OP_DIV = 522,
168  Z3_OP_ANUM = 512,
169  Z3_OP_MUL = 521,
170  Z3_OP_UGEQ = 1043,
171  Z3_OP_BSREM0 = 1038,
172  Z3_OP_PR_TH_LEMMA = 1318,
173  Z3_OP_FPA_MINUS_INF = 2314,
174  Z3_OP_BXOR = 1052,
175  Z3_OP_DISTINCT = 259,
176  Z3_OP_PR_IFF_FALSE = 1306,
177  Z3_OP_BV2INT = 1072,
178  Z3_OP_EXT_ROTATE_LEFT = 1069,
180  Z3_OP_BSUB = 1029,
181  Z3_OP_PR_ASSERTED = 1282,
182  Z3_OP_BXNOR = 1055,
183  Z3_OP_FPA_IS_ZERO = 2337,
184  Z3_OP_EXTRACT = 1059,
185  Z3_OP_PR_DER = 1300,
186  Z3_OP_DT_CONSTRUCTOR = 2048,
187  Z3_OP_GT = 517,
188  Z3_OP_BUREM = 1034,
189  Z3_OP_IMPLIES = 266,
190  Z3_OP_SLEQ = 1042,
191  Z3_OP_GE = 515,
192  Z3_OP_PB_GE = 2306,
193  Z3_OP_BAND = 1049,
194  Z3_OP_ITE = 260,
195  Z3_OP_AS_ARRAY = 778,
196  Z3_OP_FPA_IS_POSITIVE = 2341,
197  Z3_OP_RA_SELECT = 1547,
198  Z3_OP_CONST_ARRAY = 770,
199  Z3_OP_FPA_TO_REAL = 2347,
200  Z3_OP_BSDIV = 1031,
201  Z3_OP_FPA_IS_NEGATIVE = 2340,
202  Z3_OP_OR = 262,
203  Z3_OP_FPA_FP = 2342,
204  Z3_OP_PR_HYPER_RESOLVE = 1319,
205  Z3_OP_AGNUM = 513,
206  Z3_OP_FPA_IS_NAN = 2335,
207  Z3_OP_PR_PUSH_QUANT = 1298,
208  Z3_OP_FPA_FMA = 2327,
209  Z3_OP_BSMOD = 1035,
210  Z3_OP_PR_IFF_OEQ = 1311,
211  Z3_OP_INTERP = 268,
212  Z3_OP_PR_LEMMA = 1303,
214  Z3_OP_SET_SUBSET = 777,
215  Z3_OP_FPA_SQRT = 2328,
216  Z3_OP_PB_LE = 2305,
217  Z3_OP_FPA_GE = 2334,
218  Z3_OP_FPA_DIV = 2322,
220  Z3_OP_SELECT = 769,
221  Z3_OP_RA_PROJECT = 1542,
222  Z3_OP_BNEG = 1027,
223  Z3_OP_UMINUS = 520,
224  Z3_OP_REM = 524,
226  Z3_OP_TO_INT = 527,
227  Z3_OP_PR_QUANT_INST = 1301,
228  Z3_OP_SGEQ = 1044,
229  Z3_OP_POWER = 529,
230  Z3_OP_XOR3 = 1074,
231  Z3_OP_RA_IS_EMPTY = 1538,
232  Z3_OP_CARRY = 1073,
233  Z3_OP_DT_ACCESSOR = 2050,
235  Z3_OP_PR_NNF_STAR = 1314,
236  Z3_OP_PR_COMMUTATIVITY = 1307,
237  Z3_OP_ULT = 1045,
238  Z3_OP_FPA_MUL = 2321,
239  Z3_OP_BSDIV0 = 1036,
240  Z3_OP_SET_DIFFERENCE = 775,
241  Z3_OP_INT2BV = 1071,
242  Z3_OP_FPA_NUM = 2312,
243  Z3_OP_FPA_MINUS_ZERO = 2317,
244  Z3_OP_FPA_REM = 2323,
245  Z3_OP_XOR = 264,
246  Z3_OP_FPA_TO_FP = 2343,
249  Z3_OP_BNUM = 1024,
250  Z3_OP_BUDIV = 1032,
251  Z3_OP_PR_MONOTONICITY = 1289,
252  Z3_OP_PR_DEF_AXIOM = 1308,
253  Z3_OP_FALSE = 257,
254  Z3_OP_EXT_ROTATE_RIGHT = 1070,
256  Z3_OP_SIGN_EXT = 1057,
257  Z3_OP_FPA_PLUS_INF = 2313,
258  Z3_OP_PR_SKOLEMIZE = 1316,
259  Z3_OP_BCOMP = 1063,
260  Z3_OP_RA_COMPLEMENT = 1546,
261  }
262 
264  public enum Z3_param_kind {
265  Z3_PK_BOOL = 1,
266  Z3_PK_SYMBOL = 3,
267  Z3_PK_OTHER = 5,
268  Z3_PK_INVALID = 6,
269  Z3_PK_UINT = 0,
270  Z3_PK_STRING = 4,
271  Z3_PK_DOUBLE = 2,
272  }
273 
275  public enum Z3_ast_print_mode {
279  Z3_PRINT_LOW_LEVEL = 1,
280  }
281 
283  public enum Z3_error_code {
284  Z3_INVALID_PATTERN = 6,
285  Z3_MEMOUT_FAIL = 7,
286  Z3_NO_PARSER = 5,
287  Z3_OK = 0,
288  Z3_INVALID_ARG = 3,
289  Z3_EXCEPTION = 12,
290  Z3_IOB = 2,
291  Z3_INTERNAL_FATAL = 9,
292  Z3_INVALID_USAGE = 10,
294  Z3_SORT_ERROR = 1,
295  Z3_PARSER_ERROR = 4,
296  Z3_DEC_REF_ERROR = 11,
297  }
298 
300  public enum Z3_goal_prec {
301  Z3_GOAL_UNDER = 1,
302  Z3_GOAL_PRECISE = 0,
303  Z3_GOAL_UNDER_OVER = 3,
304  Z3_GOAL_OVER = 2,
305  }
306 
307 }
using System
Z3_param_kind
Z3_param_kind
Definition: z3_api.h:1313
Z3_error_code
Z3_error_code
Z3_sort_kind
Z3_sort_kind
Definition: Enumerations.cs:34
Z3_decl_kind
Z3_decl_kind
Definition: Enumerations.cs:61
Z3_goal_prec
Z3_goal_prec
Z3_ast_kind
Z3_ast_kind
Definition: Enumerations.cs:50
Z3_symbol_kind
Z3_symbol_kind
Definition: Enumerations.cs:17
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
Z3_ast_print_mode
Z3_ast_print_mode
Z3_parameter_kind
Z3_parameter_kind
Definition: Enumerations.cs:23