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() {}
  41
  42   BitVector& operator =(const BitVector& x) {
  43     if(this == &x)
  44       return *this;
  45     d_value = x.d_value;
  46     return *this;
  47   }
  48
  49   bool operator ==(const BitVector& y) const {
  50     if (d_size != y.d_size) return false;
  51     return d_value == y.d_value;
  52   }
  53
  54   bool operator !=(const BitVector& y) const {
  55     if (d_size == y.d_size) return false;
  56     return d_value != y.d_value;
  57   }
  58
  59   BitVector operator +(const BitVector& y) const {
  60     return BitVector(std::max(d_size, y.d_size), d_value + y.d_value);
  61   }
  62
  63   BitVector operator -(const BitVector& y) const {
  64     return *this + ~y + 1;
  65   }
  66
  67   BitVector operator -() const {
  68     return ~(*this) + 1;
  69   }
  70
  71   BitVector operator *(const BitVector& y) const {
  72     return BitVector(d_size, d_value * y.d_value);
  73   }
  74
  75   BitVector operator ~() const {
  76     return BitVector(d_size, d_value);
  77   }
  78
  79   size_t hash() const {
  80     return gmpz_hash(d_value.get_mpz_t());
  81   }
  82
  83   std::string toString(unsigned int base = 2) const {
  84     return d_value.get_str(base);
  85   }
  86 };
  87
  88 /**
  89  * Hash function for the BitVector constants.
  90  */
  91 struct BitVectorHashStrategy {
  92   static inline size_t hash(const BitVector& bv) {
  93     return bv.hash();
  94   }
  95 };
  96
  97 /**
  98  * The structure representing the extraction operation for bit-vectors. The
  99  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
 100  * by taking the bits at indices <code>high ... low</code>
 101  */
 102 struct BitVectorExtract  {
 103   /** The high bit of the range for this extract */
 104   unsigned high;
 105   /** The low bit of the range for this extract */
 106   unsigned low;
 107
 108   BitVectorExtract(unsigned high, unsigned low)
 109   : high(high), low(low) {}
 110
 111   bool operator == (const BitVectorExtract& extract) const {
 112     return high == extract.high && low == extract.low;
 113   }
 114 };
 115
 116 /**
 117  * Hash function for the BitVectorExtract objects.
 118  */
 119 class BitVectorExtractHashStrategy {
 120 public:
 121   static size_t hash(const BitVectorExtract& extract) {
 122     size_t hash = extract.low;
 123     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 124     return hash;
 125   }
 126 };
 127
 128 struct BitVectorSize {
 129   unsigned size;
 130   BitVectorSize(unsigned size)
 131   : size(size) {}
 132   operator unsigned () const { return size; }
 133 };
 134
 135 struct BitVectorRepeat {
 136   unsigned repeatAmount;
 137   BitVectorRepeat(unsigned repeatAmount)
 138   : repeatAmount(repeatAmount) {}
 139   operator unsigned () const { return repeatAmount; }
 140 };
 141
 142 struct BitVectorZeroExtend {
 143   unsigned zeroExtendAmount;
 144   BitVectorZeroExtend(unsigned zeroExtendAmount)
 145   : zeroExtendAmount(zeroExtendAmount) {}
 146   operator unsigned () const { return zeroExtendAmount; }
 147 };
 148
 149 struct BitVectorSignExtend {
 150   unsigned signExtendAmount;
 151   BitVectorSignExtend(unsigned signExtendAmount)
 152   : signExtendAmount(signExtendAmount) {}
 153   operator unsigned () const { return signExtendAmount; }
 154 };
 155
 156 struct BitVectorRotateLeft {
 157   unsigned rotateLeftAmount;
 158   BitVectorRotateLeft(unsigned rotateLeftAmount)
 159   : rotateLeftAmount(rotateLeftAmount) {}
 160   operator unsigned () const { return rotateLeftAmount; }
 161 };
 162
 163 struct BitVectorRotateRight {
 164   unsigned rotateRightAmount;
 165   BitVectorRotateRight(unsigned rotateRightAmount)
 166   : rotateRightAmount(rotateRightAmount) {}
 167   operator unsigned () const { return rotateRightAmount; }
 168 };
 169
 170 template <typename T>
 171 struct UnsignedHashStrategy {
 172   static inline size_t hash(const T& x) {
 173     return (size_t)x;
 174   }
 175 };
 176
 177 std::ostream& operator <<(std::ostream& os, const BitVector& bv);
 178 std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv);
 179 }
 180
 181
 182 #endif /* __CVC4__BITVECTOR_H_ */