src/util/bitvector.h

   1 /*********************                                                        */
   2 /*! \file bitvector.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Dejan Jovanovic, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 bit-vector of ones of given size. */
 244   static BitVector mkOnes(unsigned size);
 245
 246   /* Create bit-vector representing the minimum signed value of given size. */
 247   static BitVector mkMinSigned(unsigned size);
 248
 249   /* Create bit-vector representing the maximum signed value of given size. */
 250   static BitVector mkMaxSigned(unsigned size);
 251
 252  private:
 253   /**
 254    * Class invariants:
 255    *  - no overflows: 2^d_size < d_value
 256    *  - no negative numbers: d_value >= 0
 257    */
 258
 259   unsigned d_size;
 260   Integer d_value;
 261
 262 }; /* class BitVector */
 263
 264 /* -----------------------------------------------------------------------
 265  ** BitVector structs
 266  * ----------------------------------------------------------------------- */
 267
 268 /**
 269  * The structure representing the extraction operation for bit-vectors. The
 270  * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
 271  * by taking the bits at indices <code>high ... low</code>
 272  */
 273 struct CVC4_PUBLIC BitVectorExtract
 274 {
 275   /** The high bit of the range for this extract */
 276   unsigned high;
 277   /** The low bit of the range for this extract */
 278   unsigned low;
 279
 280   BitVectorExtract(unsigned high, unsigned low) : high(high), low(low) {}
 281
 282   bool operator==(const BitVectorExtract& extract) const
 283   {
 284     return high == extract.high && low == extract.low;
 285   }
 286 }; /* struct BitVectorExtract */
 287
 288 /**
 289  * The structure representing the extraction of one Boolean bit.
 290  */
 291 struct CVC4_PUBLIC BitVectorBitOf
 292 {
 293   /** The index of the bit */
 294   unsigned bitIndex;
 295   BitVectorBitOf(unsigned i) : bitIndex(i) {}
 296
 297   bool operator==(const BitVectorBitOf& other) const
 298   {
 299     return bitIndex == other.bitIndex;
 300   }
 301 }; /* struct BitVectorBitOf */
 302
 303 struct CVC4_PUBLIC BitVectorSize
 304 {
 305   unsigned size;
 306   BitVectorSize(unsigned size) : size(size) {}
 307   operator unsigned() const { return size; }
 308 }; /* struct BitVectorSize */
 309
 310 struct CVC4_PUBLIC BitVectorRepeat
 311 {
 312   unsigned repeatAmount;
 313   BitVectorRepeat(unsigned repeatAmount) : repeatAmount(repeatAmount) {}
 314   operator unsigned() const { return repeatAmount; }
 315 }; /* struct BitVectorRepeat */
 316
 317 struct CVC4_PUBLIC BitVectorZeroExtend
 318 {
 319   unsigned zeroExtendAmount;
 320   BitVectorZeroExtend(unsigned zeroExtendAmount)
 321       : zeroExtendAmount(zeroExtendAmount)
 322   {
 323   }
 324   operator unsigned() const { return zeroExtendAmount; }
 325 }; /* struct BitVectorZeroExtend */
 326
 327 struct CVC4_PUBLIC BitVectorSignExtend
 328 {
 329   unsigned signExtendAmount;
 330   BitVectorSignExtend(unsigned signExtendAmount)
 331       : signExtendAmount(signExtendAmount)
 332   {
 333   }
 334   operator unsigned() const { return signExtendAmount; }
 335 }; /* struct BitVectorSignExtend */
 336
 337 struct CVC4_PUBLIC BitVectorRotateLeft
 338 {
 339   unsigned rotateLeftAmount;
 340   BitVectorRotateLeft(unsigned rotateLeftAmount)
 341       : rotateLeftAmount(rotateLeftAmount)
 342   {
 343   }
 344   operator unsigned() const { return rotateLeftAmount; }
 345 }; /* struct BitVectorRotateLeft */
 346
 347 struct CVC4_PUBLIC BitVectorRotateRight
 348 {
 349   unsigned rotateRightAmount;
 350   BitVectorRotateRight(unsigned rotateRightAmount)
 351       : rotateRightAmount(rotateRightAmount)
 352   {
 353   }
 354   operator unsigned() const { return rotateRightAmount; }
 355 }; /* struct BitVectorRotateRight */
 356
 357 struct CVC4_PUBLIC IntToBitVector
 358 {
 359   unsigned size;
 360   IntToBitVector(unsigned size) : size(size) {}
 361   operator unsigned() const { return size; }
 362 }; /* struct IntToBitVector */
 363
 364 /* -----------------------------------------------------------------------
 365  ** Hash Function structs
 366  * ----------------------------------------------------------------------- */
 367
 368 /*
 369  * Hash function for the BitVector constants.
 370  */
 371 struct CVC4_PUBLIC BitVectorHashFunction
 372 {
 373   inline size_t operator()(const BitVector& bv) const { return bv.hash(); }
 374 }; /* struct BitVectorHashFunction */
 375
 376 /**
 377  * Hash function for the BitVectorExtract objects.
 378  */
 379 struct CVC4_PUBLIC BitVectorExtractHashFunction
 380 {
 381   size_t operator()(const BitVectorExtract& extract) const
 382   {
 383     size_t hash = extract.low;
 384     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
 385     return hash;
 386   }
 387 }; /* struct BitVectorExtractHashFunction */
 388
 389 /**
 390  * Hash function for the BitVectorBitOf objects.
 391  */
 392 struct CVC4_PUBLIC BitVectorBitOfHashFunction
 393 {
 394   size_t operator()(const BitVectorBitOf& b) const { return b.bitIndex; }
 395 }; /* struct BitVectorBitOfHashFunction */
 396
 397 template <typename T>
 398 struct CVC4_PUBLIC UnsignedHashFunction
 399 {
 400   inline size_t operator()(const T& x) const { return (size_t)x; }
 401 }; /* struct UnsignedHashFunction */
 402
 403 /* -----------------------------------------------------------------------
 404  ** Output stream
 405  * ----------------------------------------------------------------------- */
 406
 407 inline std::ostream& operator<<(std::ostream& os,
 408                                 const BitVector& bv) CVC4_PUBLIC;
 409 inline std::ostream& operator<<(std::ostream& os, const BitVector& bv)
 410 {
 411   return os << bv.toString();
 412 }
 413
 414 inline std::ostream& operator<<(std::ostream& os,
 415                                 const BitVectorExtract& bv) CVC4_PUBLIC;
 416 inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv)
 417 {
 418   return os << "[" << bv.high << ":" << bv.low << "]";
 419 }
 420
 421 inline std::ostream& operator<<(std::ostream& os,
 422                                 const BitVectorBitOf& bv) CVC4_PUBLIC;
 423 inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv)
 424 {
 425   return os << "[" << bv.bitIndex << "]";
 426 }
 427
 428 inline std::ostream& operator<<(std::ostream& os,
 429                                 const IntToBitVector& bv) CVC4_PUBLIC;
 430 inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv)
 431 {
 432   return os << "[" << bv.size << "]";
 433 }
 434
 435 }  // namespace CVC4
 436
 437 #endif /* CVC4__BITVECTOR_H */