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-2014 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
25 #include "base/exception.h"
26 #include "util/integer.h"
30 class CVC4_PUBLIC BitVector
{
36 * no overflows: 2^d_size < d_value
37 * no negative numbers: d_value >= 0
42 Integer
toSignedInt() const {
43 // returns Integer corresponding to two's complement interpretation of bv
44 unsigned size
= d_size
;
45 Integer sign_bit
= d_value
.extractBitRange(1,size
-1);
46 Integer val
= d_value
.extractBitRange(size
-1, 0);
47 Integer res
= Integer(-1) * sign_bit
.multiplyByPow2(size
- 1) + val
;
54 BitVector(unsigned size
, const Integer
& val
):
56 d_value(val
.modByPow2(size
))
59 BitVector(unsigned size
= 0)
60 : d_size(size
), d_value(0) {}
62 BitVector(unsigned size
, unsigned int z
)
63 : d_size(size
), d_value(z
) {
64 d_value
= d_value
.modByPow2(size
);
67 BitVector(unsigned size
, unsigned long int z
)
68 : d_size(size
), d_value(z
) {
69 d_value
= d_value
.modByPow2(size
);
72 BitVector(unsigned size
, const BitVector
& q
)
73 : d_size(size
), d_value(q
.d_value
) {}
75 BitVector(const std::string
& num
, unsigned base
= 2);
79 Integer
toInteger() const {
83 BitVector
& operator =(const BitVector
& x
) {
91 bool operator ==(const BitVector
& y
) const {
92 if (d_size
!= y
.d_size
) return false;
93 return d_value
== y
.d_value
;
96 bool operator !=(const BitVector
& y
) const {
97 if (d_size
!= y
.d_size
) return true;
98 return d_value
!= y
.d_value
;
101 BitVector
concat (const BitVector
& other
) const {
102 return BitVector(d_size
+ other
.d_size
, (d_value
.multiplyByPow2(other
.d_size
)) + other
.d_value
);
105 BitVector
extract(unsigned high
, unsigned low
) const {
106 return BitVector(high
- low
+ 1, d_value
.extractBitRange(high
- low
+ 1, low
));
110 Bitwise operations on BitVectors
114 BitVector
operator ^(const BitVector
& y
) const {
115 CheckArgument(d_size
== y
.d_size
, y
);
116 return BitVector(d_size
, d_value
.bitwiseXor(y
.d_value
));
120 BitVector
operator |(const BitVector
& y
) const {
121 CheckArgument(d_size
== y
.d_size
, y
);
122 return BitVector(d_size
, d_value
.bitwiseOr(y
.d_value
));
126 BitVector
operator &(const BitVector
& y
) const {
127 CheckArgument(d_size
== y
.d_size
, y
);
128 return BitVector(d_size
, d_value
.bitwiseAnd(y
.d_value
));
132 BitVector
operator ~() const {
133 return BitVector(d_size
, d_value
.bitwiseNot());
137 Arithmetic operations on BitVectors
141 bool operator <(const BitVector
& y
) const {
142 return d_value
< y
.d_value
;
145 bool operator >(const BitVector
& y
) const {
146 return d_value
> y
.d_value
;
149 bool operator <=(const BitVector
& y
) const {
150 return d_value
<= y
.d_value
;
153 bool operator >=(const BitVector
& y
) const {
154 return d_value
>= y
.d_value
;
158 BitVector
operator +(const BitVector
& y
) const {
159 CheckArgument(d_size
== y
.d_size
, y
);
160 Integer sum
= d_value
+ y
.d_value
;
161 return BitVector(d_size
, sum
);
164 BitVector
operator -(const BitVector
& y
) const {
165 CheckArgument(d_size
== y
.d_size
, y
);
166 // to maintain the invariant that we are only adding BitVectors of the
168 BitVector
one(d_size
, Integer(1));
169 return *this + ~y
+ one
;
172 BitVector
operator -() const {
173 BitVector
one(d_size
, Integer(1));
174 return ~(*this) + one
;
177 BitVector
operator *(const BitVector
& y
) const {
178 CheckArgument(d_size
== y
.d_size
, y
);
179 Integer prod
= d_value
* y
.d_value
;
180 return BitVector(d_size
, prod
);
183 BitVector
setBit(uint32_t i
) const {
184 CheckArgument(i
< d_size
, i
);
185 Integer res
= d_value
.setBit(i
);
186 return BitVector(d_size
, res
);
189 bool isBitSet(uint32_t i
) const {
190 CheckArgument(i
< d_size
, i
);
191 return d_value
.isBitSet(i
);
195 * Total division function that returns 0 when the denominator is 0.
197 BitVector
unsignedDivTotal (const BitVector
& y
) const {
199 CheckArgument(d_size
== y
.d_size
, y
);
200 if (y
.d_value
== 0) {
201 // under division by zero return -1
202 return BitVector(d_size
, Integer(1).oneExtend(1, d_size
- 1));
204 CheckArgument(d_value
>= 0, this);
205 CheckArgument(y
.d_value
> 0, y
);
206 return BitVector(d_size
, d_value
.floorDivideQuotient(y
.d_value
));
210 * Total division function that returns 0 when the denominator is 0.
212 BitVector
unsignedRemTotal(const BitVector
& y
) const {
213 CheckArgument(d_size
== y
.d_size
, y
);
214 if (y
.d_value
== 0) {
215 return BitVector(d_size
, d_value
);
217 CheckArgument(d_value
>= 0, this);
218 CheckArgument(y
.d_value
> 0, y
);
219 return BitVector(d_size
, d_value
.floorDivideRemainder(y
.d_value
));
223 bool signedLessThan(const BitVector
& y
) const {
224 CheckArgument(d_size
== y
.d_size
, y
);
225 CheckArgument(d_value
>= 0, this);
226 CheckArgument(y
.d_value
>= 0, y
);
227 Integer a
= (*this).toSignedInt();
228 Integer b
= y
.toSignedInt();
233 bool unsignedLessThan(const BitVector
& y
) const {
234 CheckArgument(d_size
== y
.d_size
, y
);
235 CheckArgument(d_value
>= 0, this);
236 CheckArgument(y
.d_value
>= 0, y
);
237 return d_value
< y
.d_value
;
240 bool signedLessThanEq(const BitVector
& y
) const {
241 CheckArgument(d_size
== y
.d_size
, y
);
242 CheckArgument(d_value
>= 0, this);
243 CheckArgument(y
.d_value
>= 0, y
);
244 Integer a
= (*this).toSignedInt();
245 Integer b
= y
.toSignedInt();
250 bool unsignedLessThanEq(const BitVector
& y
) const {
251 CheckArgument(d_size
== y
.d_size
, this);
252 CheckArgument(d_value
>= 0, this);
253 CheckArgument(y
.d_value
>= 0, y
);
254 return d_value
<= y
.d_value
;
262 BitVector
zeroExtend(unsigned amount
) const {
263 return BitVector(d_size
+ amount
, d_value
);
266 BitVector
signExtend(unsigned amount
) const {
267 Integer sign_bit
= d_value
.extractBitRange(1, d_size
-1);
268 if(sign_bit
== Integer(0)) {
269 return BitVector(d_size
+ amount
, d_value
);
271 Integer val
= d_value
.oneExtend(d_size
, amount
);
272 return BitVector(d_size
+ amount
, val
);
280 BitVector
leftShift(const BitVector
& y
) const {
281 if (y
.d_value
> Integer(d_size
)) {
282 return BitVector(d_size
, Integer(0));
284 if (y
.d_value
== 0) {
288 // making sure we don't lose information casting
289 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
290 uint32_t amount
= y
.d_value
.toUnsignedInt();
291 Integer res
= d_value
.multiplyByPow2(amount
);
292 return BitVector(d_size
, res
);
295 BitVector
logicalRightShift(const BitVector
& y
) const {
296 if(y
.d_value
> Integer(d_size
)) {
297 return BitVector(d_size
, Integer(0));
300 // making sure we don't lose information casting
301 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
302 uint32_t amount
= y
.d_value
.toUnsignedInt();
303 Integer res
= d_value
.divByPow2(amount
);
304 return BitVector(d_size
, res
);
307 BitVector
arithRightShift(const BitVector
& y
) const {
308 Integer sign_bit
= d_value
.extractBitRange(1, d_size
- 1);
309 if(y
.d_value
> Integer(d_size
)) {
310 if(sign_bit
== Integer(0)) {
311 return BitVector(d_size
, Integer(0));
313 return BitVector(d_size
, Integer(d_size
).multiplyByPow2(d_size
) -1 );
317 if (y
.d_value
== 0) {
321 // making sure we don't lose information casting
322 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
324 uint32_t amount
= y
.d_value
.toUnsignedInt();
325 Integer rest
= d_value
.divByPow2(amount
);
327 if(sign_bit
== Integer(0)) {
328 return BitVector(d_size
, rest
);
330 Integer res
= rest
.oneExtend(d_size
- amount
, amount
);
331 return BitVector(d_size
, res
);
336 Convenience functions
339 size_t hash() const {
340 return d_value
.hash() + d_size
;
343 std::string
toString(unsigned int base
= 2) const {
344 std::string str
= d_value
.toString(base
);
345 if( base
== 2 && d_size
> str
.size() ) {
347 for( unsigned int i
=0; i
< d_size
- str
.size(); ++i
) {
356 unsigned getSize() const {
360 const Integer
& getValue() const {
365 Returns k is the integer is equal to 2^{k-1} and zero
367 @return k if the integer is equal to 2^{k-1} and zero otherwise
370 return d_value
.isPow2();
373 };/* class BitVector */
377 inline BitVector::BitVector(const std::string
& num
, unsigned base
) {
378 CheckArgument(base
== 2 || base
== 16, base
);
383 d_size
= num
.size() * 4;
386 d_value
= Integer(num
, base
);
387 }/* BitVector::BitVector() */
391 * Hash function for the BitVector constants.
393 struct CVC4_PUBLIC BitVectorHashFunction
{
394 inline size_t operator()(const BitVector
& bv
) const {
397 };/* struct BitVectorHashFunction */
400 * The structure representing the extraction operation for bit-vectors. The
401 * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
402 * by taking the bits at indices <code>high ... low</code>
404 struct CVC4_PUBLIC BitVectorExtract
{
405 /** The high bit of the range for this extract */
407 /** The low bit of the range for this extract */
410 BitVectorExtract(unsigned high
, unsigned low
)
411 : high(high
), low(low
) {}
413 bool operator == (const BitVectorExtract
& extract
) const {
414 return high
== extract
.high
&& low
== extract
.low
;
416 };/* struct BitVectorExtract */
419 * Hash function for the BitVectorExtract objects.
421 struct CVC4_PUBLIC BitVectorExtractHashFunction
{
422 size_t operator()(const BitVectorExtract
& extract
) const {
423 size_t hash
= extract
.low
;
424 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
427 };/* struct BitVectorExtractHashFunction */
431 * The structure representing the extraction of one Boolean bit.
433 struct CVC4_PUBLIC BitVectorBitOf
{
434 /** The index of the bit */
436 BitVectorBitOf(unsigned i
)
439 bool operator == (const BitVectorBitOf
& other
) const {
440 return bitIndex
== other
.bitIndex
;
442 };/* struct BitVectorBitOf */
445 * Hash function for the BitVectorBitOf objects.
447 struct CVC4_PUBLIC BitVectorBitOfHashFunction
{
448 size_t operator()(const BitVectorBitOf
& b
) const {
451 };/* struct BitVectorBitOfHashFunction */
455 struct CVC4_PUBLIC BitVectorSize
{
457 BitVectorSize(unsigned size
)
459 operator unsigned () const { return size
; }
460 };/* struct BitVectorSize */
462 struct CVC4_PUBLIC BitVectorRepeat
{
463 unsigned repeatAmount
;
464 BitVectorRepeat(unsigned repeatAmount
)
465 : repeatAmount(repeatAmount
) {}
466 operator unsigned () const { return repeatAmount
; }
467 };/* struct BitVectorRepeat */
469 struct CVC4_PUBLIC BitVectorZeroExtend
{
470 unsigned zeroExtendAmount
;
471 BitVectorZeroExtend(unsigned zeroExtendAmount
)
472 : zeroExtendAmount(zeroExtendAmount
) {}
473 operator unsigned () const { return zeroExtendAmount
; }
474 };/* struct BitVectorZeroExtend */
476 struct CVC4_PUBLIC BitVectorSignExtend
{
477 unsigned signExtendAmount
;
478 BitVectorSignExtend(unsigned signExtendAmount
)
479 : signExtendAmount(signExtendAmount
) {}
480 operator unsigned () const { return signExtendAmount
; }
481 };/* struct BitVectorSignExtend */
483 struct CVC4_PUBLIC BitVectorRotateLeft
{
484 unsigned rotateLeftAmount
;
485 BitVectorRotateLeft(unsigned rotateLeftAmount
)
486 : rotateLeftAmount(rotateLeftAmount
) {}
487 operator unsigned () const { return rotateLeftAmount
; }
488 };/* struct BitVectorRotateLeft */
490 struct CVC4_PUBLIC BitVectorRotateRight
{
491 unsigned rotateRightAmount
;
492 BitVectorRotateRight(unsigned rotateRightAmount
)
493 : rotateRightAmount(rotateRightAmount
) {}
494 operator unsigned () const { return rotateRightAmount
; }
495 };/* struct BitVectorRotateRight */
497 struct CVC4_PUBLIC IntToBitVector
{
499 IntToBitVector(unsigned size
)
501 operator unsigned () const { return size
; }
502 };/* struct IntToBitVector */
504 template <typename T
>
505 struct CVC4_PUBLIC UnsignedHashFunction
{
506 inline size_t operator()(const T
& x
) const {
509 };/* struct UnsignedHashFunction */
511 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) CVC4_PUBLIC
;
512 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) {
513 return os
<< bv
.toString();
516 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) CVC4_PUBLIC
;
517 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) {
518 return os
<< "[" << bv
.high
<< ":" << bv
.low
<< "]";
521 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) CVC4_PUBLIC
;
522 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) {
523 return os
<< "[" << bv
.bitIndex
<< "]";
526 inline std::ostream
& operator <<(std::ostream
& os
, const IntToBitVector
& bv
) CVC4_PUBLIC
;
527 inline std::ostream
& operator <<(std::ostream
& os
, const IntToBitVector
& bv
) {
528 return os
<< "[" << bv
.size
<< "]";
531 }/* CVC4 namespace */
533 #endif /* __CVC4__BITVECTOR_H */