Branch data     Line data    Source code

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