src/util/bitvector.h

   1 /*********************                                                        */
   2 /*! \file bitvector.h
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: cconway, mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  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 CVC4_PUBLIC 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     //is this right? it looks like a no-op?
  95     return BitVector(d_size, d_value);
  96   }
  97
  98   BitVector concat (const BitVector& other) const {
  99     return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
 100     //return BitVector(d_size + other.d_size, (d_value * Integer(2).pow(other.d_size)) + other.d_value);
 101   }
 102
 103   BitVector extract(unsigned high, unsigned low) const {
 104     return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
 105     //return BitVector(high - low + 1, (d_value % (Integer(2).pow(high + 1))) / Integer(2).pow(low));
 106   }
 107
 108   size_t hash() const {
 109     return d_value.hash() + d_size;
 110   }
 111
 112   std::string toString(unsigned int base = 2) const {
 113     std::string str = d_value.toString(base);
 114     if( base == 2 && d_size > str.size() ) {
 115       std::string zeroes;
 116       for( unsigned int i=0; i < d_size - str.size(); ++i ) {
 117         zeroes.append("0");
 118       }
 119       return zeroes + str;
 120     } else {
 121       return str;
 122     }
 123   }
 124
 125   unsigned getSize() const {
 126     return d_size;
 127   }
 128
 129   const Integer& getValue() const {
 130     return d_value;
 131   }
 132 };/* class BitVector */
 133
 134 inline BitVector::BitVector(const std::string& num, unsigned base) {
 135   AlwaysAssert( base == 2 || base == 16 );
 136
 137   if( base == 2 ) {
 138     d_size = num.size();
 139 //    d_value = Integer(num,2);
 140 /*
 141     for( string::const_iterator it = num.begin(); it != num.end(); ++it ) {
 142       if( *it != '0' || *it != '1' ) {
 143         IllegalArgument(num, "BitVector argument is not a binary string.");
 144       }
 145       z = (Integer(2) * z) + (*it == '1');
 146       d_value = mpz_class(z.get_mpz());
 147     }
 148 */
 149   } else if( base == 16 ) {
 150     d_size = num.size() * 4;
 151 //    // Use a stream to decode the hex string
 152 //    stringstream ss;
 153 //    ss.setf(ios::hex, ios::basefield);
 154 //    ss << num;
 155 //    ss >> z;
 156 //    d_value = mpz_class(z);
 157 //    break;
 158   } else {
 159     Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
 160   }
 161
 162   d_value = Integer(num,base);
 163 }/* BitVector::BitVector() */
 164
 165
 166 /**
 167  * Hash function for the BitVector constants.
 168  */
 169 struct CVC4_PUBLIC BitVectorHashStrategy {
 170   static inline size_t hash(const BitVector& bv) {
 171     return bv.hash();
 172   }
 173 };/* struct BitVectorHashStrategy */
 174
 175 /**
 176  * The structure representing the extraction operation for bit-vectors. The
 177  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
 178  * by taking the bits at indices <code>high ... low</code>
 179  */
 180 struct CVC4_PUBLIC BitVectorExtract {
 181   /** The high bit of the range for this extract */
 182   unsigned high;
 183   /** The low bit of the range for this extract */
 184   unsigned low;
 185
 186   BitVectorExtract(unsigned high, unsigned low)
 187   : high(high), low(low) {}
 188
 189   bool operator == (const BitVectorExtract& extract) const {
 190     return high == extract.high && low == extract.low;
 191   }
 192 };/* struct BitVectorExtract */
 193
 194 /**
 195  * Hash function for the BitVectorExtract objects.
 196  */
 197 class CVC4_PUBLIC BitVectorExtractHashStrategy {
 198 public:
 199   static size_t hash(const BitVectorExtract& extract) {
 200     size_t hash = extract.low;
 201     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 202     return hash;
 203   }
 204 };/* class BitVectorExtractHashStrategy */
 205
 206 struct CVC4_PUBLIC BitVectorSize {
 207   unsigned size;
 208   BitVectorSize(unsigned size)
 209   : size(size) {}
 210   operator unsigned () const { return size; }
 211 };/* struct BitVectorSize */
 212
 213 struct CVC4_PUBLIC BitVectorRepeat {
 214   unsigned repeatAmount;
 215   BitVectorRepeat(unsigned repeatAmount)
 216   : repeatAmount(repeatAmount) {}
 217   operator unsigned () const { return repeatAmount; }
 218 };/* struct BitVectorRepeat */
 219
 220 struct CVC4_PUBLIC BitVectorZeroExtend {
 221   unsigned zeroExtendAmount;
 222   BitVectorZeroExtend(unsigned zeroExtendAmount)
 223   : zeroExtendAmount(zeroExtendAmount) {}
 224   operator unsigned () const { return zeroExtendAmount; }
 225 };/* struct BitVectorZeroExtend */
 226
 227 struct CVC4_PUBLIC BitVectorSignExtend {
 228   unsigned signExtendAmount;
 229   BitVectorSignExtend(unsigned signExtendAmount)
 230   : signExtendAmount(signExtendAmount) {}
 231   operator unsigned () const { return signExtendAmount; }
 232 };/* struct BitVectorSignExtend */
 233
 234 struct CVC4_PUBLIC BitVectorRotateLeft {
 235   unsigned rotateLeftAmount;
 236   BitVectorRotateLeft(unsigned rotateLeftAmount)
 237   : rotateLeftAmount(rotateLeftAmount) {}
 238   operator unsigned () const { return rotateLeftAmount; }
 239 };/* struct BitVectorRotateLeft */
 240
 241 struct CVC4_PUBLIC BitVectorRotateRight {
 242   unsigned rotateRightAmount;
 243   BitVectorRotateRight(unsigned rotateRightAmount)
 244   : rotateRightAmount(rotateRightAmount) {}
 245   operator unsigned () const { return rotateRightAmount; }
 246 };/* struct BitVectorRotateRight */
 247
 248 template <typename T>
 249 struct CVC4_PUBLIC UnsignedHashStrategy {
 250   static inline size_t hash(const T& x) {
 251     return (size_t)x;
 252   }
 253 };/* struct UnsignedHashStrategy */
 254
 255 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
 256 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
 257   return os << bv.toString();
 258 }
 259
 260 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) CVC4_PUBLIC;
 261 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
 262   return os << "[" << bv.high << ":" << bv.low << "]";
 263 }
 264
 265 }/* CVC4 namespace */
 266
 267 #endif /* __CVC4__BITVECTOR_H */