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_UNINTERPRETED_SORT
= 0,
43
Z3_BOOL_SORT
= 1,
44
Z3_DATATYPE_SORT
= 6,
45
}
46
48
public
enum
Z3_ast_kind
{
49
Z3_VAR_AST
= 2,
50
Z3_SORT_AST
= 4,
51
Z3_QUANTIFIER_AST
= 3,
52
Z3_UNKNOWN_AST
= 1000,
53
Z3_FUNC_DECL_AST
= 5,
54
Z3_NUMERAL_AST
= 0,
55
Z3_APP_AST
= 1,
56
}
57
59
public
enum
Z3_decl_kind
{
60
Z3_OP_LABEL
= 1792,
61
Z3_OP_PR_REWRITE
= 1294,
62
Z3_OP_UNINTERPRETED
= 2051,
63
Z3_OP_SUB
= 519,
64
Z3_OP_ZERO_EXT
= 1058,
65
Z3_OP_ADD
= 518,
66
Z3_OP_IS_INT
= 528,
67
Z3_OP_BREDOR
= 1061,
68
Z3_OP_BNOT
= 1051,
69
Z3_OP_BNOR
= 1054,
70
Z3_OP_PR_CNF_STAR
= 1315,
71
Z3_OP_RA_JOIN
= 1539,
72
Z3_OP_LE
= 514,
73
Z3_OP_SET_UNION
= 773,
74
Z3_OP_PR_UNDEF
= 1280,
75
Z3_OP_BREDAND
= 1062,
76
Z3_OP_LT
= 516,
77
Z3_OP_RA_UNION
= 1540,
78
Z3_OP_BADD
= 1028,
79
Z3_OP_BUREM0
= 1039,
80
Z3_OP_OEQ
= 267,
81
Z3_OP_PR_MODUS_PONENS
= 1284,
82
Z3_OP_RA_CLONE
= 1548,
83
Z3_OP_REPEAT
= 1060,
84
Z3_OP_RA_NEGATION_FILTER
= 1544,
85
Z3_OP_BSMOD0
= 1040,
86
Z3_OP_BLSHR
= 1065,
87
Z3_OP_BASHR
= 1066,
88
Z3_OP_PR_UNIT_RESOLUTION
= 1304,
89
Z3_OP_ROTATE_RIGHT
= 1068,
90
Z3_OP_ARRAY_DEFAULT
= 772,
91
Z3_OP_PR_PULL_QUANT
= 1296,
92
Z3_OP_PR_APPLY_DEF
= 1310,
93
Z3_OP_PR_REWRITE_STAR
= 1295,
94
Z3_OP_IDIV
= 523,
95
Z3_OP_PR_GOAL
= 1283,
96
Z3_OP_PR_IFF_TRUE
= 1305,
97
Z3_OP_LABEL_LIT
= 1793,
98
Z3_OP_BOR
= 1050,
99
Z3_OP_PR_SYMMETRY
= 1286,
100
Z3_OP_TRUE
= 256,
101
Z3_OP_SET_COMPLEMENT
= 776,
102
Z3_OP_CONCAT
= 1056,
103
Z3_OP_PR_NOT_OR_ELIM
= 1293,
104
Z3_OP_IFF
= 263,
105
Z3_OP_BSHL
= 1064,
106
Z3_OP_PR_TRANSITIVITY
= 1287,
107
Z3_OP_SGT
= 1048,
108
Z3_OP_RA_WIDEN
= 1541,
109
Z3_OP_PR_DEF_INTRO
= 1309,
110
Z3_OP_NOT
= 265,
111
Z3_OP_PR_QUANT_INTRO
= 1290,
112
Z3_OP_UGT
= 1047,
113
Z3_OP_DT_RECOGNISER
= 2049,
114
Z3_OP_SET_INTERSECT
= 774,
115
Z3_OP_BSREM
= 1033,
116
Z3_OP_RA_STORE
= 1536,
117
Z3_OP_SLT
= 1046,
118
Z3_OP_ROTATE_LEFT
= 1067,
119
Z3_OP_PR_NNF_NEG
= 1313,
120
Z3_OP_PR_REFLEXIVITY
= 1285,
121
Z3_OP_ULEQ
= 1041,
122
Z3_OP_BIT1
= 1025,
123
Z3_OP_BIT0
= 1026,
124
Z3_OP_EQ
= 258,
125
Z3_OP_BMUL
= 1030,
126
Z3_OP_ARRAY_MAP
= 771,
127
Z3_OP_STORE
= 768,
128
Z3_OP_PR_HYPOTHESIS
= 1302,
129
Z3_OP_RA_RENAME
= 1545,
130
Z3_OP_AND
= 261,
131
Z3_OP_TO_REAL
= 526,
132
Z3_OP_PR_NNF_POS
= 1312,
133
Z3_OP_PR_AND_ELIM
= 1292,
134
Z3_OP_MOD
= 525,
135
Z3_OP_BUDIV0
= 1037,
136
Z3_OP_PR_TRUE
= 1281,
137
Z3_OP_BNAND
= 1053,
138
Z3_OP_PR_ELIM_UNUSED_VARS
= 1299,
139
Z3_OP_RA_FILTER
= 1543,
140
Z3_OP_FD_LT
= 1549,
141
Z3_OP_RA_EMPTY
= 1537,
142
Z3_OP_DIV
= 522,
143
Z3_OP_ANUM
= 512,
144
Z3_OP_MUL
= 521,
145
Z3_OP_UGEQ
= 1043,
146
Z3_OP_BSREM0
= 1038,
147
Z3_OP_PR_TH_LEMMA
= 1318,
148
Z3_OP_BXOR
= 1052,
149
Z3_OP_DISTINCT
= 259,
150
Z3_OP_PR_IFF_FALSE
= 1306,
151
Z3_OP_BV2INT
= 1072,
152
Z3_OP_EXT_ROTATE_LEFT
= 1069,
153
Z3_OP_PR_PULL_QUANT_STAR
= 1297,
154
Z3_OP_BSUB
= 1029,
155
Z3_OP_PR_ASSERTED
= 1282,
156
Z3_OP_BXNOR
= 1055,
157
Z3_OP_EXTRACT
= 1059,
158
Z3_OP_PR_DER
= 1300,
159
Z3_OP_DT_CONSTRUCTOR
= 2048,
160
Z3_OP_GT
= 517,
161
Z3_OP_BUREM
= 1034,
162
Z3_OP_IMPLIES
= 266,
163
Z3_OP_SLEQ
= 1042,
164
Z3_OP_GE
= 515,
165
Z3_OP_BAND
= 1049,
166
Z3_OP_ITE
= 260,
167
Z3_OP_AS_ARRAY
= 778,
168
Z3_OP_RA_SELECT
= 1547,
169
Z3_OP_CONST_ARRAY
= 770,
170
Z3_OP_BSDIV
= 1031,
171
Z3_OP_OR
= 262,
172
Z3_OP_PR_HYPER_RESOLVE
= 1319,
173
Z3_OP_AGNUM
= 513,
174
Z3_OP_PR_PUSH_QUANT
= 1298,
175
Z3_OP_BSMOD
= 1035,
176
Z3_OP_PR_IFF_OEQ
= 1311,
177
Z3_OP_INTERP
= 268,
178
Z3_OP_PR_LEMMA
= 1303,
179
Z3_OP_SET_SUBSET
= 777,
180
Z3_OP_SELECT
= 769,
181
Z3_OP_RA_PROJECT
= 1542,
182
Z3_OP_BNEG
= 1027,
183
Z3_OP_UMINUS
= 520,
184
Z3_OP_REM
= 524,
185
Z3_OP_TO_INT
= 527,
186
Z3_OP_PR_QUANT_INST
= 1301,
187
Z3_OP_SGEQ
= 1044,
188
Z3_OP_POWER
= 529,
189
Z3_OP_XOR3
= 1074,
190
Z3_OP_RA_IS_EMPTY
= 1538,
191
Z3_OP_CARRY
= 1073,
192
Z3_OP_DT_ACCESSOR
= 2050,
193
Z3_OP_PR_TRANSITIVITY_STAR
= 1288,
194
Z3_OP_PR_NNF_STAR
= 1314,
195
Z3_OP_PR_COMMUTATIVITY
= 1307,
196
Z3_OP_ULT
= 1045,
197
Z3_OP_BSDIV0
= 1036,
198
Z3_OP_SET_DIFFERENCE
= 775,
199
Z3_OP_INT2BV
= 1071,
200
Z3_OP_XOR
= 264,
201
Z3_OP_PR_MODUS_PONENS_OEQ
= 1317,
202
Z3_OP_BNUM
= 1024,
203
Z3_OP_BUDIV
= 1032,
204
Z3_OP_PR_MONOTONICITY
= 1289,
205
Z3_OP_PR_DEF_AXIOM
= 1308,
206
Z3_OP_FALSE
= 257,
207
Z3_OP_EXT_ROTATE_RIGHT
= 1070,
208
Z3_OP_PR_DISTRIBUTIVITY
= 1291,
209
Z3_OP_SIGN_EXT
= 1057,
210
Z3_OP_PR_SKOLEMIZE
= 1316,
211
Z3_OP_BCOMP
= 1063,
212
Z3_OP_RA_COMPLEMENT
= 1546,
213
}
214
216
public
enum
Z3_param_kind
{
217
Z3_PK_BOOL
= 1,
218
Z3_PK_SYMBOL
= 3,
219
Z3_PK_OTHER
= 5,
220
Z3_PK_INVALID
= 6,
221
Z3_PK_UINT
= 0,
222
Z3_PK_STRING
= 4,
223
Z3_PK_DOUBLE
= 2,
224
}
225
227
public
enum
Z3_ast_print_mode
{
228
Z3_PRINT_SMTLIB2_COMPLIANT
= 3,
229
Z3_PRINT_SMTLIB_COMPLIANT
= 2,
230
Z3_PRINT_SMTLIB_FULL
= 0,
231
Z3_PRINT_LOW_LEVEL
= 1,
232
}
233
235
public
enum
Z3_error_code
{
236
Z3_INVALID_PATTERN
= 6,
237
Z3_MEMOUT_FAIL
= 7,
238
Z3_NO_PARSER
= 5,
239
Z3_OK
= 0,
240
Z3_INVALID_ARG
= 3,
241
Z3_EXCEPTION
= 12,
242
Z3_IOB
= 2,
243
Z3_INTERNAL_FATAL
= 9,
244
Z3_INVALID_USAGE
= 10,
245
Z3_FILE_ACCESS_ERROR
= 8,
246
Z3_SORT_ERROR
= 1,
247
Z3_PARSER_ERROR
= 4,
248
Z3_DEC_REF_ERROR
= 11,
249
}
250
252
public
enum
Z3_goal_prec
{
253
Z3_GOAL_UNDER
= 1,
254
Z3_GOAL_PRECISE
= 0,
255
Z3_GOAL_UNDER_OVER
= 3,
256
Z3_GOAL_OVER
= 2,
257
}
258
259
}
Z3_OP_LT
Definition:
z3_api.h:901
Z3_OP_PR_SKOLEMIZE
Definition:
z3_api.h:1029
Z3_OP_BSREM0
Definition:
z3_api.h:948
Z3_OP_LABEL_LIT
Definition:
z3_api.h:1052
Z3_OP_PR_HYPOTHESIS
Definition:
z3_api.h:1015
Z3_OP_NOT
Definition:
z3_api.h:891
Z3_OP_DT_CONSTRUCTOR
Definition:
z3_api.h:1055
Z3_OP_RA_CLONE
Definition:
z3_api.h:1047
Z3_OP_INT2BV
Definition:
z3_api.h:987
Microsoft.Z3.Z3_param_kind
Z3_param_kind
Z3_param_kind
Definition:
Enumerations.cs:216
Z3_OP_RA_COMPLEMENT
Definition:
z3_api.h:1045
Z3_OP_UMINUS
Definition:
z3_api.h:905
Z3_OP_AS_ARRAY
Definition:
z3_api.h:927
Z3_OP_RA_UNION
Definition:
z3_api.h:1039
Z3_OP_RA_STORE
Definition:
z3_api.h:1035
Z3_OP_SIGN_EXT
Definition:
z3_api.h:970
Z3_OP_ARRAY_DEFAULT
Definition:
z3_api.h:921
Z3_OK
Definition:
z3_api.h:1150
Z3_PARAMETER_FUNC_DECL
Definition:
z3_api.h:179
Z3_OP_PR_GOAL
Definition:
z3_api.h:996
Z3_L_TRUE
Definition:
z3_api.h:139
Z3_OP_ZERO_EXT
Definition:
z3_api.h:971
Z3_OP_PR_QUANT_INST
Definition:
z3_api.h:1014
Z3_OP_PR_ELIM_UNUSED_VARS
Definition:
z3_api.h:1012
Z3_FUNC_DECL_AST
Definition:
z3_api.h:219
Microsoft.Z3.Z3_error_code
Z3_error_code
Z3_error_code
Definition:
Enumerations.cs:235
Z3_OP_ANUM
Definition:
z3_api.h:897
Z3_OP_PR_REWRITE
Definition:
z3_api.h:1007
Z3_INVALID_USAGE
Definition:
z3_api.h:1160
Microsoft.Z3.Z3_sort_kind
Z3_sort_kind
Z3_sort_kind
Definition:
Enumerations.cs:34
Z3_OP_GT
Definition:
z3_api.h:902
Z3_OP_PR_APPLY_DEF
Definition:
z3_api.h:1023
Z3_OP_PR_REFLEXIVITY
Definition:
z3_api.h:998
System
Z3_L_FALSE
Definition:
z3_api.h:137
Z3_PK_DOUBLE
Definition:
z3_api.h:1079
Z3_OP_PR_REWRITE_STAR
Definition:
z3_api.h:1008
Z3_OP_BIT0
Definition:
z3_api.h:932
Z3_OP_BSDIV
Definition:
z3_api.h:938
Z3_OP_IS_INT
Definition:
z3_api.h:913
Z3_OP_PR_MONOTONICITY
Definition:
z3_api.h:1002
Z3_OP_MUL
Definition:
z3_api.h:906
Z3_OP_PR_TH_LEMMA
Definition:
z3_api.h:1031
Z3_GOAL_UNDER_OVER
Definition:
z3_api.h:1226
Z3_PARAMETER_SORT
Definition:
z3_api.h:177
Z3_OP_PR_HYPER_RESOLVE
Definition:
z3_api.h:1032
Z3_OP_PR_MODUS_PONENS
Definition:
z3_api.h:997
Z3_OP_PR_DISTRIBUTIVITY
Definition:
z3_api.h:1004
Z3_INVALID_ARG
Definition:
z3_api.h:1153
Z3_OP_RA_FILTER
Definition:
z3_api.h:1042
Microsoft
Microsoft.Z3.Z3_decl_kind
Z3_decl_kind
Z3_decl_kind
Definition:
Enumerations.cs:59
Z3_OP_RA_PROJECT
Definition:
z3_api.h:1041
Z3_OP_REM
Definition:
z3_api.h:909
Microsoft.Z3.Z3_goal_prec
Z3_goal_prec
Z3_goal_prec
Definition:
Enumerations.cs:252
Microsoft.Z3.Z3_ast_kind
Z3_ast_kind
Z3_ast_kind
Definition:
Enumerations.cs:48
Z3_OP_LABEL
Definition:
z3_api.h:1051
Z3_QUANTIFIER_AST
Definition:
z3_api.h:217
Z3_OP_SGT
Definition:
z3_api.h:959
Z3_OP_MOD
Definition:
z3_api.h:910
Z3_OP_SET_COMPLEMENT
Definition:
z3_api.h:925
Z3_OP_UGEQ
Definition:
z3_api.h:954
Z3_OP_SET_UNION
Definition:
z3_api.h:922
Z3_OP_PR_ASSERTED
Definition:
z3_api.h:995
Z3_FILE_ACCESS_ERROR
Definition:
z3_api.h:1158
Z3_OP_DT_ACCESSOR
Definition:
z3_api.h:1057
Z3_OP_IDIV
Definition:
z3_api.h:908
Z3_OP_PR_AND_ELIM
Definition:
z3_api.h:1005
Z3_OP_BSHL
Definition:
z3_api.h:979
Z3_OP_BUREM
Definition:
z3_api.h:941
Z3_DEC_REF_ERROR
Definition:
z3_api.h:1161
Z3_OP_RA_WIDEN
Definition:
z3_api.h:1040
Z3_PARAMETER_DOUBLE
Definition:
z3_api.h:174
Z3_PARAMETER_AST
Definition:
z3_api.h:178
Z3_IOB
Definition:
z3_api.h:1152
Z3_OP_PR_COMMUTATIVITY
Definition:
z3_api.h:1020
Z3_OP_TRUE
Definition:
z3_api.h:882
Z3_OP_EXT_ROTATE_LEFT
Definition:
z3_api.h:984
Z3_OP_AGNUM
Definition:
z3_api.h:898
Z3_OP_IMPLIES
Definition:
z3_api.h:892
Z3_OP_PR_IFF_TRUE
Definition:
z3_api.h:1018
Z3_PK_UINT
Definition:
z3_api.h:1077
Z3_OP_PR_TRANSITIVITY
Definition:
z3_api.h:1000
Z3_OP_BCOMP
Definition:
z3_api.h:977
Z3_OP_DT_RECOGNISER
Definition:
z3_api.h:1056
Z3_OP_RA_JOIN
Definition:
z3_api.h:1038
Z3_PK_STRING
Definition:
z3_api.h:1081
Z3_OP_SUB
Definition:
z3_api.h:904
Z3_OP_BADD
Definition:
z3_api.h:934
Z3_SORT_AST
Definition:
z3_api.h:218
Z3_OP_DIV
Definition:
z3_api.h:907
Z3_OP_PR_QUANT_INTRO
Definition:
z3_api.h:1003
Z3_UNKNOWN_AST
Definition:
z3_api.h:220
Z3_OP_BSMOD
Definition:
z3_api.h:942
Z3_OP_ULEQ
Definition:
z3_api.h:952
Z3_OP_RA_NEGATION_FILTER
Definition:
z3_api.h:1043
Z3_PK_OTHER
Definition:
z3_api.h:1082
Z3_UNINTERPRETED_SORT
Definition:
z3_api.h:188
Z3_OP_PR_PULL_QUANT_STAR
Definition:
z3_api.h:1010
Z3_OP_PR_DER
Definition:
z3_api.h:1013
Z3_OP_EQ
Definition:
z3_api.h:884
Z3_OP_PR_UNIT_RESOLUTION
Definition:
z3_api.h:1017
Z3_OP_BSMOD0
Definition:
z3_api.h:950
Z3_OP_TO_REAL
Definition:
z3_api.h:911
Z3_OP_EXT_ROTATE_RIGHT
Definition:
z3_api.h:985
Z3_OP_BXOR
Definition:
z3_api.h:964
Z3_OP_CONCAT
Definition:
z3_api.h:969
Z3_OP_CARRY
Definition:
z3_api.h:989
Z3_OP_BSDIV0
Definition:
z3_api.h:946
Z3_PARAMETER_RATIONAL
Definition:
z3_api.h:175
Z3_PK_INVALID
Definition:
z3_api.h:1083
Z3_OP_BUREM0
Definition:
z3_api.h:949
Z3_OP_XOR3
Definition:
z3_api.h:990
Z3_OP_OEQ
Definition:
z3_api.h:893
Z3_OP_TO_INT
Definition:
z3_api.h:912
Z3_OP_IFF
Definition:
z3_api.h:889
Z3_INVALID_PATTERN
Definition:
z3_api.h:1156
Z3_OP_BREDOR
Definition:
z3_api.h:975
Z3_OP_BUDIV
Definition:
z3_api.h:939
Z3_RELATION_SORT
Definition:
z3_api.h:195
Z3_OP_EXTRACT
Definition:
z3_api.h:972
Z3_OP_AND
Definition:
z3_api.h:887
Z3_OP_PR_TRUE
Definition:
z3_api.h:994
Z3_OP_PR_DEF_INTRO
Definition:
z3_api.h:1022
Z3_OP_PR_CNF_STAR
Definition:
z3_api.h:1028
Z3_OP_BXNOR
Definition:
z3_api.h:967
Z3_OP_DISTINCT
Definition:
z3_api.h:885
Z3_OP_BNOR
Definition:
z3_api.h:966
Z3_OP_PR_TRANSITIVITY_STAR
Definition:
z3_api.h:1001
Z3_OP_BASHR
Definition:
z3_api.h:981
Z3_DATATYPE_SORT
Definition:
z3_api.h:194
Z3_OP_BLSHR
Definition:
z3_api.h:980
Z3_PK_BOOL
Definition:
z3_api.h:1078
Z3_OP_BOR
Definition:
z3_api.h:962
Z3_APP_AST
Definition:
z3_api.h:215
Z3_OP_ITE
Definition:
z3_api.h:886
Z3_OP_XOR
Definition:
z3_api.h:890
Z3_OP_PR_NNF_NEG
Definition:
z3_api.h:1026
Z3_OP_FD_LT
Definition:
z3_api.h:1048
Z3_OP_BNUM
Definition:
z3_api.h:930
Z3_PRINT_SMTLIB2_COMPLIANT
Definition:
z3_api.h:1125
Z3_OP_BSUB
Definition:
z3_api.h:935
Z3_OP_SGEQ
Definition:
z3_api.h:955
Microsoft.Z3.Z3_symbol_kind
Z3_symbol_kind
Z3_symbol_kind
Definition:
Enumerations.cs:17
Z3_OP_BNAND
Definition:
z3_api.h:965
Z3_OP_PR_NNF_POS
Definition:
z3_api.h:1025
Z3_OP_SET_SUBSET
Definition:
z3_api.h:926
Z3_OP_PR_IFF_FALSE
Definition:
z3_api.h:1019
Z3_PRINT_LOW_LEVEL
Definition:
z3_api.h:1123
Z3_PK_SYMBOL
Definition:
z3_api.h:1080
Z3_OP_BREDAND
Definition:
z3_api.h:976
Z3_PRINT_SMTLIB_COMPLIANT
Definition:
z3_api.h:1124
Z3_OP_CONST_ARRAY
Definition:
z3_api.h:919
Z3_OP_SELECT
Definition:
z3_api.h:918
Z3_OP_UNINTERPRETED
Definition:
z3_api.h:1059
Z3_OP_PR_NOT_OR_ELIM
Definition:
z3_api.h:1006
Z3_REAL_SORT
Definition:
z3_api.h:191
Z3_OP_SLEQ
Definition:
z3_api.h:953
Z3_OP_INTERP
Definition:
z3_api.h:894
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:197
Z3_OP_PR_MODUS_PONENS_OEQ
Definition:
z3_api.h:1030
Z3_GOAL_OVER
Definition:
z3_api.h:1225
Z3_OP_GE
Definition:
z3_api.h:900
Z3_OP_SET_INTERSECT
Definition:
z3_api.h:923
Z3_OP_RA_RENAME
Definition:
z3_api.h:1044
Z3_GOAL_UNDER
Definition:
z3_api.h:1224
Z3_OP_LE
Definition:
z3_api.h:899
Z3_STRING_SYMBOL
Definition:
z3_api.h:153
Z3_OP_BNEG
Definition:
z3_api.h:933
Z3_PRINT_SMTLIB_FULL
Definition:
z3_api.h:1122
Z3_OP_SET_DIFFERENCE
Definition:
z3_api.h:924
Z3_PARSER_ERROR
Definition:
z3_api.h:1154
Z3_OP_ADD
Definition:
z3_api.h:903
Z3_SORT_ERROR
Definition:
z3_api.h:1151
Z3_OP_PR_LEMMA
Definition:
z3_api.h:1016
Z3_OP_PR_NNF_STAR
Definition:
z3_api.h:1027
Z3_OP_BMUL
Definition:
z3_api.h:936
Z3_OP_PR_DEF_AXIOM
Definition:
z3_api.h:1021
Z3_INTERNAL_FATAL
Definition:
z3_api.h:1159
Z3_PARAMETER_SYMBOL
Definition:
z3_api.h:176
Z3_EXCEPTION
Definition:
z3_api.h:1162
Z3_MEMOUT_FAIL
Definition:
z3_api.h:1157
Microsoft.Z3.Z3_ast_print_mode
Z3_ast_print_mode
Z3_ast_print_mode
Definition:
Enumerations.cs:227
Z3_OP_PR_UNDEF
Definition:
z3_api.h:993
Z3_GOAL_PRECISE
Definition:
z3_api.h:1223
Z3_OP_UGT
Definition:
z3_api.h:958
Z3_ARRAY_SORT
Definition:
z3_api.h:193
Z3_OP_POWER
Definition:
z3_api.h:914
Z3_OP_PR_PULL_QUANT
Definition:
z3_api.h:1009
Z3_PARAMETER_INT
Definition:
z3_api.h:173
Z3_OP_RA_IS_EMPTY
Definition:
z3_api.h:1037
Z3_BOOL_SORT
Definition:
z3_api.h:189
Z3_NO_PARSER
Definition:
z3_api.h:1155
Z3_OP_BUDIV0
Definition:
z3_api.h:947
Z3_OP_SLT
Definition:
z3_api.h:957
Z3_OP_ARRAY_MAP
Definition:
z3_api.h:920
Z3_OP_BNOT
Definition:
z3_api.h:963
Z3_OP_BV2INT
Definition:
z3_api.h:988
Z3_L_UNDEF
Definition:
z3_api.h:138
Z3_OP_OR
Definition:
z3_api.h:888
Z3_INT_SYMBOL
Definition:
z3_api.h:152
Z3_OP_ROTATE_RIGHT
Definition:
z3_api.h:983
Z3_OP_PR_SYMMETRY
Definition:
z3_api.h:999
Z3_OP_ROTATE_LEFT
Definition:
z3_api.h:982
Microsoft.Z3.Z3_parameter_kind
Z3_parameter_kind
Z3_parameter_kind
Definition:
Enumerations.cs:23
Z3_OP_RA_EMPTY
Definition:
z3_api.h:1036
Z3_OP_BSREM
Definition:
z3_api.h:940
Z3_OP_ULT
Definition:
z3_api.h:956
Z3_FINITE_DOMAIN_SORT
Definition:
z3_api.h:196
Z3_OP_STORE
Definition:
z3_api.h:917
Z3_OP_FALSE
Definition:
z3_api.h:883
Z3_OP_PR_IFF_OEQ
Definition:
z3_api.h:1024
Z3_INT_SORT
Definition:
z3_api.h:190
Z3_OP_BAND
Definition:
z3_api.h:961
Z3_OP_BIT1
Definition:
z3_api.h:931
Z3_OP_REPEAT
Definition:
z3_api.h:973
Z3_OP_RA_SELECT
Definition:
z3_api.h:1046
Z3_VAR_AST
Definition:
z3_api.h:216
Z3_OP_PR_PUSH_QUANT
Definition:
z3_api.h:1011
Z3_NUMERAL_AST
Definition:
z3_api.h:214
Generated on Sat Apr 25 2015 18:37:47 for Z3 by
1.8.9.1