Z3
src
api
dotnet
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
{
24
Z3_PARAMETER_FUNC_DECL
= 6,
25
Z3_PARAMETER_DOUBLE
= 1,
26
Z3_PARAMETER_SYMBOL
= 3,
27
Z3_PARAMETER_INT
= 0,
28
Z3_PARAMETER_AST
= 5,
29
Z3_PARAMETER_SORT
= 4,
30
Z3_PARAMETER_RATIONAL
= 2,
31
}
32
34
public
enum
Z3_sort_kind
{
35
Z3_BV_SORT
= 4,
36
Z3_FINITE_DOMAIN_SORT
= 8,
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,
42
Z3_FLOATING_POINT_SORT
= 9,
43
Z3_ROUNDING_MODE_SORT
= 10,
44
Z3_UNINTERPRETED_SORT
= 0,
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,
53
Z3_QUANTIFIER_AST
= 3,
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
= 2093,
65
Z3_OP_SUB
= 519,
66
Z3_OP_ZERO_EXT
= 1058,
67
Z3_OP_ADD
= 518,
68
Z3_OP_FPA_ABS
= 2068,
69
Z3_OP_IS_INT
= 528,
70
Z3_OP_BREDOR
= 1061,
71
Z3_OP_FPA_IS_INF
= 2080,
72
Z3_OP_BNOT
= 1051,
73
Z3_OP_BNOR
= 1054,
74
Z3_OP_PR_CNF_STAR
= 1315,
75
Z3_OP_FPA_TO_UBV
= 2089,
76
Z3_OP_RA_JOIN
= 1539,
77
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
= 2052,
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,
84
Z3_OP_FPA_IS_SUBNORMAL
= 2083,
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,
91
Z3_OP_RA_NEGATION_FILTER
= 1544,
92
Z3_OP_FPA_NAN
= 2059,
93
Z3_OP_BSMOD0
= 1040,
94
Z3_OP_FPA_GT
= 2076,
95
Z3_OP_BLSHR
= 1065,
96
Z3_OP_BASHR
= 1066,
97
Z3_OP_PR_UNIT_RESOLUTION
= 1304,
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,
105
Z3_OP_FPA_RM_TOWARD_POSITIVE
= 2053,
106
Z3_OP_PR_IFF_TRUE
= 1305,
107
Z3_OP_FPA_LT
= 2075,
108
Z3_OP_FPA_IS_NORMAL
= 2082,
109
Z3_OP_LABEL_LIT
= 1793,
110
Z3_OP_FPA_TO_IEEE_BV
= 2092,
111
Z3_OP_FPA_LE
= 2077,
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,
121
Z3_OP_FPA_ROUND_TO_INTEGRAL
= 2073,
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
= 2060,
128
Z3_OP_UGT
= 1047,
129
Z3_OP_FPA_NEG
= 2064,
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
= 2074,
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
= 2069,
143
Z3_OP_EQ
= 258,
144
Z3_OP_FPA_SUB
= 2063,
145
Z3_OP_BMUL
= 1030,
146
Z3_OP_ARRAY_MAP
= 771,
147
Z3_OP_STORE
= 768,
148
Z3_OP_PR_HYPOTHESIS
= 1302,
149
Z3_OP_RA_RENAME
= 1545,
150
Z3_OP_AND
= 261,
151
Z3_OP_TO_REAL
= 526,
152
Z3_OP_PR_NNF_POS
= 1312,
153
Z3_OP_PR_AND_ELIM
= 1292,
154
Z3_OP_FPA_TO_SBV
= 2090,
155
Z3_OP_MOD
= 525,
156
Z3_OP_BUDIV0
= 1037,
157
Z3_OP_FPA_MAX
= 2070,
158
Z3_OP_PR_TRUE
= 1281,
159
Z3_OP_BNAND
= 1053,
160
Z3_OP_PR_ELIM_UNUSED_VARS
= 1299,
161
Z3_OP_RA_FILTER
= 1543,
162
Z3_OP_FPA_ADD
= 2062,
163
Z3_OP_FD_LT
= 1549,
164
Z3_OP_RA_EMPTY
= 1537,
165
Z3_OP_DIV
= 522,
166
Z3_OP_ANUM
= 512,
167
Z3_OP_MUL
= 521,
168
Z3_OP_UGEQ
= 1043,
169
Z3_OP_BSREM0
= 1038,
170
Z3_OP_PR_TH_LEMMA
= 1318,
171
Z3_OP_FPA_MINUS_INF
= 2058,
172
Z3_OP_BXOR
= 1052,
173
Z3_OP_DISTINCT
= 259,
174
Z3_OP_PR_IFF_FALSE
= 1306,
175
Z3_OP_BV2INT
= 1072,
176
Z3_OP_EXT_ROTATE_LEFT
= 1069,
177
Z3_OP_PR_PULL_QUANT_STAR
= 1297,
178
Z3_OP_BSUB
= 1029,
179
Z3_OP_PR_ASSERTED
= 1282,
180
Z3_OP_BXNOR
= 1055,
181
Z3_OP_FPA_IS_ZERO
= 2081,
182
Z3_OP_EXTRACT
= 1059,
183
Z3_OP_PR_DER
= 1300,
184
Z3_OP_DT_CONSTRUCTOR
= 2048,
185
Z3_OP_GT
= 517,
186
Z3_OP_BUREM
= 1034,
187
Z3_OP_IMPLIES
= 266,
188
Z3_OP_SLEQ
= 1042,
189
Z3_OP_GE
= 515,
190
Z3_OP_BAND
= 1049,
191
Z3_OP_ITE
= 260,
192
Z3_OP_AS_ARRAY
= 778,
193
Z3_OP_FPA_IS_POSITIVE
= 2085,
194
Z3_OP_RA_SELECT
= 1547,
195
Z3_OP_CONST_ARRAY
= 770,
196
Z3_OP_FPA_TO_REAL
= 2091,
197
Z3_OP_BSDIV
= 1031,
198
Z3_OP_FPA_IS_NEGATIVE
= 2084,
199
Z3_OP_OR
= 262,
200
Z3_OP_FPA_FP
= 2086,
201
Z3_OP_PR_HYPER_RESOLVE
= 1319,
202
Z3_OP_AGNUM
= 513,
203
Z3_OP_FPA_IS_NAN
= 2079,
204
Z3_OP_PR_PUSH_QUANT
= 1298,
205
Z3_OP_FPA_FMA
= 2071,
206
Z3_OP_BSMOD
= 1035,
207
Z3_OP_PR_IFF_OEQ
= 1311,
208
Z3_OP_INTERP
= 268,
209
Z3_OP_PR_LEMMA
= 1303,
210
Z3_OP_FPA_TO_FP_UNSIGNED
= 2088,
211
Z3_OP_SET_SUBSET
= 777,
212
Z3_OP_FPA_SQRT
= 2072,
213
Z3_OP_FPA_GE
= 2078,
214
Z3_OP_FPA_DIV
= 2066,
215
Z3_OP_FPA_RM_TOWARD_ZERO
= 2055,
216
Z3_OP_SELECT
= 769,
217
Z3_OP_RA_PROJECT
= 1542,
218
Z3_OP_BNEG
= 1027,
219
Z3_OP_UMINUS
= 520,
220
Z3_OP_REM
= 524,
221
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
= 2051,
222
Z3_OP_TO_INT
= 527,
223
Z3_OP_PR_QUANT_INST
= 1301,
224
Z3_OP_SGEQ
= 1044,
225
Z3_OP_POWER
= 529,
226
Z3_OP_XOR3
= 1074,
227
Z3_OP_RA_IS_EMPTY
= 1538,
228
Z3_OP_CARRY
= 1073,
229
Z3_OP_DT_ACCESSOR
= 2050,
230
Z3_OP_PR_TRANSITIVITY_STAR
= 1288,
231
Z3_OP_PR_NNF_STAR
= 1314,
232
Z3_OP_PR_COMMUTATIVITY
= 1307,
233
Z3_OP_ULT
= 1045,
234
Z3_OP_FPA_MUL
= 2065,
235
Z3_OP_BSDIV0
= 1036,
236
Z3_OP_SET_DIFFERENCE
= 775,
237
Z3_OP_INT2BV
= 1071,
238
Z3_OP_FPA_NUM
= 2056,
239
Z3_OP_FPA_MINUS_ZERO
= 2061,
240
Z3_OP_FPA_REM
= 2067,
241
Z3_OP_XOR
= 264,
242
Z3_OP_FPA_TO_FP
= 2087,
243
Z3_OP_PR_MODUS_PONENS_OEQ
= 1317,
244
Z3_OP_FPA_RM_TOWARD_NEGATIVE
= 2054,
245
Z3_OP_BNUM
= 1024,
246
Z3_OP_BUDIV
= 1032,
247
Z3_OP_PR_MONOTONICITY
= 1289,
248
Z3_OP_PR_DEF_AXIOM
= 1308,
249
Z3_OP_FALSE
= 257,
250
Z3_OP_EXT_ROTATE_RIGHT
= 1070,
251
Z3_OP_PR_DISTRIBUTIVITY
= 1291,
252
Z3_OP_SIGN_EXT
= 1057,
253
Z3_OP_FPA_PLUS_INF
= 2057,
254
Z3_OP_PR_SKOLEMIZE
= 1316,
255
Z3_OP_BCOMP
= 1063,
256
Z3_OP_RA_COMPLEMENT
= 1546,
257
}
258
260
public
enum
Z3_param_kind
{
261
Z3_PK_BOOL
= 1,
262
Z3_PK_SYMBOL
= 3,
263
Z3_PK_OTHER
= 5,
264
Z3_PK_INVALID
= 6,
265
Z3_PK_UINT
= 0,
266
Z3_PK_STRING
= 4,
267
Z3_PK_DOUBLE
= 2,
268
}
269
271
public
enum
Z3_ast_print_mode
{
272
Z3_PRINT_SMTLIB2_COMPLIANT
= 3,
273
Z3_PRINT_SMTLIB_COMPLIANT
= 2,
274
Z3_PRINT_SMTLIB_FULL
= 0,
275
Z3_PRINT_LOW_LEVEL
= 1,
276
}
277
279
public
enum
Z3_error_code
{
280
Z3_INVALID_PATTERN
= 6,
281
Z3_MEMOUT_FAIL
= 7,
282
Z3_NO_PARSER
= 5,
283
Z3_OK
= 0,
284
Z3_INVALID_ARG
= 3,
285
Z3_EXCEPTION
= 12,
286
Z3_IOB
= 2,
287
Z3_INTERNAL_FATAL
= 9,
288
Z3_INVALID_USAGE
= 10,
289
Z3_FILE_ACCESS_ERROR
= 8,
290
Z3_SORT_ERROR
= 1,
291
Z3_PARSER_ERROR
= 4,
292
Z3_DEC_REF_ERROR
= 11,
293
}
294
296
public
enum
Z3_goal_prec
{
297
Z3_GOAL_UNDER
= 1,
298
Z3_GOAL_PRECISE
= 0,
299
Z3_GOAL_UNDER_OVER
= 3,
300
Z3_GOAL_OVER
= 2,
301
}
302
303
}
Z3_OP_LT
Definition:
z3_api.h:987
Z3_OP_PR_SKOLEMIZE
Definition:
z3_api.h:1115
Z3_OP_FPA_FP
Definition:
z3_api.h:1185
Z3_OP_BSREM0
Definition:
z3_api.h:1034
Z3_OP_FPA_LT
Definition:
z3_api.h:1173
Z3_OP_LABEL_LIT
Definition:
z3_api.h:1138
Z3_OP_FPA_NEG
Definition:
z3_api.h:1161
Z3_OP_FPA_GT
Definition:
z3_api.h:1174
Z3_OP_FPA_ROUND_TO_INTEGRAL
Definition:
z3_api.h:1170
Z3_OP_PR_HYPOTHESIS
Definition:
z3_api.h:1101
Z3_OP_FPA_NAN
Definition:
z3_api.h:1155
Z3_OP_NOT
Definition:
z3_api.h:977
Z3_OP_DT_CONSTRUCTOR
Definition:
z3_api.h:1141
Z3_OP_RA_CLONE
Definition:
z3_api.h:1133
Z3_OP_INT2BV
Definition:
z3_api.h:1073
Microsoft.Z3.Z3_param_kind
Z3_param_kind
Z3_param_kind
Definition:
Enumerations.cs:260
Z3_OP_RA_COMPLEMENT
Definition:
z3_api.h:1131
Z3_OP_UMINUS
Definition:
z3_api.h:991
Z3_OP_AS_ARRAY
Definition:
z3_api.h:1013
Z3_OP_RA_UNION
Definition:
z3_api.h:1125
Z3_ROUNDING_MODE_SORT
Definition:
z3_api.h:198
Z3_OP_RA_STORE
Definition:
z3_api.h:1121
Z3_OP_FPA_LE
Definition:
z3_api.h:1175
Z3_OP_SIGN_EXT
Definition:
z3_api.h:1056
Z3_OP_ARRAY_DEFAULT
Definition:
z3_api.h:1007
Z3_OK
Definition:
z3_api.h:1285
Z3_PARAMETER_FUNC_DECL
Definition:
z3_api.h:179
Z3_OP_PR_GOAL
Definition:
z3_api.h:1082
Z3_L_TRUE
Definition:
z3_api.h:139
Z3_OP_ZERO_EXT
Definition:
z3_api.h:1057
Z3_OP_PR_QUANT_INST
Definition:
z3_api.h:1100
Z3_OP_PR_ELIM_UNUSED_VARS
Definition:
z3_api.h:1098
Z3_FUNC_DECL_AST
Definition:
z3_api.h:221
Microsoft.Z3.Z3_error_code
Z3_error_code
Z3_error_code
Definition:
Enumerations.cs:279
Z3_OP_ANUM
Definition:
z3_api.h:983
Z3_OP_PR_REWRITE
Definition:
z3_api.h:1093
Z3_INVALID_USAGE
Definition:
z3_api.h:1295
Z3_OP_FPA_MINUS_ZERO
Definition:
z3_api.h:1157
Microsoft.Z3.Z3_sort_kind
Z3_sort_kind
Z3_sort_kind
Definition:
Enumerations.cs:34
Z3_OP_FPA_ADD
Definition:
z3_api.h:1159
Z3_OP_FPA_SQRT
Definition:
z3_api.h:1169
Z3_OP_GT
Definition:
z3_api.h:988
Z3_OP_PR_APPLY_DEF
Definition:
z3_api.h:1109
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Definition:
z3_api.h:1146
Z3_OP_PR_REFLEXIVITY
Definition:
z3_api.h:1084
System
Z3_L_FALSE
Definition:
z3_api.h:137
Z3_PK_DOUBLE
Definition:
z3_api.h:1214
Z3_OP_PR_REWRITE_STAR
Definition:
z3_api.h:1094
Z3_OP_FPA_TO_UBV
Definition:
z3_api.h:1188
Z3_OP_FPA_TO_REAL
Definition:
z3_api.h:1190
Z3_OP_BIT0
Definition:
z3_api.h:1018
Z3_OP_BSDIV
Definition:
z3_api.h:1024
Z3_OP_IS_INT
Definition:
z3_api.h:999
Z3_OP_PR_MONOTONICITY
Definition:
z3_api.h:1088
Z3_OP_MUL
Definition:
z3_api.h:992
Z3_OP_PR_TH_LEMMA
Definition:
z3_api.h:1117
Z3_GOAL_UNDER_OVER
Definition:
z3_api.h:1361
Z3_PARAMETER_SORT
Definition:
z3_api.h:177
Z3_OP_PR_HYPER_RESOLVE
Definition:
z3_api.h:1118
Z3_OP_PR_MODUS_PONENS
Definition:
z3_api.h:1083
Z3_OP_PR_DISTRIBUTIVITY
Definition:
z3_api.h:1090
Z3_OP_FPA_TO_FP_UNSIGNED
Definition:
z3_api.h:1187
Z3_INVALID_ARG
Definition:
z3_api.h:1288
Z3_OP_RA_FILTER
Definition:
z3_api.h:1128
Microsoft
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Definition:
z3_api.h:1147
Microsoft.Z3.Z3_decl_kind
Z3_decl_kind
Z3_decl_kind
Definition:
Enumerations.cs:61
Z3_OP_RA_PROJECT
Definition:
z3_api.h:1127
Z3_OP_REM
Definition:
z3_api.h:995
Microsoft.Z3.Z3_goal_prec
Z3_goal_prec
Z3_goal_prec
Definition:
Enumerations.cs:296
Microsoft.Z3.Z3_ast_kind
Z3_ast_kind
Z3_ast_kind
Definition:
Enumerations.cs:50
Z3_OP_LABEL
Definition:
z3_api.h:1137
Z3_QUANTIFIER_AST
Definition:
z3_api.h:219
Z3_OP_SGT
Definition:
z3_api.h:1045
Z3_OP_MOD
Definition:
z3_api.h:996
Z3_OP_SET_COMPLEMENT
Definition:
z3_api.h:1011
Z3_OP_UGEQ
Definition:
z3_api.h:1040
Z3_OP_SET_UNION
Definition:
z3_api.h:1008
Z3_OP_PR_ASSERTED
Definition:
z3_api.h:1081
Z3_FILE_ACCESS_ERROR
Definition:
z3_api.h:1293
Z3_OP_FPA_PLUS_ZERO
Definition:
z3_api.h:1156
Z3_OP_FPA_GE
Definition:
z3_api.h:1176
Z3_OP_DT_ACCESSOR
Definition:
z3_api.h:1143
Z3_OP_IDIV
Definition:
z3_api.h:994
Z3_OP_PR_AND_ELIM
Definition:
z3_api.h:1091
Z3_OP_FPA_MUL
Definition:
z3_api.h:1162
Z3_OP_BSHL
Definition:
z3_api.h:1065
Z3_OP_BUREM
Definition:
z3_api.h:1027
Z3_DEC_REF_ERROR
Definition:
z3_api.h:1296
Z3_OP_RA_WIDEN
Definition:
z3_api.h:1126
Z3_PARAMETER_DOUBLE
Definition:
z3_api.h:174
Z3_PARAMETER_AST
Definition:
z3_api.h:178
Z3_FLOATING_POINT_SORT
Definition:
z3_api.h:197
Z3_IOB
Definition:
z3_api.h:1287
Z3_OP_PR_COMMUTATIVITY
Definition:
z3_api.h:1106
Z3_OP_TRUE
Definition:
z3_api.h:968
Z3_OP_EXT_ROTATE_LEFT
Definition:
z3_api.h:1070
Z3_OP_AGNUM
Definition:
z3_api.h:984
Z3_OP_IMPLIES
Definition:
z3_api.h:978
Z3_OP_PR_IFF_TRUE
Definition:
z3_api.h:1104
Z3_PK_UINT
Definition:
z3_api.h:1212
Z3_OP_PR_TRANSITIVITY
Definition:
z3_api.h:1086
Z3_OP_BCOMP
Definition:
z3_api.h:1063
Z3_OP_DT_RECOGNISER
Definition:
z3_api.h:1142
Z3_OP_RA_JOIN
Definition:
z3_api.h:1124
Z3_PK_STRING
Definition:
z3_api.h:1216
Z3_OP_SUB
Definition:
z3_api.h:990
Z3_OP_FPA_MAX
Definition:
z3_api.h:1167
Z3_OP_BADD
Definition:
z3_api.h:1020
Z3_SORT_AST
Definition:
z3_api.h:220
Z3_OP_DIV
Definition:
z3_api.h:993
Z3_OP_PR_QUANT_INTRO
Definition:
z3_api.h:1089
Z3_UNKNOWN_AST
Definition:
z3_api.h:222
Z3_OP_FPA_TO_FP
Definition:
z3_api.h:1186
Z3_OP_BSMOD
Definition:
z3_api.h:1028
Z3_OP_ULEQ
Definition:
z3_api.h:1038
Z3_OP_RA_NEGATION_FILTER
Definition:
z3_api.h:1129
Z3_PK_OTHER
Definition:
z3_api.h:1217
Z3_UNINTERPRETED_SORT
Definition:
z3_api.h:188
Z3_OP_PR_PULL_QUANT_STAR
Definition:
z3_api.h:1096
Z3_OP_PR_DER
Definition:
z3_api.h:1099
Z3_OP_EQ
Definition:
z3_api.h:970
Z3_OP_FPA_IS_NEGATIVE
Definition:
z3_api.h:1182
Z3_OP_PR_UNIT_RESOLUTION
Definition:
z3_api.h:1103
Z3_OP_BSMOD0
Definition:
z3_api.h:1036
Z3_OP_TO_REAL
Definition:
z3_api.h:997
Z3_OP_EXT_ROTATE_RIGHT
Definition:
z3_api.h:1071
Z3_OP_FPA_RM_TOWARD_NEGATIVE
Definition:
z3_api.h:1149
Z3_OP_BXOR
Definition:
z3_api.h:1050
Z3_OP_CONCAT
Definition:
z3_api.h:1055
Z3_OP_CARRY
Definition:
z3_api.h:1075
Z3_OP_BSDIV0
Definition:
z3_api.h:1032
Z3_PARAMETER_RATIONAL
Definition:
z3_api.h:175
Z3_PK_INVALID
Definition:
z3_api.h:1218
Z3_OP_BUREM0
Definition:
z3_api.h:1035
Z3_OP_XOR3
Definition:
z3_api.h:1076
Z3_OP_OEQ
Definition:
z3_api.h:979
Z3_OP_TO_INT
Definition:
z3_api.h:998
Z3_OP_IFF
Definition:
z3_api.h:975
Z3_INVALID_PATTERN
Definition:
z3_api.h:1291
Z3_OP_BREDOR
Definition:
z3_api.h:1061
Z3_OP_BUDIV
Definition:
z3_api.h:1025
Z3_OP_FPA_IS_ZERO
Definition:
z3_api.h:1179
Z3_RELATION_SORT
Definition:
z3_api.h:195
Z3_OP_EXTRACT
Definition:
z3_api.h:1058
Z3_OP_AND
Definition:
z3_api.h:973
Z3_OP_PR_TRUE
Definition:
z3_api.h:1080
Z3_OP_PR_DEF_INTRO
Definition:
z3_api.h:1108
Z3_OP_PR_CNF_STAR
Definition:
z3_api.h:1114
Z3_OP_BXNOR
Definition:
z3_api.h:1053
Z3_OP_DISTINCT
Definition:
z3_api.h:971
Z3_OP_BNOR
Definition:
z3_api.h:1052
Z3_OP_FPA_TO_SBV
Definition:
z3_api.h:1189
Z3_OP_PR_TRANSITIVITY_STAR
Definition:
z3_api.h:1087
Z3_OP_BASHR
Definition:
z3_api.h:1067
Z3_DATATYPE_SORT
Definition:
z3_api.h:194
Z3_OP_BLSHR
Definition:
z3_api.h:1066
Z3_PK_BOOL
Definition:
z3_api.h:1213
Z3_OP_BOR
Definition:
z3_api.h:1048
Z3_APP_AST
Definition:
z3_api.h:217
Z3_OP_ITE
Definition:
z3_api.h:972
Z3_OP_FPA_RM_TOWARD_POSITIVE
Definition:
z3_api.h:1148
Z3_OP_XOR
Definition:
z3_api.h:976
Z3_OP_PR_NNF_NEG
Definition:
z3_api.h:1112
Z3_OP_FD_LT
Definition:
z3_api.h:1134
Z3_OP_BNUM
Definition:
z3_api.h:1016
Z3_PRINT_SMTLIB2_COMPLIANT
Definition:
z3_api.h:1260
Z3_OP_BSUB
Definition:
z3_api.h:1021
Z3_OP_SGEQ
Definition:
z3_api.h:1041
Z3_OP_FPA_FMA
Definition:
z3_api.h:1168
Z3_OP_FPA_EQ
Definition:
z3_api.h:1172
Z3_OP_FPA_IS_NAN
Definition:
z3_api.h:1177
Microsoft.Z3.Z3_symbol_kind
Z3_symbol_kind
Z3_symbol_kind
Definition:
Enumerations.cs:17
Z3_OP_BNAND
Definition:
z3_api.h:1051
Z3_OP_PR_NNF_POS
Definition:
z3_api.h:1111
Z3_OP_SET_SUBSET
Definition:
z3_api.h:1012
Z3_OP_FPA_MINUS_INF
Definition:
z3_api.h:1154
Z3_OP_FPA_RM_TOWARD_ZERO
Definition:
z3_api.h:1150
Z3_OP_PR_IFF_FALSE
Definition:
z3_api.h:1105
Z3_PRINT_LOW_LEVEL
Definition:
z3_api.h:1258
Z3_PK_SYMBOL
Definition:
z3_api.h:1215
Z3_OP_BREDAND
Definition:
z3_api.h:1062
Z3_PRINT_SMTLIB_COMPLIANT
Definition:
z3_api.h:1259
Z3_OP_FPA_NUM
Definition:
z3_api.h:1152
Z3_OP_CONST_ARRAY
Definition:
z3_api.h:1005
Z3_OP_SELECT
Definition:
z3_api.h:1004
Z3_OP_UNINTERPRETED
Definition:
z3_api.h:1194
Z3_OP_PR_NOT_OR_ELIM
Definition:
z3_api.h:1092
Z3_REAL_SORT
Definition:
z3_api.h:191
Z3_OP_SLEQ
Definition:
z3_api.h:1039
Z3_OP_INTERP
Definition:
z3_api.h:980
Microsoft.Z3.Z3_lbool
Z3_lbool
Z3_lbool
Definition:
Enumerations.cs:10
Z3_BV_SORT
Definition:
z3_api.h:192
Z3_UNKNOWN_SORT
Definition:
z3_api.h:199
Z3_OP_PR_MODUS_PONENS_OEQ
Definition:
z3_api.h:1116
Z3_GOAL_OVER
Definition:
z3_api.h:1360
Z3_OP_GE
Definition:
z3_api.h:986
Z3_OP_FPA_ABS
Definition:
z3_api.h:1165
Z3_OP_SET_INTERSECT
Definition:
z3_api.h:1009
Z3_OP_RA_RENAME
Definition:
z3_api.h:1130
Z3_GOAL_UNDER
Definition:
z3_api.h:1359
Z3_OP_LE
Definition:
z3_api.h:985
Z3_OP_FPA_IS_SUBNORMAL
Definition:
z3_api.h:1181
Z3_STRING_SYMBOL
Definition:
z3_api.h:153
Z3_OP_BNEG
Definition:
z3_api.h:1019
Z3_PRINT_SMTLIB_FULL
Definition:
z3_api.h:1257
Z3_OP_SET_DIFFERENCE
Definition:
z3_api.h:1010
Z3_PARSER_ERROR
Definition:
z3_api.h:1289
Z3_OP_FPA_REM
Definition:
z3_api.h:1164
Z3_OP_ADD
Definition:
z3_api.h:989
Z3_SORT_ERROR
Definition:
z3_api.h:1286
Z3_OP_PR_LEMMA
Definition:
z3_api.h:1102
Z3_OP_FPA_PLUS_INF
Definition:
z3_api.h:1153
Z3_OP_FPA_SUB
Definition:
z3_api.h:1160
Z3_OP_PR_NNF_STAR
Definition:
z3_api.h:1113
Z3_OP_BMUL
Definition:
z3_api.h:1022
Z3_OP_FPA_TO_IEEE_BV
Definition:
z3_api.h:1192
Z3_OP_FPA_IS_INF
Definition:
z3_api.h:1178
Z3_OP_PR_DEF_AXIOM
Definition:
z3_api.h:1107
Z3_INTERNAL_FATAL
Definition:
z3_api.h:1294
Z3_PARAMETER_SYMBOL
Definition:
z3_api.h:176
Z3_OP_FPA_MIN
Definition:
z3_api.h:1166
Z3_OP_FPA_IS_POSITIVE
Definition:
z3_api.h:1183
Z3_EXCEPTION
Definition:
z3_api.h:1297
Z3_MEMOUT_FAIL
Definition:
z3_api.h:1292
Microsoft.Z3.Z3_ast_print_mode
Z3_ast_print_mode
Z3_ast_print_mode
Definition:
Enumerations.cs:271
Z3_OP_PR_UNDEF
Definition:
z3_api.h:1079
Z3_GOAL_PRECISE
Definition:
z3_api.h:1358
Z3_OP_UGT
Definition:
z3_api.h:1044
Z3_ARRAY_SORT
Definition:
z3_api.h:193
Z3_OP_POWER
Definition:
z3_api.h:1000
Z3_OP_PR_PULL_QUANT
Definition:
z3_api.h:1095
Z3_PARAMETER_INT
Definition:
z3_api.h:173
Z3_OP_FPA_DIV
Definition:
z3_api.h:1163
Z3_OP_RA_IS_EMPTY
Definition:
z3_api.h:1123
Z3_BOOL_SORT
Definition:
z3_api.h:189
Z3_NO_PARSER
Definition:
z3_api.h:1290
Z3_OP_BUDIV0
Definition:
z3_api.h:1033
Z3_OP_SLT
Definition:
z3_api.h:1043
Z3_OP_ARRAY_MAP
Definition:
z3_api.h:1006
Z3_OP_BNOT
Definition:
z3_api.h:1049
Z3_OP_BV2INT
Definition:
z3_api.h:1074
Z3_L_UNDEF
Definition:
z3_api.h:138
Z3_OP_OR
Definition:
z3_api.h:974
Z3_OP_FPA_IS_NORMAL
Definition:
z3_api.h:1180
Z3_INT_SYMBOL
Definition:
z3_api.h:152
Z3_OP_ROTATE_RIGHT
Definition:
z3_api.h:1069
Z3_OP_PR_SYMMETRY
Definition:
z3_api.h:1085
Z3_OP_ROTATE_LEFT
Definition:
z3_api.h:1068
Microsoft.Z3.Z3_parameter_kind
Z3_parameter_kind
Z3_parameter_kind
Definition:
Enumerations.cs:23
Z3_OP_RA_EMPTY
Definition:
z3_api.h:1122
Z3_OP_BSREM
Definition:
z3_api.h:1026
Z3_OP_ULT
Definition:
z3_api.h:1042
Z3_FINITE_DOMAIN_SORT
Definition:
z3_api.h:196
Z3_OP_STORE
Definition:
z3_api.h:1003
Z3_OP_FALSE
Definition:
z3_api.h:969
Z3_OP_PR_IFF_OEQ
Definition:
z3_api.h:1110
Z3_INT_SORT
Definition:
z3_api.h:190
Z3_OP_BAND
Definition:
z3_api.h:1047
Z3_OP_BIT1
Definition:
z3_api.h:1017
Z3_OP_REPEAT
Definition:
z3_api.h:1059
Z3_OP_RA_SELECT
Definition:
z3_api.h:1132
Z3_VAR_AST
Definition:
z3_api.h:218
Z3_OP_PR_PUSH_QUANT
Definition:
z3_api.h:1097
Z3_NUMERAL_AST
Definition:
z3_api.h:216
Generated on Thu Jul 9 2015 19:05:13 for Z3 by
1.8.9.1