Z3
src
api
java
enumerations
Z3_decl_kind.java
Go to the documentation of this file.
1
5
package
com.microsoft.z3.enumerations;
6
7
import
java.util.HashMap;
8
import
java.util.Map;
9
13
public
enum
Z3_decl_kind
{
14
Z3_OP_TRUE
(256),
15
Z3_OP_FALSE
(257),
16
Z3_OP_EQ
(258),
17
Z3_OP_DISTINCT
(259),
18
Z3_OP_ITE
(260),
19
Z3_OP_AND
(261),
20
Z3_OP_OR
(262),
21
Z3_OP_IFF
(263),
22
Z3_OP_XOR
(264),
23
Z3_OP_NOT
(265),
24
Z3_OP_IMPLIES
(266),
25
Z3_OP_OEQ
(267),
26
Z3_OP_INTERP
(268),
27
Z3_OP_ANUM
(512),
28
Z3_OP_AGNUM
(513),
29
Z3_OP_LE
(514),
30
Z3_OP_GE
(515),
31
Z3_OP_LT
(516),
32
Z3_OP_GT
(517),
33
Z3_OP_ADD
(518),
34
Z3_OP_SUB
(519),
35
Z3_OP_UMINUS
(520),
36
Z3_OP_MUL
(521),
37
Z3_OP_DIV
(522),
38
Z3_OP_IDIV
(523),
39
Z3_OP_REM
(524),
40
Z3_OP_MOD
(525),
41
Z3_OP_TO_REAL
(526),
42
Z3_OP_TO_INT
(527),
43
Z3_OP_IS_INT
(528),
44
Z3_OP_POWER
(529),
45
Z3_OP_STORE
(768),
46
Z3_OP_SELECT
(769),
47
Z3_OP_CONST_ARRAY
(770),
48
Z3_OP_ARRAY_MAP
(771),
49
Z3_OP_ARRAY_DEFAULT
(772),
50
Z3_OP_SET_UNION
(773),
51
Z3_OP_SET_INTERSECT
(774),
52
Z3_OP_SET_DIFFERENCE
(775),
53
Z3_OP_SET_COMPLEMENT
(776),
54
Z3_OP_SET_SUBSET
(777),
55
Z3_OP_AS_ARRAY
(778),
56
Z3_OP_ARRAY_EXT
(779),
57
Z3_OP_BNUM
(1024),
58
Z3_OP_BIT1
(1025),
59
Z3_OP_BIT0
(1026),
60
Z3_OP_BNEG
(1027),
61
Z3_OP_BADD
(1028),
62
Z3_OP_BSUB
(1029),
63
Z3_OP_BMUL
(1030),
64
Z3_OP_BSDIV
(1031),
65
Z3_OP_BUDIV
(1032),
66
Z3_OP_BSREM
(1033),
67
Z3_OP_BUREM
(1034),
68
Z3_OP_BSMOD
(1035),
69
Z3_OP_BSDIV0
(1036),
70
Z3_OP_BUDIV0
(1037),
71
Z3_OP_BSREM0
(1038),
72
Z3_OP_BUREM0
(1039),
73
Z3_OP_BSMOD0
(1040),
74
Z3_OP_ULEQ
(1041),
75
Z3_OP_SLEQ
(1042),
76
Z3_OP_UGEQ
(1043),
77
Z3_OP_SGEQ
(1044),
78
Z3_OP_ULT
(1045),
79
Z3_OP_SLT
(1046),
80
Z3_OP_UGT
(1047),
81
Z3_OP_SGT
(1048),
82
Z3_OP_BAND
(1049),
83
Z3_OP_BOR
(1050),
84
Z3_OP_BNOT
(1051),
85
Z3_OP_BXOR
(1052),
86
Z3_OP_BNAND
(1053),
87
Z3_OP_BNOR
(1054),
88
Z3_OP_BXNOR
(1055),
89
Z3_OP_CONCAT
(1056),
90
Z3_OP_SIGN_EXT
(1057),
91
Z3_OP_ZERO_EXT
(1058),
92
Z3_OP_EXTRACT
(1059),
93
Z3_OP_REPEAT
(1060),
94
Z3_OP_BREDOR
(1061),
95
Z3_OP_BREDAND
(1062),
96
Z3_OP_BCOMP
(1063),
97
Z3_OP_BSHL
(1064),
98
Z3_OP_BLSHR
(1065),
99
Z3_OP_BASHR
(1066),
100
Z3_OP_ROTATE_LEFT
(1067),
101
Z3_OP_ROTATE_RIGHT
(1068),
102
Z3_OP_EXT_ROTATE_LEFT
(1069),
103
Z3_OP_EXT_ROTATE_RIGHT
(1070),
104
Z3_OP_INT2BV
(1071),
105
Z3_OP_BV2INT
(1072),
106
Z3_OP_CARRY
(1073),
107
Z3_OP_XOR3
(1074),
108
Z3_OP_BSMUL_NO_OVFL
(1075),
109
Z3_OP_BUMUL_NO_OVFL
(1076),
110
Z3_OP_BSMUL_NO_UDFL
(1077),
111
Z3_OP_BSDIV_I
(1078),
112
Z3_OP_BUDIV_I
(1079),
113
Z3_OP_BSREM_I
(1080),
114
Z3_OP_BUREM_I
(1081),
115
Z3_OP_BSMOD_I
(1082),
116
Z3_OP_PR_UNDEF
(1280),
117
Z3_OP_PR_TRUE
(1281),
118
Z3_OP_PR_ASSERTED
(1282),
119
Z3_OP_PR_GOAL
(1283),
120
Z3_OP_PR_MODUS_PONENS
(1284),
121
Z3_OP_PR_REFLEXIVITY
(1285),
122
Z3_OP_PR_SYMMETRY
(1286),
123
Z3_OP_PR_TRANSITIVITY
(1287),
124
Z3_OP_PR_TRANSITIVITY_STAR
(1288),
125
Z3_OP_PR_MONOTONICITY
(1289),
126
Z3_OP_PR_QUANT_INTRO
(1290),
127
Z3_OP_PR_DISTRIBUTIVITY
(1291),
128
Z3_OP_PR_AND_ELIM
(1292),
129
Z3_OP_PR_NOT_OR_ELIM
(1293),
130
Z3_OP_PR_REWRITE
(1294),
131
Z3_OP_PR_REWRITE_STAR
(1295),
132
Z3_OP_PR_PULL_QUANT
(1296),
133
Z3_OP_PR_PULL_QUANT_STAR
(1297),
134
Z3_OP_PR_PUSH_QUANT
(1298),
135
Z3_OP_PR_ELIM_UNUSED_VARS
(1299),
136
Z3_OP_PR_DER
(1300),
137
Z3_OP_PR_QUANT_INST
(1301),
138
Z3_OP_PR_HYPOTHESIS
(1302),
139
Z3_OP_PR_LEMMA
(1303),
140
Z3_OP_PR_UNIT_RESOLUTION
(1304),
141
Z3_OP_PR_IFF_TRUE
(1305),
142
Z3_OP_PR_IFF_FALSE
(1306),
143
Z3_OP_PR_COMMUTATIVITY
(1307),
144
Z3_OP_PR_DEF_AXIOM
(1308),
145
Z3_OP_PR_DEF_INTRO
(1309),
146
Z3_OP_PR_APPLY_DEF
(1310),
147
Z3_OP_PR_IFF_OEQ
(1311),
148
Z3_OP_PR_NNF_POS
(1312),
149
Z3_OP_PR_NNF_NEG
(1313),
150
Z3_OP_PR_NNF_STAR
(1314),
151
Z3_OP_PR_CNF_STAR
(1315),
152
Z3_OP_PR_SKOLEMIZE
(1316),
153
Z3_OP_PR_MODUS_PONENS_OEQ
(1317),
154
Z3_OP_PR_TH_LEMMA
(1318),
155
Z3_OP_PR_HYPER_RESOLVE
(1319),
156
Z3_OP_RA_STORE
(1536),
157
Z3_OP_RA_EMPTY
(1537),
158
Z3_OP_RA_IS_EMPTY
(1538),
159
Z3_OP_RA_JOIN
(1539),
160
Z3_OP_RA_UNION
(1540),
161
Z3_OP_RA_WIDEN
(1541),
162
Z3_OP_RA_PROJECT
(1542),
163
Z3_OP_RA_FILTER
(1543),
164
Z3_OP_RA_NEGATION_FILTER
(1544),
165
Z3_OP_RA_RENAME
(1545),
166
Z3_OP_RA_COMPLEMENT
(1546),
167
Z3_OP_RA_SELECT
(1547),
168
Z3_OP_RA_CLONE
(1548),
169
Z3_OP_FD_CONSTANT
(1549),
170
Z3_OP_FD_LT
(1550),
171
Z3_OP_SEQ_UNIT
(1551),
172
Z3_OP_SEQ_EMPTY
(1552),
173
Z3_OP_SEQ_CONCAT
(1553),
174
Z3_OP_SEQ_PREFIX
(1554),
175
Z3_OP_SEQ_SUFFIX
(1555),
176
Z3_OP_SEQ_CONTAINS
(1556),
177
Z3_OP_SEQ_EXTRACT
(1557),
178
Z3_OP_SEQ_REPLACE
(1558),
179
Z3_OP_SEQ_AT
(1559),
180
Z3_OP_SEQ_LENGTH
(1560),
181
Z3_OP_SEQ_INDEX
(1561),
182
Z3_OP_SEQ_TO_RE
(1562),
183
Z3_OP_SEQ_IN_RE
(1563),
184
Z3_OP_RE_PLUS
(1564),
185
Z3_OP_RE_STAR
(1565),
186
Z3_OP_RE_OPTION
(1566),
187
Z3_OP_RE_CONCAT
(1567),
188
Z3_OP_RE_UNION
(1568),
189
Z3_OP_LABEL
(1792),
190
Z3_OP_LABEL_LIT
(1793),
191
Z3_OP_DT_CONSTRUCTOR
(2048),
192
Z3_OP_DT_RECOGNISER
(2049),
193
Z3_OP_DT_ACCESSOR
(2050),
194
Z3_OP_DT_UPDATE_FIELD
(2051),
195
Z3_OP_PB_AT_MOST
(2304),
196
Z3_OP_PB_LE
(2305),
197
Z3_OP_PB_GE
(2306),
198
Z3_OP_PB_EQ
(2307),
199
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
(2308),
200
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
(2309),
201
Z3_OP_FPA_RM_TOWARD_POSITIVE
(2310),
202
Z3_OP_FPA_RM_TOWARD_NEGATIVE
(2311),
203
Z3_OP_FPA_RM_TOWARD_ZERO
(2312),
204
Z3_OP_FPA_NUM
(2313),
205
Z3_OP_FPA_PLUS_INF
(2314),
206
Z3_OP_FPA_MINUS_INF
(2315),
207
Z3_OP_FPA_NAN
(2316),
208
Z3_OP_FPA_PLUS_ZERO
(2317),
209
Z3_OP_FPA_MINUS_ZERO
(2318),
210
Z3_OP_FPA_ADD
(2319),
211
Z3_OP_FPA_SUB
(2320),
212
Z3_OP_FPA_NEG
(2321),
213
Z3_OP_FPA_MUL
(2322),
214
Z3_OP_FPA_DIV
(2323),
215
Z3_OP_FPA_REM
(2324),
216
Z3_OP_FPA_ABS
(2325),
217
Z3_OP_FPA_MIN
(2326),
218
Z3_OP_FPA_MAX
(2327),
219
Z3_OP_FPA_FMA
(2328),
220
Z3_OP_FPA_SQRT
(2329),
221
Z3_OP_FPA_ROUND_TO_INTEGRAL
(2330),
222
Z3_OP_FPA_EQ
(2331),
223
Z3_OP_FPA_LT
(2332),
224
Z3_OP_FPA_GT
(2333),
225
Z3_OP_FPA_LE
(2334),
226
Z3_OP_FPA_GE
(2335),
227
Z3_OP_FPA_IS_NAN
(2336),
228
Z3_OP_FPA_IS_INF
(2337),
229
Z3_OP_FPA_IS_ZERO
(2338),
230
Z3_OP_FPA_IS_NORMAL
(2339),
231
Z3_OP_FPA_IS_SUBNORMAL
(2340),
232
Z3_OP_FPA_IS_NEGATIVE
(2341),
233
Z3_OP_FPA_IS_POSITIVE
(2342),
234
Z3_OP_FPA_FP
(2343),
235
Z3_OP_FPA_TO_FP
(2344),
236
Z3_OP_FPA_TO_FP_UNSIGNED
(2345),
237
Z3_OP_FPA_TO_UBV
(2346),
238
Z3_OP_FPA_TO_SBV
(2347),
239
Z3_OP_FPA_TO_REAL
(2348),
240
Z3_OP_FPA_TO_IEEE_BV
(2349),
241
Z3_OP_FPA_MIN_I
(2350),
242
Z3_OP_FPA_MAX_I
(2351),
243
Z3_OP_INTERNAL
(2352),
244
Z3_OP_UNINTERPRETED
(2353);
245
246
private
final
int
intValue;
247
248
Z3_decl_kind
(
int
v) {
249
this.intValue = v;
250
}
251
252
// Cannot initialize map in constructor, so need to do it lazily.
253
// Easiest thread-safe way is the initialization-on-demand holder pattern.
254
private
static
class
Z3_decl_kind_MappingHolder {
255
private
static
final
Map<Integer, Z3_decl_kind> intMapping =
new
HashMap<>();
256
static
{
257
for
(
Z3_decl_kind
k :
Z3_decl_kind
.values())
258
intMapping.put(k.toInt(), k);
259
}
260
}
261
262
public
static
final
Z3_decl_kind
fromInt
(
int
v) {
263
Z3_decl_kind
k = Z3_decl_kind_MappingHolder.intMapping.get(v);
264
if
(k != null)
return
k;
265
throw
new
IllegalArgumentException(
"Illegal value "
+ v +
" for Z3_decl_kind"
);
266
}
267
268
public
final
int
toInt
() {
return
this.intValue; }
269
}
270
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AGNUM
Z3_OP_AGNUM
Definition:
Z3_decl_kind.java:28
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TH_LEMMA
Z3_OP_PR_TH_LEMMA
Definition:
Z3_decl_kind.java:154
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LABEL
Z3_OP_LABEL
Definition:
Z3_decl_kind.java:189
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXTRACT
Z3_OP_EXTRACT
Definition:
Z3_decl_kind.java:92
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE
Z3_OP_FPA_RM_TOWARD_POSITIVE
Definition:
Z3_decl_kind.java:201
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_FP
Z3_OP_FPA_TO_FP
Definition:
Z3_decl_kind.java:235
com.microsoft.z3.enumerations.Z3_decl_kind.fromInt
static final Z3_decl_kind fromInt(int v)
Definition:
Z3_decl_kind.java:262
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_EXTRACT
Z3_OP_SEQ_EXTRACT
Definition:
Z3_decl_kind.java:177
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_MUL
Z3_OP_MUL
Definition:
Z3_decl_kind.java:36
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REFLEXIVITY
Z3_OP_PR_REFLEXIVITY
Definition:
Z3_decl_kind.java:121
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_EMPTY
Z3_OP_SEQ_EMPTY
Definition:
Z3_decl_kind.java:172
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNOR
Z3_OP_BNOR
Definition:
Z3_decl_kind.java:87
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_LEMMA
Z3_OP_PR_LEMMA
Definition:
Z3_decl_kind.java:139
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BREDAND
Z3_OP_BREDAND
Definition:
Z3_decl_kind.java:95
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_GT
Z3_OP_GT
Definition:
Z3_decl_kind.java:32
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BXNOR
Z3_OP_BXNOR
Definition:
Z3_decl_kind.java:88
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_INT2BV
Z3_OP_INT2BV
Definition:
Z3_decl_kind.java:104
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_CONCAT
Z3_OP_SEQ_CONCAT
Definition:
Z3_decl_kind.java:173
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_DIV
Z3_OP_FPA_DIV
Definition:
Z3_decl_kind.java:214
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM
Z3_OP_PR_NOT_OR_ELIM
Definition:
Z3_decl_kind.java:129
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AND
Z3_OP_AND
Definition:
Z3_decl_kind.java:19
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_NUM
Z3_OP_FPA_NUM
Definition:
Z3_decl_kind.java:204
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PB_EQ
Z3_OP_PB_EQ
Definition:
Z3_decl_kind.java:198
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ULT
Z3_OP_ULT
Definition:
Z3_decl_kind.java:78
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUMUL_NO_OVFL
Z3_OP_BUMUL_NO_OVFL
Definition:
Z3_decl_kind.java:109
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REWRITE
Z3_OP_PR_REWRITE
Definition:
Z3_decl_kind.java:130
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_UPDATE_FIELD
Z3_OP_DT_UPDATE_FIELD
Definition:
Z3_decl_kind.java:194
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_GE
Z3_OP_FPA_GE
Definition:
Z3_decl_kind.java:226
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_INTERP
Z3_OP_INTERP
Definition:
Z3_decl_kind.java:26
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD0
Z3_OP_BSMOD0
Definition:
Z3_decl_kind.java:73
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_TO_RE
Z3_OP_SEQ_TO_RE
Definition:
Z3_decl_kind.java:182
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_decl_kind
Z3_decl_kind(int v)
Definition:
Z3_decl_kind.java:248
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV
Z3_OP_BSDIV
Definition:
Z3_decl_kind.java:64
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Definition:
Z3_decl_kind.java:199
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BAND
Z3_OP_BAND
Definition:
Z3_decl_kind.java:82
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UMINUS
Z3_OP_UMINUS
Definition:
Z3_decl_kind.java:35
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LT
Z3_OP_LT
Definition:
Z3_decl_kind.java:31
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PB_LE
Z3_OP_PB_LE
Definition:
Z3_decl_kind.java:196
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_REAL
Z3_OP_FPA_TO_REAL
Definition:
Z3_decl_kind.java:239
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_GOAL
Z3_OP_PR_GOAL
Definition:
Z3_decl_kind.java:119
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_PLUS_INF
Z3_OP_FPA_PLUS_INF
Definition:
Z3_decl_kind.java:205
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_IS_EMPTY
Z3_OP_RA_IS_EMPTY
Definition:
Z3_decl_kind.java:158
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_AT
Z3_OP_SEQ_AT
Definition:
Z3_decl_kind.java:179
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MONOTONICITY
Z3_OP_PR_MONOTONICITY
Definition:
Z3_decl_kind.java:125
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_FP
Z3_OP_FPA_FP
Definition:
Z3_decl_kind.java:234
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MIN_I
Z3_OP_FPA_MIN_I
Definition:
Z3_decl_kind.java:241
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_STAR
Z3_OP_PR_NNF_STAR
Definition:
Z3_decl_kind.java:150
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_OR
Z3_OP_OR
Definition:
Z3_decl_kind.java:20
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_TRUE
Z3_OP_PR_IFF_TRUE
Definition:
Z3_decl_kind.java:141
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_CNF_STAR
Z3_OP_PR_CNF_STAR
Definition:
Z3_decl_kind.java:151
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSREM_I
Z3_OP_BSREM_I
Definition:
Z3_decl_kind.java:113
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_CONSTRUCTOR
Z3_OP_DT_CONSTRUCTOR
Definition:
Z3_decl_kind.java:191
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL
Z3_OP_FPA_ROUND_TO_INTEGRAL
Definition:
Z3_decl_kind.java:221
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BLSHR
Z3_OP_BLSHR
Definition:
Z3_decl_kind.java:98
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNUM
Z3_OP_BNUM
Definition:
Z3_decl_kind.java:57
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_CONTAINS
Z3_OP_SEQ_CONTAINS
Definition:
Z3_decl_kind.java:176
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV0
Z3_OP_BSDIV0
Definition:
Z3_decl_kind.java:69
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_COMPLEMENT
Z3_OP_SET_COMPLEMENT
Definition:
Z3_decl_kind.java:53
com.microsoft.z3.enumerations.Z3_decl_kind
Definition:
Z3_decl_kind.java:13
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSUB
Z3_OP_BSUB
Definition:
Z3_decl_kind.java:62
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_UNION
Z3_OP_RE_UNION
Definition:
Z3_decl_kind.java:188
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_SKOLEMIZE
Z3_OP_PR_SKOLEMIZE
Definition:
Z3_decl_kind.java:152
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_WIDEN
Z3_OP_RA_WIDEN
Definition:
Z3_decl_kind.java:161
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SELECT
Z3_OP_SELECT
Definition:
Z3_decl_kind.java:46
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT
Z3_OP_EXT_ROTATE_RIGHT
Definition:
Z3_decl_kind.java:103
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED
Z3_OP_FPA_TO_FP_UNSIGNED
Definition:
Z3_decl_kind.java:236
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_UBV
Z3_OP_FPA_TO_UBV
Definition:
Z3_decl_kind.java:237
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_HYPER_RESOLVE
Z3_OP_PR_HYPER_RESOLVE
Definition:
Z3_decl_kind.java:155
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SUB
Z3_OP_SUB
Definition:
Z3_decl_kind.java:34
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_STAR
Z3_OP_RE_STAR
Definition:
Z3_decl_kind.java:185
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FD_CONSTANT
Z3_OP_FD_CONSTANT
Definition:
Z3_decl_kind.java:169
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_REM
Z3_OP_FPA_REM
Definition:
Z3_decl_kind.java:215
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRANSITIVITY
Z3_OP_PR_TRANSITIVITY
Definition:
Z3_decl_kind.java:123
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV0
Z3_OP_BUDIV0
Definition:
Z3_decl_kind.java:70
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_NEG
Z3_OP_PR_NNF_NEG
Definition:
Z3_decl_kind.java:149
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_REPEAT
Z3_OP_REPEAT
Definition:
Z3_decl_kind.java:93
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL
Z3_OP_FPA_IS_SUBNORMAL
Definition:
Z3_decl_kind.java:231
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_ADD
Z3_OP_FPA_ADD
Definition:
Z3_decl_kind.java:210
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MAX
Z3_OP_FPA_MAX
Definition:
Z3_decl_kind.java:218
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_STORE
Z3_OP_STORE
Definition:
Z3_decl_kind.java:45
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UGT
Z3_OP_UGT
Definition:
Z3_decl_kind.java:80
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_CLONE
Z3_OP_RA_CLONE
Definition:
Z3_decl_kind.java:168
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FALSE
Z3_OP_FALSE
Definition:
Z3_decl_kind.java:15
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DIV
Z3_OP_DIV
Definition:
Z3_decl_kind.java:37
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_GT
Z3_OP_FPA_GT
Definition:
Z3_decl_kind.java:224
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV_I
Z3_OP_BSDIV_I
Definition:
Z3_decl_kind.java:111
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_REM
Z3_OP_REM
Definition:
Z3_decl_kind.java:39
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DEF_INTRO
Z3_OP_PR_DEF_INTRO
Definition:
Z3_decl_kind.java:145
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_NEG
Z3_OP_FPA_NEG
Definition:
Z3_decl_kind.java:212
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FD_LT
Z3_OP_FD_LT
Definition:
Z3_decl_kind.java:170
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_FILTER
Z3_OP_RA_FILTER
Definition:
Z3_decl_kind.java:163
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_UNDEF
Z3_OP_PR_UNDEF
Definition:
Z3_decl_kind.java:116
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT
Z3_OP_EXT_ROTATE_LEFT
Definition:
Z3_decl_kind.java:102
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV
Z3_OP_BUDIV
Definition:
Z3_decl_kind.java:65
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMUL_NO_OVFL
Z3_OP_BSMUL_NO_OVFL
Definition:
Z3_decl_kind.java:108
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ROTATE_RIGHT
Z3_OP_ROTATE_RIGHT
Definition:
Z3_decl_kind.java:101
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BOR
Z3_OP_BOR
Definition:
Z3_decl_kind.java:83
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_POS
Z3_OP_PR_NNF_POS
Definition:
Z3_decl_kind.java:148
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION
Z3_OP_PR_UNIT_RESOLUTION
Definition:
Z3_decl_kind.java:140
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_SUFFIX
Z3_OP_SEQ_SUFFIX
Definition:
Z3_decl_kind.java:175
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DER
Z3_OP_PR_DER
Definition:
Z3_decl_kind.java:136
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_XOR
Z3_OP_XOR
Definition:
Z3_decl_kind.java:22
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ANUM
Z3_OP_ANUM
Definition:
Z3_decl_kind.java:27
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_CONCAT
Z3_OP_RE_CONCAT
Definition:
Z3_decl_kind.java:187
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SLEQ
Z3_OP_SLEQ
Definition:
Z3_decl_kind.java:75
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_ACCESSOR
Z3_OP_DT_ACCESSOR
Definition:
Z3_decl_kind.java:193
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNAND
Z3_OP_BNAND
Definition:
Z3_decl_kind.java:86
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ITE
Z3_OP_ITE
Definition:
Z3_decl_kind.java:18
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_NAN
Z3_OP_FPA_NAN
Definition:
Z3_decl_kind.java:207
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SGEQ
Z3_OP_SGEQ
Definition:
Z3_decl_kind.java:77
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_IN_RE
Z3_OP_SEQ_IN_RE
Definition:
Z3_decl_kind.java:183
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_SQRT
Z3_OP_FPA_SQRT
Definition:
Z3_decl_kind.java:220
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ASSERTED
Z3_OP_PR_ASSERTED
Definition:
Z3_decl_kind.java:118
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_MAP
Z3_OP_ARRAY_MAP
Definition:
Z3_decl_kind.java:48
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_XOR3
Z3_OP_XOR3
Definition:
Z3_decl_kind.java:107
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_LT
Z3_OP_FPA_LT
Definition:
Z3_decl_kind.java:223
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TO_INT
Z3_OP_TO_INT
Definition:
Z3_decl_kind.java:42
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_SUBSET
Z3_OP_SET_SUBSET
Definition:
Z3_decl_kind.java:54
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_STORE
Z3_OP_RA_STORE
Definition:
Z3_decl_kind.java:156
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ZERO_EXT
Z3_OP_ZERO_EXT
Definition:
Z3_decl_kind.java:91
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_EQ
Z3_OP_FPA_EQ
Definition:
Z3_decl_kind.java:222
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LE
Z3_OP_LE
Definition:
Z3_decl_kind.java:29
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRUE
Z3_OP_PR_TRUE
Definition:
Z3_decl_kind.java:117
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMUL_NO_UDFL
Z3_OP_BSMUL_NO_UDFL
Definition:
Z3_decl_kind.java:110
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_NOT
Z3_OP_NOT
Definition:
Z3_decl_kind.java:23
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_LE
Z3_OP_FPA_LE
Definition:
Z3_decl_kind.java:225
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONCAT
Z3_OP_CONCAT
Definition:
Z3_decl_kind.java:89
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BADD
Z3_OP_BADD
Definition:
Z3_decl_kind.java:61
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ULEQ
Z3_OP_ULEQ
Definition:
Z3_decl_kind.java:74
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BREDOR
Z3_OP_BREDOR
Definition:
Z3_decl_kind.java:94
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_COMPLEMENT
Z3_OP_RA_COMPLEMENT
Definition:
Z3_decl_kind.java:166
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_JOIN
Z3_OP_RA_JOIN
Definition:
Z3_decl_kind.java:159
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY
Z3_OP_PR_COMMUTATIVITY
Definition:
Z3_decl_kind.java:143
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE
Z3_OP_FPA_IS_NEGATIVE
Definition:
Z3_decl_kind.java:232
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV_I
Z3_OP_BUDIV_I
Definition:
Z3_decl_kind.java:112
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DEF_AXIOM
Z3_OP_PR_DEF_AXIOM
Definition:
Z3_decl_kind.java:144
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_UNION
Z3_OP_SET_UNION
Definition:
Z3_decl_kind.java:50
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MODUS_PONENS
Z3_OP_PR_MODUS_PONENS
Definition:
Z3_decl_kind.java:120
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT0
Z3_OP_BIT0
Definition:
Z3_decl_kind.java:59
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNOT
Z3_OP_BNOT
Definition:
Z3_decl_kind.java:84
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BV2INT
Z3_OP_BV2INT
Definition:
Z3_decl_kind.java:105
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IFF
Z3_OP_IFF
Definition:
Z3_decl_kind.java:21
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BCOMP
Z3_OP_BCOMP
Definition:
Z3_decl_kind.java:96
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_MOD
Z3_OP_MOD
Definition:
Z3_decl_kind.java:40
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_PLUS
Z3_OP_RE_PLUS
Definition:
Z3_decl_kind.java:184
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_RECOGNISER
Z3_OP_DT_RECOGNISER
Definition:
Z3_decl_kind.java:192
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSHL
Z3_OP_BSHL
Definition:
Z3_decl_kind.java:97
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD
Z3_OP_BSMOD
Definition:
Z3_decl_kind.java:68
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS
Z3_OP_PR_ELIM_UNUSED_VARS
Definition:
Z3_decl_kind.java:135
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSREM
Z3_OP_BSREM
Definition:
Z3_decl_kind.java:66
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_LENGTH
Z3_OP_SEQ_LENGTH
Definition:
Z3_decl_kind.java:180
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSREM0
Z3_OP_BSREM0
Definition:
Z3_decl_kind.java:71
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MUL
Z3_OP_FPA_MUL
Definition:
Z3_decl_kind.java:213
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Definition:
Z3_decl_kind.java:200
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_SBV
Z3_OP_FPA_TO_SBV
Definition:
Z3_decl_kind.java:238
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_REPLACE
Z3_OP_SEQ_REPLACE
Definition:
Z3_decl_kind.java:178
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_FALSE
Z3_OP_PR_IFF_FALSE
Definition:
Z3_decl_kind.java:142
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO
Z3_OP_FPA_PLUS_ZERO
Definition:
Z3_decl_kind.java:208
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ROTATE_LEFT
Z3_OP_ROTATE_LEFT
Definition:
Z3_decl_kind.java:100
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV
Z3_OP_FPA_TO_IEEE_BV
Definition:
Z3_decl_kind.java:240
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM_I
Z3_OP_BUREM_I
Definition:
Z3_decl_kind.java:114
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_APPLY_DEF
Z3_OP_PR_APPLY_DEF
Definition:
Z3_decl_kind.java:146
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT1
Z3_OP_BIT1
Definition:
Z3_decl_kind.java:58
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REWRITE_STAR
Z3_OP_PR_REWRITE_STAR
Definition:
Z3_decl_kind.java:131
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AS_ARRAY
Z3_OP_AS_ARRAY
Definition:
Z3_decl_kind.java:55
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_OEQ
Z3_OP_OEQ
Definition:
Z3_decl_kind.java:25
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EQ
Z3_OP_EQ
Definition:
Z3_decl_kind.java:16
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IMPLIES
Z3_OP_IMPLIES
Definition:
Z3_decl_kind.java:24
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PULL_QUANT
Z3_OP_PR_PULL_QUANT
Definition:
Z3_decl_kind.java:132
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DISTINCT
Z3_OP_DISTINCT
Definition:
Z3_decl_kind.java:17
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UGEQ
Z3_OP_UGEQ
Definition:
Z3_decl_kind.java:76
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PB_AT_MOST
Z3_OP_PB_AT_MOST
Definition:
Z3_decl_kind.java:195
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IS_INT
Z3_OP_IS_INT
Definition:
Z3_decl_kind.java:43
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_OPTION
Z3_OP_RE_OPTION
Definition:
Z3_decl_kind.java:186
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LABEL_LIT
Z3_OP_LABEL_LIT
Definition:
Z3_decl_kind.java:190
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_RENAME
Z3_OP_RA_RENAME
Definition:
Z3_decl_kind.java:165
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ
Z3_OP_PR_MODUS_PONENS_OEQ
Definition:
Z3_decl_kind.java:153
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_QUANT_INTRO
Z3_OP_PR_QUANT_INTRO
Definition:
Z3_decl_kind.java:126
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SLT
Z3_OP_SLT
Definition:
Z3_decl_kind.java:79
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MAX_I
Z3_OP_FPA_MAX_I
Definition:
Z3_decl_kind.java:242
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNEG
Z3_OP_BNEG
Definition:
Z3_decl_kind.java:60
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER
Z3_OP_RA_NEGATION_FILTER
Definition:
Z3_decl_kind.java:164
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UNINTERPRETED
Z3_OP_UNINTERPRETED
Definition:
Z3_decl_kind.java:244
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE
Z3_OP_FPA_RM_TOWARD_NEGATIVE
Definition:
Z3_decl_kind.java:202
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BASHR
Z3_OP_BASHR
Definition:
Z3_decl_kind.java:99
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ADD
Z3_OP_ADD
Definition:
Z3_decl_kind.java:33
com.microsoft.z3.enumerations.Z3_decl_kind.toInt
final int toInt()
Definition:
Z3_decl_kind.java:268
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO
Z3_OP_FPA_RM_TOWARD_ZERO
Definition:
Z3_decl_kind.java:203
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM
Z3_OP_BUREM
Definition:
Z3_decl_kind.java:67
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_POWER
Z3_OP_POWER
Definition:
Z3_decl_kind.java:44
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_PROJECT
Z3_OP_RA_PROJECT
Definition:
Z3_decl_kind.java:162
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_EXT
Z3_OP_ARRAY_EXT
Definition:
Z3_decl_kind.java:56
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY
Z3_OP_PR_DISTRIBUTIVITY
Definition:
Z3_decl_kind.java:127
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE
Z3_OP_FPA_IS_POSITIVE
Definition:
Z3_decl_kind.java:233
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_UNIT
Z3_OP_SEQ_UNIT
Definition:
Z3_decl_kind.java:171
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD_I
Z3_OP_BSMOD_I
Definition:
Z3_decl_kind.java:115
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR
Z3_OP_PR_PULL_QUANT_STAR
Definition:
Z3_decl_kind.java:133
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BXOR
Z3_OP_BXOR
Definition:
Z3_decl_kind.java:85
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_NORMAL
Z3_OP_FPA_IS_NORMAL
Definition:
Z3_decl_kind.java:230
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_DIFFERENCE
Z3_OP_SET_DIFFERENCE
Definition:
Z3_decl_kind.java:52
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IDIV
Z3_OP_IDIV
Definition:
Z3_decl_kind.java:38
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_UNION
Z3_OP_RA_UNION
Definition:
Z3_decl_kind.java:160
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_HYPOTHESIS
Z3_OP_PR_HYPOTHESIS
Definition:
Z3_decl_kind.java:138
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_AND_ELIM
Z3_OP_PR_AND_ELIM
Definition:
Z3_decl_kind.java:128
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TRUE
Z3_OP_TRUE
Definition:
Z3_decl_kind.java:14
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_QUANT_INST
Z3_OP_PR_QUANT_INST
Definition:
Z3_decl_kind.java:137
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SIGN_EXT
Z3_OP_SIGN_EXT
Definition:
Z3_decl_kind.java:90
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_OEQ
Z3_OP_PR_IFF_OEQ
Definition:
Z3_decl_kind.java:147
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_SYMMETRY
Z3_OP_PR_SYMMETRY
Definition:
Z3_decl_kind.java:122
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PUSH_QUANT
Z3_OP_PR_PUSH_QUANT
Definition:
Z3_decl_kind.java:134
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONST_ARRAY
Z3_OP_CONST_ARRAY
Definition:
Z3_decl_kind.java:47
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MINUS_INF
Z3_OP_FPA_MINUS_INF
Definition:
Z3_decl_kind.java:206
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TO_REAL
Z3_OP_TO_REAL
Definition:
Z3_decl_kind.java:41
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BMUL
Z3_OP_BMUL
Definition:
Z3_decl_kind.java:63
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_INDEX
Z3_OP_SEQ_INDEX
Definition:
Z3_decl_kind.java:181
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_INTERSECT
Z3_OP_SET_INTERSECT
Definition:
Z3_decl_kind.java:51
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_EMPTY
Z3_OP_RA_EMPTY
Definition:
Z3_decl_kind.java:157
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_NAN
Z3_OP_FPA_IS_NAN
Definition:
Z3_decl_kind.java:227
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR
Z3_OP_PR_TRANSITIVITY_STAR
Definition:
Z3_decl_kind.java:124
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_ZERO
Z3_OP_FPA_IS_ZERO
Definition:
Z3_decl_kind.java:229
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_ABS
Z3_OP_FPA_ABS
Definition:
Z3_decl_kind.java:216
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_PREFIX
Z3_OP_SEQ_PREFIX
Definition:
Z3_decl_kind.java:174
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_DEFAULT
Z3_OP_ARRAY_DEFAULT
Definition:
Z3_decl_kind.java:49
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MIN
Z3_OP_FPA_MIN
Definition:
Z3_decl_kind.java:217
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_FMA
Z3_OP_FPA_FMA
Definition:
Z3_decl_kind.java:219
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_GE
Z3_OP_GE
Definition:
Z3_decl_kind.java:30
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_INTERNAL
Z3_OP_INTERNAL
Definition:
Z3_decl_kind.java:243
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SGT
Z3_OP_SGT
Definition:
Z3_decl_kind.java:81
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PB_GE
Z3_OP_PB_GE
Definition:
Z3_decl_kind.java:197
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_INF
Z3_OP_FPA_IS_INF
Definition:
Z3_decl_kind.java:228
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CARRY
Z3_OP_CARRY
Definition:
Z3_decl_kind.java:106
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_SUB
Z3_OP_FPA_SUB
Definition:
Z3_decl_kind.java:211
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM0
Z3_OP_BUREM0
Definition:
Z3_decl_kind.java:72
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_SELECT
Z3_OP_RA_SELECT
Definition:
Z3_decl_kind.java:167
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO
Z3_OP_FPA_MINUS_ZERO
Definition:
Z3_decl_kind.java:209
Generated on Sat Nov 12 2016 22:01:04 for Z3 by
1.8.12