1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_BV ::cvc5::theory::bv::TheoryBV "theory/bv/theory_bv.h"
typechecker "theory/bv/theory_bv_type_rules.h"
properties finite
properties check propagate presolve ppStaticLearn
rewriter ::cvc5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
constant BITVECTOR_TYPE \
::cvc5::BitVectorSize \
"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \
"util/bitvector.h" \
"bit-vector type"
cardinality BITVECTOR_TYPE \
"::cvc5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
"theory/bv/theory_bv_type_rules.h"
constant CONST_BITVECTOR \
::cvc5::BitVector \
::cvc5::BitVectorHashFunction \
"util/bitvector.h" \
"a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class"
enumerator BITVECTOR_TYPE \
"::cvc5::theory::bv::BitVectorEnumerator" \
"theory/bv/type_enumerator.h"
well-founded BITVECTOR_TYPE \
true \
"(*cvc5::theory::TypeEnumerator(%TYPE%))" \
"theory/type_enumerator.h"
### non-parameterized operator kinds ------------------------------------------
## concatentation kind
operator BITVECTOR_CONCAT 2: "concatenation of two or more bit-vectors"
## bit-wise kinds
operator BITVECTOR_AND 2: "bitwise and of two or more bit-vectors"
operator BITVECTOR_COMP 2 "equality comparison of two bit-vectors (returns one bit)"
operator BITVECTOR_OR 2: "bitwise or of two or more bit-vectors"
operator BITVECTOR_XOR 2: "bitwise xor of two or more bit-vectors"
operator BITVECTOR_NOT 1 "bitwise not of a bit-vector"
operator BITVECTOR_NAND 2 "bitwise nand of two bit-vectors"
operator BITVECTOR_NOR 2 "bitwise nor of two bit-vectors"
operator BITVECTOR_XNOR 2 "bitwise xnor of two bit-vectors"
## arithmetic kinds
operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors"
operator BITVECTOR_NEG 1 "unary negation of a bit-vector"
operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors"
operator BITVECTOR_SUB 2 "subtraction of two bit-vectors"
operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)"
operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)"
operator BITVECTOR_SDIV 2 "2's complement signed division"
operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)"
operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)"
# total division kinds
## shift kinds
operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)"
operator BITVECTOR_LSHR 2 "bit-vector logical shift right (the two bit-vector parameters must have same width)"
operator BITVECTOR_SHL 2 "bit-vector shift left (the two bit-vector parameters must have same width)"
## inequality kinds
operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal (the two bit-vector parameters must have same width)"
operator BITVECTOR_ULT 2 "bit-vector unsigned less than (the two bit-vector parameters must have same width)"
operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width)"
operator BITVECTOR_UGT 2 "bit-vector unsigned greater than (the two bit-vector parameters must have same width)"
operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vector parameters must have same width)"
operator BITVECTOR_SLT 2 "bit-vector signed less than (the two bit-vector parameters must have same width)"
operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)"
operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)"
# inequalities with return type bit-vector of size 1
operator BITVECTOR_ULTBV 2 "bit-vector unsigned less than but returns bv of size 1 instead of boolean"
operator BITVECTOR_SLTBV 2 "bit-vector signed less than but returns bv of size 1 instead of boolean"
## reduction kinds
operator BITVECTOR_REDAND 1 "bit-vector redand"
operator BITVECTOR_REDOR 1 "bit-vector redor"
## if-then-else kind
operator BITVECTOR_ITE 3 "same semantics as regular ITE, but condition is bv of size 1 instead of Boolean"
## conversion kinds
operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer; parameter is a bit-vector"
## internal kinds
operator BITVECTOR_ACKERMANNIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)"
operator BITVECTOR_ACKERMANNIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)"
operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)"
### parameterized operator kinds ----------------------------------------------
constant BITVECTOR_BITOF_OP \
::cvc5::BitVectorBitOf \
::cvc5::BitVectorBitOfHashFunction \
"util/bitvector.h" \
"operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class"
parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term"
constant BITVECTOR_EXTRACT_OP \
::cvc5::BitVectorExtract \
::cvc5::BitVectorExtractHashFunction \
"util/bitvector.h" \
"operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class"
parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term"
constant BITVECTOR_REPEAT_OP \
::cvc5::BitVectorRepeat \
"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \
"util/bitvector.h" \
"operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class"
parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term"
constant BITVECTOR_ROTATE_LEFT_OP \
::cvc5::BitVectorRotateLeft \
"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \
"util/bitvector.h" \
"operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class"
parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term"
constant BITVECTOR_ROTATE_RIGHT_OP \
::cvc5::BitVectorRotateRight \
"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \
"util/bitvector.h" \
"operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class"
parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term"
constant BITVECTOR_SIGN_EXTEND_OP \
::cvc5::BitVectorSignExtend \
"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \
"util/bitvector.h" \
"operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class"
parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term"
constant BITVECTOR_ZERO_EXTEND_OP \
::cvc5::BitVectorZeroExtend \
"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \
"util/bitvector.h" \
"operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class"
parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term"
constant INT_TO_BITVECTOR_OP \
::cvc5::IntToBitVector \
"::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \
"util/bitvector.h" \
"operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class"
parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term"
### type rules for non-parameterized operator kinds ---------------------------
typerule CONST_BITVECTOR ::cvc5::theory::bv::BitVectorConstantTypeRule
## concatentation kind
typerule BITVECTOR_CONCAT ::cvc5::theory::bv::BitVectorConcatTypeRule
## bit-wise kinds
typerule BITVECTOR_AND ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_COMP ::cvc5::theory::bv::BitVectorBVPredTypeRule
typerule BITVECTOR_NAND ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NOT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_OR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_XNOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_XOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
## arithmetic kinds
typerule BITVECTOR_MULT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NEG ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_PLUS ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SUB ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_UDIV ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_UREM ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SDIV ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SMOD ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SREM ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
## shift kinds
typerule BITVECTOR_ASHR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_LSHR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SHL ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
## inequality kinds
typerule BITVECTOR_ULE ::cvc5::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_ULT ::cvc5::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_UGE ::cvc5::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_UGT ::cvc5::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SLE ::cvc5::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SLT ::cvc5::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGE ::cvc5::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGT ::cvc5::theory::bv::BitVectorPredicateTypeRule
# inequalities with return type bit-vector of size 1
typerule BITVECTOR_ULTBV ::cvc5::theory::bv::BitVectorBVPredTypeRule
typerule BITVECTOR_SLTBV ::cvc5::theory::bv::BitVectorBVPredTypeRule
## if-then-else kind
typerule BITVECTOR_ITE ::cvc5::theory::bv::BitVectorITETypeRule
## reduction kinds
typerule BITVECTOR_REDAND ::cvc5::theory::bv::BitVectorUnaryPredicateTypeRule
typerule BITVECTOR_REDOR ::cvc5::theory::bv::BitVectorUnaryPredicateTypeRule
## conversion kinds
typerule BITVECTOR_TO_NAT ::cvc5::theory::bv::BitVectorConversionTypeRule
## internal kinds
typerule BITVECTOR_ACKERMANNIZE_UDIV ::cvc5::theory::bv::BitVectorAckermanizationUdivTypeRule
typerule BITVECTOR_ACKERMANNIZE_UREM ::cvc5::theory::bv::BitVectorAckermanizationUremTypeRule
typerule BITVECTOR_EAGER_ATOM ::cvc5::theory::bv::BitVectorEagerAtomTypeRule
### type rules for parameterized operator kinds -------------------------------
typerule BITVECTOR_BITOF_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_BITOF ::cvc5::theory::bv::BitVectorBitOfTypeRule
typerule BITVECTOR_EXTRACT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_EXTRACT ::cvc5::theory::bv::BitVectorExtractTypeRule
typerule BITVECTOR_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_REPEAT ::cvc5::theory::bv::BitVectorRepeatTypeRule
typerule BITVECTOR_ROTATE_LEFT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_ROTATE_LEFT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ROTATE_RIGHT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_ROTATE_RIGHT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SIGN_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_SIGN_EXTEND ::cvc5::theory::bv::BitVectorExtendTypeRule
typerule BITVECTOR_ZERO_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_ZERO_EXTEND ::cvc5::theory::bv::BitVectorExtendTypeRule
typerule INT_TO_BITVECTOR_OP ::cvc5::theory::bv::IntToBitVectorOpTypeRule
typerule INT_TO_BITVECTOR ::cvc5::theory::bv::BitVectorConversionTypeRule
endtheory
|
