4 * Created on: Mar 31, 2010
8 #ifndef __CVC4__BITVECTOR_H_
9 #define __CVC4__BITVECTOR_H_
13 #include "util/gmp_util.h"
24 BitVector(unsigned size
, const mpz_class
& val
) : d_size(size
), d_value(val
) {}
28 BitVector(unsigned size
= 0)
29 : d_size(size
), d_value(0) {}
31 BitVector(unsigned size
, unsigned int z
)
32 : d_size(size
), d_value(z
) {}
34 BitVector(unsigned size
, unsigned long int z
)
35 : d_size(size
), d_value(z
) {}
37 BitVector(unsigned size
, const BitVector
& q
)
38 : d_size(size
), d_value(q
.d_value
) {}
40 BitVector(unsigned size
, const std::string
& num
, unsigned base
= 2)
41 : d_size(size
), d_value(0) {}
45 BitVector
& operator =(const BitVector
& x
) {
52 bool operator ==(const BitVector
& y
) const {
53 if (d_size
!= y
.d_size
) return false;
54 return d_value
== y
.d_value
;
57 bool operator !=(const BitVector
& y
) const {
58 if (d_size
== y
.d_size
) return false;
59 return d_value
!= y
.d_value
;
62 BitVector
operator +(const BitVector
& y
) const {
63 return BitVector(std::max(d_size
, y
.d_size
), d_value
+ y
.d_value
);
66 BitVector
operator -(const BitVector
& y
) const {
67 return *this + ~y
+ 1;
70 BitVector
operator -() const {
74 BitVector
operator *(const BitVector
& y
) const {
75 return BitVector(d_size
, d_value
* y
.d_value
);
78 BitVector
operator ~() const {
79 return BitVector(d_size
, d_value
);
83 return gmpz_hash(d_value
.get_mpz_t());
86 std::string
toString(unsigned int base
= 2) const {
87 return d_value
.get_str(base
);
90 unsigned getSize() const {
96 * Hash function for the BitVector constants.
98 struct BitVectorHashStrategy
{
99 static inline size_t hash(const BitVector
& bv
) {
105 * The structure representing the extraction operation for bit-vectors. The
106 * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
107 * by taking the bits at indices <code>high ... low</code>
109 struct BitVectorExtract
{
110 /** The high bit of the range for this extract */
112 /** The low bit of the range for this extract */
115 BitVectorExtract(unsigned high
, unsigned low
)
116 : high(high
), low(low
) {}
118 bool operator == (const BitVectorExtract
& extract
) const {
119 return high
== extract
.high
&& low
== extract
.low
;
124 * Hash function for the BitVectorExtract objects.
126 class BitVectorExtractHashStrategy
{
128 static size_t hash(const BitVectorExtract
& extract
) {
129 size_t hash
= extract
.low
;
130 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
135 struct BitVectorSize
{
137 BitVectorSize(unsigned size
)
139 operator unsigned () const { return size
; }
142 struct BitVectorRepeat
{
143 unsigned repeatAmount
;
144 BitVectorRepeat(unsigned repeatAmount
)
145 : repeatAmount(repeatAmount
) {}
146 operator unsigned () const { return repeatAmount
; }
149 struct BitVectorZeroExtend
{
150 unsigned zeroExtendAmount
;
151 BitVectorZeroExtend(unsigned zeroExtendAmount
)
152 : zeroExtendAmount(zeroExtendAmount
) {}
153 operator unsigned () const { return zeroExtendAmount
; }
156 struct BitVectorSignExtend
{
157 unsigned signExtendAmount
;
158 BitVectorSignExtend(unsigned signExtendAmount
)
159 : signExtendAmount(signExtendAmount
) {}
160 operator unsigned () const { return signExtendAmount
; }
163 struct BitVectorRotateLeft
{
164 unsigned rotateLeftAmount
;
165 BitVectorRotateLeft(unsigned rotateLeftAmount
)
166 : rotateLeftAmount(rotateLeftAmount
) {}
167 operator unsigned () const { return rotateLeftAmount
; }
170 struct BitVectorRotateRight
{
171 unsigned rotateRightAmount
;
172 BitVectorRotateRight(unsigned rotateRightAmount
)
173 : rotateRightAmount(rotateRightAmount
) {}
174 operator unsigned () const { return rotateRightAmount
; }
177 template <typename T
>
178 struct UnsignedHashStrategy
{
179 static inline size_t hash(const T
& x
) {
184 std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
);
185 std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
);
189 #endif /* __CVC4__BITVECTOR_H_ */