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
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h"
typechecker "theory/bv/theory_bv_type_rules.h"
properties finite
properties check propagate presolve ppStaticLearn
rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
constant BITVECTOR_TYPE \
::CVC4::BitVectorSize \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSize >" \
"util/bitvector.h" \
"bit-vector type"
cardinality BITVECTOR_TYPE \
"::CVC4::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
"theory/bv/theory_bv_type_rules.h"
constant CONST_BITVECTOR \
::CVC4::BitVector \
::CVC4::BitVectorHashFunction \
"util/bitvector.h" \
"a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class"
enumerator BITVECTOR_TYPE \
"::CVC4::theory::bv::BitVectorEnumerator" \
"theory/bv/type_enumerator.h"
well-founded BITVECTOR_TYPE \
true \
"(*CVC4::theory::TypeEnumerator(%TYPE%))" \
"theory/type_enumerator.h"
operator BITVECTOR_CONCAT 2: "concatenation of two or more bit-vectors"
operator BITVECTOR_AND 2: "bitwise and of two or more bit-vectors"
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"
operator BITVECTOR_COMP 2 "equality comparison of two bit-vectors (returns one bit)"
operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors"
operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors"
operator BITVECTOR_SUB 2 "subtraction of two bit-vectors"
operator BITVECTOR_NEG 1 "unary negation of a bit-vector"
operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0)"
operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0)"
operator BITVECTOR_SDIV 2 "2's complement signed division"
operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)"
operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)"
# total division kinds
operator BITVECTOR_UDIV_TOTAL 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_TOTAL 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)"
operator BITVECTOR_SHL 2 "bit-vector shift left (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_ASHR 2 "bit-vector arithmetic shift right (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_ULE 2 "bit-vector unsigned less 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_UGE 2 "bit-vector unsigned greater 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_SLE 2 "bit-vector signed less 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)"
operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)"
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"
operator BITVECTOR_ITE 3 "same semantics as regular ITE, but condition is bv of size 1 instead of Boolean"
operator BITVECTOR_REDOR 1 "bit-vector redor"
operator BITVECTOR_REDAND 1 "bit-vector redand"
operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)"
operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)"
operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)"
constant BITVECTOR_BITOF_OP \
::CVC4::BitVectorBitOf \
::CVC4::BitVectorBitOfHashFunction \
"util/bitvector.h" \
"operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf class"
constant BITVECTOR_EXTRACT_OP \
::CVC4::BitVectorExtract \
::CVC4::BitVectorExtractHashFunction \
"util/bitvector.h" \
"operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class"
constant BITVECTOR_REPEAT_OP \
::CVC4::BitVectorRepeat \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \
"util/bitvector.h" \
"operator for the bit-vector repeat; payload is an instance of the CVC4::BitVectorRepeat class"
constant BITVECTOR_ZERO_EXTEND_OP \
::CVC4::BitVectorZeroExtend \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \
"util/bitvector.h" \
"operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend class"
constant BITVECTOR_SIGN_EXTEND_OP \
::CVC4::BitVectorSignExtend \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \
"util/bitvector.h" \
"operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend class"
constant BITVECTOR_ROTATE_LEFT_OP \
::CVC4::BitVectorRotateLeft \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \
"util/bitvector.h" \
"operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft class"
constant BITVECTOR_ROTATE_RIGHT_OP \
::CVC4::BitVectorRotateRight \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \
"util/bitvector.h" \
"operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight 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"
parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term"
parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term"
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"
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"
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"
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 INT_TO_BITVECTOR_OP \
::CVC4::IntToBitVector \
"::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \
"util/bitvector.h" \
"operator for the integer conversion to bit-vector; payload is an instance of the CVC4::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"
operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer; parameter is a bit-vector"
typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule
typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_OR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_XOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NOT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_UDIV_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_UREM_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SHL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_LSHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ASHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ULT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_ULE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_UGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_UGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SLT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorBVPredTypeRule
typerule BITVECTOR_ULTBV ::CVC4::theory::bv::BitVectorBVPredTypeRule
typerule BITVECTOR_SLTBV ::CVC4::theory::bv::BitVectorBVPredTypeRule
typerule BITVECTOR_ITE ::CVC4::theory::bv::BitVectorITETypeRule
typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule
typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule
typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule
typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule
typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule
typerule INT_TO_BITVECTOR_OP ::CVC4::theory::bv::IntToBitVectorOpTypeRule
typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule
endtheory
|
