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) {
 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
 127 inline BitVector::BitVector(const std::string& num, unsigned base) {
 128   AlwaysAssert( base == 2 || base == 16 );
 129
 130   if( base == 2 ) {
 131     d_size = num.size();
 132 //    d_value = Integer(num,2);
 133 /*
 134     for( string::const_iterator it = num.begin(); it != num.end(); ++it ) {
 135       if( *it != '0' || *it != '1' ) {
 136         IllegalArgument(num, "BitVector argument is not a binary string.");
 137       }
 138       z = (Integer(2) * z) + (*it == '1');
 139       d_value = mpz_class(z.get_mpz());
 140     }
 141 */
 142   } else if( base == 16 ) {
 143     d_size = num.size() * 4;
 144 //    // Use a stream to decode the hex string
 145 //    stringstream ss;
 146 //    ss.setf(ios::hex, ios::basefield);
 147 //    ss << num;
 148 //    ss >> z;
 149 //    d_value = mpz_class(z);
 150 //    break;
 151   } else {
 152     Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
 153   }
 154
 155   d_value = Integer(num,base);
 156 }
 157
 158
 159 /**
 160  * Hash function for the BitVector constants.
 161  */
 162 struct BitVectorHashStrategy {
 163   static inline size_t hash(const BitVector& bv) {
 164     return bv.hash();
 165   }
 166 };
 167
 168 /**
 169  * The structure representing the extraction operation for bit-vectors. The
 170  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
 171  * by taking the bits at indices <code>high ... low</code>
 172  */
 173 struct BitVectorExtract  {
 174   /** The high bit of the range for this extract */
 175   unsigned high;
 176   /** The low bit of the range for this extract */
 177   unsigned low;
 178
 179   BitVectorExtract(unsigned high, unsigned low)
 180   : high(high), low(low) {}
 181
 182   bool operator == (const BitVectorExtract& extract) const {
 183     return high == extract.high && low == extract.low;
 184   }
 185 };
 186
 187 /**
 188  * Hash function for the BitVectorExtract objects.
 189  */
 190 class BitVectorExtractHashStrategy {
 191 public:
 192   static size_t hash(const BitVectorExtract& extract) {
 193     size_t hash = extract.low;
 194     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 195     return hash;
 196   }
 197 };
 198
 199 struct BitVectorSize {
 200   unsigned size;
 201   BitVectorSize(unsigned size)
 202   : size(size) {}
 203   operator unsigned () const { return size; }
 204 };
 205
 206 struct BitVectorRepeat {
 207   unsigned repeatAmount;
 208   BitVectorRepeat(unsigned repeatAmount)
 209   : repeatAmount(repeatAmount) {}
 210   operator unsigned () const { return repeatAmount; }
 211 };
 212
 213 struct BitVectorZeroExtend {
 214   unsigned zeroExtendAmount;
 215   BitVectorZeroExtend(unsigned zeroExtendAmount)
 216   : zeroExtendAmount(zeroExtendAmount) {}
 217   operator unsigned () const { return zeroExtendAmount; }
 218 };
 219
 220 struct BitVectorSignExtend {
 221   unsigned signExtendAmount;
 222   BitVectorSignExtend(unsigned signExtendAmount)
 223   : signExtendAmount(signExtendAmount) {}
 224   operator unsigned () const { return signExtendAmount; }
 225 };
 226
 227 struct BitVectorRotateLeft {
 228   unsigned rotateLeftAmount;
 229   BitVectorRotateLeft(unsigned rotateLeftAmount)
 230   : rotateLeftAmount(rotateLeftAmount) {}
 231   operator unsigned () const { return rotateLeftAmount; }
 232 };
 233
 234 struct BitVectorRotateRight {
 235   unsigned rotateRightAmount;
 236   BitVectorRotateRight(unsigned rotateRightAmount)
 237   : rotateRightAmount(rotateRightAmount) {}
 238   operator unsigned () const { return rotateRightAmount; }
 239 };
 240
 241 template <typename T>
 242 struct UnsignedHashStrategy {
 243   static inline size_t hash(const T& x) {
 244     return (size_t)x;
 245   }
 246 };
 247
 248 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
 249   return os << bv.toString();
 250 }
 251
 252 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
 253   return os << "[" << bv.high << ":" << bv.low << "]";
 254 }
 255
 256 }/* CVC4 namespace */
 257
 258 #endif /* __CVC4__BITVECTOR_H */