cvc4-1.3
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  return BitVector(d_size, 0u);
201  }
202  CheckArgument(d_value >= 0, this);
203  CheckArgument(y.d_value > 0, y);
204  return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
205  }
206 
211  CheckArgument(d_size == y.d_size, y);
212  if (y.d_value == 0) {
213  return BitVector(d_size, 0u);
214  }
215  CheckArgument(d_value >= 0, this);
216  CheckArgument(y.d_value > 0, y);
217  return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
218  }
219 
220 
221  bool signedLessThan(const BitVector& y) const {
222  CheckArgument(d_size == y.d_size, y);
223  CheckArgument(d_value >= 0, this);
224  CheckArgument(y.d_value >= 0, y);
225  Integer a = (*this).toSignedInt();
226  Integer b = y.toSignedInt();
227 
228  return a < b;
229  }
230 
231  bool unsignedLessThan(const BitVector& y) const {
232  CheckArgument(d_size == y.d_size, y);
233  CheckArgument(d_value >= 0, this);
234  CheckArgument(y.d_value >= 0, y);
235  return d_value < y.d_value;
236  }
237 
238  bool signedLessThanEq(const BitVector& y) const {
239  CheckArgument(d_size == y.d_size, y);
240  CheckArgument(d_value >= 0, this);
241  CheckArgument(y.d_value >= 0, y);
242  Integer a = (*this).toSignedInt();
243  Integer b = y.toSignedInt();
244 
245  return a <= b;
246  }
247 
248  bool unsignedLessThanEq(const BitVector& y) const {
249  CheckArgument(d_size == y.d_size, this);
250  CheckArgument(d_value >= 0, this);
251  CheckArgument(y.d_value >= 0, y);
252  return d_value <= y.d_value;
253  }
254 
255 
256  /*
257  Extend operations
258  */
259 
260  BitVector zeroExtend(unsigned amount) const {
261  return BitVector(d_size + amount, d_value);
262  }
263 
264  BitVector signExtend(unsigned amount) const {
265  Integer sign_bit = d_value.extractBitRange(1, d_size -1);
266  if(sign_bit == Integer(0)) {
267  return BitVector(d_size + amount, d_value);
268  } else {
269  Integer val = d_value.oneExtend(d_size, amount);
270  return BitVector(d_size+ amount, val);
271  }
272  }
273 
274  /*
275  Shifts on BitVectors
276  */
277 
278  BitVector leftShift(const BitVector& y) const {
279  if (y.d_value > Integer(d_size)) {
280  return BitVector(d_size, Integer(0));
281  }
282  if (y.d_value == 0) {
283  return *this;
284  }
285 
286  // making sure we don't lose information casting
287  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
288  uint32_t amount = y.d_value.toUnsignedInt();
289  Integer res = d_value.multiplyByPow2(amount);
290  return BitVector(d_size, res);
291  }
292 
294  if(y.d_value > Integer(d_size)) {
295  return BitVector(d_size, Integer(0));
296  }
297 
298  // making sure we don't lose information casting
299  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
300  uint32_t amount = y.d_value.toUnsignedInt();
301  Integer res = d_value.divByPow2(amount);
302  return BitVector(d_size, res);
303  }
304 
306  Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
307  if(y.d_value > Integer(d_size)) {
308  if(sign_bit == Integer(0)) {
309  return BitVector(d_size, Integer(0));
310  } else {
311  return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 );
312  }
313  }
314 
315  if (y.d_value == 0) {
316  return *this;
317  }
318 
319  // making sure we don't lose information casting
320  CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
321 
322  uint32_t amount = y.d_value.toUnsignedInt();
323  Integer rest = d_value.divByPow2(amount);
324 
325  if(sign_bit == Integer(0)) {
326  return BitVector(d_size, rest);
327  }
328  Integer res = rest.oneExtend(d_size - amount, amount);
329  return BitVector(d_size, res);
330  }
331 
332 
333  /*
334  Convenience functions
335  */
336 
337  size_t hash() const {
338  return d_value.hash() + d_size;
339  }
340 
341  std::string toString(unsigned int base = 2) const {
342  std::string str = d_value.toString(base);
343  if( base == 2 && d_size > str.size() ) {
344  std::string zeroes;
345  for( unsigned int i=0; i < d_size - str.size(); ++i ) {
346  zeroes.append("0");
347  }
348  return zeroes + str;
349  } else {
350  return str;
351  }
352  }
353 
354  unsigned getSize() const {
355  return d_size;
356  }
357 
358  const Integer& getValue() const {
359  return d_value;
360  }
361 
367  unsigned isPow2() {
368  return d_value.isPow2();
369  }
370 
371 };/* class BitVector */
372 
373 
374 
375 inline BitVector::BitVector(const std::string& num, unsigned base) {
376  CheckArgument(base == 2 || base == 16, base);
377 
378  if( base == 2 ) {
379  d_size = num.size();
380  } else {
381  d_size = num.size() * 4;
382  }
383 
384  d_value = Integer(num, base);
385 }/* BitVector::BitVector() */
386 
387 
392  inline size_t operator()(const BitVector& bv) const {
393  return bv.hash();
394  }
395 };/* struct BitVectorHashFunction */
396 
404  unsigned high;
406  unsigned low;
407 
408  BitVectorExtract(unsigned high, unsigned low)
409  : high(high), low(low) {}
410 
411  bool operator == (const BitVectorExtract& extract) const {
412  return high == extract.high && low == extract.low;
413  }
414 };/* struct BitVectorExtract */
415 
420  size_t operator()(const BitVectorExtract& extract) const {
421  size_t hash = extract.low;
422  hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
423  return hash;
424  }
425 };/* struct BitVectorExtractHashFunction */
426 
427 
433  unsigned bitIndex;
434  BitVectorBitOf(unsigned i)
435  : bitIndex(i) {}
436 
437  bool operator == (const BitVectorBitOf& other) const {
438  return bitIndex == other.bitIndex;
439  }
440 };/* struct BitVectorBitOf */
441 
446  size_t operator()(const BitVectorBitOf& b) const {
447  return b.bitIndex;
448  }
449 };/* struct BitVectorBitOfHashFunction */
450 
451 
452 
454  unsigned size;
455  BitVectorSize(unsigned size)
456  : size(size) {}
457  operator unsigned () const { return size; }
458 };/* struct BitVectorSize */
459 
461  unsigned repeatAmount;
462  BitVectorRepeat(unsigned repeatAmount)
463  : repeatAmount(repeatAmount) {}
464  operator unsigned () const { return repeatAmount; }
465 };/* struct BitVectorRepeat */
466 
469  BitVectorZeroExtend(unsigned zeroExtendAmount)
470  : zeroExtendAmount(zeroExtendAmount) {}
471  operator unsigned () const { return zeroExtendAmount; }
472 };/* struct BitVectorZeroExtend */
473 
476  BitVectorSignExtend(unsigned signExtendAmount)
477  : signExtendAmount(signExtendAmount) {}
478  operator unsigned () const { return signExtendAmount; }
479 };/* struct BitVectorSignExtend */
480 
483  BitVectorRotateLeft(unsigned rotateLeftAmount)
484  : rotateLeftAmount(rotateLeftAmount) {}
485  operator unsigned () const { return rotateLeftAmount; }
486 };/* struct BitVectorRotateLeft */
487 
490  BitVectorRotateRight(unsigned rotateRightAmount)
491  : rotateRightAmount(rotateRightAmount) {}
492  operator unsigned () const { return rotateRightAmount; }
493 };/* struct BitVectorRotateRight */
494 
496  unsigned size;
497  IntToBitVector(unsigned size)
498  : size(size) {}
499  operator unsigned () const { return size; }
500 };/* struct IntToBitVector */
501 
502 template <typename T>
504  inline size_t operator()(const T& x) const {
505  return (size_t)x;
506  }
507 };/* struct UnsignedHashFunction */
508 
509 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
510 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
511  return os << bv.toString();
512 }
513 
514 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) CVC4_PUBLIC;
515 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
516  return os << "[" << bv.high << ":" << bv.low << "]";
517 }
518 
519 inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) CVC4_PUBLIC;
520 inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
521  return os << "[" << bv.bitIndex << "]";
522 }
523 
524 inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) CVC4_PUBLIC;
525 inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) {
526  return os << "[" << bv.size << "]";
527 }
528 
529 }/* CVC4 namespace */
530 
531 #endif /* __CVC4__BITVECTOR_H */
BitVector leftShift(const BitVector &y) const
Definition: bitvector.h:278
Hash function for the BitVectorBitOf objects.
Definition: bitvector.h:445
Integer setBit(uint32_t i) const
Returns the Integer obtained by setting the ith bit of the current Integer to 1.
bool isBitSet(uint32_t i) const
Definition: bitvector.h:188
Hash function for the BitVector constants.
Definition: bitvector.h:391
size_t operator()(const BitVector &bv) const
Definition: bitvector.h:392
bool signedLessThanEq(const BitVector &y) const
Definition: bitvector.h:238
Integer toInteger() const
Definition: bitvector.h:78
uint32_t toUnsignedInt() const
BitVectorSize(unsigned size)
Definition: bitvector.h:455
Integer divByPow2(uint32_t exp) const
Returns y / 2^exp.
BitVectorBitOf(unsigned i)
Definition: bitvector.h:434
size_t hash() const
Definition: bitvector.h:337
unsigned low
The low bit of the range for this extract.
Definition: bitvector.h:406
BitVector setBit(uint32_t i) const
Definition: bitvector.h:182
BitVector(unsigned size, const Integer &val)
Definition: bitvector.h:53
BitVectorExtract(unsigned high, unsigned low)
Definition: bitvector.h:408
Integer multiplyByPow2(uint32_t pow) const
Return this*(2^pow).
The structure representing the extraction of one Boolean bit.
Definition: bitvector.h:431
BitVector(unsigned size, unsigned long int z)
Definition: bitvector.h:66
BitVectorZeroExtend(unsigned zeroExtendAmount)
Definition: bitvector.h:469
BitVector unsignedRemTotal(const BitVector &y) const
Total division function that returns 0 when the denominator is 0.
Definition: bitvector.h:210
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:358
BitVector concat(const BitVector &other) const
Definition: bitvector.h:100
BitVectorRotateLeft(unsigned rotateLeftAmount)
Definition: bitvector.h:483
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:367
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
unsigned high
The high bit of the range for this extract.
Definition: bitvector.h:404
BitVectorRotateRight(unsigned rotateRightAmount)
Definition: bitvector.h:490
BitVectorSignExtend(unsigned signExtendAmount)
Definition: bitvector.h:476
BitVector(unsigned size=0)
Definition: bitvector.h:58
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
BitVector zeroExtend(unsigned amount) const
Definition: bitvector.h:260
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
std::string toString(unsigned int base=2) const
Definition: bitvector.h:341
Hash function for the BitVectorExtract objects.
Definition: bitvector.h:419
BitVector signExtend(unsigned amount) const
Definition: bitvector.h:264
Macros that should be defined everywhere during the building of the libraries and driver binary...
IntToBitVector(unsigned size)
Definition: bitvector.h:497
BitVector(unsigned size, unsigned int z)
Definition: bitvector.h:61
size_t operator()(const T &x) const
Definition: bitvector.h:504
BitVector arithRightShift(const BitVector &y) const
Definition: bitvector.h:305
unsigned getSize() const
Definition: bitvector.h:354
BitVector logicalRightShift(const BitVector &y) const
Definition: bitvector.h:293
size_t operator()(const BitVectorExtract &extract) const
Definition: bitvector.h:420
BitVectorRepeat(unsigned repeatAmount)
Definition: bitvector.h:462
BitVector(unsigned size, const BitVector &q)
Definition: bitvector.h:71
bool unsignedLessThan(const BitVector &y) const
Definition: bitvector.h:231
BitVector extract(unsigned high, unsigned low) const
Definition: bitvector.h:104
Integer extractBitRange(uint32_t bitCount, uint32_t low) const
See GMP Documentation.
bool signedLessThan(const BitVector &y) const
Definition: bitvector.h:221
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:433
bool unsignedLessThanEq(const BitVector &y) const
Definition: bitvector.h:248
Integer oneExtend(uint32_t size, uint32_t amount) const
Returns the integer with the binary representation of size bits extended with amount 1's...
size_t operator()(const BitVectorBitOf &b) const
Definition: bitvector.h:446
The structure representing the extraction operation for bit-vectors.
Definition: bitvector.h:402