src/util/bitvector.h

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