src/util/bitvector.h

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