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