1 /********************* */
4 ** Original author: Dejan Jovanovic
5 ** Major contributors: Morgan Deters, Liana Hadarean
6 ** Minor contributors (to current version): Christopher L. Conway
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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
24 #include "util/exception.h"
25 #include "util/integer.h"
29 class CVC4_PUBLIC BitVector
{
35 * no overflows: 2^d_size < d_value
36 * no negative numbers: d_value >= 0
41 Integer
toSignedInt() const {
42 // returns Integer corresponding to two's complement interpretation of bv
43 unsigned size
= d_size
;
44 Integer sign_bit
= d_value
.extractBitRange(1,size
-1);
45 Integer val
= d_value
.extractBitRange(size
-1, 0);
46 Integer res
= Integer(-1) * sign_bit
.multiplyByPow2(size
- 1) + val
;
53 BitVector(unsigned size
, const Integer
& val
):
55 d_value(val
.modByPow2(size
))
58 BitVector(unsigned size
= 0)
59 : d_size(size
), d_value(0) {}
61 BitVector(unsigned size
, unsigned int z
)
62 : d_size(size
), d_value(z
) {
63 d_value
= d_value
.modByPow2(size
);
66 BitVector(unsigned size
, unsigned long int z
)
67 : d_size(size
), d_value(z
) {
68 d_value
= d_value
.modByPow2(size
);
71 BitVector(unsigned size
, const BitVector
& q
)
72 : d_size(size
), d_value(q
.d_value
) {}
74 BitVector(const std::string
& num
, unsigned base
= 2);
78 Integer
toInteger() const {
82 BitVector
& operator =(const BitVector
& x
) {
90 bool operator ==(const BitVector
& y
) const {
91 if (d_size
!= y
.d_size
) return false;
92 return d_value
== y
.d_value
;
95 bool operator !=(const BitVector
& y
) const {
96 if (d_size
!= y
.d_size
) return true;
97 return d_value
!= y
.d_value
;
100 BitVector
concat (const BitVector
& other
) const {
101 return BitVector(d_size
+ other
.d_size
, (d_value
.multiplyByPow2(other
.d_size
)) + other
.d_value
);
104 BitVector
extract(unsigned high
, unsigned low
) const {
105 return BitVector(high
- low
+ 1, d_value
.extractBitRange(high
- low
+ 1, low
));
109 Bitwise operations on BitVectors
113 BitVector
operator ^(const BitVector
& y
) const {
114 CheckArgument(d_size
== y
.d_size
, y
);
115 return BitVector(d_size
, d_value
.bitwiseXor(y
.d_value
));
119 BitVector
operator |(const BitVector
& y
) const {
120 CheckArgument(d_size
== y
.d_size
, y
);
121 return BitVector(d_size
, d_value
.bitwiseOr(y
.d_value
));
125 BitVector
operator &(const BitVector
& y
) const {
126 CheckArgument(d_size
== y
.d_size
, y
);
127 return BitVector(d_size
, d_value
.bitwiseAnd(y
.d_value
));
131 BitVector
operator ~() const {
132 return BitVector(d_size
, d_value
.bitwiseNot());
136 Arithmetic operations on BitVectors
140 bool operator <(const BitVector
& y
) const {
141 return d_value
< y
.d_value
;
144 bool operator >(const BitVector
& y
) const {
145 return d_value
> y
.d_value
;
148 bool operator <=(const BitVector
& y
) const {
149 return d_value
<= y
.d_value
;
152 bool operator >=(const BitVector
& y
) const {
153 return d_value
>= y
.d_value
;
157 BitVector
operator +(const BitVector
& y
) const {
158 CheckArgument(d_size
== y
.d_size
, y
);
159 Integer sum
= d_value
+ y
.d_value
;
160 return BitVector(d_size
, sum
);
163 BitVector
operator -(const BitVector
& y
) const {
164 CheckArgument(d_size
== y
.d_size
, y
);
165 // to maintain the invariant that we are only adding BitVectors of the
167 BitVector
one(d_size
, Integer(1));
168 return *this + ~y
+ one
;
171 BitVector
operator -() const {
172 BitVector
one(d_size
, Integer(1));
173 return ~(*this) + one
;
176 BitVector
operator *(const BitVector
& y
) const {
177 CheckArgument(d_size
== y
.d_size
, y
);
178 Integer prod
= d_value
* y
.d_value
;
179 return BitVector(d_size
, prod
);
182 BitVector
setBit(uint32_t i
) const {
183 CheckArgument(i
< d_size
, i
);
184 Integer res
= d_value
.setBit(i
);
185 return BitVector(d_size
, res
);
188 bool isBitSet(uint32_t i
) const {
189 CheckArgument(i
< d_size
, i
);
190 return d_value
.isBitSet(i
);
194 * Total division function that returns 0 when the denominator is 0.
196 BitVector
unsignedDivTotal (const BitVector
& y
) const {
198 CheckArgument(d_size
== y
.d_size
, y
);
199 if (y
.d_value
== 0) {
200 // under division by zero return -1
201 return BitVector(d_size
, Integer(1).oneExtend(1, d_size
- 1));
203 CheckArgument(d_value
>= 0, this);
204 CheckArgument(y
.d_value
> 0, y
);
205 return BitVector(d_size
, d_value
.floorDivideQuotient(y
.d_value
));
209 * Total division function that returns 0 when the denominator is 0.
211 BitVector
unsignedRemTotal(const BitVector
& y
) const {
212 CheckArgument(d_size
== y
.d_size
, y
);
213 if (y
.d_value
== 0) {
214 return BitVector(d_size
, d_value
);
216 CheckArgument(d_value
>= 0, this);
217 CheckArgument(y
.d_value
> 0, y
);
218 return BitVector(d_size
, d_value
.floorDivideRemainder(y
.d_value
));
222 bool signedLessThan(const BitVector
& y
) const {
223 CheckArgument(d_size
== y
.d_size
, y
);
224 CheckArgument(d_value
>= 0, this);
225 CheckArgument(y
.d_value
>= 0, y
);
226 Integer a
= (*this).toSignedInt();
227 Integer b
= y
.toSignedInt();
232 bool unsignedLessThan(const BitVector
& y
) const {
233 CheckArgument(d_size
== y
.d_size
, y
);
234 CheckArgument(d_value
>= 0, this);
235 CheckArgument(y
.d_value
>= 0, y
);
236 return d_value
< y
.d_value
;
239 bool signedLessThanEq(const BitVector
& y
) const {
240 CheckArgument(d_size
== y
.d_size
, y
);
241 CheckArgument(d_value
>= 0, this);
242 CheckArgument(y
.d_value
>= 0, y
);
243 Integer a
= (*this).toSignedInt();
244 Integer b
= y
.toSignedInt();
249 bool unsignedLessThanEq(const BitVector
& y
) const {
250 CheckArgument(d_size
== y
.d_size
, this);
251 CheckArgument(d_value
>= 0, this);
252 CheckArgument(y
.d_value
>= 0, y
);
253 return d_value
<= y
.d_value
;
261 BitVector
zeroExtend(unsigned amount
) const {
262 return BitVector(d_size
+ amount
, d_value
);
265 BitVector
signExtend(unsigned amount
) const {
266 Integer sign_bit
= d_value
.extractBitRange(1, d_size
-1);
267 if(sign_bit
== Integer(0)) {
268 return BitVector(d_size
+ amount
, d_value
);
270 Integer val
= d_value
.oneExtend(d_size
, amount
);
271 return BitVector(d_size
+ amount
, val
);
279 BitVector
leftShift(const BitVector
& y
) const {
280 if (y
.d_value
> Integer(d_size
)) {
281 return BitVector(d_size
, Integer(0));
283 if (y
.d_value
== 0) {
287 // making sure we don't lose information casting
288 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
289 uint32_t amount
= y
.d_value
.toUnsignedInt();
290 Integer res
= d_value
.multiplyByPow2(amount
);
291 return BitVector(d_size
, res
);
294 BitVector
logicalRightShift(const BitVector
& y
) const {
295 if(y
.d_value
> Integer(d_size
)) {
296 return BitVector(d_size
, Integer(0));
299 // making sure we don't lose information casting
300 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
301 uint32_t amount
= y
.d_value
.toUnsignedInt();
302 Integer res
= d_value
.divByPow2(amount
);
303 return BitVector(d_size
, res
);
306 BitVector
arithRightShift(const BitVector
& y
) const {
307 Integer sign_bit
= d_value
.extractBitRange(1, d_size
- 1);
308 if(y
.d_value
> Integer(d_size
)) {
309 if(sign_bit
== Integer(0)) {
310 return BitVector(d_size
, Integer(0));
312 return BitVector(d_size
, Integer(d_size
).multiplyByPow2(d_size
) -1 );
316 if (y
.d_value
== 0) {
320 // making sure we don't lose information casting
321 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
323 uint32_t amount
= y
.d_value
.toUnsignedInt();
324 Integer rest
= d_value
.divByPow2(amount
);
326 if(sign_bit
== Integer(0)) {
327 return BitVector(d_size
, rest
);
329 Integer res
= rest
.oneExtend(d_size
- amount
, amount
);
330 return BitVector(d_size
, res
);
335 Convenience functions
338 size_t hash() const {
339 return d_value
.hash() + d_size
;
342 std::string
toString(unsigned int base
= 2) const {
343 std::string str
= d_value
.toString(base
);
344 if( base
== 2 && d_size
> str
.size() ) {
346 for( unsigned int i
=0; i
< d_size
- str
.size(); ++i
) {
355 unsigned getSize() const {
359 const Integer
& getValue() const {
364 Returns k is the integer is equal to 2^{k-1} and zero
366 @return k if the integer is equal to 2^{k-1} and zero otherwise
369 return d_value
.isPow2();
372 };/* class BitVector */
376 inline BitVector::BitVector(const std::string
& num
, unsigned base
) {
377 CheckArgument(base
== 2 || base
== 16, base
);
382 d_size
= num
.size() * 4;
385 d_value
= Integer(num
, base
);
386 }/* BitVector::BitVector() */
390 * Hash function for the BitVector constants.
392 struct CVC4_PUBLIC BitVectorHashFunction
{
393 inline size_t operator()(const BitVector
& bv
) const {
396 };/* struct BitVectorHashFunction */
399 * The structure representing the extraction operation for bit-vectors. The
400 * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
401 * by taking the bits at indices <code>high ... low</code>
403 struct CVC4_PUBLIC BitVectorExtract
{
404 /** The high bit of the range for this extract */
406 /** The low bit of the range for this extract */
409 BitVectorExtract(unsigned high
, unsigned low
)
410 : high(high
), low(low
) {}
412 bool operator == (const BitVectorExtract
& extract
) const {
413 return high
== extract
.high
&& low
== extract
.low
;
415 };/* struct BitVectorExtract */
418 * Hash function for the BitVectorExtract objects.
420 struct CVC4_PUBLIC BitVectorExtractHashFunction
{
421 size_t operator()(const BitVectorExtract
& extract
) const {
422 size_t hash
= extract
.low
;
423 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
426 };/* struct BitVectorExtractHashFunction */
430 * The structure representing the extraction of one Boolean bit.
432 struct CVC4_PUBLIC BitVectorBitOf
{
433 /** The index of the bit */
435 BitVectorBitOf(unsigned i
)
438 bool operator == (const BitVectorBitOf
& other
) const {
439 return bitIndex
== other
.bitIndex
;
441 };/* struct BitVectorBitOf */
444 * Hash function for the BitVectorBitOf objects.
446 struct CVC4_PUBLIC BitVectorBitOfHashFunction
{
447 size_t operator()(const BitVectorBitOf
& b
) const {
450 };/* struct BitVectorBitOfHashFunction */
454 struct CVC4_PUBLIC BitVectorSize
{
456 BitVectorSize(unsigned size
)
458 operator unsigned () const { return size
; }
459 };/* struct BitVectorSize */
461 struct CVC4_PUBLIC BitVectorRepeat
{
462 unsigned repeatAmount
;
463 BitVectorRepeat(unsigned repeatAmount
)
464 : repeatAmount(repeatAmount
) {}
465 operator unsigned () const { return repeatAmount
; }
466 };/* struct BitVectorRepeat */
468 struct CVC4_PUBLIC BitVectorZeroExtend
{
469 unsigned zeroExtendAmount
;
470 BitVectorZeroExtend(unsigned zeroExtendAmount
)
471 : zeroExtendAmount(zeroExtendAmount
) {}
472 operator unsigned () const { return zeroExtendAmount
; }
473 };/* struct BitVectorZeroExtend */
475 struct CVC4_PUBLIC BitVectorSignExtend
{
476 unsigned signExtendAmount
;
477 BitVectorSignExtend(unsigned signExtendAmount
)
478 : signExtendAmount(signExtendAmount
) {}
479 operator unsigned () const { return signExtendAmount
; }
480 };/* struct BitVectorSignExtend */
482 struct CVC4_PUBLIC BitVectorRotateLeft
{
483 unsigned rotateLeftAmount
;
484 BitVectorRotateLeft(unsigned rotateLeftAmount
)
485 : rotateLeftAmount(rotateLeftAmount
) {}
486 operator unsigned () const { return rotateLeftAmount
; }
487 };/* struct BitVectorRotateLeft */
489 struct CVC4_PUBLIC BitVectorRotateRight
{
490 unsigned rotateRightAmount
;
491 BitVectorRotateRight(unsigned rotateRightAmount
)
492 : rotateRightAmount(rotateRightAmount
) {}
493 operator unsigned () const { return rotateRightAmount
; }
494 };/* struct BitVectorRotateRight */
496 struct CVC4_PUBLIC IntToBitVector
{
498 IntToBitVector(unsigned size
)
500 operator unsigned () const { return size
; }
501 };/* struct IntToBitVector */
503 template <typename T
>
504 struct CVC4_PUBLIC UnsignedHashFunction
{
505 inline size_t operator()(const T
& x
) const {
508 };/* struct UnsignedHashFunction */
510 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) CVC4_PUBLIC
;
511 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) {
512 return os
<< bv
.toString();
515 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) CVC4_PUBLIC
;
516 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) {
517 return os
<< "[" << bv
.high
<< ":" << bv
.low
<< "]";
520 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) CVC4_PUBLIC
;
521 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) {
522 return os
<< "[" << bv
.bitIndex
<< "]";
525 inline std::ostream
& operator <<(std::ostream
& os
, const IntToBitVector
& bv
) CVC4_PUBLIC
;
526 inline std::ostream
& operator <<(std::ostream
& os
, const IntToBitVector
& bv
) {
527 return os
<< "[" << bv
.size
<< "]";
530 }/* CVC4 namespace */
532 #endif /* __CVC4__BITVECTOR_H */