src/util/bitvector.h

   1 /*********************                                                        */
   2 /*! \file bitvector.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Andres Noetzli, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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
  17 #include "cvc4_public.h"
  18
  19 #ifndef CVC4__BITVECTOR_H
  20 #define CVC4__BITVECTOR_H
  21
  22 #include <cstdint>
  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 {
  32  public:
  33   BitVector(unsigned size, const Integer& val)
  34       : d_size(size), d_value(val.modByPow2(size))
  35   {
  36   }
  37
  38   BitVector(unsigned size = 0) : d_size(size), d_value(0) {}
  39
  40   /**
  41    * BitVector constructor using a 32-bit unsigned integer for the value.
  42    *
  43    * Note: we use an explicit bit-width here to be consistent across
  44    * platforms (long is 32-bit when compiling 64-bit binaries on
  45    * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
  46    */
  47   BitVector(unsigned size, uint32_t z) : d_size(size), d_value(z)
  48   {
  49     d_value = d_value.modByPow2(size);
  50   }
  51
  52   /**
  53    * BitVector constructor using a 64-bit unsigned integer for the value.
  54    *
  55    * Note: we use an explicit bit-width here to be consistent across
  56    * platforms (long is 32-bit when compiling 64-bit binaries on
  57    * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
  58    */
  59   BitVector(unsigned size, uint64_t z) : d_size(size), d_value(z)
  60   {
  61     d_value = d_value.modByPow2(size);
  62   }
  63
  64   BitVector(unsigned size, const BitVector& q)
  65       : d_size(size), d_value(q.d_value)
  66   {
  67   }
  68
  69   /**
  70    * BitVector constructor.
  71    *
  72    * The value of the bit-vector is passed in as string of base 2, 10 or 16.
  73    * The size of resulting bit-vector is
  74    * - base  2: the size of the binary string
  75    * - base 10: the min. size required to represent the decimal as a bit-vector
  76    * - base 16: the max. size required to represent the hexadecimal as a
  77    *            bit-vector (4 * size of the given value string)
  78    *
  79    * @param num The value of the bit-vector in string representation.
  80    * @param base The base of the string representation.
  81    */
  82   BitVector(const std::string& num, unsigned base = 2)
  83   {
  84     CheckArgument(base == 2 || base == 10 || base == 16, base);
  85     d_value = Integer(num, base);
  86     switch (base)
  87     {
  88       case 10: d_size = d_value.length(); break;
  89       case 16: d_size = num.size() * 4; break;
  90       default: d_size = num.size();
  91     }
  92   }
  93
  94   ~BitVector() {}
  95
  96   BitVector& operator=(const BitVector& x)
  97   {
  98     if (this == &x) return *this;
  99     d_size = x.d_size;
 100     d_value = x.d_value;
 101     return *this;
 102   }
 103
 104   /* Get size (bit-width). */
 105   unsigned getSize() const;
 106   /* Get value. */
 107   const Integer& getValue() const;
 108
 109   /* Return value. */
 110   Integer toInteger() const;
 111   /* Return Integer corresponding to two's complement interpretation of this. */
 112   Integer toSignedInteger() const;
 113   /* Return (binary) string representation. */
 114   std::string toString(unsigned int base = 2) const;
 115
 116   /* Return hash value. */
 117   size_t hash() const;
 118
 119   /* Set bit at index 'i'. */
 120   BitVector setBit(uint32_t i) const;
 121   /* Return true if bit at index 'i' is set. */
 122   bool isBitSet(uint32_t i) const;
 123
 124   /* Return k if the value of this is equal to 2^{k-1}, and zero otherwise. */
 125   unsigned isPow2() const;
 126
 127   /* -----------------------------------------------------------------------
 128    ** Operators
 129    * ----------------------------------------------------------------------- */
 130
 131   /* String Operations ----------------------------------------------------- */
 132
 133   /* Return the concatenation of this and bit-vector 'other'. */
 134   BitVector concat(const BitVector& other) const;
 135
 136   /* Return the bit range from index 'high' to index 'low'. */
 137   BitVector extract(unsigned high, unsigned low) const;
 138
 139   /* (Dis)Equality --------------------------------------------------------- */
 140
 141   /* Return true if this is equal to 'y'. */
 142   bool operator==(const BitVector& y) const;
 143
 144   /* Return true if this is not equal to 'y'. */
 145   bool operator!=(const BitVector& y) const;
 146
 147   /* Unsigned Inequality --------------------------------------------------- */
 148
 149   /* Return true if this is unsigned less than bit-vector 'y'. */
 150   bool operator<(const BitVector& y) const;
 151
 152   /* Return true if this is unsigned less than or equal to bit-vector 'y'. */
 153   bool operator<=(const BitVector& y) const;
 154
 155   /* Return true if this is unsigned greater than bit-vector 'y'. */
 156   bool operator>(const BitVector& y) const;
 157
 158   /* Return true if this is unsigned greater than or equal to bit-vector 'y'. */
 159   bool operator>=(const BitVector& y) const;
 160
 161   /* Return true if this is unsigned less than bit-vector 'y'.
 162    * This function is a synonym for operator < but performs additional
 163    * argument checks.*/
 164   bool unsignedLessThan(const BitVector& y) const;
 165
 166   /* Return true if this is unsigned less than or equal to bit-vector 'y'.
 167    * This function is a synonym for operator >= but performs additional
 168    * argument checks.*/
 169   bool unsignedLessThanEq(const BitVector& y) const;
 170
 171   /* Signed Inequality ----------------------------------------------------- */
 172
 173   /* Return true if this is signed less than bit-vector 'y'. */
 174   bool signedLessThan(const BitVector& y) const;
 175
 176   /* Return true if this is signed less than or equal to bit-vector 'y'. */
 177   bool signedLessThanEq(const BitVector& y) const;
 178
 179   /* Bit-wise operations --------------------------------------------------- */
 180
 181   /* Return a bit-vector representing the bit-wise xor (this ^ y). */
 182   BitVector operator^(const BitVector& y) const;
 183
 184   /* Return a bit-vector representing the bit-wise or (this | y). */
 185   BitVector operator|(const BitVector& y) const;
 186
 187   /* Return a bit-vector representing the bit-wise and (this & y). */
 188   BitVector operator&(const BitVector& y) const;
 189
 190   /* Return a bit-vector representing the bit-wise not of this. */
 191   BitVector operator~() const;
 192
 193   /* Arithmetic operations ------------------------------------------------- */
 194
 195   /* Return a bit-vector representing the addition (this + y). */
 196   BitVector operator+(const BitVector& y) const;
 197
 198   /* Return a bit-vector representing the subtraction (this - y). */
 199   BitVector operator-(const BitVector& y) const;
 200
 201   /* Return a bit-vector representing the negation of this. */
 202   BitVector operator-() const;
 203
 204   /* Return a bit-vector representing the multiplication (this * y). */
 205   BitVector operator*(const BitVector& y) const;
 206
 207   /* Total division function.
 208    * Returns a bit-vector representing 2^d_size-1 (signed: -1) when the
 209    * denominator is zero, and a bit-vector representing the unsigned division
 210    * (this / y), otherwise.  */
 211   BitVector unsignedDivTotal(const BitVector& y) const;
 212
 213   /* Total remainder function.
 214    * Returns this when the denominator is zero, and the unsigned remainder
 215    * (this % y), otherwise.  */
 216   BitVector unsignedRemTotal(const BitVector& y) const;
 217
 218   /* Extend operations ----------------------------------------------------- */
 219
 220   /* Return a bit-vector representing this extended by 'n' zero bits. */
 221   BitVector zeroExtend(unsigned n) const;
 222
 223   /* Return a bit-vector representing this extended by 'n' bits of the value
 224    * of the signed bit. */
 225   BitVector signExtend(unsigned n) const;
 226
 227   /* Shift operations ------------------------------------------------------ */
 228
 229   /* Return a bit-vector representing a left shift of this by 'y'. */
 230   BitVector leftShift(const BitVector& y) const;
 231
 232   /* Return a bit-vector representing a logical right shift of this by 'y'. */
 233   BitVector logicalRightShift(const BitVector& y) const;
 234
 235   /* Return a bit-vector representing an arithmetic right shift of this
 236    * by 'y'.*/
 237   BitVector arithRightShift(const BitVector& y) const;
 238
 239   /* -----------------------------------------------------------------------
 240    ** Static helpers.
 241    * ----------------------------------------------------------------------- */
 242
 243   /* Create zero bit-vector of given size. */
 244   static BitVector mkZero(unsigned size);
 245
 246   /* Create bit-vector representing value 1 of given size. */
 247   static BitVector mkOne(unsigned size);
 248
 249   /* Create bit-vector of ones of given size. */
 250   static BitVector mkOnes(unsigned size);
 251
 252   /* Create bit-vector representing the minimum signed value of given size. */
 253   static BitVector mkMinSigned(unsigned size);
 254
 255   /* Create bit-vector representing the maximum signed value of given size. */
 256   static BitVector mkMaxSigned(unsigned size);
 257
 258  private:
 259   /**
 260    * Class invariants:
 261    *  - no overflows: 2^d_size < d_value
 262    *  - no negative numbers: d_value >= 0
 263    */
 264
 265   unsigned d_size;
 266   Integer d_value;
 267
 268 }; /* class BitVector */
 269
 270 /* -----------------------------------------------------------------------
 271  ** BitVector structs
 272  * ----------------------------------------------------------------------- */
 273
 274 /**
 275  * The structure representing the extraction operation for bit-vectors. The
 276  * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
 277  * by taking the bits at indices <code>high ... low</code>
 278  */
 279 struct CVC4_PUBLIC BitVectorExtract
 280 {
 281   /** The high bit of the range for this extract */
 282   unsigned d_high;
 283   /** The low bit of the range for this extract */
 284   unsigned d_low;
 285
 286   BitVectorExtract(unsigned high, unsigned low) : d_high(high), d_low(low) {}
 287
 288   bool operator==(const BitVectorExtract& extract) const
 289   {
 290     return d_high == extract.d_high && d_low == extract.d_low;
 291   }
 292 }; /* struct BitVectorExtract */
 293
 294 /**
 295  * The structure representing the extraction of one Boolean bit.
 296  */
 297 struct CVC4_PUBLIC BitVectorBitOf
 298 {
 299   /** The index of the bit */
 300   unsigned d_bitIndex;
 301   BitVectorBitOf(unsigned i) : d_bitIndex(i) {}
 302
 303   bool operator==(const BitVectorBitOf& other) const
 304   {
 305     return d_bitIndex == other.d_bitIndex;
 306   }
 307 }; /* struct BitVectorBitOf */
 308
 309 struct CVC4_PUBLIC BitVectorSize
 310 {
 311   unsigned d_size;
 312   BitVectorSize(unsigned size) : d_size(size) {}
 313   operator unsigned() const { return d_size; }
 314 }; /* struct BitVectorSize */
 315
 316 struct CVC4_PUBLIC BitVectorRepeat
 317 {
 318   unsigned d_repeatAmount;
 319   BitVectorRepeat(unsigned repeatAmount) : d_repeatAmount(repeatAmount) {}
 320   operator unsigned() const { return d_repeatAmount; }
 321 }; /* struct BitVectorRepeat */
 322
 323 struct CVC4_PUBLIC BitVectorZeroExtend
 324 {
 325   unsigned d_zeroExtendAmount;
 326   BitVectorZeroExtend(unsigned zeroExtendAmount)
 327       : d_zeroExtendAmount(zeroExtendAmount)
 328   {
 329   }
 330   operator unsigned() const { return d_zeroExtendAmount; }
 331 }; /* struct BitVectorZeroExtend */
 332
 333 struct CVC4_PUBLIC BitVectorSignExtend
 334 {
 335   unsigned d_signExtendAmount;
 336   BitVectorSignExtend(unsigned signExtendAmount)
 337       : d_signExtendAmount(signExtendAmount)
 338   {
 339   }
 340   operator unsigned() const { return d_signExtendAmount; }
 341 }; /* struct BitVectorSignExtend */
 342
 343 struct CVC4_PUBLIC BitVectorRotateLeft
 344 {
 345   unsigned d_rotateLeftAmount;
 346   BitVectorRotateLeft(unsigned rotateLeftAmount)
 347       : d_rotateLeftAmount(rotateLeftAmount)
 348   {
 349   }
 350   operator unsigned() const { return d_rotateLeftAmount; }
 351 }; /* struct BitVectorRotateLeft */
 352
 353 struct CVC4_PUBLIC BitVectorRotateRight
 354 {
 355   unsigned d_rotateRightAmount;
 356   BitVectorRotateRight(unsigned rotateRightAmount)
 357       : d_rotateRightAmount(rotateRightAmount)
 358   {
 359   }
 360   operator unsigned() const { return d_rotateRightAmount; }
 361 }; /* struct BitVectorRotateRight */
 362
 363 struct CVC4_PUBLIC IntToBitVector
 364 {
 365   unsigned d_size;
 366   IntToBitVector(unsigned size) : d_size(size) {}
 367   operator unsigned() const { return d_size; }
 368 }; /* struct IntToBitVector */
 369
 370 /* -----------------------------------------------------------------------
 371  ** Hash Function structs
 372  * ----------------------------------------------------------------------- */
 373
 374 /*
 375  * Hash function for the BitVector constants.
 376  */
 377 struct CVC4_PUBLIC BitVectorHashFunction
 378 {
 379   inline size_t operator()(const BitVector& bv) const { return bv.hash(); }
 380 }; /* struct BitVectorHashFunction */
 381
 382 /**
 383  * Hash function for the BitVectorExtract objects.
 384  */
 385 struct CVC4_PUBLIC BitVectorExtractHashFunction
 386 {
 387   size_t operator()(const BitVectorExtract& extract) const
 388   {
 389     size_t hash = extract.d_low;
 390     hash ^= extract.d_high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 391     return hash;
 392   }
 393 }; /* struct BitVectorExtractHashFunction */
 394
 395 /**
 396  * Hash function for the BitVectorBitOf objects.
 397  */
 398 struct CVC4_PUBLIC BitVectorBitOfHashFunction
 399 {
 400   size_t operator()(const BitVectorBitOf& b) const { return b.d_bitIndex; }
 401 }; /* struct BitVectorBitOfHashFunction */
 402
 403 template <typename T>
 404 struct CVC4_PUBLIC UnsignedHashFunction
 405 {
 406   inline size_t operator()(const T& x) const { return (size_t)x; }
 407 }; /* struct UnsignedHashFunction */
 408
 409 /* -----------------------------------------------------------------------
 410  ** Output stream
 411  * ----------------------------------------------------------------------- */
 412
 413 inline std::ostream& operator<<(std::ostream& os,
 414                                 const BitVector& bv) CVC4_PUBLIC;
 415 inline std::ostream& operator<<(std::ostream& os, const BitVector& bv)
 416 {
 417   return os << bv.toString();
 418 }
 419
 420 inline std::ostream& operator<<(std::ostream& os,
 421                                 const BitVectorExtract& bv) CVC4_PUBLIC;
 422 inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv)
 423 {
 424   return os << "[" << bv.d_high << ":" << bv.d_low << "]";
 425 }
 426
 427 inline std::ostream& operator<<(std::ostream& os,
 428                                 const BitVectorBitOf& bv) CVC4_PUBLIC;
 429 inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv)
 430 {
 431   return os << "[" << bv.d_bitIndex << "]";
 432 }
 433
 434 inline std::ostream& operator<<(std::ostream& os,
 435                                 const IntToBitVector& bv) CVC4_PUBLIC;
 436 inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv)
 437 {
 438   return os << "[" << bv.d_size << "]";
 439 }
 440
 441 }  // namespace CVC4
 442
 443 #endif /* CVC4__BITVECTOR_H */