src/util/bitvector.h

   1 /*
   2  * bitvector.h
   3  *
   4  *  Created on: Mar 31, 2010
   5  *      Author: dejan
   6  */
   7
   8 #ifndef __CVC4__BITVECTOR_H_
   9 #define __CVC4__BITVECTOR_H_
  10
  11 #include <string>
  12 #include <iostream>
  13 #include "util/gmp_util.h"
  14
  15 namespace CVC4 {
  16
  17 class BitVector {
  18
  19 private:
  20
  21   unsigned d_size;
  22   mpz_class d_value;
  23
  24   BitVector(unsigned size, const mpz_class& val) : d_size(size), d_value(val) {}
  25
  26 public:
  27
  28   BitVector(unsigned size = 0)
  29   : d_size(size), d_value(0) {}
  30
  31   BitVector(unsigned size, unsigned int z)
  32   : d_size(size), d_value(z) {}
  33
  34   BitVector(unsigned size, unsigned long int z)
  35   : d_size(size), d_value(z) {}
  36
  37   BitVector(unsigned size, const BitVector& q)
  38   : d_size(size), d_value(q.d_value) {}
  39
  40   BitVector(unsigned size, const std::string& num, unsigned base = 2)
  41   : d_size(size), d_value(0) {}
  42
  43   ~BitVector() {}
  44
  45   BitVector& operator =(const BitVector& x) {
  46     if(this == &x)
  47       return *this;
  48     d_value = x.d_value;
  49     return *this;
  50   }
  51
  52   bool operator ==(const BitVector& y) const {
  53     if (d_size != y.d_size) return false;
  54     return d_value == y.d_value;
  55   }
  56
  57   bool operator !=(const BitVector& y) const {
  58     if (d_size == y.d_size) return false;
  59     return d_value != y.d_value;
  60   }
  61
  62   BitVector operator +(const BitVector& y) const {
  63     return BitVector(std::max(d_size, y.d_size), d_value + y.d_value);
  64   }
  65
  66   BitVector operator -(const BitVector& y) const {
  67     return *this + ~y + 1;
  68   }
  69
  70   BitVector operator -() const {
  71     return ~(*this) + 1;
  72   }
  73
  74   BitVector operator *(const BitVector& y) const {
  75     return BitVector(d_size, d_value * y.d_value);
  76   }
  77
  78   BitVector operator ~() const {
  79     return BitVector(d_size, d_value);
  80   }
  81
  82   size_t hash() const {
  83     return gmpz_hash(d_value.get_mpz_t());
  84   }
  85
  86   std::string toString(unsigned int base = 2) const {
  87     return d_value.get_str(base);
  88   }
  89
  90   unsigned getSize() const {
  91     return d_size;
  92   }
  93 };
  94
  95 /**
  96  * Hash function for the BitVector constants.
  97  */
  98 struct BitVectorHashStrategy {
  99   static inline size_t hash(const BitVector& bv) {
 100     return bv.hash();
 101   }
 102 };
 103
 104 /**
 105  * The structure representing the extraction operation for bit-vectors. The
 106  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
 107  * by taking the bits at indices <code>high ... low</code>
 108  */
 109 struct BitVectorExtract  {
 110   /** The high bit of the range for this extract */
 111   unsigned high;
 112   /** The low bit of the range for this extract */
 113   unsigned low;
 114
 115   BitVectorExtract(unsigned high, unsigned low)
 116   : high(high), low(low) {}
 117
 118   bool operator == (const BitVectorExtract& extract) const {
 119     return high == extract.high && low == extract.low;
 120   }
 121 };
 122
 123 /**
 124  * Hash function for the BitVectorExtract objects.
 125  */
 126 class BitVectorExtractHashStrategy {
 127 public:
 128   static size_t hash(const BitVectorExtract& extract) {
 129     size_t hash = extract.low;
 130     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 131     return hash;
 132   }
 133 };
 134
 135 struct BitVectorSize {
 136   unsigned size;
 137   BitVectorSize(unsigned size)
 138   : size(size) {}
 139   operator unsigned () const { return size; }
 140 };
 141
 142 struct BitVectorRepeat {
 143   unsigned repeatAmount;
 144   BitVectorRepeat(unsigned repeatAmount)
 145   : repeatAmount(repeatAmount) {}
 146   operator unsigned () const { return repeatAmount; }
 147 };
 148
 149 struct BitVectorZeroExtend {
 150   unsigned zeroExtendAmount;
 151   BitVectorZeroExtend(unsigned zeroExtendAmount)
 152   : zeroExtendAmount(zeroExtendAmount) {}
 153   operator unsigned () const { return zeroExtendAmount; }
 154 };
 155
 156 struct BitVectorSignExtend {
 157   unsigned signExtendAmount;
 158   BitVectorSignExtend(unsigned signExtendAmount)
 159   : signExtendAmount(signExtendAmount) {}
 160   operator unsigned () const { return signExtendAmount; }
 161 };
 162
 163 struct BitVectorRotateLeft {
 164   unsigned rotateLeftAmount;
 165   BitVectorRotateLeft(unsigned rotateLeftAmount)
 166   : rotateLeftAmount(rotateLeftAmount) {}
 167   operator unsigned () const { return rotateLeftAmount; }
 168 };
 169
 170 struct BitVectorRotateRight {
 171   unsigned rotateRightAmount;
 172   BitVectorRotateRight(unsigned rotateRightAmount)
 173   : rotateRightAmount(rotateRightAmount) {}
 174   operator unsigned () const { return rotateRightAmount; }
 175 };
 176
 177 template <typename T>
 178 struct UnsignedHashStrategy {
 179   static inline size_t hash(const T& x) {
 180     return (size_t)x;
 181   }
 182 };
 183
 184 std::ostream& operator <<(std::ostream& os, const BitVector& bv);
 185 std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv);
 186 }
 187
 188
 189 #endif /* __CVC4__BITVECTOR_H_ */