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): taking, 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/gmp_util.h"
  28 #include "util/integer.h"
  29
  30 namespace CVC4 {
  31
  32 class BitVector {
  33
  34 private:
  35
  36   unsigned d_size;
  37   Integer d_value;
  38
  39   BitVector(unsigned size, const Integer& val) : d_size(size), d_value(val) {}
  40
  41 public:
  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_value = x.d_value;
  63     return *this;
  64   }
  65
  66   bool operator ==(const BitVector& y) const {
  67     if (d_size != y.d_size) return false;
  68     return d_value == y.d_value;
  69   }
  70
  71   bool operator !=(const BitVector& y) const {
  72     if (d_size == y.d_size) return false;
  73     return d_value != y.d_value;
  74   }
  75
  76   BitVector operator +(const BitVector& y) const {
  77     return BitVector(std::max(d_size, y.d_size), d_value + y.d_value);
  78   }
  79
  80   BitVector operator -(const BitVector& y) const {
  81     return *this + ~y + 1;
  82   }
  83
  84   BitVector operator -() const {
  85     return ~(*this) + 1;
  86   }
  87
  88   BitVector operator *(const BitVector& y) const {
  89     return BitVector(d_size, d_value * y.d_value);
  90   }
  91
  92   BitVector operator ~() const {
  93     return BitVector(d_size, d_value);
  94   }
  95
  96   size_t hash() const {
  97     return d_value.hash();
  98   }
  99
 100   std::string toString(unsigned int base = 2) const {
 101     std::string str = d_value.toString(base);
 102     if( base == 2 && d_size > str.size() ) {
 103       std::string zeroes;
 104       for( unsigned int i=0; i < d_size - str.size(); ++i ) {
 105         zeroes.append("0");
 106       }
 107       return zeroes + str;
 108     } else {
 109       return str;
 110     }
 111   }
 112
 113   unsigned getSize() const {
 114     return d_size;
 115   }
 116 };
 117
 118 inline BitVector::BitVector(const std::string& num, unsigned base) {
 119   AlwaysAssert( base == 2 || base == 16 );
 120
 121   if( base == 2 ) {
 122     d_size = num.size();
 123 //    d_value = Integer(num,2);
 124 /*
 125     for( string::const_iterator it = num.begin(); it != num.end(); ++it ) {
 126       if( *it != '0' || *it != '1' ) {
 127         IllegalArgument(num, "BitVector argument is not a binary string.");
 128       }
 129       z = (Integer(2) * z) + (*it == '1');
 130       d_value = mpz_class(z.get_mpz());
 131     }
 132 */
 133   } else if( base == 16 ) {
 134     d_size = num.size() * 4;
 135 //    // Use a stream to decode the hex string
 136 //    stringstream ss;
 137 //    ss.setf(ios::hex, ios::basefield);
 138 //    ss << num;
 139 //    ss >> z;
 140 //    d_value = mpz_class(z);
 141 //    break;
 142   } else {
 143     Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
 144   }
 145
 146   d_value = Integer(num,base);
 147 }
 148
 149
 150 /**
 151  * Hash function for the BitVector constants.
 152  */
 153 struct BitVectorHashStrategy {
 154   static inline size_t hash(const BitVector& bv) {
 155     return bv.hash();
 156   }
 157 };
 158
 159 /**
 160  * The structure representing the extraction operation for bit-vectors. The
 161  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
 162  * by taking the bits at indices <code>high ... low</code>
 163  */
 164 struct BitVectorExtract  {
 165   /** The high bit of the range for this extract */
 166   unsigned high;
 167   /** The low bit of the range for this extract */
 168   unsigned low;
 169
 170   BitVectorExtract(unsigned high, unsigned low)
 171   : high(high), low(low) {}
 172
 173   bool operator == (const BitVectorExtract& extract) const {
 174     return high == extract.high && low == extract.low;
 175   }
 176 };
 177
 178 /**
 179  * Hash function for the BitVectorExtract objects.
 180  */
 181 class BitVectorExtractHashStrategy {
 182 public:
 183   static size_t hash(const BitVectorExtract& extract) {
 184     size_t hash = extract.low;
 185     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 186     return hash;
 187   }
 188 };
 189
 190 struct BitVectorSize {
 191   unsigned size;
 192   BitVectorSize(unsigned size)
 193   : size(size) {}
 194   operator unsigned () const { return size; }
 195 };
 196
 197 struct BitVectorRepeat {
 198   unsigned repeatAmount;
 199   BitVectorRepeat(unsigned repeatAmount)
 200   : repeatAmount(repeatAmount) {}
 201   operator unsigned () const { return repeatAmount; }
 202 };
 203
 204 struct BitVectorZeroExtend {
 205   unsigned zeroExtendAmount;
 206   BitVectorZeroExtend(unsigned zeroExtendAmount)
 207   : zeroExtendAmount(zeroExtendAmount) {}
 208   operator unsigned () const { return zeroExtendAmount; }
 209 };
 210
 211 struct BitVectorSignExtend {
 212   unsigned signExtendAmount;
 213   BitVectorSignExtend(unsigned signExtendAmount)
 214   : signExtendAmount(signExtendAmount) {}
 215   operator unsigned () const { return signExtendAmount; }
 216 };
 217
 218 struct BitVectorRotateLeft {
 219   unsigned rotateLeftAmount;
 220   BitVectorRotateLeft(unsigned rotateLeftAmount)
 221   : rotateLeftAmount(rotateLeftAmount) {}
 222   operator unsigned () const { return rotateLeftAmount; }
 223 };
 224
 225 struct BitVectorRotateRight {
 226   unsigned rotateRightAmount;
 227   BitVectorRotateRight(unsigned rotateRightAmount)
 228   : rotateRightAmount(rotateRightAmount) {}
 229   operator unsigned () const { return rotateRightAmount; }
 230 };
 231
 232 template <typename T>
 233 struct UnsignedHashStrategy {
 234   static inline size_t hash(const T& x) {
 235     return (size_t)x;
 236   }
 237 };
 238
 239 std::ostream& operator <<(std::ostream& os, const BitVector& bv);
 240 std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv);
 241 }
 242
 243
 244 #endif /* __CVC4__BITVECTOR_H_ */