1 /********************* */
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Dejan Jovanovic, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_public.h"
20 #ifndef __CVC4__BITVECTOR_H
21 #define __CVC4__BITVECTOR_H
25 #include "base/exception.h"
26 #include "util/integer.h"
30 class CVC4_PUBLIC BitVector
{
33 BitVector(unsigned size
, const Integer
& val
):
35 d_value(val
.modByPow2(size
))
38 BitVector(unsigned size
= 0)
39 : d_size(size
), d_value(0) {}
41 BitVector(unsigned size
, unsigned int z
)
42 : d_size(size
), d_value(z
) {
43 d_value
= d_value
.modByPow2(size
);
46 BitVector(unsigned size
, unsigned long int z
)
47 : d_size(size
), d_value(z
) {
48 d_value
= d_value
.modByPow2(size
);
51 BitVector(unsigned size
, const BitVector
& q
)
52 : d_size(size
), d_value(q
.d_value
) {}
54 BitVector(const std::string
& num
, unsigned base
= 2);
58 Integer
toInteger() const {
62 BitVector
& operator =(const BitVector
& x
) {
70 bool operator ==(const BitVector
& y
) const {
71 if (d_size
!= y
.d_size
) return false;
72 return d_value
== y
.d_value
;
75 bool operator !=(const BitVector
& y
) const {
76 if (d_size
!= y
.d_size
) return true;
77 return d_value
!= y
.d_value
;
80 BitVector
concat (const BitVector
& other
) const {
81 return BitVector(d_size
+ other
.d_size
, (d_value
.multiplyByPow2(other
.d_size
)) + other
.d_value
);
84 BitVector
extract(unsigned high
, unsigned low
) const {
85 return BitVector(high
- low
+ 1, d_value
.extractBitRange(high
- low
+ 1, low
));
89 Bitwise operations on BitVectors
93 BitVector
operator ^(const BitVector
& y
) const {
94 CheckArgument(d_size
== y
.d_size
, y
);
95 return BitVector(d_size
, d_value
.bitwiseXor(y
.d_value
));
99 BitVector
operator |(const BitVector
& y
) const {
100 CheckArgument(d_size
== y
.d_size
, y
);
101 return BitVector(d_size
, d_value
.bitwiseOr(y
.d_value
));
105 BitVector
operator &(const BitVector
& y
) const {
106 CheckArgument(d_size
== y
.d_size
, y
);
107 return BitVector(d_size
, d_value
.bitwiseAnd(y
.d_value
));
111 BitVector
operator ~() const {
112 return BitVector(d_size
, d_value
.bitwiseNot());
116 Arithmetic operations on BitVectors
120 bool operator <(const BitVector
& y
) const {
121 return d_value
< y
.d_value
;
124 bool operator >(const BitVector
& y
) const {
125 return d_value
> y
.d_value
;
128 bool operator <=(const BitVector
& y
) const {
129 return d_value
<= y
.d_value
;
132 bool operator >=(const BitVector
& y
) const {
133 return d_value
>= y
.d_value
;
137 BitVector
operator +(const BitVector
& y
) const {
138 CheckArgument(d_size
== y
.d_size
, y
);
139 Integer sum
= d_value
+ y
.d_value
;
140 return BitVector(d_size
, sum
);
143 BitVector
operator -(const BitVector
& y
) const {
144 CheckArgument(d_size
== y
.d_size
, y
);
145 // to maintain the invariant that we are only adding BitVectors of the
147 BitVector
one(d_size
, Integer(1));
148 return *this + ~y
+ one
;
151 BitVector
operator -() const {
152 BitVector
one(d_size
, Integer(1));
153 return ~(*this) + one
;
156 BitVector
operator *(const BitVector
& y
) const {
157 CheckArgument(d_size
== y
.d_size
, y
);
158 Integer prod
= d_value
* y
.d_value
;
159 return BitVector(d_size
, prod
);
162 BitVector
setBit(uint32_t i
) const {
163 CheckArgument(i
< d_size
, i
);
164 Integer res
= d_value
.setBit(i
);
165 return BitVector(d_size
, res
);
168 bool isBitSet(uint32_t i
) const {
169 CheckArgument(i
< d_size
, i
);
170 return d_value
.isBitSet(i
);
174 * Total division function that returns 0 when the denominator is 0.
176 BitVector
unsignedDivTotal (const BitVector
& y
) const {
178 CheckArgument(d_size
== y
.d_size
, y
);
179 if (y
.d_value
== 0) {
180 // under division by zero return -1
181 return BitVector(d_size
, Integer(1).oneExtend(1, d_size
- 1));
183 CheckArgument(d_value
>= 0, this);
184 CheckArgument(y
.d_value
> 0, y
);
185 return BitVector(d_size
, d_value
.floorDivideQuotient(y
.d_value
));
189 * Total division function that returns 0 when the denominator is 0.
191 BitVector
unsignedRemTotal(const BitVector
& y
) const {
192 CheckArgument(d_size
== y
.d_size
, y
);
193 if (y
.d_value
== 0) {
194 return BitVector(d_size
, d_value
);
196 CheckArgument(d_value
>= 0, this);
197 CheckArgument(y
.d_value
> 0, y
);
198 return BitVector(d_size
, d_value
.floorDivideRemainder(y
.d_value
));
202 bool signedLessThan(const BitVector
& y
) const {
203 CheckArgument(d_size
== y
.d_size
, y
);
204 CheckArgument(d_value
>= 0, this);
205 CheckArgument(y
.d_value
>= 0, y
);
206 Integer a
= (*this).toSignedInt();
207 Integer b
= y
.toSignedInt();
212 bool unsignedLessThan(const BitVector
& y
) const {
213 CheckArgument(d_size
== y
.d_size
, y
);
214 CheckArgument(d_value
>= 0, this);
215 CheckArgument(y
.d_value
>= 0, y
);
216 return d_value
< y
.d_value
;
219 bool signedLessThanEq(const BitVector
& y
) const {
220 CheckArgument(d_size
== y
.d_size
, y
);
221 CheckArgument(d_value
>= 0, this);
222 CheckArgument(y
.d_value
>= 0, y
);
223 Integer a
= (*this).toSignedInt();
224 Integer b
= y
.toSignedInt();
229 bool unsignedLessThanEq(const BitVector
& y
) const {
230 CheckArgument(d_size
== y
.d_size
, this);
231 CheckArgument(d_value
>= 0, this);
232 CheckArgument(y
.d_value
>= 0, y
);
233 return d_value
<= y
.d_value
;
240 BitVector
zeroExtend(unsigned amount
) const {
241 return BitVector(d_size
+ amount
, d_value
);
244 BitVector
signExtend(unsigned amount
) const {
245 Integer sign_bit
= d_value
.extractBitRange(1, d_size
-1);
246 if(sign_bit
== Integer(0)) {
247 return BitVector(d_size
+ amount
, d_value
);
249 Integer val
= d_value
.oneExtend(d_size
, amount
);
250 return BitVector(d_size
+ amount
, val
);
257 BitVector
leftShift(const BitVector
& y
) const {
258 if (y
.d_value
> Integer(d_size
)) {
259 return BitVector(d_size
, Integer(0));
261 if (y
.d_value
== 0) {
265 // making sure we don't lose information casting
266 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
267 uint32_t amount
= y
.d_value
.toUnsignedInt();
268 Integer res
= d_value
.multiplyByPow2(amount
);
269 return BitVector(d_size
, res
);
272 BitVector
logicalRightShift(const BitVector
& y
) const {
273 if(y
.d_value
> Integer(d_size
)) {
274 return BitVector(d_size
, Integer(0));
277 // making sure we don't lose information casting
278 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
279 uint32_t amount
= y
.d_value
.toUnsignedInt();
280 Integer res
= d_value
.divByPow2(amount
);
281 return BitVector(d_size
, res
);
284 BitVector
arithRightShift(const BitVector
& y
) const {
285 Integer sign_bit
= d_value
.extractBitRange(1, d_size
- 1);
286 if(y
.d_value
> Integer(d_size
)) {
287 if(sign_bit
== Integer(0)) {
288 return BitVector(d_size
, Integer(0));
290 return BitVector(d_size
, Integer(d_size
).multiplyByPow2(d_size
) -1 );
294 if (y
.d_value
== 0) {
298 // making sure we don't lose information casting
299 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
301 uint32_t amount
= y
.d_value
.toUnsignedInt();
302 Integer rest
= d_value
.divByPow2(amount
);
304 if(sign_bit
== Integer(0)) {
305 return BitVector(d_size
, rest
);
307 Integer res
= rest
.oneExtend(d_size
- amount
, amount
);
308 return BitVector(d_size
, res
);
313 Convenience functions
316 size_t hash() const {
317 return d_value
.hash() + d_size
;
320 std::string
toString(unsigned int base
= 2) const {
321 std::string str
= d_value
.toString(base
);
322 if( base
== 2 && d_size
> str
.size() ) {
324 for( unsigned int i
=0; i
< d_size
- str
.size(); ++i
) {
333 unsigned getSize() const {
337 const Integer
& getValue() const {
341 Integer
toSignedInt() const {
342 // returns Integer corresponding to two's complement interpretation of bv
343 unsigned size
= d_size
;
344 Integer sign_bit
= d_value
.extractBitRange(1,size
-1);
345 Integer val
= d_value
.extractBitRange(size
-1, 0);
346 Integer res
= Integer(-1) * sign_bit
.multiplyByPow2(size
- 1) + val
;
351 Returns k is the integer is equal to 2^{k-1} and zero
353 @return k if the integer is equal to 2^{k-1} and zero otherwise
356 return d_value
.isPow2();
362 * no overflows: 2^d_size < d_value
363 * no negative numbers: d_value >= 0
368 };/* class BitVector */
372 inline BitVector::BitVector(const std::string
& num
, unsigned base
) {
373 CheckArgument(base
== 2 || base
== 16, base
);
378 d_size
= num
.size() * 4;
381 d_value
= Integer(num
, base
);
382 }/* BitVector::BitVector() */
386 * Hash function for the BitVector constants.
388 struct CVC4_PUBLIC BitVectorHashFunction
{
389 inline size_t operator()(const BitVector
& bv
) const {
392 };/* struct BitVectorHashFunction */
395 * The structure representing the extraction operation for bit-vectors. The
396 * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
397 * by taking the bits at indices <code>high ... low</code>
399 struct CVC4_PUBLIC BitVectorExtract
{
400 /** The high bit of the range for this extract */
402 /** The low bit of the range for this extract */
405 BitVectorExtract(unsigned high
, unsigned low
)
406 : high(high
), low(low
) {}
408 bool operator == (const BitVectorExtract
& extract
) const {
409 return high
== extract
.high
&& low
== extract
.low
;
411 };/* struct BitVectorExtract */
414 * Hash function for the BitVectorExtract objects.
416 struct CVC4_PUBLIC BitVectorExtractHashFunction
{
417 size_t operator()(const BitVectorExtract
& extract
) const {
418 size_t hash
= extract
.low
;
419 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
422 };/* struct BitVectorExtractHashFunction */
426 * The structure representing the extraction of one Boolean bit.
428 struct CVC4_PUBLIC BitVectorBitOf
{
429 /** The index of the bit */
431 BitVectorBitOf(unsigned i
)
434 bool operator == (const BitVectorBitOf
& other
) const {
435 return bitIndex
== other
.bitIndex
;
437 };/* struct BitVectorBitOf */
440 * Hash function for the BitVectorBitOf objects.
442 struct CVC4_PUBLIC BitVectorBitOfHashFunction
{
443 size_t operator()(const BitVectorBitOf
& b
) const {
446 };/* struct BitVectorBitOfHashFunction */
450 struct CVC4_PUBLIC BitVectorSize
{
452 BitVectorSize(unsigned size
)
454 operator unsigned () const { return size
; }
455 };/* struct BitVectorSize */
457 struct CVC4_PUBLIC BitVectorRepeat
{
458 unsigned repeatAmount
;
459 BitVectorRepeat(unsigned repeatAmount
)
460 : repeatAmount(repeatAmount
) {}
461 operator unsigned () const { return repeatAmount
; }
462 };/* struct BitVectorRepeat */
464 struct CVC4_PUBLIC BitVectorZeroExtend
{
465 unsigned zeroExtendAmount
;
466 BitVectorZeroExtend(unsigned zeroExtendAmount
)
467 : zeroExtendAmount(zeroExtendAmount
) {}
468 operator unsigned () const { return zeroExtendAmount
; }
469 };/* struct BitVectorZeroExtend */
471 struct CVC4_PUBLIC BitVectorSignExtend
{
472 unsigned signExtendAmount
;
473 BitVectorSignExtend(unsigned signExtendAmount
)
474 : signExtendAmount(signExtendAmount
) {}
475 operator unsigned () const { return signExtendAmount
; }
476 };/* struct BitVectorSignExtend */
478 struct CVC4_PUBLIC BitVectorRotateLeft
{
479 unsigned rotateLeftAmount
;
480 BitVectorRotateLeft(unsigned rotateLeftAmount
)
481 : rotateLeftAmount(rotateLeftAmount
) {}
482 operator unsigned () const { return rotateLeftAmount
; }
483 };/* struct BitVectorRotateLeft */
485 struct CVC4_PUBLIC BitVectorRotateRight
{
486 unsigned rotateRightAmount
;
487 BitVectorRotateRight(unsigned rotateRightAmount
)
488 : rotateRightAmount(rotateRightAmount
) {}
489 operator unsigned () const { return rotateRightAmount
; }
490 };/* struct BitVectorRotateRight */
492 struct CVC4_PUBLIC IntToBitVector
{
494 IntToBitVector(unsigned size
)
496 operator unsigned () const { return size
; }
497 };/* struct IntToBitVector */
499 template <typename T
>
500 struct CVC4_PUBLIC UnsignedHashFunction
{
501 inline size_t operator()(const T
& x
) const {
504 };/* struct UnsignedHashFunction */
506 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) CVC4_PUBLIC
;
507 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) {
508 return os
<< bv
.toString();
511 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) CVC4_PUBLIC
;
512 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) {
513 return os
<< "[" << bv
.high
<< ":" << bv
.low
<< "]";
516 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) CVC4_PUBLIC
;
517 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) {
518 return os
<< "[" << bv
.bitIndex
<< "]";
521 inline std::ostream
& operator <<(std::ostream
& os
, const IntToBitVector
& bv
) CVC4_PUBLIC
;
522 inline std::ostream
& operator <<(std::ostream
& os
, const IntToBitVector
& bv
) {
523 return os
<< "[" << bv
.size
<< "]";
526 }/* CVC4 namespace */
528 #endif /* __CVC4__BITVECTOR_H */