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