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