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
(2051),
14
Z3_OP_SUB
(519),
15
Z3_OP_ZERO_EXT
(1058),
16
Z3_OP_ADD
(518),
17
Z3_OP_IS_INT
(528),
18
Z3_OP_BREDOR
(1061),
19
Z3_OP_BNOT
(1051),
20
Z3_OP_BNOR
(1054),
21
Z3_OP_PR_CNF_STAR
(1315),
22
Z3_OP_RA_JOIN
(1539),
23
Z3_OP_LE
(514),
24
Z3_OP_SET_UNION
(773),
25
Z3_OP_PR_UNDEF
(1280),
26
Z3_OP_BREDAND
(1062),
27
Z3_OP_LT
(516),
28
Z3_OP_RA_UNION
(1540),
29
Z3_OP_BADD
(1028),
30
Z3_OP_BUREM0
(1039),
31
Z3_OP_OEQ
(267),
32
Z3_OP_PR_MODUS_PONENS
(1284),
33
Z3_OP_RA_CLONE
(1548),
34
Z3_OP_REPEAT
(1060),
35
Z3_OP_RA_NEGATION_FILTER
(1544),
36
Z3_OP_BSMOD0
(1040),
37
Z3_OP_BLSHR
(1065),
38
Z3_OP_BASHR
(1066),
39
Z3_OP_PR_UNIT_RESOLUTION
(1304),
40
Z3_OP_ROTATE_RIGHT
(1068),
41
Z3_OP_ARRAY_DEFAULT
(772),
42
Z3_OP_PR_PULL_QUANT
(1296),
43
Z3_OP_PR_APPLY_DEF
(1310),
44
Z3_OP_PR_REWRITE_STAR
(1295),
45
Z3_OP_IDIV
(523),
46
Z3_OP_PR_GOAL
(1283),
47
Z3_OP_PR_IFF_TRUE
(1305),
48
Z3_OP_LABEL_LIT
(1793),
49
Z3_OP_BOR
(1050),
50
Z3_OP_PR_SYMMETRY
(1286),
51
Z3_OP_TRUE
(256),
52
Z3_OP_SET_COMPLEMENT
(776),
53
Z3_OP_CONCAT
(1056),
54
Z3_OP_PR_NOT_OR_ELIM
(1293),
55
Z3_OP_IFF
(263),
56
Z3_OP_BSHL
(1064),
57
Z3_OP_PR_TRANSITIVITY
(1287),
58
Z3_OP_SGT
(1048),
59
Z3_OP_RA_WIDEN
(1541),
60
Z3_OP_PR_DEF_INTRO
(1309),
61
Z3_OP_NOT
(265),
62
Z3_OP_PR_QUANT_INTRO
(1290),
63
Z3_OP_UGT
(1047),
64
Z3_OP_DT_RECOGNISER
(2049),
65
Z3_OP_SET_INTERSECT
(774),
66
Z3_OP_BSREM
(1033),
67
Z3_OP_RA_STORE
(1536),
68
Z3_OP_SLT
(1046),
69
Z3_OP_ROTATE_LEFT
(1067),
70
Z3_OP_PR_NNF_NEG
(1313),
71
Z3_OP_PR_REFLEXIVITY
(1285),
72
Z3_OP_ULEQ
(1041),
73
Z3_OP_BIT1
(1025),
74
Z3_OP_BIT0
(1026),
75
Z3_OP_EQ
(258),
76
Z3_OP_BMUL
(1030),
77
Z3_OP_ARRAY_MAP
(771),
78
Z3_OP_STORE
(768),
79
Z3_OP_PR_HYPOTHESIS
(1302),
80
Z3_OP_RA_RENAME
(1545),
81
Z3_OP_AND
(261),
82
Z3_OP_TO_REAL
(526),
83
Z3_OP_PR_NNF_POS
(1312),
84
Z3_OP_PR_AND_ELIM
(1292),
85
Z3_OP_MOD
(525),
86
Z3_OP_BUDIV0
(1037),
87
Z3_OP_PR_TRUE
(1281),
88
Z3_OP_BNAND
(1053),
89
Z3_OP_PR_ELIM_UNUSED_VARS
(1299),
90
Z3_OP_RA_FILTER
(1543),
91
Z3_OP_FD_LT
(1549),
92
Z3_OP_RA_EMPTY
(1537),
93
Z3_OP_DIV
(522),
94
Z3_OP_ANUM
(512),
95
Z3_OP_MUL
(521),
96
Z3_OP_UGEQ
(1043),
97
Z3_OP_BSREM0
(1038),
98
Z3_OP_PR_TH_LEMMA
(1318),
99
Z3_OP_BXOR
(1052),
100
Z3_OP_DISTINCT
(259),
101
Z3_OP_PR_IFF_FALSE
(1306),
102
Z3_OP_BV2INT
(1072),
103
Z3_OP_EXT_ROTATE_LEFT
(1069),
104
Z3_OP_PR_PULL_QUANT_STAR
(1297),
105
Z3_OP_BSUB
(1029),
106
Z3_OP_PR_ASSERTED
(1282),
107
Z3_OP_BXNOR
(1055),
108
Z3_OP_EXTRACT
(1059),
109
Z3_OP_PR_DER
(1300),
110
Z3_OP_DT_CONSTRUCTOR
(2048),
111
Z3_OP_GT
(517),
112
Z3_OP_BUREM
(1034),
113
Z3_OP_IMPLIES
(266),
114
Z3_OP_SLEQ
(1042),
115
Z3_OP_GE
(515),
116
Z3_OP_BAND
(1049),
117
Z3_OP_ITE
(260),
118
Z3_OP_AS_ARRAY
(778),
119
Z3_OP_RA_SELECT
(1547),
120
Z3_OP_CONST_ARRAY
(770),
121
Z3_OP_BSDIV
(1031),
122
Z3_OP_OR
(262),
123
Z3_OP_PR_HYPER_RESOLVE
(1319),
124
Z3_OP_AGNUM
(513),
125
Z3_OP_PR_PUSH_QUANT
(1298),
126
Z3_OP_BSMOD
(1035),
127
Z3_OP_PR_IFF_OEQ
(1311),
128
Z3_OP_INTERP
(268),
129
Z3_OP_PR_LEMMA
(1303),
130
Z3_OP_SET_SUBSET
(777),
131
Z3_OP_SELECT
(769),
132
Z3_OP_RA_PROJECT
(1542),
133
Z3_OP_BNEG
(1027),
134
Z3_OP_UMINUS
(520),
135
Z3_OP_REM
(524),
136
Z3_OP_TO_INT
(527),
137
Z3_OP_PR_QUANT_INST
(1301),
138
Z3_OP_SGEQ
(1044),
139
Z3_OP_POWER
(529),
140
Z3_OP_XOR3
(1074),
141
Z3_OP_RA_IS_EMPTY
(1538),
142
Z3_OP_CARRY
(1073),
143
Z3_OP_DT_ACCESSOR
(2050),
144
Z3_OP_PR_TRANSITIVITY_STAR
(1288),
145
Z3_OP_PR_NNF_STAR
(1314),
146
Z3_OP_PR_COMMUTATIVITY
(1307),
147
Z3_OP_ULT
(1045),
148
Z3_OP_BSDIV0
(1036),
149
Z3_OP_SET_DIFFERENCE
(775),
150
Z3_OP_INT2BV
(1071),
151
Z3_OP_XOR
(264),
152
Z3_OP_PR_MODUS_PONENS_OEQ
(1317),
153
Z3_OP_BNUM
(1024),
154
Z3_OP_BUDIV
(1032),
155
Z3_OP_PR_MONOTONICITY
(1289),
156
Z3_OP_PR_DEF_AXIOM
(1308),
157
Z3_OP_FALSE
(257),
158
Z3_OP_EXT_ROTATE_RIGHT
(1070),
159
Z3_OP_PR_DISTRIBUTIVITY
(1291),
160
Z3_OP_SIGN_EXT
(1057),
161
Z3_OP_PR_SKOLEMIZE
(1316),
162
Z3_OP_BCOMP
(1063),
163
Z3_OP_RA_COMPLEMENT
(1546);
164
165
private
final
int
intValue;
166
167
Z3_decl_kind
(
int
v) {
168
this.intValue = v;
169
}
170
171
public
static
final
Z3_decl_kind
fromInt
(
int
v) {
172
for
(
Z3_decl_kind
k: values())
173
if
(k.intValue == v)
return
k;
174
return
values()[0];
175
}
176
177
public
final
int
toInt
() {
return
this.intValue; }
178
}
179
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AGNUM
Z3_OP_AGNUM
Definition:
Z3_decl_kind.java:124
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TH_LEMMA
Z3_OP_PR_TH_LEMMA
Definition:
Z3_decl_kind.java:98
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:108
com.microsoft.z3.enumerations.Z3_decl_kind.fromInt
static final Z3_decl_kind fromInt(int v)
Definition:
Z3_decl_kind.java:171
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_MUL
Z3_OP_MUL
Definition:
Z3_decl_kind.java:95
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REFLEXIVITY
Z3_OP_PR_REFLEXIVITY
Definition:
Z3_decl_kind.java:71
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNOR
Z3_OP_BNOR
Definition:
Z3_decl_kind.java:20
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_LEMMA
Z3_OP_PR_LEMMA
Definition:
Z3_decl_kind.java:129
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BREDAND
Z3_OP_BREDAND
Definition:
Z3_decl_kind.java:26
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_GT
Z3_OP_GT
Definition:
Z3_decl_kind.java:111
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BXNOR
Z3_OP_BXNOR
Definition:
Z3_decl_kind.java:107
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_INT2BV
Z3_OP_INT2BV
Definition:
Z3_decl_kind.java:150
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM
Z3_OP_PR_NOT_OR_ELIM
Definition:
Z3_decl_kind.java:54
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AND
Z3_OP_AND
Definition:
Z3_decl_kind.java:81
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ULT
Z3_OP_ULT
Definition:
Z3_decl_kind.java:147
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_INTERP
Z3_OP_INTERP
Definition:
Z3_decl_kind.java:128
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD0
Z3_OP_BSMOD0
Definition:
Z3_decl_kind.java:36
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_decl_kind
Z3_decl_kind(int v)
Definition:
Z3_decl_kind.java:167
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV
Z3_OP_BSDIV
Definition:
Z3_decl_kind.java:121
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BAND
Z3_OP_BAND
Definition:
Z3_decl_kind.java:116
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UMINUS
Z3_OP_UMINUS
Definition:
Z3_decl_kind.java:134
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LT
Z3_OP_LT
Definition:
Z3_decl_kind.java:27
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_GOAL
Z3_OP_PR_GOAL
Definition:
Z3_decl_kind.java:46
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_IS_EMPTY
Z3_OP_RA_IS_EMPTY
Definition:
Z3_decl_kind.java:141
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MONOTONICITY
Z3_OP_PR_MONOTONICITY
Definition:
Z3_decl_kind.java:155
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_STAR
Z3_OP_PR_NNF_STAR
Definition:
Z3_decl_kind.java:145
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_OR
Z3_OP_OR
Definition:
Z3_decl_kind.java:122
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_TRUE
Z3_OP_PR_IFF_TRUE
Definition:
Z3_decl_kind.java:47
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_CNF_STAR
Z3_OP_PR_CNF_STAR
Definition:
Z3_decl_kind.java:21
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_CONSTRUCTOR
Z3_OP_DT_CONSTRUCTOR
Definition:
Z3_decl_kind.java:110
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BLSHR
Z3_OP_BLSHR
Definition:
Z3_decl_kind.java:37
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNUM
Z3_OP_BNUM
Definition:
Z3_decl_kind.java:153
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV0
Z3_OP_BSDIV0
Definition:
Z3_decl_kind.java:148
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_COMPLEMENT
Z3_OP_SET_COMPLEMENT
Definition:
Z3_decl_kind.java:52
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:105
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_SKOLEMIZE
Z3_OP_PR_SKOLEMIZE
Definition:
Z3_decl_kind.java:161
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_WIDEN
Z3_OP_RA_WIDEN
Definition:
Z3_decl_kind.java:59
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SELECT
Z3_OP_SELECT
Definition:
Z3_decl_kind.java:131
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT
Z3_OP_EXT_ROTATE_RIGHT
Definition:
Z3_decl_kind.java:158
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_HYPER_RESOLVE
Z3_OP_PR_HYPER_RESOLVE
Definition:
Z3_decl_kind.java:123
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_PR_TRANSITIVITY
Z3_OP_PR_TRANSITIVITY
Definition:
Z3_decl_kind.java:57
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV0
Z3_OP_BUDIV0
Definition:
Z3_decl_kind.java:86
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_NEG
Z3_OP_PR_NNF_NEG
Definition:
Z3_decl_kind.java:70
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_REPEAT
Z3_OP_REPEAT
Definition:
Z3_decl_kind.java:34
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_STORE
Z3_OP_STORE
Definition:
Z3_decl_kind.java:78
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UGT
Z3_OP_UGT
Definition:
Z3_decl_kind.java:63
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_CLONE
Z3_OP_RA_CLONE
Definition:
Z3_decl_kind.java:33
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FALSE
Z3_OP_FALSE
Definition:
Z3_decl_kind.java:157
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DIV
Z3_OP_DIV
Definition:
Z3_decl_kind.java:93
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_REM
Z3_OP_REM
Definition:
Z3_decl_kind.java:135
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DEF_INTRO
Z3_OP_PR_DEF_INTRO
Definition:
Z3_decl_kind.java:60
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FD_LT
Z3_OP_FD_LT
Definition:
Z3_decl_kind.java:91
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_FILTER
Z3_OP_RA_FILTER
Definition:
Z3_decl_kind.java:90
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_UNDEF
Z3_OP_PR_UNDEF
Definition:
Z3_decl_kind.java:25
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT
Z3_OP_EXT_ROTATE_LEFT
Definition:
Z3_decl_kind.java:103
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV
Z3_OP_BUDIV
Definition:
Z3_decl_kind.java:154
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ROTATE_RIGHT
Z3_OP_ROTATE_RIGHT
Definition:
Z3_decl_kind.java:40
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BOR
Z3_OP_BOR
Definition:
Z3_decl_kind.java:49
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_POS
Z3_OP_PR_NNF_POS
Definition:
Z3_decl_kind.java:83
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION
Z3_OP_PR_UNIT_RESOLUTION
Definition:
Z3_decl_kind.java:39
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DER
Z3_OP_PR_DER
Definition:
Z3_decl_kind.java:109
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_XOR
Z3_OP_XOR
Definition:
Z3_decl_kind.java:151
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ANUM
Z3_OP_ANUM
Definition:
Z3_decl_kind.java:94
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SLEQ
Z3_OP_SLEQ
Definition:
Z3_decl_kind.java:114
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_ACCESSOR
Z3_OP_DT_ACCESSOR
Definition:
Z3_decl_kind.java:143
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNAND
Z3_OP_BNAND
Definition:
Z3_decl_kind.java:88
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ITE
Z3_OP_ITE
Definition:
Z3_decl_kind.java:117
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SGEQ
Z3_OP_SGEQ
Definition:
Z3_decl_kind.java:138
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ASSERTED
Z3_OP_PR_ASSERTED
Definition:
Z3_decl_kind.java:106
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_MAP
Z3_OP_ARRAY_MAP
Definition:
Z3_decl_kind.java:77
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_XOR3
Z3_OP_XOR3
Definition:
Z3_decl_kind.java:140
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TO_INT
Z3_OP_TO_INT
Definition:
Z3_decl_kind.java:136
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_SUBSET
Z3_OP_SET_SUBSET
Definition:
Z3_decl_kind.java:130
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_STORE
Z3_OP_RA_STORE
Definition:
Z3_decl_kind.java:67
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_LE
Z3_OP_LE
Definition:
Z3_decl_kind.java:23
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRUE
Z3_OP_PR_TRUE
Definition:
Z3_decl_kind.java:87
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_NOT
Z3_OP_NOT
Definition:
Z3_decl_kind.java:61
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONCAT
Z3_OP_CONCAT
Definition:
Z3_decl_kind.java:53
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BADD
Z3_OP_BADD
Definition:
Z3_decl_kind.java:29
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ULEQ
Z3_OP_ULEQ
Definition:
Z3_decl_kind.java:72
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BREDOR
Z3_OP_BREDOR
Definition:
Z3_decl_kind.java:18
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_COMPLEMENT
Z3_OP_RA_COMPLEMENT
Definition:
Z3_decl_kind.java:163
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_JOIN
Z3_OP_RA_JOIN
Definition:
Z3_decl_kind.java:22
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY
Z3_OP_PR_COMMUTATIVITY
Definition:
Z3_decl_kind.java:146
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DEF_AXIOM
Z3_OP_PR_DEF_AXIOM
Definition:
Z3_decl_kind.java:156
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_UNION
Z3_OP_SET_UNION
Definition:
Z3_decl_kind.java:24
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MODUS_PONENS
Z3_OP_PR_MODUS_PONENS
Definition:
Z3_decl_kind.java:32
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT0
Z3_OP_BIT0
Definition:
Z3_decl_kind.java:74
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNOT
Z3_OP_BNOT
Definition:
Z3_decl_kind.java:19
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BV2INT
Z3_OP_BV2INT
Definition:
Z3_decl_kind.java:102
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IFF
Z3_OP_IFF
Definition:
Z3_decl_kind.java:55
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BCOMP
Z3_OP_BCOMP
Definition:
Z3_decl_kind.java:162
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_MOD
Z3_OP_MOD
Definition:
Z3_decl_kind.java:85
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_RECOGNISER
Z3_OP_DT_RECOGNISER
Definition:
Z3_decl_kind.java:64
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSHL
Z3_OP_BSHL
Definition:
Z3_decl_kind.java:56
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD
Z3_OP_BSMOD
Definition:
Z3_decl_kind.java:126
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS
Z3_OP_PR_ELIM_UNUSED_VARS
Definition:
Z3_decl_kind.java:89
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_BSREM0
Z3_OP_BSREM0
Definition:
Z3_decl_kind.java:97
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_FALSE
Z3_OP_PR_IFF_FALSE
Definition:
Z3_decl_kind.java:101
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ROTATE_LEFT
Z3_OP_ROTATE_LEFT
Definition:
Z3_decl_kind.java:69
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_APPLY_DEF
Z3_OP_PR_APPLY_DEF
Definition:
Z3_decl_kind.java:43
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT1
Z3_OP_BIT1
Definition:
Z3_decl_kind.java:73
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REWRITE_STAR
Z3_OP_PR_REWRITE_STAR
Definition:
Z3_decl_kind.java:44
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AS_ARRAY
Z3_OP_AS_ARRAY
Definition:
Z3_decl_kind.java:118
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_OEQ
Z3_OP_OEQ
Definition:
Z3_decl_kind.java:31
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EQ
Z3_OP_EQ
Definition:
Z3_decl_kind.java:75
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IMPLIES
Z3_OP_IMPLIES
Definition:
Z3_decl_kind.java:113
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PULL_QUANT
Z3_OP_PR_PULL_QUANT
Definition:
Z3_decl_kind.java:42
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DISTINCT
Z3_OP_DISTINCT
Definition:
Z3_decl_kind.java:100
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UGEQ
Z3_OP_UGEQ
Definition:
Z3_decl_kind.java:96
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IS_INT
Z3_OP_IS_INT
Definition:
Z3_decl_kind.java:17
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LABEL_LIT
Z3_OP_LABEL_LIT
Definition:
Z3_decl_kind.java:48
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_RENAME
Z3_OP_RA_RENAME
Definition:
Z3_decl_kind.java:80
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ
Z3_OP_PR_MODUS_PONENS_OEQ
Definition:
Z3_decl_kind.java:152
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_QUANT_INTRO
Z3_OP_PR_QUANT_INTRO
Definition:
Z3_decl_kind.java:62
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SLT
Z3_OP_SLT
Definition:
Z3_decl_kind.java:68
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNEG
Z3_OP_BNEG
Definition:
Z3_decl_kind.java:133
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER
Z3_OP_RA_NEGATION_FILTER
Definition:
Z3_decl_kind.java:35
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_BASHR
Z3_OP_BASHR
Definition:
Z3_decl_kind.java:38
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:177
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM
Z3_OP_BUREM
Definition:
Z3_decl_kind.java:112
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_POWER
Z3_OP_POWER
Definition:
Z3_decl_kind.java:139
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_PROJECT
Z3_OP_RA_PROJECT
Definition:
Z3_decl_kind.java:132
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY
Z3_OP_PR_DISTRIBUTIVITY
Definition:
Z3_decl_kind.java:159
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR
Z3_OP_PR_PULL_QUANT_STAR
Definition:
Z3_decl_kind.java:104
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BXOR
Z3_OP_BXOR
Definition:
Z3_decl_kind.java:99
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_DIFFERENCE
Z3_OP_SET_DIFFERENCE
Definition:
Z3_decl_kind.java:149
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IDIV
Z3_OP_IDIV
Definition:
Z3_decl_kind.java:45
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_UNION
Z3_OP_RA_UNION
Definition:
Z3_decl_kind.java:28
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_HYPOTHESIS
Z3_OP_PR_HYPOTHESIS
Definition:
Z3_decl_kind.java:79
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_AND_ELIM
Z3_OP_PR_AND_ELIM
Definition:
Z3_decl_kind.java:84
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TRUE
Z3_OP_TRUE
Definition:
Z3_decl_kind.java:51
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:160
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_OEQ
Z3_OP_PR_IFF_OEQ
Definition:
Z3_decl_kind.java:127
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_SYMMETRY
Z3_OP_PR_SYMMETRY
Definition:
Z3_decl_kind.java:50
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PUSH_QUANT
Z3_OP_PR_PUSH_QUANT
Definition:
Z3_decl_kind.java:125
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONST_ARRAY
Z3_OP_CONST_ARRAY
Definition:
Z3_decl_kind.java:120
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TO_REAL
Z3_OP_TO_REAL
Definition:
Z3_decl_kind.java:82
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BMUL
Z3_OP_BMUL
Definition:
Z3_decl_kind.java:76
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_INTERSECT
Z3_OP_SET_INTERSECT
Definition:
Z3_decl_kind.java:65
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_EMPTY
Z3_OP_RA_EMPTY
Definition:
Z3_decl_kind.java:92
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR
Z3_OP_PR_TRANSITIVITY_STAR
Definition:
Z3_decl_kind.java:144
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_DEFAULT
Z3_OP_ARRAY_DEFAULT
Definition:
Z3_decl_kind.java:41
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_GE
Z3_OP_GE
Definition:
Z3_decl_kind.java:115
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SGT
Z3_OP_SGT
Definition:
Z3_decl_kind.java:58
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CARRY
Z3_OP_CARRY
Definition:
Z3_decl_kind.java:142
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM0
Z3_OP_BUREM0
Definition:
Z3_decl_kind.java:30
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_SELECT
Z3_OP_RA_SELECT
Definition:
Z3_decl_kind.java:119
Generated on Sat Apr 25 2015 18:37:49 for Z3 by
1.8.9.1