1 /********************* */
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Liana Hadarean, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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 A fixed-size bit-vector.
14 ** A fixed-size bit-vector, implemented as a wrapper around Integer.
16 ** \todo document this file
19 #include "cvc4_public.h"
21 #ifndef __CVC4__BITVECTOR_H
22 #define __CVC4__BITVECTOR_H
26 #include "base/exception.h"
27 #include "util/integer.h"
31 class CVC4_PUBLIC BitVector
{
34 BitVector(unsigned size
, const Integer
& val
):
36 d_value(val
.modByPow2(size
))
39 BitVector(unsigned size
= 0)
40 : d_size(size
), d_value(0) {}
42 BitVector(unsigned size
, unsigned int z
)
43 : d_size(size
), d_value(z
) {
44 d_value
= d_value
.modByPow2(size
);
47 BitVector(unsigned size
, unsigned long int z
)
48 : d_size(size
), d_value(z
) {
49 d_value
= d_value
.modByPow2(size
);
52 BitVector(unsigned size
, const BitVector
& q
)
53 : d_size(size
), d_value(q
.d_value
) {}
55 BitVector(const std::string
& num
, unsigned base
= 2)
57 CheckArgument(base
== 2 || base
== 16, base
);
58 d_size
= base
== 2 ? num
.size() : num
.size() * 4;
59 d_value
= Integer(num
, base
);
64 BitVector
& operator=(const BitVector
& x
)
66 if (this == &x
) return *this;
72 unsigned getSize() const
77 const Integer
& getValue() const
82 Integer
toInteger() const
88 * Return Integer corresponding to two's complement interpretation of bv.
90 Integer
toSignedInteger() const
92 unsigned size
= d_size
;
93 Integer sign_bit
= d_value
.extractBitRange(1, size
- 1);
94 Integer val
= d_value
.extractBitRange(size
- 1, 0);
95 Integer res
= Integer(-1) * sign_bit
.multiplyByPow2(size
- 1) + val
;
101 return d_value
.hash() + d_size
;
104 std::string
toString(unsigned int base
= 2) const
106 std::string str
= d_value
.toString(base
);
107 if (base
== 2 && d_size
> str
.size())
110 for (unsigned int i
= 0; i
< d_size
- str
.size(); ++i
)
122 BitVector
setBit(uint32_t i
) const
124 CheckArgument(i
< d_size
, i
);
125 Integer res
= d_value
.setBit(i
);
126 return BitVector(d_size
, res
);
129 bool isBitSet(uint32_t i
) const
131 CheckArgument(i
< d_size
, i
);
132 return d_value
.isBitSet(i
);
137 * Return k if the integer is equal to 2^{k-1} and zero otherwise.
140 return d_value
.isPow2();
143 /* -----------------------------------------------------------------------
145 * ----------------------------------------------------------------------- */
147 /* String Operations ----------------------------------------------------- */
149 BitVector
concat (const BitVector
& other
) const {
150 return BitVector(d_size
+ other
.d_size
, (d_value
.multiplyByPow2(other
.d_size
)) + other
.d_value
);
153 BitVector
extract(unsigned high
, unsigned low
) const {
154 return BitVector(high
- low
+ 1, d_value
.extractBitRange(high
- low
+ 1, low
));
157 /* (Dis)Equality --------------------------------------------------------- */
159 bool operator ==(const BitVector
& y
) const {
160 if (d_size
!= y
.d_size
) return false;
161 return d_value
== y
.d_value
;
164 bool operator !=(const BitVector
& y
) const {
165 if (d_size
!= y
.d_size
) return true;
166 return d_value
!= y
.d_value
;
169 /* Unsigned Inequality --------------------------------------------------- */
171 bool operator <(const BitVector
& y
) const {
172 return d_value
< y
.d_value
;
175 bool unsignedLessThan(const BitVector
& y
) const {
176 CheckArgument(d_size
== y
.d_size
, y
);
177 CheckArgument(d_value
>= 0, this);
178 CheckArgument(y
.d_value
>= 0, y
);
179 return d_value
< y
.d_value
;
182 bool operator <=(const BitVector
& y
) const {
183 return d_value
<= y
.d_value
;
186 bool unsignedLessThanEq(const BitVector
& y
) const {
187 CheckArgument(d_size
== y
.d_size
, this);
188 CheckArgument(d_value
>= 0, this);
189 CheckArgument(y
.d_value
>= 0, y
);
190 return d_value
<= y
.d_value
;
193 bool operator >(const BitVector
& y
) const {
194 return d_value
> y
.d_value
;
197 bool operator >=(const BitVector
& y
) const {
198 return d_value
>= y
.d_value
;
201 /* Signed Inequality ----------------------------------------------------- */
203 bool signedLessThan(const BitVector
& y
) const {
204 CheckArgument(d_size
== y
.d_size
, y
);
205 CheckArgument(d_value
>= 0, this);
206 CheckArgument(y
.d_value
>= 0, y
);
207 Integer a
= (*this).toSignedInteger();
208 Integer b
= y
.toSignedInteger();
213 bool signedLessThanEq(const BitVector
& y
) const {
214 CheckArgument(d_size
== y
.d_size
, y
);
215 CheckArgument(d_value
>= 0, this);
216 CheckArgument(y
.d_value
>= 0, y
);
217 Integer a
= (*this).toSignedInteger();
218 Integer b
= y
.toSignedInteger();
223 /* Bit-wise operations --------------------------------------------------- */
226 BitVector
operator ^(const BitVector
& y
) const {
227 CheckArgument(d_size
== y
.d_size
, y
);
228 return BitVector(d_size
, d_value
.bitwiseXor(y
.d_value
));
232 BitVector
operator |(const BitVector
& y
) const {
233 CheckArgument(d_size
== y
.d_size
, y
);
234 return BitVector(d_size
, d_value
.bitwiseOr(y
.d_value
));
238 BitVector
operator &(const BitVector
& y
) const {
239 CheckArgument(d_size
== y
.d_size
, y
);
240 return BitVector(d_size
, d_value
.bitwiseAnd(y
.d_value
));
244 BitVector
operator ~() const {
245 return BitVector(d_size
, d_value
.bitwiseNot());
249 /* Arithmetic operations ------------------------------------------------- */
251 BitVector
operator +(const BitVector
& y
) const {
252 CheckArgument(d_size
== y
.d_size
, y
);
253 Integer sum
= d_value
+ y
.d_value
;
254 return BitVector(d_size
, sum
);
257 BitVector
operator -(const BitVector
& y
) const {
258 CheckArgument(d_size
== y
.d_size
, y
);
259 // to maintain the invariant that we are only adding BitVectors of the
261 BitVector
one(d_size
, Integer(1));
262 return *this + ~y
+ one
;
265 BitVector
operator -() const {
266 BitVector
one(d_size
, Integer(1));
267 return ~(*this) + one
;
270 BitVector
operator *(const BitVector
& y
) const {
271 CheckArgument(d_size
== y
.d_size
, y
);
272 Integer prod
= d_value
* y
.d_value
;
273 return BitVector(d_size
, prod
);
277 * Total division function.
278 * Returns 2^d_size-1 (signed: -1) when the denominator is zero
279 * (d_value / 0 = 2^d_size - 1).
281 BitVector
unsignedDivTotal (const BitVector
& y
) const {
283 CheckArgument(d_size
== y
.d_size
, y
);
284 if (y
.d_value
== 0) {
285 // under division by zero return -1
286 return BitVector(d_size
, Integer(1).oneExtend(1, d_size
- 1));
288 CheckArgument(d_value
>= 0, this);
289 CheckArgument(y
.d_value
> 0, y
);
290 return BitVector(d_size
, d_value
.floorDivideQuotient(y
.d_value
));
294 * Total remainder function.
295 * Returns d_value when the denominator is zero (d_value % 0 = d_value).
297 BitVector
unsignedRemTotal(const BitVector
& y
) const {
298 CheckArgument(d_size
== y
.d_size
, y
);
299 if (y
.d_value
== 0) {
300 return BitVector(d_size
, d_value
);
302 CheckArgument(d_value
>= 0, this);
303 CheckArgument(y
.d_value
> 0, y
);
304 return BitVector(d_size
, d_value
.floorDivideRemainder(y
.d_value
));
308 /* Extend operations ----------------------------------------------------- */
310 BitVector
zeroExtend(unsigned amount
) const {
311 return BitVector(d_size
+ amount
, d_value
);
314 BitVector
signExtend(unsigned amount
) const {
315 Integer sign_bit
= d_value
.extractBitRange(1, d_size
-1);
316 if(sign_bit
== Integer(0)) {
317 return BitVector(d_size
+ amount
, d_value
);
319 Integer val
= d_value
.oneExtend(d_size
, amount
);
320 return BitVector(d_size
+ amount
, val
);
324 /* Shift operations ------------------------------------------------------ */
326 BitVector
leftShift(const BitVector
& y
) const {
327 if (y
.d_value
> Integer(d_size
)) {
328 return BitVector(d_size
, Integer(0));
330 if (y
.d_value
== 0) {
333 // making sure we don't lose information casting
334 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
335 uint32_t amount
= y
.d_value
.toUnsignedInt();
336 Integer res
= d_value
.multiplyByPow2(amount
);
337 return BitVector(d_size
, res
);
340 BitVector
logicalRightShift(const BitVector
& y
) const {
341 if(y
.d_value
> Integer(d_size
)) {
342 return BitVector(d_size
, Integer(0));
344 // making sure we don't lose information casting
345 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
346 uint32_t amount
= y
.d_value
.toUnsignedInt();
347 Integer res
= d_value
.divByPow2(amount
);
348 return BitVector(d_size
, res
);
351 BitVector
arithRightShift(const BitVector
& y
) const {
352 Integer sign_bit
= d_value
.extractBitRange(1, d_size
- 1);
353 if(y
.d_value
> Integer(d_size
)) {
354 if(sign_bit
== Integer(0)) {
355 return BitVector(d_size
, Integer(0));
357 return BitVector(d_size
, Integer(d_size
).multiplyByPow2(d_size
) -1 );
361 if (y
.d_value
== 0) {
365 // making sure we don't lose information casting
366 CheckArgument(y
.d_value
< Integer(1).multiplyByPow2(32), y
);
368 uint32_t amount
= y
.d_value
.toUnsignedInt();
369 Integer rest
= d_value
.divByPow2(amount
);
371 if(sign_bit
== Integer(0)) {
372 return BitVector(d_size
, rest
);
374 Integer res
= rest
.oneExtend(d_size
- amount
, amount
);
375 return BitVector(d_size
, res
);
378 /* -----------------------------------------------------------------------
380 * ----------------------------------------------------------------------- */
382 /* Create bit-vector of ones of given size. */
383 static BitVector
mkOnes(unsigned size
)
385 CheckArgument(size
> 0, size
);
386 return BitVector(1, Integer(1)).signExtend(size
- 1);
389 /* Create bit-vector representing the minimum signed value of given size. */
390 static BitVector
mkMinSigned(unsigned size
)
392 CheckArgument(size
> 0, size
);
393 return BitVector(size
).setBit(size
- 1);
396 /* Create bit-vector representing the maximum signed value of given size. */
397 static BitVector
mkMaxSigned(unsigned size
)
399 CheckArgument(size
> 0, size
);
400 return ~BitVector::mkMinSigned(size
);
407 * - no overflows: 2^d_size < d_value
408 * - no negative numbers: d_value >= 0
414 };/* class BitVector */
418 /* -----------------------------------------------------------------------
420 * ----------------------------------------------------------------------- */
423 * The structure representing the extraction operation for bit-vectors. The
424 * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
425 * by taking the bits at indices <code>high ... low</code>
427 struct CVC4_PUBLIC BitVectorExtract
429 /** The high bit of the range for this extract */
431 /** The low bit of the range for this extract */
434 BitVectorExtract(unsigned high
, unsigned low
) : high(high
), low(low
) {}
436 bool operator==(const BitVectorExtract
& extract
) const
438 return high
== extract
.high
&& low
== extract
.low
;
440 }; /* struct BitVectorExtract */
443 * The structure representing the extraction of one Boolean bit.
445 struct CVC4_PUBLIC BitVectorBitOf
{
446 /** The index of the bit */
448 BitVectorBitOf(unsigned i
)
451 bool operator == (const BitVectorBitOf
& other
) const {
452 return bitIndex
== other
.bitIndex
;
454 };/* struct BitVectorBitOf */
456 struct CVC4_PUBLIC BitVectorSize
{
458 BitVectorSize(unsigned size
)
460 operator unsigned () const { return size
; }
461 };/* struct BitVectorSize */
463 struct CVC4_PUBLIC BitVectorRepeat
{
464 unsigned repeatAmount
;
465 BitVectorRepeat(unsigned repeatAmount
)
466 : repeatAmount(repeatAmount
) {}
467 operator unsigned () const { return repeatAmount
; }
468 };/* struct BitVectorRepeat */
470 struct CVC4_PUBLIC BitVectorZeroExtend
{
471 unsigned zeroExtendAmount
;
472 BitVectorZeroExtend(unsigned zeroExtendAmount
)
473 : zeroExtendAmount(zeroExtendAmount
) {}
474 operator unsigned () const { return zeroExtendAmount
; }
475 };/* struct BitVectorZeroExtend */
477 struct CVC4_PUBLIC BitVectorSignExtend
{
478 unsigned signExtendAmount
;
479 BitVectorSignExtend(unsigned signExtendAmount
)
480 : signExtendAmount(signExtendAmount
) {}
481 operator unsigned () const { return signExtendAmount
; }
482 };/* struct BitVectorSignExtend */
484 struct CVC4_PUBLIC BitVectorRotateLeft
{
485 unsigned rotateLeftAmount
;
486 BitVectorRotateLeft(unsigned rotateLeftAmount
)
487 : rotateLeftAmount(rotateLeftAmount
) {}
488 operator unsigned () const { return rotateLeftAmount
; }
489 };/* struct BitVectorRotateLeft */
491 struct CVC4_PUBLIC BitVectorRotateRight
{
492 unsigned rotateRightAmount
;
493 BitVectorRotateRight(unsigned rotateRightAmount
)
494 : rotateRightAmount(rotateRightAmount
) {}
495 operator unsigned () const { return rotateRightAmount
; }
496 };/* struct BitVectorRotateRight */
498 struct CVC4_PUBLIC IntToBitVector
{
500 IntToBitVector(unsigned size
)
502 operator unsigned () const { return size
; }
503 };/* struct IntToBitVector */
506 /* -----------------------------------------------------------------------
507 ** Hash Function structs
508 * ----------------------------------------------------------------------- */
511 * Hash function for the BitVector constants.
513 struct CVC4_PUBLIC BitVectorHashFunction
{
514 inline size_t operator()(const BitVector
& bv
) const {
517 };/* struct BitVectorHashFunction */
520 * Hash function for the BitVectorExtract objects.
522 struct CVC4_PUBLIC BitVectorExtractHashFunction
{
523 size_t operator()(const BitVectorExtract
& extract
) const {
524 size_t hash
= extract
.low
;
525 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
528 };/* struct BitVectorExtractHashFunction */
531 * Hash function for the BitVectorBitOf objects.
533 struct CVC4_PUBLIC BitVectorBitOfHashFunction
{
534 size_t operator()(const BitVectorBitOf
& b
) const {
537 };/* struct BitVectorBitOfHashFunction */
539 template <typename T
>
540 struct CVC4_PUBLIC UnsignedHashFunction
{
541 inline size_t operator()(const T
& x
) const {
544 };/* struct UnsignedHashFunction */
547 /* -----------------------------------------------------------------------
549 * ----------------------------------------------------------------------- */
551 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) CVC4_PUBLIC
;
552 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) {
553 return os
<< bv
.toString();
556 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) CVC4_PUBLIC
;
557 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) {
558 return os
<< "[" << bv
.high
<< ":" << bv
.low
<< "]";
561 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) CVC4_PUBLIC
;
562 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) {
563 return os
<< "[" << bv
.bitIndex
<< "]";
566 inline std::ostream
& operator <<(std::ostream
& os
, const IntToBitVector
& bv
) CVC4_PUBLIC
;
567 inline std::ostream
& operator <<(std::ostream
& os
, const IntToBitVector
& bv
) {
568 return os
<< "[" << bv
.size
<< "]";
571 }/* CVC4 namespace */
573 #endif /* __CVC4__BITVECTOR_H */