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
{
40 BitVector(unsigned size
, const Integer
& val
)
41 : d_size(size
), d_value(val
) {}
43 BitVector(unsigned size
= 0)
44 : d_size(size
), d_value(0) {}
46 BitVector(unsigned size
, unsigned int z
)
47 : d_size(size
), d_value(z
) {}
49 BitVector(unsigned size
, unsigned long int z
)
50 : d_size(size
), d_value(z
) {}
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);
59 BitVector
& operator =(const BitVector
& x
) {
67 bool operator ==(const BitVector
& y
) const {
68 if (d_size
!= y
.d_size
) return false;
69 return d_value
== y
.d_value
;
72 bool operator !=(const BitVector
& y
) const {
73 if (d_size
== y
.d_size
) return false;
74 return d_value
!= y
.d_value
;
77 BitVector
operator +(const BitVector
& y
) const {
78 return BitVector(std::max(d_size
, y
.d_size
), d_value
+ y
.d_value
);
81 BitVector
operator -(const BitVector
& y
) const {
82 return *this + ~y
+ 1;
85 BitVector
operator -() const {
89 BitVector
operator *(const BitVector
& y
) const {
90 return BitVector(d_size
, d_value
* y
.d_value
);
93 BitVector
operator ~() const {
94 //is this right? it looks like a no-op?
95 return BitVector(d_size
, d_value
);
98 BitVector
concat (const BitVector
& other
) const {
99 return BitVector(d_size
+ other
.d_size
, (d_value
.multiplyByPow2(other
.d_size
)) + other
.d_value
);
100 //return BitVector(d_size + other.d_size, (d_value * Integer(2).pow(other.d_size)) + other.d_value);
103 BitVector
extract(unsigned high
, unsigned low
) const {
104 return BitVector(high
- low
+ 1, d_value
.extractBitRange(high
- low
+ 1, low
));
105 //return BitVector(high - low + 1, (d_value % (Integer(2).pow(high + 1))) / Integer(2).pow(low));
108 size_t hash() const {
109 return d_value
.hash() + d_size
;
112 std::string
toString(unsigned int base
= 2) const {
113 std::string str
= d_value
.toString(base
);
114 if( base
== 2 && d_size
> str
.size() ) {
116 for( unsigned int i
=0; i
< d_size
- str
.size(); ++i
) {
125 unsigned getSize() const {
129 const Integer
& getValue() const {
132 };/* class BitVector */
134 inline BitVector::BitVector(const std::string
& num
, unsigned base
) {
135 AlwaysAssert( base
== 2 || base
== 16 );
139 // d_value = Integer(num,2);
141 for( string::const_iterator it = num.begin(); it != num.end(); ++it ) {
142 if( *it != '0' || *it != '1' ) {
143 IllegalArgument(num, "BitVector argument is not a binary string.");
145 z = (Integer(2) * z) + (*it == '1');
146 d_value = mpz_class(z.get_mpz());
149 } else if( base
== 16 ) {
150 d_size
= num
.size() * 4;
151 // // Use a stream to decode the hex string
153 // ss.setf(ios::hex, ios::basefield);
156 // d_value = mpz_class(z);
159 Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
162 d_value
= Integer(num
,base
);
163 }/* BitVector::BitVector() */
167 * Hash function for the BitVector constants.
169 struct CVC4_PUBLIC BitVectorHashStrategy
{
170 static inline size_t hash(const BitVector
& bv
) {
173 };/* struct BitVectorHashStrategy */
176 * The structure representing the extraction operation for bit-vectors. The
177 * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
178 * by taking the bits at indices <code>high ... low</code>
180 struct CVC4_PUBLIC BitVectorExtract
{
181 /** The high bit of the range for this extract */
183 /** The low bit of the range for this extract */
186 BitVectorExtract(unsigned high
, unsigned low
)
187 : high(high
), low(low
) {}
189 bool operator == (const BitVectorExtract
& extract
) const {
190 return high
== extract
.high
&& low
== extract
.low
;
192 };/* struct BitVectorExtract */
195 * Hash function for the BitVectorExtract objects.
197 class CVC4_PUBLIC BitVectorExtractHashStrategy
{
199 static size_t hash(const BitVectorExtract
& extract
) {
200 size_t hash
= extract
.low
;
201 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
204 };/* class BitVectorExtractHashStrategy */
206 struct CVC4_PUBLIC BitVectorSize
{
208 BitVectorSize(unsigned size
)
210 operator unsigned () const { return size
; }
211 };/* struct BitVectorSize */
213 struct CVC4_PUBLIC BitVectorRepeat
{
214 unsigned repeatAmount
;
215 BitVectorRepeat(unsigned repeatAmount
)
216 : repeatAmount(repeatAmount
) {}
217 operator unsigned () const { return repeatAmount
; }
218 };/* struct BitVectorRepeat */
220 struct CVC4_PUBLIC BitVectorZeroExtend
{
221 unsigned zeroExtendAmount
;
222 BitVectorZeroExtend(unsigned zeroExtendAmount
)
223 : zeroExtendAmount(zeroExtendAmount
) {}
224 operator unsigned () const { return zeroExtendAmount
; }
225 };/* struct BitVectorZeroExtend */
227 struct CVC4_PUBLIC BitVectorSignExtend
{
228 unsigned signExtendAmount
;
229 BitVectorSignExtend(unsigned signExtendAmount
)
230 : signExtendAmount(signExtendAmount
) {}
231 operator unsigned () const { return signExtendAmount
; }
232 };/* struct BitVectorSignExtend */
234 struct CVC4_PUBLIC BitVectorRotateLeft
{
235 unsigned rotateLeftAmount
;
236 BitVectorRotateLeft(unsigned rotateLeftAmount
)
237 : rotateLeftAmount(rotateLeftAmount
) {}
238 operator unsigned () const { return rotateLeftAmount
; }
239 };/* struct BitVectorRotateLeft */
241 struct CVC4_PUBLIC BitVectorRotateRight
{
242 unsigned rotateRightAmount
;
243 BitVectorRotateRight(unsigned rotateRightAmount
)
244 : rotateRightAmount(rotateRightAmount
) {}
245 operator unsigned () const { return rotateRightAmount
; }
246 };/* struct BitVectorRotateRight */
248 template <typename T
>
249 struct CVC4_PUBLIC UnsignedHashStrategy
{
250 static inline size_t hash(const T
& x
) {
253 };/* struct UnsignedHashStrategy */
255 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) CVC4_PUBLIC
;
256 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) {
257 return os
<< bv
.toString();
260 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) CVC4_PUBLIC
;
261 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) {
262 return os
<< "[" << bv
.high
<< ":" << bv
.low
<< "]";
265 }/* CVC4 namespace */
267 #endif /* __CVC4__BITVECTOR_H */