src/util/bitvector.h

   1 /*********************                                                        */
   2 /*! \file bitvector.h
   3  ** \verbatim
   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
  13  **
  14  ** \brief [[ Add one-line brief description here ]]
  15  **
  16  ** [[ Add lengthier description here ]]
  17  ** \todo document this file
  18  **/
  19
  20 #include "cvc4_public.h"
  21
  22 #ifndef __CVC4__BITVECTOR_H
  23 #define __CVC4__BITVECTOR_H
  24
  25 #include <iostream>
  26 #include "util/Assert.h"
  27 #include "util/integer.h"
  28
  29 namespace CVC4 {
  30
  31 class BitVector {
  32
  33 private:
  34
  35   unsigned d_size;
  36   Integer d_value;
  37
  38 public:
  39
  40   BitVector(unsigned size, const Integer& val)
  41   : d_size(size), d_value(val) {}
  42
  43   BitVector(unsigned size = 0)
  44   : d_size(size), d_value(0) {}
  45
  46   BitVector(unsigned size, unsigned int z)
  47   : d_size(size), d_value(z) {}
  48
  49   BitVector(unsigned size, unsigned long int z)
  50   : d_size(size), d_value(z) {}
  51
  52   BitVector(unsigned size, const BitVector& q)
  53   : d_size(size), d_value(q.d_value) {}
  54
  55   BitVector(const std::string& num, unsigned base = 2);
  56
  57   ~BitVector() {}
  58
  59   BitVector& operator =(const BitVector& x) {
  60     if(this == &x)
  61       return *this;
  62     d_size = x.d_size;
  63     d_value = x.d_value;
  64     return *this;
  65   }
  66
  67   bool operator ==(const BitVector& y) const {
  68     if (d_size != y.d_size) return false;
  69     return d_value == y.d_value;
  70   }
  71
  72   bool operator !=(const BitVector& y) const {
  73     if (d_size == y.d_size) return false;
  74     return d_value != y.d_value;
  75   }
  76
  77   BitVector operator +(const BitVector& y) const {
  78     return BitVector(std::max(d_size, y.d_size), d_value + y.d_value);
  79   }
  80
  81   BitVector operator -(const BitVector& y) const {
  82     return *this + ~y + 1;
  83   }
  84
  85   BitVector operator -() const {
  86     return ~(*this) + 1;
  87   }
  88
  89   BitVector operator *(const BitVector& y) const {
  90     return BitVector(d_size, d_value * y.d_value);
  91   }
  92
  93   BitVector operator ~() const {
  94     return BitVector(d_size, d_value);
  95   }
  96
  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);
  99   }
 100
 101   BitVector extract(unsigned high, unsigned low) const {
 102     return BitVector(high - low + 1, (d_value % (Integer(2).pow(high + 1))) / Integer(2).pow(low));
 103   }
 104
 105   size_t hash() const {
 106     return d_value.hash() + d_size;
 107   }
 108
 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() ) {
 112       std::string zeroes;
 113       for( unsigned int i=0; i < d_size - str.size(); ++i ) {
 114         zeroes.append("0");
 115       }
 116       return zeroes + str;
 117     } else {
 118       return str;
 119     }
 120   }
 121
 122   unsigned getSize() const {
 123     return d_size;
 124   }
 125
 126   const Integer& getValue() const {
 127     return d_value;
 128   }
 129 };/* class BitVector */
 130
 131 inline BitVector::BitVector(const std::string& num, unsigned base) {
 132   AlwaysAssert( base == 2 || base == 16 );
 133
 134   if( base == 2 ) {
 135     d_size = num.size();
 136 //    d_value = Integer(num,2);
 137 /*
 138     for( string::const_iterator it = num.begin(); it != num.end(); ++it ) {
 139       if( *it != '0' || *it != '1' ) {
 140         IllegalArgument(num, "BitVector argument is not a binary string.");
 141       }
 142       z = (Integer(2) * z) + (*it == '1');
 143       d_value = mpz_class(z.get_mpz());
 144     }
 145 */
 146   } else if( base == 16 ) {
 147     d_size = num.size() * 4;
 148 //    // Use a stream to decode the hex string
 149 //    stringstream ss;
 150 //    ss.setf(ios::hex, ios::basefield);
 151 //    ss << num;
 152 //    ss >> z;
 153 //    d_value = mpz_class(z);
 154 //    break;
 155   } else {
 156     Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
 157   }
 158
 159   d_value = Integer(num,base);
 160 }
 161
 162
 163 /**
 164  * Hash function for the BitVector constants.
 165  */
 166 struct BitVectorHashStrategy {
 167   static inline size_t hash(const BitVector& bv) {
 168     return bv.hash();
 169   }
 170 };
 171
 172 /**
 173  * The structure representing the extraction operation for bit-vectors. The
 174  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
 175  * by taking the bits at indices <code>high ... low</code>
 176  */
 177 struct BitVectorExtract  {
 178   /** The high bit of the range for this extract */
 179   unsigned high;
 180   /** The low bit of the range for this extract */
 181   unsigned low;
 182
 183   BitVectorExtract(unsigned high, unsigned low)
 184   : high(high), low(low) {}
 185
 186   bool operator == (const BitVectorExtract& extract) const {
 187     return high == extract.high && low == extract.low;
 188   }
 189 };
 190
 191 /**
 192  * Hash function for the BitVectorExtract objects.
 193  */
 194 class BitVectorExtractHashStrategy {
 195 public:
 196   static size_t hash(const BitVectorExtract& extract) {
 197     size_t hash = extract.low;
 198     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 199     return hash;
 200   }
 201 };
 202
 203 struct BitVectorSize {
 204   unsigned size;
 205   BitVectorSize(unsigned size)
 206   : size(size) {}
 207   operator unsigned () const { return size; }
 208 };
 209
 210 struct BitVectorRepeat {
 211   unsigned repeatAmount;
 212   BitVectorRepeat(unsigned repeatAmount)
 213   : repeatAmount(repeatAmount) {}
 214   operator unsigned () const { return repeatAmount; }
 215 };
 216
 217 struct BitVectorZeroExtend {
 218   unsigned zeroExtendAmount;
 219   BitVectorZeroExtend(unsigned zeroExtendAmount)
 220   : zeroExtendAmount(zeroExtendAmount) {}
 221   operator unsigned () const { return zeroExtendAmount; }
 222 };
 223
 224 struct BitVectorSignExtend {
 225   unsigned signExtendAmount;
 226   BitVectorSignExtend(unsigned signExtendAmount)
 227   : signExtendAmount(signExtendAmount) {}
 228   operator unsigned () const { return signExtendAmount; }
 229 };
 230
 231 struct BitVectorRotateLeft {
 232   unsigned rotateLeftAmount;
 233   BitVectorRotateLeft(unsigned rotateLeftAmount)
 234   : rotateLeftAmount(rotateLeftAmount) {}
 235   operator unsigned () const { return rotateLeftAmount; }
 236 };
 237
 238 struct BitVectorRotateRight {
 239   unsigned rotateRightAmount;
 240   BitVectorRotateRight(unsigned rotateRightAmount)
 241   : rotateRightAmount(rotateRightAmount) {}
 242   operator unsigned () const { return rotateRightAmount; }
 243 };
 244
 245 template <typename T>
 246 struct UnsignedHashStrategy {
 247   static inline size_t hash(const T& x) {
 248     return (size_t)x;
 249   }
 250 };
 251
 252 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
 253   return os << bv.toString();
 254 }
 255
 256 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
 257   return os << "[" << bv.high << ":" << bv.low << "]";
 258 }
 259
 260 }/* CVC4 namespace */
 261
 262 #endif /* __CVC4__BITVECTOR_H */