1 /********************* */
4 ** Original author: dejan
5 ** Major contributors: cconway, mdeters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief [[ Add one-line brief description here ]]
16 ** [[ Add lengthier description here ]]
17 ** \todo document this file
20 #include "cvc4_public.h"
22 #ifndef __CVC4__BITVECTOR_H
23 #define __CVC4__BITVECTOR_H
26 #include "util/Assert.h"
27 #include "util/integer.h"
31 class CVC4_PUBLIC BitVector
{
37 * no overflows: 2^d_size < d_value
38 * no negative numbers: d_value >= 0
43 Integer
toSignedInt() const {
44 // returns Integer corresponding to two's complement interpretation of bv
45 unsigned size
= d_size
;
46 Integer sign_bit
= d_value
.extractBitRange(1,size
-1);
47 Integer val
= d_value
.extractBitRange(size
-1, 0);
48 Integer res
= Integer(-1) * sign_bit
.multiplyByPow2(size
- 1) + val
;
55 BitVector(unsigned size
, const Integer
& val
):
57 d_value(val
.modByPow2(size
))
60 BitVector(unsigned size
= 0)
61 : d_size(size
), d_value(0) {}
63 BitVector(unsigned size
, unsigned int z
)
64 : d_size(size
), d_value(z
) {
65 d_value
= d_value
.modByPow2(size
);
68 BitVector(unsigned size
, unsigned long int z
)
69 : d_size(size
), d_value(z
) {
70 d_value
= d_value
.modByPow2(size
);
73 BitVector(unsigned size
, const BitVector
& q
)
74 : d_size(size
), d_value(q
.d_value
) {}
76 BitVector(const std::string
& num
, unsigned base
= 2);
80 Integer
toInteger() const {
84 BitVector
& operator =(const BitVector
& x
) {
92 bool operator ==(const BitVector
& y
) const {
93 if (d_size
!= y
.d_size
) return false;
94 return d_value
== y
.d_value
;
97 bool operator !=(const BitVector
& y
) const {
98 if (d_size
!= y
.d_size
) return true;
99 return d_value
!= y
.d_value
;
102 BitVector
equals(const BitVector
& y
) const {
103 Assert(d_size
== y
.d_size
);
104 return d_value
== y
.d_value
;
107 BitVector
concat (const BitVector
& other
) const {
108 return BitVector(d_size
+ other
.d_size
, (d_value
.multiplyByPow2(other
.d_size
)) + other
.d_value
);
111 BitVector
extract(unsigned high
, unsigned low
) const {
112 return BitVector(high
- low
+ 1, d_value
.extractBitRange(high
- low
+ 1, low
));
116 Bitwise operations on BitVectors
120 BitVector
operator ^(const BitVector
& y
) const {
121 Assert (d_size
== y
.d_size
);
122 return BitVector(d_size
, d_value
.bitwiseXor(y
.d_value
));
126 BitVector
operator |(const BitVector
& y
) const {
127 Assert (d_size
== y
.d_size
);
128 return BitVector(d_size
, d_value
.bitwiseOr(y
.d_value
));
132 BitVector
operator &(const BitVector
& y
) const {
133 Assert (d_size
== y
.d_size
);
134 return BitVector(d_size
, d_value
.bitwiseAnd(y
.d_value
));
138 BitVector
operator ~() const {
139 return BitVector(d_size
, d_value
.bitwiseNot());
143 Arithmetic operations on BitVectors
147 bool operator <(const BitVector
& y
) const {
148 return d_value
< y
.d_value
;
151 bool operator >(const BitVector
& y
) const {
152 return d_value
> y
.d_value
;
155 bool operator <=(const BitVector
& y
) const {
156 return d_value
<= y
.d_value
;
159 bool operator >=(const BitVector
& y
) const {
160 return d_value
>= y
.d_value
;
164 BitVector
operator +(const BitVector
& y
) const {
165 Assert (d_size
== y
.d_size
);
166 Integer sum
= d_value
+ y
.d_value
;
167 return BitVector(d_size
, sum
);
170 BitVector
operator -(const BitVector
& y
) const {
171 Assert (d_size
== y
.d_size
);
172 // to maintain the invariant that we are only adding BitVectors of the
174 BitVector
one(d_size
, Integer(1));
175 return *this + ~y
+ one
;
178 BitVector
operator -() const {
179 BitVector
one(d_size
, Integer(1));
180 return ~(*this) + one
;
183 BitVector
operator *(const BitVector
& y
) const {
184 Assert (d_size
== y
.d_size
);
185 Integer prod
= d_value
* y
.d_value
;
186 return BitVector(d_size
, prod
);
189 BitVector
unsignedDiv (const BitVector
& y
) const {
190 Assert (d_size
== y
.d_size
);
191 // TODO: decide whether we really want these semantics
192 if (y
.d_value
== 0) {
193 return BitVector(d_size
, Integer(0));
195 Assert (d_value
>= 0 && y
.d_value
> 0);
196 return BitVector(d_size
, d_value
.floorDivideQuotient(y
.d_value
));
199 BitVector
unsignedRem(const BitVector
& y
) const {
200 Assert (d_size
== y
.d_size
);
201 // TODO: decide whether we really want these semantics
202 if (y
.d_value
== 0) {
203 return BitVector(d_size
, Integer(0));
205 Assert (d_value
>= 0 && y
.d_value
> 0);
206 return BitVector(d_size
, d_value
.floorDivideRemainder(y
.d_value
));
210 bool signedLessThan(const BitVector
& y
) const {
211 Assert(d_size
== y
.d_size
);
212 Assert(d_value
>= 0 && y
.d_value
>= 0);
213 Integer a
= (*this).toSignedInt();
214 Integer b
= y
.toSignedInt();
219 bool unsignedLessThan(const BitVector
& y
) const {
220 Assert(d_size
== y
.d_size
);
221 Assert(d_value
>= 0 && y
.d_value
>= 0);
222 return d_value
< y
.d_value
;
225 bool signedLessThanEq(const BitVector
& y
) const {
226 Assert(d_size
== y
.d_size
);
227 Assert(d_value
>= 0 && y
.d_value
>= 0);
228 Integer a
= (*this).toSignedInt();
229 Integer b
= y
.toSignedInt();
234 bool unsignedLessThanEq(const BitVector
& y
) const {
235 Assert(d_size
== y
.d_size
);
236 Assert(d_value
>= 0 && y
.d_value
>= 0);
237 return d_value
<= y
.d_value
;
245 BitVector
zeroExtend(unsigned amount
) const {
246 return BitVector(d_size
+ amount
, d_value
);
249 BitVector
signExtend(unsigned amount
) const {
250 Integer sign_bit
= d_value
.extractBitRange(1, d_size
-1);
251 if(sign_bit
== Integer(0)) {
252 return BitVector(d_size
+ amount
, d_value
);
254 Integer val
= d_value
.oneExtend(d_size
, amount
);
255 return BitVector(d_size
+ amount
, val
);
263 BitVector
leftShift(const BitVector
& y
) const {
264 if (y
.d_value
> Integer(d_size
)) {
265 return BitVector(d_size
, Integer(0));
267 if (y
.d_value
== 0) {
271 // making sure we don't lose information casting
272 Assert(y
.d_value
< Integer(1).multiplyByPow2(32));
273 uint32_t amount
= y
.d_value
.toUnsignedInt();
274 Integer res
= d_value
.multiplyByPow2(amount
);
275 return BitVector(d_size
, res
);
278 BitVector
logicalRightShift(const BitVector
& y
) const {
279 if(y
.d_value
> Integer(d_size
)) {
280 return BitVector(d_size
, Integer(0));
283 // making sure we don't lose information casting
284 Assert(y
.d_value
< Integer(1).multiplyByPow2(32));
285 uint32_t amount
= y
.d_value
.toUnsignedInt();
286 Integer res
= d_value
.divByPow2(amount
);
287 return BitVector(d_size
, res
);
290 BitVector
arithRightShift(const BitVector
& y
) const {
291 Integer sign_bit
= d_value
.extractBitRange(1, d_size
- 1);
292 if(y
.d_value
> Integer(d_size
)) {
293 if(sign_bit
== Integer(0)) {
294 return BitVector(d_size
, Integer(0));
296 return BitVector(d_size
, Integer(d_size
).multiplyByPow2(d_size
) -1 );
300 if (y
.d_value
== 0) {
304 // making sure we don't lose information casting
305 Assert(y
.d_value
< Integer(1).multiplyByPow2(32));
307 uint32_t amount
= y
.d_value
.toUnsignedInt();
308 Integer rest
= d_value
.divByPow2(amount
);
310 if(sign_bit
== Integer(0)) {
311 return BitVector(d_size
, rest
);
313 Integer res
= rest
.oneExtend(d_size
- amount
, amount
);
314 return BitVector(d_size
, res
);
319 Convenience functions
322 size_t hash() const {
323 return d_value
.hash() + d_size
;
326 std::string
toString(unsigned int base
= 2) const {
327 std::string str
= d_value
.toString(base
);
328 if( base
== 2 && d_size
> str
.size() ) {
330 for( unsigned int i
=0; i
< d_size
- str
.size(); ++i
) {
339 unsigned getSize() const {
343 const Integer
& getValue() const {
348 Returns k is the integer is equal to 2^{k-1} and zero
350 @return k if the integer is equal to 2^{k-1} and zero otherwise
353 return d_value
.isPow2();
356 };/* class BitVector */
360 inline BitVector::BitVector(const std::string
& num
, unsigned base
) {
361 AlwaysAssert( base
== 2 || base
== 16 );
365 } else if( base
== 16 ) {
366 d_size
= num
.size() * 4;
368 Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
371 d_value
= Integer(num
,base
);
372 }/* BitVector::BitVector() */
376 * Hash function for the BitVector constants.
378 struct CVC4_PUBLIC BitVectorHashFunction
{
379 inline size_t operator()(const BitVector
& bv
) const {
382 };/* struct BitVectorHashFunction */
385 * The structure representing the extraction operation for bit-vectors. The
386 * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
387 * by taking the bits at indices <code>high ... low</code>
389 struct CVC4_PUBLIC BitVectorExtract
{
390 /** The high bit of the range for this extract */
392 /** The low bit of the range for this extract */
395 BitVectorExtract(unsigned high
, unsigned low
)
396 : high(high
), low(low
) {}
398 bool operator == (const BitVectorExtract
& extract
) const {
399 return high
== extract
.high
&& low
== extract
.low
;
401 };/* struct BitVectorExtract */
404 * Hash function for the BitVectorExtract objects.
406 struct CVC4_PUBLIC BitVectorExtractHashFunction
{
407 size_t operator()(const BitVectorExtract
& extract
) const {
408 size_t hash
= extract
.low
;
409 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
412 };/* struct BitVectorExtractHashFunction */
416 * The structure representing the extraction of one Boolean bit.
418 struct CVC4_PUBLIC BitVectorBitOf
{
419 /** The index of the bit */
421 BitVectorBitOf(unsigned i
)
424 bool operator == (const BitVectorBitOf
& other
) const {
425 return bitIndex
== other
.bitIndex
;
427 };/* struct BitVectorBitOf */
430 * Hash function for the BitVectorBitOf objects.
432 struct CVC4_PUBLIC BitVectorBitOfHashFunction
{
433 size_t operator()(const BitVectorBitOf
& b
) const {
436 };/* struct BitVectorBitOfHashFunction */
440 struct CVC4_PUBLIC BitVectorSize
{
442 BitVectorSize(unsigned size
)
444 operator unsigned () const { return size
; }
445 };/* struct BitVectorSize */
447 struct CVC4_PUBLIC BitVectorRepeat
{
448 unsigned repeatAmount
;
449 BitVectorRepeat(unsigned repeatAmount
)
450 : repeatAmount(repeatAmount
) {}
451 operator unsigned () const { return repeatAmount
; }
452 };/* struct BitVectorRepeat */
454 struct CVC4_PUBLIC BitVectorZeroExtend
{
455 unsigned zeroExtendAmount
;
456 BitVectorZeroExtend(unsigned zeroExtendAmount
)
457 : zeroExtendAmount(zeroExtendAmount
) {}
458 operator unsigned () const { return zeroExtendAmount
; }
459 };/* struct BitVectorZeroExtend */
461 struct CVC4_PUBLIC BitVectorSignExtend
{
462 unsigned signExtendAmount
;
463 BitVectorSignExtend(unsigned signExtendAmount
)
464 : signExtendAmount(signExtendAmount
) {}
465 operator unsigned () const { return signExtendAmount
; }
466 };/* struct BitVectorSignExtend */
468 struct CVC4_PUBLIC BitVectorRotateLeft
{
469 unsigned rotateLeftAmount
;
470 BitVectorRotateLeft(unsigned rotateLeftAmount
)
471 : rotateLeftAmount(rotateLeftAmount
) {}
472 operator unsigned () const { return rotateLeftAmount
; }
473 };/* struct BitVectorRotateLeft */
475 struct CVC4_PUBLIC BitVectorRotateRight
{
476 unsigned rotateRightAmount
;
477 BitVectorRotateRight(unsigned rotateRightAmount
)
478 : rotateRightAmount(rotateRightAmount
) {}
479 operator unsigned () const { return rotateRightAmount
; }
480 };/* struct BitVectorRotateRight */
482 template <typename T
>
483 struct CVC4_PUBLIC UnsignedHashFunction
{
484 inline size_t operator()(const T
& x
) const {
487 };/* struct UnsignedHashFunction */
489 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) CVC4_PUBLIC
;
490 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) {
491 return os
<< bv
.toString();
494 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) CVC4_PUBLIC
;
495 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) {
496 return os
<< "[" << bv
.high
<< ":" << bv
.low
<< "]";
499 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) CVC4_PUBLIC
;
500 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorBitOf
& bv
) {
501 return os
<< "[" << bv
.bitIndex
<< "]";
504 }/* CVC4 namespace */
506 #endif /* __CVC4__BITVECTOR_H */