src/util/bitvector.h

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