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
= 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,
77
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
= 2308,
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
= 2339,
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
= 2315,
93
Z3_OP_BSMOD0
= 1040,
94
Z3_OP_FPA_GT
= 2332,
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
= 2309,
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,
121
Z3_OP_FPA_ROUND_TO_INTEGRAL
= 2329,
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,
162
Z3_OP_PR_ELIM_UNUSED_VARS
= 1299,
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,
179
Z3_OP_PR_PULL_QUANT_STAR
= 1297,
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,
213
Z3_OP_FPA_TO_FP_UNSIGNED
= 2344,
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,
219
Z3_OP_FPA_RM_TOWARD_ZERO
= 2311,
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,
225
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
= 2307,
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,
234
Z3_OP_PR_TRANSITIVITY_STAR
= 1288,
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,
247
Z3_OP_PR_MODUS_PONENS_OEQ
= 1317,
248
Z3_OP_FPA_RM_TOWARD_NEGATIVE
= 2310,
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,
255
Z3_OP_PR_DISTRIBUTIVITY
= 1291,
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
{
276
Z3_PRINT_SMTLIB2_COMPLIANT
= 3,
277
Z3_PRINT_SMTLIB_COMPLIANT
= 2,
278
Z3_PRINT_SMTLIB_FULL
= 0,
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,
293
Z3_FILE_ACCESS_ERROR
= 8,
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
}
Z3_OP_DT_UPDATE_FIELD
Definition:
z3_api.h:1166
Z3_OP_LT
Definition:
z3_api.h:1009
Z3_OP_PR_SKOLEMIZE
Definition:
z3_api.h:1137
Z3_OP_FPA_FP
Definition:
z3_api.h:1213
Z3_OP_BSREM0
Definition:
z3_api.h:1056
Z3_OP_FPA_LT
Definition:
z3_api.h:1201
Z3_OP_LABEL_LIT
Definition:
z3_api.h:1160
Z3_OP_FPA_NEG
Definition:
z3_api.h:1189
Z3_OP_FPA_GT
Definition:
z3_api.h:1202
Z3_OP_FPA_ROUND_TO_INTEGRAL
Definition:
z3_api.h:1198
Z3_OP_PR_HYPOTHESIS
Definition:
z3_api.h:1123
Z3_OP_FPA_NAN
Definition:
z3_api.h:1183
Z3_OP_NOT
Definition:
z3_api.h:999
Z3_OP_DT_CONSTRUCTOR
Definition:
z3_api.h:1163
Z3_OP_RA_CLONE
Definition:
z3_api.h:1155
Z3_OP_INT2BV
Definition:
z3_api.h:1095
System
using System
Definition:
InterpolationContext.cs:7
Microsoft.Z3.Z3_param_kind
Z3_param_kind
Z3_param_kind
Definition:
Enumerations.cs:264
Z3_OP_RA_COMPLEMENT
Definition:
z3_api.h:1153
Z3_OP_UMINUS
Definition:
z3_api.h:1013
Z3_OP_AS_ARRAY
Definition:
z3_api.h:1035
Z3_OP_RA_UNION
Definition:
z3_api.h:1147
Z3_ROUNDING_MODE_SORT
Definition:
z3_api.h:206
Z3_OP_RA_STORE
Definition:
z3_api.h:1143
Z3_OP_FPA_LE
Definition:
z3_api.h:1203
Z3_OP_SIGN_EXT
Definition:
z3_api.h:1078
Z3_OP_ARRAY_DEFAULT
Definition:
z3_api.h:1029
Z3_OK
Definition:
z3_api.h:1313
Z3_PARAMETER_FUNC_DECL
Definition:
z3_api.h:187
Z3_OP_PR_GOAL
Definition:
z3_api.h:1104
Z3_L_TRUE
Definition:
z3_api.h:147
Z3_OP_ZERO_EXT
Definition:
z3_api.h:1079
Z3_OP_PR_QUANT_INST
Definition:
z3_api.h:1122
Z3_OP_PR_ELIM_UNUSED_VARS
Definition:
z3_api.h:1120
Z3_FUNC_DECL_AST
Definition:
z3_api.h:229
Microsoft.Z3.Z3_error_code
Z3_error_code
Z3_error_code
Definition:
Enumerations.cs:283
Z3_OP_ANUM
Definition:
z3_api.h:1005
Z3_OP_PR_REWRITE
Definition:
z3_api.h:1115
Z3_INVALID_USAGE
Definition:
z3_api.h:1323
Z3_OP_FPA_MINUS_ZERO
Definition:
z3_api.h:1185
Microsoft.Z3.Z3_sort_kind
Z3_sort_kind
Z3_sort_kind
Definition:
Enumerations.cs:34
Z3_OP_FPA_ADD
Definition:
z3_api.h:1187
Z3_OP_FPA_SQRT
Definition:
z3_api.h:1197
Z3_OP_GT
Definition:
z3_api.h:1010
Z3_OP_PR_APPLY_DEF
Definition:
z3_api.h:1131
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Definition:
z3_api.h:1174
Z3_OP_PR_REFLEXIVITY
Definition:
z3_api.h:1106
Z3_L_FALSE
Definition:
z3_api.h:145
Z3_PK_DOUBLE
Definition:
z3_api.h:1242
Z3_OP_PR_REWRITE_STAR
Definition:
z3_api.h:1116
Z3_OP_FPA_TO_UBV
Definition:
z3_api.h:1216
Z3_OP_FPA_TO_REAL
Definition:
z3_api.h:1218
Z3_OP_BIT0
Definition:
z3_api.h:1040
Z3_OP_BSDIV
Definition:
z3_api.h:1046
Z3_OP_IS_INT
Definition:
z3_api.h:1021
Z3_OP_PR_MONOTONICITY
Definition:
z3_api.h:1110
Z3_OP_MUL
Definition:
z3_api.h:1014
Z3_OP_PR_TH_LEMMA
Definition:
z3_api.h:1139
Z3_GOAL_UNDER_OVER
Definition:
z3_api.h:1390
Z3_PARAMETER_SORT
Definition:
z3_api.h:185
Z3_OP_PR_HYPER_RESOLVE
Definition:
z3_api.h:1140
Z3_OP_PR_MODUS_PONENS
Definition:
z3_api.h:1105
Z3_OP_PR_DISTRIBUTIVITY
Definition:
z3_api.h:1112
Z3_OP_FPA_TO_FP_UNSIGNED
Definition:
z3_api.h:1215
Z3_INVALID_ARG
Definition:
z3_api.h:1316
Z3_OP_RA_FILTER
Definition:
z3_api.h:1150
Microsoft
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Definition:
z3_api.h:1175
Microsoft.Z3.Z3_decl_kind
Z3_decl_kind
Z3_decl_kind
Definition:
Enumerations.cs:61
Z3_OP_RA_PROJECT
Definition:
z3_api.h:1149
Z3_OP_REM
Definition:
z3_api.h:1017
Microsoft.Z3.Z3_goal_prec
Z3_goal_prec
Z3_goal_prec
Definition:
Enumerations.cs:300
Microsoft.Z3.Z3_ast_kind
Z3_ast_kind
Z3_ast_kind
Definition:
Enumerations.cs:50
Z3_OP_LABEL
Definition:
z3_api.h:1159
Z3_QUANTIFIER_AST
Definition:
z3_api.h:227
Z3_OP_SGT
Definition:
z3_api.h:1067
Z3_OP_MOD
Definition:
z3_api.h:1018
Z3_OP_SET_COMPLEMENT
Definition:
z3_api.h:1033
Z3_OP_UGEQ
Definition:
z3_api.h:1062
Z3_OP_SET_UNION
Definition:
z3_api.h:1030
Z3_OP_PR_ASSERTED
Definition:
z3_api.h:1103
Z3_FILE_ACCESS_ERROR
Definition:
z3_api.h:1321
Z3_OP_FPA_PLUS_ZERO
Definition:
z3_api.h:1184
Z3_OP_FPA_GE
Definition:
z3_api.h:1204
Z3_OP_DT_ACCESSOR
Definition:
z3_api.h:1165
Z3_OP_IDIV
Definition:
z3_api.h:1016
Z3_OP_PR_AND_ELIM
Definition:
z3_api.h:1113
Z3_OP_PB_AT_MOST
Definition:
z3_api.h:1169
Z3_OP_FPA_MUL
Definition:
z3_api.h:1190
Z3_OP_BSHL
Definition:
z3_api.h:1087
Z3_OP_BUREM
Definition:
z3_api.h:1049
Z3_DEC_REF_ERROR
Definition:
z3_api.h:1324
Z3_OP_RA_WIDEN
Definition:
z3_api.h:1148
Z3_PARAMETER_DOUBLE
Definition:
z3_api.h:182
Z3_PARAMETER_AST
Definition:
z3_api.h:186
Z3_FLOATING_POINT_SORT
Definition:
z3_api.h:205
Z3_IOB
Definition:
z3_api.h:1315
Z3_OP_PR_COMMUTATIVITY
Definition:
z3_api.h:1128
Z3_OP_TRUE
Definition:
z3_api.h:990
Z3_OP_EXT_ROTATE_LEFT
Definition:
z3_api.h:1092
Z3_OP_AGNUM
Definition:
z3_api.h:1006
Z3_OP_IMPLIES
Definition:
z3_api.h:1000
Z3_OP_PR_IFF_TRUE
Definition:
z3_api.h:1126
Z3_PK_UINT
Definition:
z3_api.h:1240
Z3_OP_PR_TRANSITIVITY
Definition:
z3_api.h:1108
Z3_OP_BCOMP
Definition:
z3_api.h:1085
Z3_OP_DT_RECOGNISER
Definition:
z3_api.h:1164
Z3_OP_RA_JOIN
Definition:
z3_api.h:1146
Z3_PK_STRING
Definition:
z3_api.h:1244
Z3_OP_PB_LE
Definition:
z3_api.h:1170
Z3_OP_SUB
Definition:
z3_api.h:1012
Z3_OP_FPA_MAX
Definition:
z3_api.h:1195
Z3_OP_BADD
Definition:
z3_api.h:1042
Z3_SORT_AST
Definition:
z3_api.h:228
Z3_OP_DIV
Definition:
z3_api.h:1015
Z3_OP_PR_QUANT_INTRO
Definition:
z3_api.h:1111
Z3_UNKNOWN_AST
Definition:
z3_api.h:230
Z3_OP_FPA_TO_FP
Definition:
z3_api.h:1214
Z3_OP_BSMOD
Definition:
z3_api.h:1050
Z3_OP_ULEQ
Definition:
z3_api.h:1060
Z3_OP_RA_NEGATION_FILTER
Definition:
z3_api.h:1151
Z3_PK_OTHER
Definition:
z3_api.h:1245
Z3_UNINTERPRETED_SORT
Definition:
z3_api.h:196
Z3_OP_PR_PULL_QUANT_STAR
Definition:
z3_api.h:1118
Z3_OP_PR_DER
Definition:
z3_api.h:1121
Z3_OP_EQ
Definition:
z3_api.h:992
Z3_OP_FPA_IS_NEGATIVE
Definition:
z3_api.h:1210
Z3_OP_PR_UNIT_RESOLUTION
Definition:
z3_api.h:1125
Z3_OP_BSMOD0
Definition:
z3_api.h:1058
Z3_OP_TO_REAL
Definition:
z3_api.h:1019
Z3_OP_EXT_ROTATE_RIGHT
Definition:
z3_api.h:1093
Z3_OP_FPA_RM_TOWARD_NEGATIVE
Definition:
z3_api.h:1177
Z3_OP_BXOR
Definition:
z3_api.h:1072
Z3_OP_CONCAT
Definition:
z3_api.h:1077
Z3_OP_CARRY
Definition:
z3_api.h:1097
Z3_OP_BSDIV0
Definition:
z3_api.h:1054
Z3_PARAMETER_RATIONAL
Definition:
z3_api.h:183
Z3_PK_INVALID
Definition:
z3_api.h:1246
Z3_OP_BUREM0
Definition:
z3_api.h:1057
Z3_OP_XOR3
Definition:
z3_api.h:1098
Z3_OP_OEQ
Definition:
z3_api.h:1001
Z3_OP_TO_INT
Definition:
z3_api.h:1020
Z3_OP_IFF
Definition:
z3_api.h:997
Z3_INVALID_PATTERN
Definition:
z3_api.h:1319
Z3_OP_BREDOR
Definition:
z3_api.h:1083
Z3_OP_BUDIV
Definition:
z3_api.h:1047
Z3_OP_FPA_IS_ZERO
Definition:
z3_api.h:1207
Z3_RELATION_SORT
Definition:
z3_api.h:203
Z3_OP_EXTRACT
Definition:
z3_api.h:1080
Z3_OP_AND
Definition:
z3_api.h:995
Z3_OP_PR_TRUE
Definition:
z3_api.h:1102
Z3_OP_PR_DEF_INTRO
Definition:
z3_api.h:1130
Z3_OP_PR_CNF_STAR
Definition:
z3_api.h:1136
Z3_OP_BXNOR
Definition:
z3_api.h:1075
Z3_OP_DISTINCT
Definition:
z3_api.h:993
Z3_OP_BNOR
Definition:
z3_api.h:1074
Z3_OP_FPA_TO_SBV
Definition:
z3_api.h:1217
Z3_OP_PR_TRANSITIVITY_STAR
Definition:
z3_api.h:1109
Z3_OP_BASHR
Definition:
z3_api.h:1089
Z3_DATATYPE_SORT
Definition:
z3_api.h:202
Z3_OP_BLSHR
Definition:
z3_api.h:1088
Z3_PK_BOOL
Definition:
z3_api.h:1241
Z3_OP_BOR
Definition:
z3_api.h:1070
Z3_APP_AST
Definition:
z3_api.h:225
Z3_OP_ITE
Definition:
z3_api.h:994
Z3_OP_FPA_RM_TOWARD_POSITIVE
Definition:
z3_api.h:1176
Z3_OP_XOR
Definition:
z3_api.h:998
Z3_OP_PR_NNF_NEG
Definition:
z3_api.h:1134
Z3_OP_FD_LT
Definition:
z3_api.h:1156
Z3_OP_BNUM
Definition:
z3_api.h:1038
Z3_PRINT_SMTLIB2_COMPLIANT
Definition:
z3_api.h:1288
Z3_OP_BSUB
Definition:
z3_api.h:1043
Z3_OP_SGEQ
Definition:
z3_api.h:1063
Z3_OP_FPA_FMA
Definition:
z3_api.h:1196
Z3_OP_FPA_EQ
Definition:
z3_api.h:1200
Z3_OP_FPA_IS_NAN
Definition:
z3_api.h:1205
Microsoft.Z3.Z3_symbol_kind
Z3_symbol_kind
Z3_symbol_kind
Definition:
Enumerations.cs:17
Z3_OP_BNAND
Definition:
z3_api.h:1073
Z3_OP_PR_NNF_POS
Definition:
z3_api.h:1133
Z3_OP_SET_SUBSET
Definition:
z3_api.h:1034
Z3_OP_FPA_MINUS_INF
Definition:
z3_api.h:1182
Z3_OP_FPA_RM_TOWARD_ZERO
Definition:
z3_api.h:1178
Z3_OP_PR_IFF_FALSE
Definition:
z3_api.h:1127
Z3_PRINT_LOW_LEVEL
Definition:
z3_api.h:1286
Z3_PK_SYMBOL
Definition:
z3_api.h:1243
Z3_OP_BREDAND
Definition:
z3_api.h:1084
Z3_PRINT_SMTLIB_COMPLIANT
Definition:
z3_api.h:1287
Z3_OP_FPA_NUM
Definition:
z3_api.h:1180
Z3_OP_CONST_ARRAY
Definition:
z3_api.h:1027
Z3_OP_SELECT
Definition:
z3_api.h:1026
Z3_OP_UNINTERPRETED
Definition:
z3_api.h:1222
Z3_OP_PR_NOT_OR_ELIM
Definition:
z3_api.h:1114
Z3_REAL_SORT
Definition:
z3_api.h:199
Z3_OP_SLEQ
Definition:
z3_api.h:1061
Z3_OP_INTERP
Definition:
z3_api.h:1002
Microsoft.Z3.Z3_lbool
Z3_lbool
Z3_lbool
Definition:
Enumerations.cs:10
Z3_BV_SORT
Definition:
z3_api.h:200
Z3_UNKNOWN_SORT
Definition:
z3_api.h:207
Z3_OP_PR_MODUS_PONENS_OEQ
Definition:
z3_api.h:1138
Z3_GOAL_OVER
Definition:
z3_api.h:1389
Z3_OP_GE
Definition:
z3_api.h:1008
Z3_OP_FPA_ABS
Definition:
z3_api.h:1193
Z3_OP_SET_INTERSECT
Definition:
z3_api.h:1031
Z3_OP_RA_RENAME
Definition:
z3_api.h:1152
Z3_GOAL_UNDER
Definition:
z3_api.h:1388
Z3_OP_LE
Definition:
z3_api.h:1007
Z3_OP_FPA_IS_SUBNORMAL
Definition:
z3_api.h:1209
Z3_STRING_SYMBOL
Definition:
z3_api.h:161
Z3_OP_BNEG
Definition:
z3_api.h:1041
Z3_PRINT_SMTLIB_FULL
Definition:
z3_api.h:1285
Z3_OP_SET_DIFFERENCE
Definition:
z3_api.h:1032
Z3_PARSER_ERROR
Definition:
z3_api.h:1317
Z3_OP_FPA_REM
Definition:
z3_api.h:1192
Z3_OP_ADD
Definition:
z3_api.h:1011
Z3_SORT_ERROR
Definition:
z3_api.h:1314
Z3_OP_PR_LEMMA
Definition:
z3_api.h:1124
Z3_OP_FPA_PLUS_INF
Definition:
z3_api.h:1181
Z3_OP_FPA_SUB
Definition:
z3_api.h:1188
Z3_OP_PR_NNF_STAR
Definition:
z3_api.h:1135
Z3_OP_BMUL
Definition:
z3_api.h:1044
Z3_OP_PB_GE
Definition:
z3_api.h:1171
Z3_OP_FPA_TO_IEEE_BV
Definition:
z3_api.h:1220
Z3_OP_FPA_IS_INF
Definition:
z3_api.h:1206
Z3_OP_PR_DEF_AXIOM
Definition:
z3_api.h:1129
Z3_INTERNAL_FATAL
Definition:
z3_api.h:1322
Z3_PARAMETER_SYMBOL
Definition:
z3_api.h:184
Z3_OP_FPA_MIN
Definition:
z3_api.h:1194
Z3_OP_FPA_IS_POSITIVE
Definition:
z3_api.h:1211
Z3_EXCEPTION
Definition:
z3_api.h:1325
Z3_MEMOUT_FAIL
Definition:
z3_api.h:1320
Microsoft.Z3.Z3_ast_print_mode
Z3_ast_print_mode
Z3_ast_print_mode
Definition:
Enumerations.cs:275
Z3_OP_PR_UNDEF
Definition:
z3_api.h:1101
Z3_GOAL_PRECISE
Definition:
z3_api.h:1387
Z3_OP_UGT
Definition:
z3_api.h:1066
Z3_ARRAY_SORT
Definition:
z3_api.h:201
Z3_OP_POWER
Definition:
z3_api.h:1022
Z3_OP_PR_PULL_QUANT
Definition:
z3_api.h:1117
Z3_PARAMETER_INT
Definition:
z3_api.h:181
Z3_OP_FPA_DIV
Definition:
z3_api.h:1191
Z3_OP_RA_IS_EMPTY
Definition:
z3_api.h:1145
Z3_BOOL_SORT
Definition:
z3_api.h:197
Z3_NO_PARSER
Definition:
z3_api.h:1318
Z3_OP_BUDIV0
Definition:
z3_api.h:1055
Z3_OP_SLT
Definition:
z3_api.h:1065
Z3_OP_ARRAY_MAP
Definition:
z3_api.h:1028
Z3_OP_BNOT
Definition:
z3_api.h:1071
Z3_OP_BV2INT
Definition:
z3_api.h:1096
Z3_L_UNDEF
Definition:
z3_api.h:146
Z3_OP_OR
Definition:
z3_api.h:996
Z3_OP_FPA_IS_NORMAL
Definition:
z3_api.h:1208
Z3_INT_SYMBOL
Definition:
z3_api.h:160
Z3_OP_ROTATE_RIGHT
Definition:
z3_api.h:1091
Z3_OP_PR_SYMMETRY
Definition:
z3_api.h:1107
Z3_OP_ROTATE_LEFT
Definition:
z3_api.h:1090
Microsoft.Z3.Z3_parameter_kind
Z3_parameter_kind
Z3_parameter_kind
Definition:
Enumerations.cs:23
Z3_OP_RA_EMPTY
Definition:
z3_api.h:1144
Z3_OP_BSREM
Definition:
z3_api.h:1048
Z3_OP_ULT
Definition:
z3_api.h:1064
Z3_FINITE_DOMAIN_SORT
Definition:
z3_api.h:204
Z3_OP_STORE
Definition:
z3_api.h:1025
Z3_OP_FALSE
Definition:
z3_api.h:991
Z3_OP_PR_IFF_OEQ
Definition:
z3_api.h:1132
Z3_INT_SORT
Definition:
z3_api.h:198
Z3_OP_BAND
Definition:
z3_api.h:1069
Z3_OP_BIT1
Definition:
z3_api.h:1039
Z3_OP_REPEAT
Definition:
z3_api.h:1081
Z3_OP_RA_SELECT
Definition:
z3_api.h:1154
Z3_VAR_AST
Definition:
z3_api.h:226
Z3_OP_PR_PUSH_QUANT
Definition:
z3_api.h:1119
Z3_NUMERAL_AST
Definition:
z3_api.h:224
Generated on Tue Jul 19 2016 21:26:48 for Z3 by
1.8.11