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
) {}
42 BitVector
& operator =(const BitVector
& x
) {
49 bool operator ==(const BitVector
& y
) const {
50 if (d_size
!= y
.d_size
) return false;
51 return d_value
== y
.d_value
;
54 bool operator !=(const BitVector
& y
) const {
55 if (d_size
== y
.d_size
) return false;
56 return d_value
!= y
.d_value
;
59 BitVector
operator +(const BitVector
& y
) const {
60 return BitVector(std::max(d_size
, y
.d_size
), d_value
+ y
.d_value
);
63 BitVector
operator -(const BitVector
& y
) const {
64 return *this + ~y
+ 1;
67 BitVector
operator -() const {
71 BitVector
operator *(const BitVector
& y
) const {
72 return BitVector(d_size
, d_value
* y
.d_value
);
75 BitVector
operator ~() const {
76 return BitVector(d_size
, d_value
);
80 return gmpz_hash(d_value
.get_mpz_t());
83 std::string
toString(unsigned int base
= 2) const {
84 return d_value
.get_str(base
);
89 * Hash function for the BitVector constants.
91 struct BitVectorHashStrategy
{
92 static inline size_t hash(const BitVector
& bv
) {
98 * The structure representing the extraction operation for bit-vectors. The
99 * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
100 * by taking the bits at indices <code>high ... low</code>
102 struct BitVectorExtract
{
103 /** The high bit of the range for this extract */
105 /** The low bit of the range for this extract */
108 bool operator == (const BitVectorExtract
& extract
) const {
109 return high
== extract
.high
&& low
== extract
.low
;
114 * Hash function for the BitVectorExtract objects.
116 class BitVectorExtractHashStrategy
{
118 static size_t hash(const BitVectorExtract
& extract
) {
119 size_t hash
= extract
.low
;
120 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
126 * Hash function for the unsigned integers.
128 struct UnsignedHashStrategy
{
129 static inline size_t hash(unsigned x
) {
134 std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
);
135 std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
);
139 #endif /* __CVC4__BITVECTOR_H_ */