1 /********************* */
4 ** Original author: dejan
5 ** Major contributors: cconway
6 ** Minor contributors (to current version): mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 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"
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 return BitVector(d_size
, d_value
);
97 BitVector
concat (const BitVector
& other
) const {
98 return BitVector(d_size
+ other
.d_size
, (d_value
* Integer(2).pow(other
.d_size
)) + other
.d_value
);
101 BitVector
extract(unsigned high
, unsigned low
) {
102 return BitVector(high
- low
+ 1, (d_value
% (Integer(2).pow(high
+ 1))) / Integer(2).pow(low
));
105 size_t hash() const {
106 return d_value
.hash() + d_size
;
109 std::string
toString(unsigned int base
= 2) const {
110 std::string str
= d_value
.toString(base
);
111 if( base
== 2 && d_size
> str
.size() ) {
113 for( unsigned int i
=0; i
< d_size
- str
.size(); ++i
) {
122 unsigned getSize() const {
127 inline BitVector::BitVector(const std::string
& num
, unsigned base
) {
128 AlwaysAssert( base
== 2 || base
== 16 );
132 // d_value = Integer(num,2);
134 for( string::const_iterator it = num.begin(); it != num.end(); ++it ) {
135 if( *it != '0' || *it != '1' ) {
136 IllegalArgument(num, "BitVector argument is not a binary string.");
138 z = (Integer(2) * z) + (*it == '1');
139 d_value = mpz_class(z.get_mpz());
142 } else if( base
== 16 ) {
143 d_size
= num
.size() * 4;
144 // // Use a stream to decode the hex string
146 // ss.setf(ios::hex, ios::basefield);
149 // d_value = mpz_class(z);
152 Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
155 d_value
= Integer(num
,base
);
160 * Hash function for the BitVector constants.
162 struct BitVectorHashStrategy
{
163 static inline size_t hash(const BitVector
& bv
) {
169 * The structure representing the extraction operation for bit-vectors. The
170 * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
171 * by taking the bits at indices <code>high ... low</code>
173 struct BitVectorExtract
{
174 /** The high bit of the range for this extract */
176 /** The low bit of the range for this extract */
179 BitVectorExtract(unsigned high
, unsigned low
)
180 : high(high
), low(low
) {}
182 bool operator == (const BitVectorExtract
& extract
) const {
183 return high
== extract
.high
&& low
== extract
.low
;
188 * Hash function for the BitVectorExtract objects.
190 class BitVectorExtractHashStrategy
{
192 static size_t hash(const BitVectorExtract
& extract
) {
193 size_t hash
= extract
.low
;
194 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
199 struct BitVectorSize
{
201 BitVectorSize(unsigned size
)
203 operator unsigned () const { return size
; }
206 struct BitVectorRepeat
{
207 unsigned repeatAmount
;
208 BitVectorRepeat(unsigned repeatAmount
)
209 : repeatAmount(repeatAmount
) {}
210 operator unsigned () const { return repeatAmount
; }
213 struct BitVectorZeroExtend
{
214 unsigned zeroExtendAmount
;
215 BitVectorZeroExtend(unsigned zeroExtendAmount
)
216 : zeroExtendAmount(zeroExtendAmount
) {}
217 operator unsigned () const { return zeroExtendAmount
; }
220 struct BitVectorSignExtend
{
221 unsigned signExtendAmount
;
222 BitVectorSignExtend(unsigned signExtendAmount
)
223 : signExtendAmount(signExtendAmount
) {}
224 operator unsigned () const { return signExtendAmount
; }
227 struct BitVectorRotateLeft
{
228 unsigned rotateLeftAmount
;
229 BitVectorRotateLeft(unsigned rotateLeftAmount
)
230 : rotateLeftAmount(rotateLeftAmount
) {}
231 operator unsigned () const { return rotateLeftAmount
; }
234 struct BitVectorRotateRight
{
235 unsigned rotateRightAmount
;
236 BitVectorRotateRight(unsigned rotateRightAmount
)
237 : rotateRightAmount(rotateRightAmount
) {}
238 operator unsigned () const { return rotateRightAmount
; }
241 template <typename T
>
242 struct UnsignedHashStrategy
{
243 static inline size_t hash(const T
& x
) {
248 inline std::ostream
& operator <<(std::ostream
& os
, const BitVector
& bv
) {
249 return os
<< bv
.toString();
252 inline std::ostream
& operator <<(std::ostream
& os
, const BitVectorExtract
& bv
) {
253 return os
<< "[" << bv
.high
<< ":" << bv
.low
<< "]";
256 }/* CVC4 namespace */
258 #endif /* __CVC4__BITVECTOR_H */