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-2017 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 BitVector
concat (const BitVector
& other
) const {
71 return BitVector(d_size
+ other
.d_size
, (d_value
.multiplyByPow2(other
.d_size
)) + other
.d_value
);
74 BitVector
extract(unsigned high
, unsigned low
) const {
75 return BitVector(high
- low
+ 1, d_value
.extractBitRange(high
- low
+ 1, low
));
82 bool operator ==(const BitVector
& y
) const {
83 if (d_size
!= y
.d_size
) return false;
84 return d_value
== y
.d_value
;
87 bool operator !=(const BitVector
& y
) const {
88 if (d_size
!= y
.d_size
) return true;
89 return d_value
!= y
.d_value
;
96 bool operator <(const BitVector
& y
) const {
97 return d_value
< y
.d_value
;
100 bool unsignedLessThan(const BitVector
& y
) const {
101 CheckArgument(d_size
== y
.d_size
, y
);
102 CheckArgument(d_value
>= 0, this);
103 CheckArgument(y
.d_value
>= 0, y
);
104 return d_value
< y
.d_value
;
107 bool operator <=(const BitVector
& y
) const {
108 return d_value
<= y
.d_value
;
111 bool unsignedLessThanEq(const BitVector
& y
) const {
112 CheckArgument(d_size
== y
.d_size
, this);
113 CheckArgument(d_value
>= 0, this);
114 CheckArgument(y
.d_value
>= 0, y
);
115 return d_value
<= y
.d_value
;
118 bool operator >(const BitVector
& y
) const {
119 return d_value
> y
.d_value
;
122 bool operator >=(const BitVector
& y
) const {
123 return d_value
>= y
.d_value
;
130 bool signedLessThan(const BitVector
& y
) const {
131 CheckArgument(d_size
== y
.d_size
, y
);
132 CheckArgument(d_value
>= 0, this);
133 CheckArgument(y
.d_value
>= 0, y
);
134 Integer a
= (*this).toSignedInt();
135 Integer b
= y
.toSignedInt();
140 bool signedLessThanEq(const BitVector
& y
) const {
141 CheckArgument(d_size
== y
.d_size
, y
);
142 CheckArgument(d_value
>= 0, this);
143 CheckArgument(y
.d_value
>= 0, y
);
144 Integer a
= (*this).toSignedInt();
145 Integer b
= y
.toSignedInt();
155 BitVector
operator ^(const BitVector
& y
) const {
156 CheckArgument(d_size
== y
.d_size
, y
);
157 return BitVector(d_size
, d_value
.bitwiseXor(y
.d_value
));
161 BitVector
operator |(const BitVector
& y
) const {
162 CheckArgument(d_size
== y
.d_size
, y
);
163 return BitVector(d_size
, d_value
.bitwiseOr(y
.d_value
));
167 BitVector
operator &(const BitVector
& y
) const {
168 CheckArgument(d_size
== y
.d_size
, y
);
169 return BitVector(d_size
, d_value
.bitwiseAnd(y
.d_value
));
173 BitVector
operator ~() const {
174 return BitVector(d_size
, d_value
.bitwiseNot());
179 * Arithmetic operations
182 BitVector
operator +(const BitVector
& y
) const {
183 CheckArgument(d_size
== y
.d_size
, y
);
184 Integer sum
= d_value
+ y
.d_value
;
185 return BitVector(d_size
, sum
);
188 BitVector
operator -(const BitVector
& y
) const {
189 CheckArgument(d_size
== y
.d_size
, y
);
190 // to maintain the invariant that we are only adding BitVectors of the
192 BitVector
one(d_size
, Integer(1));
193 return *this + ~y
+ one
;
196 BitVector
operator -() const {
197 BitVector
one(d_size
, Integer(1));
198 return ~(*this) + one
;
201 BitVector
operator *(const BitVector
& y
) const {
202 CheckArgument(d_size
== y
.d_size
, y
);
203 Integer prod
= d_value
* y
.d_value
;
204 return BitVector(d_size
, prod
);
208 * Total division function.
209 * Returns 2^d_size-1 (signed: -1) when the denominator is zero
210 * (d_value / 0 = 2^d_size - 1).
212 BitVector
unsignedDivTotal (const BitVector
& y
) const {
214 CheckArgument(d_size
== y
.d_size
, y
);
215 if (y
.d_value
== 0) {
216 // under division by zero return -1
217 return BitVector(d_size
, Integer(1).oneExtend(1, d_size
- 1));
219 CheckArgument(d_value
>= 0, this);
220 CheckArgument(y
.d_value
> 0, y
);
221 return BitVector(d_size
, d_value
.floorDivideQuotient(y
.d_value
));
225 * Total remainder function.
226 * Returns d_value when the denominator is zero (d_value % 0 = d_value).
228 BitVector
unsignedRemTotal(const BitVector
& y
) const {
229 CheckArgument(d_size
== y
.d_size
, y
);
230 if (y
.d_value
== 0) {
231 return BitVector(d_size
, d_value
);
233 CheckArgument(d_value
>= 0, this);
234 CheckArgument(y
.d_value
> 0, y
);
235 return BitVector(d_size
, d_value
.floorDivideRemainder(y
.d_value
));
243 BitVector
zeroExtend(unsigned amount
) const {
244 return BitVector(d_size
+ amount
, d_value
);
247 BitVector
signExtend(unsigned amount
) const {
248 Integer sign_bit
= d_value
.extractBitRange(1, d_size
-1);
249 if(sign_bit
== Integer(0)) {
250 return BitVector(d_size
+ amount
, d_value
);
252 Integer val
= d_value
.oneExtend(d_size
, amount
);
253 return BitVector(d_size
+ amount
, val
);
260 BitVector
leftShift(const BitVector
& y
) const {
261 if (y
.d_value
> Integer(d_size
)) {
262 return BitVector(d_size
, Integer(0));
264 if (y
.d_value
== 0) {
267 // making sure we don't lose information casting
268 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
269 uint32_t amount
= y
.d_value
.toUnsignedInt();
270 Integer res
= d_value
.multiplyByPow2(amount
);
271 return BitVector(d_size
, res
);
274 BitVector
logicalRightShift(const BitVector
& y
) const {
275 if(y
.d_value
> Integer(d_size
)) {
276 return BitVector(d_size
, Integer(0));
278 // making sure we don't lose information casting
279 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
280 uint32_t amount
= y
.d_value
.toUnsignedInt();
281 Integer res
= d_value
.divByPow2(amount
);
282 return BitVector(d_size
, res
);
285 BitVector
arithRightShift(const BitVector
& y
) const {
286 Integer sign_bit
= d_value
.extractBitRange(1, d_size
- 1);
287 if(y
.d_value
> Integer(d_size
)) {
288 if(sign_bit
== Integer(0)) {
289 return BitVector(d_size
, Integer(0));
291 return BitVector(d_size
, Integer(d_size
).multiplyByPow2(d_size
) -1 );
295 if (y
.d_value
== 0) {
299 // making sure we don't lose information casting
300 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
302 uint32_t amount
= y
.d_value
.toUnsignedInt();
303 Integer rest
= d_value
.divByPow2(amount
);
305 if(sign_bit
== Integer(0)) {
306 return BitVector(d_size
, rest
);
308 Integer res
= rest
.oneExtend(d_size
- amount
, amount
);
309 return BitVector(d_size
, res
);
314 * Convenience functions
317 size_t hash() const {
318 return d_value
.hash() + d_size
;
321 std::string
toString(unsigned int base
= 2) const {
322 std::string str
= d_value
.toString(base
);
323 if( base
== 2 && d_size
> str
.size() ) {
325 for( unsigned int i
=0; i
< d_size
- str
.size(); ++i
) {
334 unsigned getSize() const {
338 const Integer
& getValue() const {
342 BitVector
setBit(uint32_t i
) const {
343 CheckArgument(i
< d_size
, i
);
344 Integer res
= d_value
.setBit(i
);
345 return BitVector(d_size
, res
);
348 bool isBitSet(uint32_t i
) const {
349 CheckArgument(i
< d_size
, i
);
350 return d_value
.isBitSet(i
);
354 * Return Integer corresponding to two's complement interpretation of bv.
356 Integer
toSignedInt() const {
357 unsigned size
= d_size
;
358 Integer sign_bit
= d_value
.extractBitRange(1,size
-1);
359 Integer val
= d_value
.extractBitRange(size
-1, 0);
360 Integer res
= Integer(-1) * sign_bit
.multiplyByPow2(size
- 1) + val
;
365 * Return k if the integer is equal to 2^{k-1} and zero otherwise.
368 return d_value
.isPow2();
374 * - no overflows: 2^d_size < d_value
375 * - no negative numbers: d_value >= 0
380 };/* class BitVector */
384 inline BitVector::BitVector(const std::string
& num
, unsigned base
) {
385 CheckArgument(base
== 2 || base
== 16, base
);
390 d_size
= num
.size() * 4;
393 d_value
= Integer(num
, base
);
394 }/* BitVector::BitVector() */
398 * Hash function for the BitVector constants.
400 struct CVC4_PUBLIC BitVectorHashFunction
{
401 inline size_t operator()(const BitVector
& bv
) const {
404 };/* struct BitVectorHashFunction */
407 * The structure representing the extraction operation for bit-vectors. The
408 * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
409 * by taking the bits at indices <code>high ... low</code>
411 struct CVC4_PUBLIC BitVectorExtract
{
412 /** The high bit of the range for this extract */
414 /** The low bit of the range for this extract */
417 BitVectorExtract(unsigned high
, unsigned low
)
418 : high(high
), low(low
) {}
420 bool operator == (const BitVectorExtract
& extract
) const {
421 return high
== extract
.high
&& low
== extract
.low
;
423 };/* struct BitVectorExtract */
426 * Hash function for the BitVectorExtract objects.
428 struct CVC4_PUBLIC BitVectorExtractHashFunction
{
429 size_t operator()(const BitVectorExtract
& extract
) const {
430 size_t hash
= extract
.low
;
431 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
434 };/* struct BitVectorExtractHashFunction */
438 * The structure representing the extraction of one Boolean bit.
440 struct CVC4_PUBLIC BitVectorBitOf
{
441 /** The index of the bit */
443 BitVectorBitOf(unsigned i
)
446 bool operator == (const BitVectorBitOf
& other
) const {
447 return bitIndex
== other
.bitIndex
;
449 };/* struct BitVectorBitOf */
452 * Hash function for the BitVectorBitOf objects.
454 struct CVC4_PUBLIC BitVectorBitOfHashFunction
{
455 size_t operator()(const BitVectorBitOf
& b
) const {
458 };/* struct BitVectorBitOfHashFunction */
462 struct CVC4_PUBLIC BitVectorSize
{
464 BitVectorSize(unsigned size
)
466 operator unsigned () const { return size
; }
467 };/* struct BitVectorSize */
469 struct CVC4_PUBLIC BitVectorRepeat
{
470 unsigned repeatAmount
;
471 BitVectorRepeat(unsigned repeatAmount
)
472 : repeatAmount(repeatAmount
) {}
473 operator unsigned () const { return repeatAmount
; }
474 };/* struct BitVectorRepeat */
476 struct CVC4_PUBLIC BitVectorZeroExtend
{
477 unsigned zeroExtendAmount
;
478 BitVectorZeroExtend(unsigned zeroExtendAmount
)
479 : zeroExtendAmount(zeroExtendAmount
) {}
480 operator unsigned () const { return zeroExtendAmount
; }
481 };/* struct BitVectorZeroExtend */
483 struct CVC4_PUBLIC BitVectorSignExtend
{
484 unsigned signExtendAmount
;
485 BitVectorSignExtend(unsigned signExtendAmount
)
486 : signExtendAmount(signExtendAmount
) {}
487 operator unsigned () const { return signExtendAmount
; }
488 };/* struct BitVectorSignExtend */
490 struct CVC4_PUBLIC BitVectorRotateLeft
{
491 unsigned rotateLeftAmount
;
492 BitVectorRotateLeft(unsigned rotateLeftAmount
)
493 : rotateLeftAmount(rotateLeftAmount
) {}
494 operator unsigned () const { return rotateLeftAmount
; }
495 };/* struct BitVectorRotateLeft */
497 struct CVC4_PUBLIC BitVectorRotateRight
{
498 unsigned rotateRightAmount
;
499 BitVectorRotateRight(unsigned rotateRightAmount
)
500 : rotateRightAmount(rotateRightAmount
) {}
501 operator unsigned () const { return rotateRightAmount
; }
502 };/* struct BitVectorRotateRight */
504 struct CVC4_PUBLIC IntToBitVector
{
506 IntToBitVector(unsigned size
)
508 operator unsigned () const { return size
; }
509 };/* struct IntToBitVector */
511 template <typename T
>
512 struct CVC4_PUBLIC UnsignedHashFunction
{
513 inline size_t operator()(const T
& x
) const {
516 };/* struct UnsignedHashFunction */
518 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) CVC4_PUBLIC
;
519 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) {
520 return os
<< bv
.toString();
523 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) CVC4_PUBLIC
;
524 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) {
525 return os
<< "[" << bv
.high
<< ":" << bv
.low
<< "]";
528 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) CVC4_PUBLIC
;
529 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) {
530 return os
<< "[" << bv
.bitIndex
<< "]";
533 inline std::ostream
& operator <<(std::ostream
& os
, const IntToBitVector
& bv
) CVC4_PUBLIC
;
534 inline std::ostream
& operator <<(std::ostream
& os
, const IntToBitVector
& bv
) {
535 return os
<< "[" << bv
.size
<< "]";
538 }/* CVC4 namespace */
540 #endif /* __CVC4__BITVECTOR_H */