cvc4-1.4
bitvector.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__BITVECTOR_H
21 #define __CVC4__BITVECTOR_H
22 
23 #include <iostream>
24 #include "util/exception.h"
25 #include "util/integer.h"
26 
27 namespace CVC4 {
28 
30 
31 private:
32 
33  /*
34  Class invariants:
35  * no overflows: 2^d_size < d_value
36  * no negative numbers: d_value >= 0
37  */
38  unsigned d_size;
39  Integer d_value;
40 
41  Integer toSignedInt() const {
42  // returns Integer corresponding to two's complement interpretation of bv
43  unsigned size = d_size;
44  Integer sign_bit = d_value.extractBitRange(1,size-1);
45  Integer val = d_value.extractBitRange(size-1, 0);
46  Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
47  return res;
48  }
49 
50 
51 public:
52 
53  BitVector(unsigned size, const Integer& val):
54  d_size(size),
55  d_value(val.modByPow2(size))
56  {}
57 
58  BitVector(unsigned size = 0)
59  : d_size(size), d_value(0) {}
60 
61  BitVector(unsigned size, unsigned int z)
62  : d_size(size), d_value(z) {
63  d_value = d_value.modByPow2(size);
64  }
65 
66  BitVector(unsigned size, unsigned long int z)
67  : d_size(size), d_value(z) {
68  d_value = d_value.modByPow2(size);
69  }
70 
71  BitVector(unsigned size, const BitVector& q)
72  : d_size(size), d_value(q.d_value) {}
73 
74  BitVector(const std::string& num, unsigned base = 2);
75 
77 
78  Integer toInteger() const {
79  return d_value;
80  }
81 
82  BitVector& operator =(const BitVector& x) {
83  if(this == &x)
84  return *this;
85  d_size = x.d_size;
86  d_value = x.d_value;
87  return *this;
88  }
89 
90  bool operator ==(const BitVector& y) const {
91  if (d_size != y.d_size) return false;
92  return d_value == y.d_value;
93  }
94 
95  bool operator !=(const BitVector& y) const {
96  if (d_size != y.d_size) return true;
97  return d_value != y.d_value;
98  }
99 
100  BitVector concat (const BitVector& other) const {
101  return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
102  }
103 
104  BitVector extract(unsigned high, unsigned low) const {
105  return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
106  }
107 
108  /*
109  Bitwise operations on BitVectors
110  */
111 
112  // xor
113  BitVector operator ^(const BitVector& y) const {
114  CheckArgument(d_size == y.d_size, y);
115  return BitVector(d_size, d_value.bitwiseXor(y.d_value));
116  }
117 
118  // or
119  BitVector operator |(const BitVector& y) const {
120  CheckArgument(d_size == y.d_size, y);
121  return BitVector(d_size, d_value.bitwiseOr(y.d_value));
122  }
123 
124  // and
125  BitVector operator &(const BitVector& y) const {
126  CheckArgument(d_size == y.d_size, y);
127  return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
128  }
129 
130  // not
131  BitVector operator ~() const {
132  return BitVector(d_size, d_value.bitwiseNot());
133  }
134 
135  /*
136  Arithmetic operations on BitVectors
137  */
138 
139 
140  bool operator <(const BitVector& y) const {
141  return d_value < y.d_value;
142  }
143 
144  bool operator >(const BitVector& y) const {
145  return d_value > y.d_value ;
146  }
147 
148  bool operator <=(const BitVector& y) const {
149  return d_value <= y.d_value;
150  }
151 
152  bool operator >=(const BitVector& y) const {
153  return d_value >= y.d_value ;
154  }
155 
156 
157  BitVector operator +(const BitVector& y) const {
158  CheckArgument(d_size == y.d_size, y);
159  Integer sum = d_value + y.d_value;
160  return BitVector(d_size, sum);
161  }
162 
163  BitVector operator -(const BitVector& y) const {
164  CheckArgument(d_size == y.d_size, y);
165  // to maintain the invariant that we are only adding BitVectors of the
166  // same size
167  BitVector one(d_size, Integer(1));
168  return *this + ~y + one;
169  }
170 
171  BitVector operator -() const {
172  BitVector one(d_size, Integer(1));
173  return ~(*this) + one;
174  }
175 
176  BitVector operator *(const BitVector& y) const {
177  CheckArgument(d_size == y.d_size, y);
178  Integer prod = d_value * y.d_value;
179  return BitVector(d_size, prod);
180  }
181 
182  BitVector setBit(uint32_t i) const {
183  CheckArgument(i < d_size, i);
184  Integer res = d_value.setBit(i);
185  return BitVector(d_size, res);
186  }
187 
188  bool isBitSet(uint32_t i) const {
189  CheckArgument(i < d_size, i);
190  return d_value.isBitSet(i);
191  }
192 
197 
198  CheckArgument(d_size == y.d_size, y);
199  if (y.d_value == 0) {
200  // under division by zero return -1
201  return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
202  }
203  CheckArgument(d_value >= 0, this);
204  CheckArgument(y.d_value > 0, y);
205  return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
206  }
207 
212  CheckArgument(d_size == y.d_size, y);
213  if (y.d_value == 0) {
214  return BitVector(d_size, d_value);
215  }
216  CheckArgument(d_value >= 0, this);
217  CheckArgument(y.d_value > 0, y);
218  return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
219  }
220 
221 
222  bool signedLessThan(const BitVector& y) const {
223  CheckArgument(d_size == y.d_size, y);
224  CheckArgument(d_value >= 0, this);
225  CheckArgument(y.d_value >= 0, y);
226  Integer a = (*this).toSignedInt();
227  Integer b = y.toSignedInt();
228 
229  return a < b;
230  }
231 
232  bool unsignedLessThan(const BitVector& y) const {
233  CheckArgument(d_size == y.d_size, y);
234  CheckArgument(d_value >= 0, this);
235  CheckArgument(y.d_value >= 0, y);
236  return d_value < y.d_value;
237  }
238 
239  bool signedLessThanEq(const BitVector& y) const {
240  CheckArgument(d_size == y.d_size, y);
241  CheckArgument(d_value >= 0, this);
242  CheckArgument(y.d_value >= 0, y);
243  Integer a = (*this).toSignedInt();
244  Integer b = y.toSignedInt();
245 
246  return a <= b;
247  }
248 
249  bool unsignedLessThanEq(const BitVector& y) const {
250  CheckArgument(d_size == y.d_size, this);
251  CheckArgument(d_value >= 0, this);
252  CheckArgument(y.d_value >= 0, y);
253  return d_value <= y.d_value;
254  }
255 
256 
257  /*
258  Extend operations
259  */
260 
261  BitVector zeroExtend(unsigned amount) const {
262  return BitVector(d_size + amount, d_value);
263  }
264 
265  BitVector signExtend(unsigned amount) const {
266  Integer sign_bit = d_value.extractBitRange(1, d_size -1);
267  if(sign_bit == Integer(0)) {
268  return BitVector(d_size + amount, d_value);
269  } else {
270  Integer val = d_value.oneExtend(d_size, amount);
271  return BitVector(d_size+ amount, val);
272  }
273  }
274 
275  /*
276  Shifts on BitVectors
277  */
278 
279  BitVector leftShift(const BitVector& y) const {
280  if (y.d_value > Integer(d_size)) {
281  return BitVector(d_size, Integer(0));
282  }
283  if (y.d_value == 0) {
284  return *this;
285  }
286 
287  // making sure we don't lose information casting
288  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
289  uint32_t amount = y.d_value.toUnsignedInt();
290  Integer res = d_value.multiplyByPow2(amount);
291  return BitVector(d_size, res);
292  }
293 
295  if(y.d_value > Integer(d_size)) {
296  return BitVector(d_size, Integer(0));
297  }
298 
299  // making sure we don't lose information casting
300  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
301  uint32_t amount = y.d_value.toUnsignedInt();
302  Integer res = d_value.divByPow2(amount);
303  return BitVector(d_size, res);
304  }
305 
307  Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
308  if(y.d_value > Integer(d_size)) {
309  if(sign_bit == Integer(0)) {
310  return BitVector(d_size, Integer(0));
311  } else {
312  return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 );
313  }
314  }
315 
316  if (y.d_value == 0) {
317  return *this;
318  }
319 
320  // making sure we don't lose information casting
321  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
322 
323  uint32_t amount = y.d_value.toUnsignedInt();
324  Integer rest = d_value.divByPow2(amount);
325 
326  if(sign_bit == Integer(0)) {
327  return BitVector(d_size, rest);
328  }
329  Integer res = rest.oneExtend(d_size - amount, amount);
330  return BitVector(d_size, res);
331  }
332 
333 
334  /*
335  Convenience functions
336  */
337 
338  size_t hash() const {
339  return d_value.hash() + d_size;
340  }
341 
342  std::string toString(unsigned int base = 2) const {
343  std::string str = d_value.toString(base);
344  if( base == 2 && d_size > str.size() ) {
345  std::string zeroes;
346  for( unsigned int i=0; i < d_size - str.size(); ++i ) {
347  zeroes.append("0");
348  }
349  return zeroes + str;
350  } else {
351  return str;
352  }
353  }
354 
355  unsigned getSize() const {
356  return d_size;
357  }
358 
359  const Integer& getValue() const {
360  return d_value;
361  }
362 
368  unsigned isPow2() {
369  return d_value.isPow2();
370  }
371 
372 };/* class BitVector */
373 
374 
375 
376 inline BitVector::BitVector(const std::string& num, unsigned base) {
377  CheckArgument(base == 2 || base == 16, base);
378 
379  if( base == 2 ) {
380  d_size = num.size();
381  } else {
382  d_size = num.size() * 4;
383  }
384 
385  d_value = Integer(num, base);
386 }/* BitVector::BitVector() */
387 
388 
393  inline size_t operator()(const BitVector& bv) const {
394  return bv.hash();
395  }
396 };/* struct BitVectorHashFunction */
397 
405  unsigned high;
407  unsigned low;
408 
409  BitVectorExtract(unsigned high, unsigned low)
410  : high(high), low(low) {}
411 
412  bool operator == (const BitVectorExtract& extract) const {
413  return high == extract.high && low == extract.low;
414  }
415 };/* struct BitVectorExtract */
416 
421  size_t operator()(const BitVectorExtract& extract) const {
422  size_t hash = extract.low;
423  hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
424  return hash;
425  }
426 };/* struct BitVectorExtractHashFunction */
427 
428 
434  unsigned bitIndex;
435  BitVectorBitOf(unsigned i)
436  : bitIndex(i) {}
437 
438  bool operator == (const BitVectorBitOf& other) const {
439  return bitIndex == other.bitIndex;
440  }
441 };/* struct BitVectorBitOf */
442 
447  size_t operator()(const BitVectorBitOf& b) const {
448  return b.bitIndex;
449  }
450 };/* struct BitVectorBitOfHashFunction */
451 
452 
453 
455  unsigned size;
456  BitVectorSize(unsigned size)
457  : size(size) {}
458  operator unsigned () const { return size; }
459 };/* struct BitVectorSize */
460 
462  unsigned repeatAmount;
463  BitVectorRepeat(unsigned repeatAmount)
464  : repeatAmount(repeatAmount) {}
465  operator unsigned () const { return repeatAmount; }
466 };/* struct BitVectorRepeat */
467 
470  BitVectorZeroExtend(unsigned zeroExtendAmount)
471  : zeroExtendAmount(zeroExtendAmount) {}
472  operator unsigned () const { return zeroExtendAmount; }
473 };/* struct BitVectorZeroExtend */
474 
477  BitVectorSignExtend(unsigned signExtendAmount)
478  : signExtendAmount(signExtendAmount) {}
479  operator unsigned () const { return signExtendAmount; }
480 };/* struct BitVectorSignExtend */
481 
484  BitVectorRotateLeft(unsigned rotateLeftAmount)
485  : rotateLeftAmount(rotateLeftAmount) {}
486  operator unsigned () const { return rotateLeftAmount; }
487 };/* struct BitVectorRotateLeft */
488 
491  BitVectorRotateRight(unsigned rotateRightAmount)
492  : rotateRightAmount(rotateRightAmount) {}
493  operator unsigned () const { return rotateRightAmount; }
494 };/* struct BitVectorRotateRight */
495 
497  unsigned size;
498  IntToBitVector(unsigned size)
499  : size(size) {}
500  operator unsigned () const { return size; }
501 };/* struct IntToBitVector */
502 
503 template <typename T>
505  inline size_t operator()(const T& x) const {
506  return (size_t)x;
507  }
508 };/* struct UnsignedHashFunction */
509 
510 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
511 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
512  return os << bv.toString();
513 }
514 
515 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) CVC4_PUBLIC;
516 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
517  return os << "[" << bv.high << ":" << bv.low << "]";
518 }
519 
520 inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) CVC4_PUBLIC;
521 inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
522  return os << "[" << bv.bitIndex << "]";
523 }
524 
525 inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) CVC4_PUBLIC;
526 inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) {
527  return os << "[" << bv.size << "]";
528 }
529 
530 }/* CVC4 namespace */
531 
532 #endif /* __CVC4__BITVECTOR_H */
BitVector leftShift(const BitVector &y) const
Definition: bitvector.h:279
Hash function for the BitVectorBitOf objects.
Definition: bitvector.h:446
Integer setBit(uint32_t i) const
bool isBitSet(uint32_t i) const
Definition: bitvector.h:188
std::string toString(int base=10) const
Hash function for the BitVector constants.
Definition: bitvector.h:392
size_t operator()(const BitVector &bv) const
Definition: bitvector.h:393
bool signedLessThanEq(const BitVector &y) const
Definition: bitvector.h:239
Integer toInteger() const
Definition: bitvector.h:78
uint32_t toUnsignedInt() const
Integer floorDivideQuotient(const Integer &y) const
Returns the floor(this / y)
BitVectorSize(unsigned size)
Definition: bitvector.h:456
Integer divByPow2(uint32_t exp) const
BitVectorBitOf(unsigned i)
Definition: bitvector.h:435
size_t hash() const
Definition: bitvector.h:338
unsigned low
The low bit of the range for this extract.
Definition: bitvector.h:407
BitVector setBit(uint32_t i) const
Definition: bitvector.h:182
BitVector(unsigned size, const Integer &val)
Definition: bitvector.h:53
bool isBitSet(uint32_t i) const
BitVectorExtract(unsigned high, unsigned low)
Definition: bitvector.h:409
Integer multiplyByPow2(uint32_t pow) const
Return this*(2^pow).
size_t hash() const
Computes the hash of the node from the first word of the numerator, the denominator.
The structure representing the extraction of one Boolean bit.
Definition: bitvector.h:432
BitVector(unsigned size, unsigned long int z)
Definition: bitvector.h:66
BitVectorZeroExtend(unsigned zeroExtendAmount)
Definition: bitvector.h:470
BitVector unsignedRemTotal(const BitVector &y) const
Total division function that returns 0 when the denominator is 0.
Definition: bitvector.h:211
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
CVC4's exception base class and some associated utilities.
const Integer & getValue() const
Definition: bitvector.h:359
BitVector concat(const BitVector &other) const
Definition: bitvector.h:100
BitVectorRotateLeft(unsigned rotateLeftAmount)
Definition: bitvector.h:484
BitVector unsignedDivTotal(const BitVector &y) const
Total division function that returns 0 when the denominator is 0.
Definition: bitvector.h:196
unsigned isPow2()
Returns k is the integer is equal to 2^{k-1} and zero otherwise.
Definition: bitvector.h:368
unsigned high
The high bit of the range for this extract.
Definition: bitvector.h:405
BitVectorRotateRight(unsigned rotateRightAmount)
Definition: bitvector.h:491
BitVectorSignExtend(unsigned signExtendAmount)
Definition: bitvector.h:477
BitVector(unsigned size=0)
Definition: bitvector.h:58
Integer floorDivideRemainder(const Integer &y) const
Returns r == this - floor(this/y)*y.
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
BitVector zeroExtend(unsigned amount) const
Definition: bitvector.h:261
std::string toString(unsigned int base=2) const
Definition: bitvector.h:342
Hash function for the BitVectorExtract objects.
Definition: bitvector.h:420
Integer bitwiseNot() const
BitVector signExtend(unsigned amount) const
Definition: bitvector.h:265
Macros that should be defined everywhere during the building of the libraries and driver binary...
IntToBitVector(unsigned size)
Definition: bitvector.h:498
Integer bitwiseXor(const Integer &y) const
Integer modByPow2(uint32_t exp) const
BitVector(unsigned size, unsigned int z)
Definition: bitvector.h:61
size_t operator()(const T &x) const
Definition: bitvector.h:505
BitVector arithRightShift(const BitVector &y) const
Definition: bitvector.h:306
unsigned getSize() const
Definition: bitvector.h:355
Integer bitwiseOr(const Integer &y) const
std::ostream & operator<<(std::ostream &out, const SubrangeBound &bound)
BitVector logicalRightShift(const BitVector &y) const
Definition: bitvector.h:294
size_t operator()(const BitVectorExtract &extract) const
Definition: bitvector.h:421
BitVectorRepeat(unsigned repeatAmount)
Definition: bitvector.h:463
BitVector(unsigned size, const BitVector &q)
Definition: bitvector.h:71
bool unsignedLessThan(const BitVector &y) const
Definition: bitvector.h:232
BitVector extract(unsigned high, unsigned low) const
Definition: bitvector.h:104
Integer extractBitRange(uint32_t bitCount, uint32_t low) const
See CLN Documentation.
bool signedLessThan(const BitVector &y) const
Definition: bitvector.h:222
bool operator!=(enum Result::Sat s, const Result &r)
bool operator==(enum Result::Sat s, const Result &r)
unsigned bitIndex
The index of the bit.
Definition: bitvector.h:434
bool unsignedLessThanEq(const BitVector &y) const
Definition: bitvector.h:249
Integer oneExtend(uint32_t size, uint32_t amount) const
size_t operator()(const BitVectorBitOf &b) const
Definition: bitvector.h:447
The structure representing the extraction operation for bit-vectors.
Definition: bitvector.h:403
Integer bitwiseAnd(const Integer &y) const
unsigned isPow2() const
Returns k if the integer is equal to 2^(k-1)