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   /*
  36     Class invariants:
  37     * no overflows: 2^d_size < d_value
  38     * no negative numbers: d_value >= 0
  39    */
  40   unsigned d_size;
  41   Integer d_value;
  42
  43   Integer toSignedInt() const {
  44     // returns Integer corresponding to two's complement interpretation of bv
  45     unsigned size = d_size;
  46     Integer sign_bit = d_value.extractBitRange(1,size-1);
  47     Integer val = d_value.extractBitRange(size-1, 0);
  48     Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
  49     return res;
  50   }
  51
  52
  53 public:
  54
  55   BitVector(unsigned size, const Integer& val):
  56     d_size(size),
  57     d_value(val.modByPow2(size))
  58       {}
  59
  60   BitVector(unsigned size = 0)
  61     : d_size(size), d_value(0) {}
  62
  63   BitVector(unsigned size, unsigned int z)
  64     : d_size(size), d_value(z) {
  65     d_value = d_value.modByPow2(size);
  66   }
  67
  68   BitVector(unsigned size, unsigned long int z)
  69     : d_size(size), d_value(z) {
  70     d_value = d_value.modByPow2(size);
  71   }
  72
  73   BitVector(unsigned size, const BitVector& q)
  74     : d_size(size), d_value(q.d_value) {}
  75
  76   BitVector(const std::string& num, unsigned base = 2);
  77
  78   ~BitVector() {}
  79
  80   Integer toInteger() const {
  81     return d_value;
  82   }
  83
  84   BitVector& operator =(const BitVector& x) {
  85     if(this == &x)
  86       return *this;
  87     d_size = x.d_size;
  88     d_value = x.d_value;
  89     return *this;
  90   }
  91
  92   bool operator ==(const BitVector& y) const {
  93     if (d_size != y.d_size) return false;
  94     return d_value == y.d_value;
  95   }
  96
  97   bool operator !=(const BitVector& y) const {
  98     if (d_size != y.d_size) return true;
  99     return d_value != y.d_value;
 100   }
 101
 102   BitVector equals(const BitVector&  y) const {
 103     Assert(d_size == y.d_size);
 104     return d_value == y.d_value;
 105   }
 106
 107   BitVector concat (const BitVector& other) const {
 108     return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
 109   }
 110
 111   BitVector extract(unsigned high, unsigned low) const {
 112     return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
 113   }
 114
 115   /*
 116     Bitwise operations on BitVectors
 117    */
 118
 119   // xor
 120   BitVector operator ^(const BitVector& y) const {
 121     Assert (d_size == y.d_size);
 122     return BitVector(d_size, d_value.bitwiseXor(y.d_value));
 123   }
 124
 125   // or
 126   BitVector operator |(const BitVector& y) const {
 127     Assert (d_size == y.d_size);
 128     return BitVector(d_size, d_value.bitwiseOr(y.d_value));
 129   }
 130
 131   // and
 132   BitVector operator &(const BitVector& y) const {
 133     Assert (d_size == y.d_size);
 134     return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
 135   }
 136
 137   // not
 138   BitVector operator ~() const {
 139     return BitVector(d_size, d_value.bitwiseNot());
 140   }
 141
 142   /*
 143     Arithmetic operations on BitVectors
 144    */
 145
 146
 147   bool operator <(const BitVector& y) const {
 148     return d_value < y.d_value;
 149   }
 150
 151   bool operator >(const BitVector& y) const {
 152     return d_value > y.d_value ;
 153   }
 154
 155   bool operator <=(const BitVector& y) const {
 156     return d_value <= y.d_value;
 157   }
 158
 159   bool operator >=(const BitVector& y) const {
 160     return d_value >= y.d_value ;
 161   }
 162
 163
 164   BitVector operator +(const BitVector& y) const {
 165     Assert (d_size == y.d_size);
 166     Integer sum = d_value +  y.d_value;
 167     return BitVector(d_size, sum);
 168   }
 169
 170   BitVector operator -(const BitVector& y) const {
 171     Assert (d_size == y.d_size);
 172     // to maintain the invariant that we are only adding BitVectors of the
 173     // same size
 174     BitVector one(d_size, Integer(1));
 175     return *this + ~y + one;
 176   }
 177
 178   BitVector operator -() const {
 179     BitVector one(d_size, Integer(1));
 180     return ~(*this) + one;
 181   }
 182
 183   BitVector operator *(const BitVector& y) const {
 184     Assert (d_size == y.d_size);
 185     Integer prod = d_value * y.d_value;
 186     return BitVector(d_size, prod);
 187   }
 188
 189   BitVector unsignedDiv (const BitVector& y) const {
 190     Assert (d_size == y.d_size);
 191     Assert (d_value >= 0 && y.d_value > 0);
 192     return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
 193   }
 194
 195   BitVector unsignedRem(const BitVector& y) const {
 196     Assert (d_size == y.d_size);
 197     Assert (d_value >= 0 && y.d_value > 0);
 198     return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
 199   }
 200
 201
 202   bool signedLessThan(const BitVector& y) const {
 203     Assert(d_size == y.d_size);
 204     Assert(d_value >= 0 && y.d_value >= 0);
 205     Integer a = (*this).toSignedInt();
 206     Integer b = y.toSignedInt();
 207
 208     return a < b;
 209   }
 210
 211   bool unsignedLessThan(const BitVector& y) const {
 212     Assert(d_size == y.d_size);
 213     Assert(d_value >= 0 && y.d_value >= 0);
 214     return d_value < y.d_value;
 215   }
 216
 217   bool signedLessThanEq(const BitVector& y) const {
 218     Assert(d_size == y.d_size);
 219     Assert(d_value >= 0 && y.d_value >= 0);
 220     Integer a = (*this).toSignedInt();
 221     Integer b = y.toSignedInt();
 222
 223     return a <= b;
 224   }
 225
 226   bool unsignedLessThanEq(const BitVector& y) const {
 227     Assert(d_size == y.d_size);
 228     Assert(d_value >= 0 && y.d_value >= 0);
 229     return d_value <= y.d_value;
 230   }
 231
 232
 233   /*
 234     Extend operations
 235    */
 236
 237   BitVector zeroExtend(unsigned amount) const {
 238     return BitVector(d_size + amount, d_value);
 239   }
 240
 241   BitVector signExtend(unsigned amount) const {
 242     Integer sign_bit = d_value.extractBitRange(1, d_size -1);
 243     if(sign_bit == Integer(0)) {
 244       return BitVector(d_size + amount, d_value);
 245     } else {
 246       Integer val = d_value.oneExtend(d_size, amount);
 247       return BitVector(d_size+ amount, val);
 248     }
 249   }
 250
 251   /*
 252     Shifts on BitVectors
 253    */
 254
 255   BitVector leftShift(const BitVector& y) const {
 256     if (y.d_value > Integer(d_size)) {
 257       return BitVector(d_size, Integer(0));
 258     }
 259     if (y.d_value == 0) {
 260       return *this;
 261     }
 262
 263     // making sure we don't lose information casting
 264     Assert(y.d_value < Integer(1).multiplyByPow2(32));
 265     uint32_t amount = y.d_value.toUnsignedInt();
 266     Integer res = d_value.multiplyByPow2(amount);
 267     return BitVector(d_size, res);
 268   }
 269
 270   BitVector logicalRightShift(const BitVector& y) const {
 271     if(y.d_value > Integer(d_size)) {
 272       return BitVector(d_size, Integer(0));
 273     }
 274
 275     // making sure we don't lose information casting
 276     Assert(y.d_value < Integer(1).multiplyByPow2(32));
 277     uint32_t amount = y.d_value.toUnsignedInt();
 278     Integer res = d_value.divByPow2(amount);
 279     return BitVector(d_size, res);
 280   }
 281
 282   BitVector arithRightShift(const BitVector& y) const {
 283     Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
 284     if(y.d_value > Integer(d_size)) {
 285       if(sign_bit == Integer(0)) {
 286         return BitVector(d_size, Integer(0));
 287       } else {
 288         return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 );
 289       }
 290     }
 291
 292     if (y.d_value == 0) {
 293       return *this;
 294     }
 295
 296     // making sure we don't lose information casting
 297     Assert(y.d_value < Integer(1).multiplyByPow2(32));
 298
 299     uint32_t amount  = y.d_value.toUnsignedInt();
 300     Integer rest = d_value.divByPow2(amount);
 301
 302     if(sign_bit == Integer(0)) {
 303       return BitVector(d_size, rest);
 304     }
 305     Integer res = rest.oneExtend(d_size - amount, amount);
 306     return BitVector(d_size, res);
 307   }
 308
 309
 310   /*
 311     Convenience functions
 312    */
 313
 314   size_t hash() const {
 315     return d_value.hash() + d_size;
 316   }
 317
 318   std::string toString(unsigned int base = 2) const {
 319     std::string str = d_value.toString(base);
 320     if( base == 2 && d_size > str.size() ) {
 321       std::string zeroes;
 322       for( unsigned int i=0; i < d_size - str.size(); ++i ) {
 323         zeroes.append("0");
 324       }
 325       return zeroes + str;
 326     } else {
 327       return str;
 328     }
 329   }
 330
 331   unsigned getSize() const {
 332     return d_size;
 333   }
 334
 335   const Integer& getValue() const {
 336     return d_value;
 337   }
 338
 339   /**
 340    Returns k is the integer is equal to 2^k and zero
 341    otherwise
 342    @return k if the integer is equal to 2^k and zero otherwise
 343    */
 344   unsigned isPow2() {
 345     return d_value.isPow2();
 346   }
 347
 348 };/* class BitVector */
 349
 350
 351
 352 inline BitVector::BitVector(const std::string& num, unsigned base) {
 353   AlwaysAssert( base == 2 || base == 16 );
 354
 355   if( base == 2 ) {
 356     d_size = num.size();
 357   } else if( base == 16 ) {
 358     d_size = num.size() * 4;
 359   } else {
 360     Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
 361   }
 362
 363   d_value = Integer(num,base);
 364 }/* BitVector::BitVector() */
 365
 366
 367 /**
 368  * Hash function for the BitVector constants.
 369  */
 370 struct CVC4_PUBLIC BitVectorHashStrategy {
 371   static inline size_t hash(const BitVector& bv) {
 372     return bv.hash();
 373   }
 374 };/* struct BitVectorHashStrategy */
 375
 376 /**
 377  * The structure representing the extraction operation for bit-vectors. The
 378  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
 379  * by taking the bits at indices <code>high ... low</code>
 380  */
 381 struct CVC4_PUBLIC BitVectorExtract {
 382   /** The high bit of the range for this extract */
 383   unsigned high;
 384   /** The low bit of the range for this extract */
 385   unsigned low;
 386
 387   BitVectorExtract(unsigned high, unsigned low)
 388   : high(high), low(low) {}
 389
 390   bool operator == (const BitVectorExtract& extract) const {
 391     return high == extract.high && low == extract.low;
 392   }
 393 };/* struct BitVectorExtract */
 394
 395 /**
 396  * Hash function for the BitVectorExtract objects.
 397  */
 398 class CVC4_PUBLIC BitVectorExtractHashStrategy {
 399 public:
 400   static size_t hash(const BitVectorExtract& extract) {
 401     size_t hash = extract.low;
 402     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 403     return hash;
 404   }
 405 };/* class BitVectorExtractHashStrategy */
 406
 407
 408 /**
 409  * The structure representing the extraction of one Boolean bit.
 410  */
 411 struct CVC4_PUBLIC BitVectorBitOf {
 412   /** The index of the bit */
 413   unsigned bitIndex;
 414   BitVectorBitOf(unsigned i)
 415     : bitIndex(i) {}
 416
 417   bool operator == (const BitVectorBitOf& other) const {
 418     return bitIndex == other.bitIndex;
 419   }
 420 };/* struct BitVectorBitOf */
 421
 422 /**
 423  * Hash function for the BitVectorBitOf objects.
 424  */
 425 class CVC4_PUBLIC BitVectorBitOfHashStrategy {
 426 public:
 427   static size_t hash(const BitVectorBitOf& b) {
 428     return b.bitIndex;
 429   }
 430 };/* class BitVectorBitOfHashStrategy */
 431
 432
 433
 434 struct CVC4_PUBLIC BitVectorSize {
 435   unsigned size;
 436   BitVectorSize(unsigned size)
 437   : size(size) {}
 438   operator unsigned () const { return size; }
 439 };/* struct BitVectorSize */
 440
 441 struct CVC4_PUBLIC BitVectorRepeat {
 442   unsigned repeatAmount;
 443   BitVectorRepeat(unsigned repeatAmount)
 444   : repeatAmount(repeatAmount) {}
 445   operator unsigned () const { return repeatAmount; }
 446 };/* struct BitVectorRepeat */
 447
 448 struct CVC4_PUBLIC BitVectorZeroExtend {
 449   unsigned zeroExtendAmount;
 450   BitVectorZeroExtend(unsigned zeroExtendAmount)
 451   : zeroExtendAmount(zeroExtendAmount) {}
 452   operator unsigned () const { return zeroExtendAmount; }
 453 };/* struct BitVectorZeroExtend */
 454
 455 struct CVC4_PUBLIC BitVectorSignExtend {
 456   unsigned signExtendAmount;
 457   BitVectorSignExtend(unsigned signExtendAmount)
 458   : signExtendAmount(signExtendAmount) {}
 459   operator unsigned () const { return signExtendAmount; }
 460 };/* struct BitVectorSignExtend */
 461
 462 struct CVC4_PUBLIC BitVectorRotateLeft {
 463   unsigned rotateLeftAmount;
 464   BitVectorRotateLeft(unsigned rotateLeftAmount)
 465   : rotateLeftAmount(rotateLeftAmount) {}
 466   operator unsigned () const { return rotateLeftAmount; }
 467 };/* struct BitVectorRotateLeft */
 468
 469 struct CVC4_PUBLIC BitVectorRotateRight {
 470   unsigned rotateRightAmount;
 471   BitVectorRotateRight(unsigned rotateRightAmount)
 472   : rotateRightAmount(rotateRightAmount) {}
 473   operator unsigned () const { return rotateRightAmount; }
 474 };/* struct BitVectorRotateRight */
 475
 476 template <typename T>
 477 struct CVC4_PUBLIC UnsignedHashStrategy {
 478   static inline size_t hash(const T& x) {
 479     return (size_t)x;
 480   }
 481 };/* struct UnsignedHashStrategy */
 482
 483 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
 484 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
 485   return os << bv.toString();
 486 }
 487
 488 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) CVC4_PUBLIC;
 489 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
 490   return os << "[" << bv.high << ":" << bv.low << "]";
 491 }
 492
 493 inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) CVC4_PUBLIC;
 494 inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) {
 495   return os << "[" << bv.bitIndex << "]";
 496 }
 497
 498
 499
 500 }/* CVC4 namespace */
 501
 502 #endif /* __CVC4__BITVECTOR_H */