Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/bitvector.h	Lines:	68	72	94.4 %
Date:	2021-08-01	Branches:	23	33	69.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Andres Noetzli, Dejan Jovanovic
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * A fixed-size bit-vector, implemented as a wrapper around Integer.
 */

#include "cvc5_public.h"

#ifndef CVC5__BITVECTOR_H
#define CVC5__BITVECTOR_H

#include <iosfwd>
#include <iostream>

#include "base/exception.h"
#include "util/integer.h"

namespace cvc5 {

class BitVector
{
 public:
  BitVector(unsigned size, const Integer& val)
      : d_size(size), d_value(val.modByPow2(size))
  {
  }

  BitVector(unsigned size = 0) : d_size(size), d_value(0) {}

  /**
   * BitVector constructor using a 32-bit unsigned integer for the value.
   *
   * Note: we use an explicit bit-width here to be consistent across
   * platforms (long is 32-bit when compiling 64-bit binaries on
   * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
   */
  BitVector(unsigned size, uint32_t z) : d_size(size), d_value(z)
  {
    d_value = d_value.modByPow2(size);
  }

  /**
   * BitVector constructor using a 64-bit unsigned integer for the value.
   *
   * Note: we use an explicit bit-width here to be consistent across
   * platforms (long is 32-bit when compiling 64-bit binaries on
   * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
   */
  BitVector(unsigned size, uint64_t z) : d_size(size), d_value(z)
  {
    d_value = d_value.modByPow2(size);
  }

  BitVector(unsigned size, const BitVector& q)
      : d_size(size), d_value(q.d_value)
  {
  }

  /**
   * BitVector constructor.
   *
   * The value of the bit-vector is passed in as string of base 2, 10 or 16.
   * The size of resulting bit-vector is
   * - base  2: the size of the binary string
   * - base 10: the min. size required to represent the decimal as a bit-vector
   * - base 16: the max. size required to represent the hexadecimal as a
   *            bit-vector (4 * size of the given value string)
   *
   * @param num The value of the bit-vector in string representation.
   * @param base The base of the string representation.
   */
  BitVector(const std::string& num, unsigned base = 2)
  {
    CheckArgument(base == 2 || base == 10 || base == 16, base);
    d_value = Integer(num, base);
    switch (base)
    {
      case 10: d_size = d_value.length(); break;
      case 16: d_size = num.size() * 4; break;
      default: d_size = num.size();
    }
  }

  ~BitVector() {}

  BitVector& operator=(const BitVector& x)
  {
    if (this == &x) return *this;
    d_size = x.d_size;
    d_value = x.d_value;
    return *this;
  }

  /* Get size (bit-width). */
  unsigned getSize() const;
  /* Get value. */
  const Integer& getValue() const;

  /* Return value. */
  Integer toInteger() const;
  /* Return Integer corresponding to two's complement interpretation of this. */
  Integer toSignedInteger() const;
  /* Return (binary) string representation. */
  std::string toString(unsigned int base = 2) const;

  /* Return hash value. */
  size_t hash() const;

  /**
   * Set bit at index 'i' to given value.
   * Returns a reference to this bit-vector to allow for chaining.
   *
   * value: True to set bit to 1, and false to set it to 0.
   *
   * Note: Least significant bit is at index 0.
   */
  BitVector& setBit(uint32_t i, bool value);

  /** Return true if bit at index 'i' is 1, and false otherwise. */
  bool isBitSet(uint32_t i) const;

  /* Return k if the value of this is equal to 2^{k-1}, and zero otherwise. */
  unsigned isPow2() const;

  /* -----------------------------------------------------------------------
   ** Operators
   * ----------------------------------------------------------------------- */

  /* String Operations ----------------------------------------------------- */

  /* Return the concatenation of this and bit-vector 'other'. */
  BitVector concat(const BitVector& other) const;

  /* Return the bit range from index 'high' to index 'low'. */
  BitVector extract(unsigned high, unsigned low) const;

  /* (Dis)Equality --------------------------------------------------------- */

  /* Return true if this is equal to 'y'. */
  bool operator==(const BitVector& y) const;

  /* Return true if this is not equal to 'y'. */
  bool operator!=(const BitVector& y) const;

  /* Unsigned Inequality --------------------------------------------------- */

  /* Return true if this is unsigned less than bit-vector 'y'. */
  bool operator<(const BitVector& y) const;

  /* Return true if this is unsigned less than or equal to bit-vector 'y'. */
  bool operator<=(const BitVector& y) const;

  /* Return true if this is unsigned greater than bit-vector 'y'. */
  bool operator>(const BitVector& y) const;

  /* Return true if this is unsigned greater than or equal to bit-vector 'y'. */
  bool operator>=(const BitVector& y) const;

  /* Return true if this is unsigned less than bit-vector 'y'.
   * This function is a synonym for operator < but performs additional
   * argument checks.*/
  bool unsignedLessThan(const BitVector& y) const;

  /* Return true if this is unsigned less than or equal to bit-vector 'y'.
   * This function is a synonym for operator >= but performs additional
   * argument checks.*/
  bool unsignedLessThanEq(const BitVector& y) const;

  /* Signed Inequality ----------------------------------------------------- */

  /* Return true if this is signed less than bit-vector 'y'. */
  bool signedLessThan(const BitVector& y) const;

  /* Return true if this is signed less than or equal to bit-vector 'y'. */
  bool signedLessThanEq(const BitVector& y) const;

  /* Bit-wise operations --------------------------------------------------- */

  /* Return a bit-vector representing the bit-wise xor (this ^ y). */
  BitVector operator^(const BitVector& y) const;

  /* Return a bit-vector representing the bit-wise or (this | y). */
  BitVector operator|(const BitVector& y) const;

  /* Return a bit-vector representing the bit-wise and (this & y). */
  BitVector operator&(const BitVector& y) const;

  /* Return a bit-vector representing the bit-wise not of this. */
  BitVector operator~() const;

  /* Arithmetic operations ------------------------------------------------- */

  /* Return a bit-vector representing the addition (this + y). */
  BitVector operator+(const BitVector& y) const;

  /* Return a bit-vector representing the subtraction (this - y). */
  BitVector operator-(const BitVector& y) const;

  /* Return a bit-vector representing the negation of this. */
  BitVector operator-() const;

  /* Return a bit-vector representing the multiplication (this * y). */
  BitVector operator*(const BitVector& y) const;

  /* Total division function.
   * Returns a bit-vector representing 2^d_size-1 (signed: -1) when the
   * denominator is zero, and a bit-vector representing the unsigned division
   * (this / y), otherwise.  */
  BitVector unsignedDivTotal(const BitVector& y) const;

  /* Total remainder function.
   * Returns this when the denominator is zero, and the unsigned remainder
   * (this % y), otherwise.  */
  BitVector unsignedRemTotal(const BitVector& y) const;

  /* Extend operations ----------------------------------------------------- */

  /* Return a bit-vector representing this extended by 'n' zero bits. */
  BitVector zeroExtend(unsigned n) const;

  /* Return a bit-vector representing this extended by 'n' bits of the value
   * of the signed bit. */
  BitVector signExtend(unsigned n) const;

  /* Shift operations ------------------------------------------------------ */

  /* Return a bit-vector representing a left shift of this by 'y'. */
  BitVector leftShift(const BitVector& y) const;

  /* Return a bit-vector representing a logical right shift of this by 'y'. */
  BitVector logicalRightShift(const BitVector& y) const;

  /* Return a bit-vector representing an arithmetic right shift of this
   * by 'y'.*/
  BitVector arithRightShift(const BitVector& y) const;

  /* -----------------------------------------------------------------------
   ** Static helpers.
   * ----------------------------------------------------------------------- */

  /* Create zero bit-vector of given size. */
  static BitVector mkZero(unsigned size);

  /* Create bit-vector representing value 1 of given size. */
  static BitVector mkOne(unsigned size);

  /* Create bit-vector of ones of given size. */
  static BitVector mkOnes(unsigned size);

  /* Create bit-vector representing the minimum signed value of given size. */
  static BitVector mkMinSigned(unsigned size);

  /* Create bit-vector representing the maximum signed value of given size. */
  static BitVector mkMaxSigned(unsigned size);

 private:
  /**
   * Class invariants:
   *  - no overflows: 2^d_size < d_value
   *  - no negative numbers: d_value >= 0
   */

  unsigned d_size;
  Integer d_value;

}; /* class BitVector */

/* -----------------------------------------------------------------------
 * BitVector structs
 * ----------------------------------------------------------------------- */

/**
 * The structure representing the extraction operation for bit-vectors. The
 * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
 * by taking the bits at indices <code>high ... low</code>
 */
struct BitVectorExtract
{
  /** The high bit of the range for this extract */
  unsigned d_high;
  /** The low bit of the range for this extract */
  unsigned d_low;

  BitVectorExtract(unsigned high, unsigned low) : d_high(high), d_low(low) {}

  bool operator==(const BitVectorExtract& extract) const
  {
    return d_high == extract.d_high && d_low == extract.d_low;
  }
}; /* struct BitVectorExtract */

/**
 * The structure representing the extraction of one Boolean bit.
 */
struct BitVectorBitOf
{
  /** The index of the bit */
  unsigned d_bitIndex;
  BitVectorBitOf(unsigned i) : d_bitIndex(i) {}

  bool operator==(const BitVectorBitOf& other) const
  {
    return d_bitIndex == other.d_bitIndex;
  }
}; /* struct BitVectorBitOf */

struct BitVectorSize
{
  unsigned d_size;
  BitVectorSize(unsigned size) : d_size(size) {}
  operator unsigned() const { return d_size; }
}; /* struct BitVectorSize */

struct BitVectorRepeat
{
  unsigned d_repeatAmount;
  BitVectorRepeat(unsigned repeatAmount) : d_repeatAmount(repeatAmount) {}
  operator unsigned() const { return d_repeatAmount; }
}; /* struct BitVectorRepeat */

struct BitVectorZeroExtend
{
  unsigned d_zeroExtendAmount;
  BitVectorZeroExtend(unsigned zeroExtendAmount)
      : d_zeroExtendAmount(zeroExtendAmount)
  {
  }
  operator unsigned() const { return d_zeroExtendAmount; }
}; /* struct BitVectorZeroExtend */

struct BitVectorSignExtend
{
  unsigned d_signExtendAmount;
  BitVectorSignExtend(unsigned signExtendAmount)
      : d_signExtendAmount(signExtendAmount)
  {
  }
  operator unsigned() const { return d_signExtendAmount; }
}; /* struct BitVectorSignExtend */

struct BitVectorRotateLeft
{
  unsigned d_rotateLeftAmount;
  BitVectorRotateLeft(unsigned rotateLeftAmount)
      : d_rotateLeftAmount(rotateLeftAmount)
  {
  }
  operator unsigned() const { return d_rotateLeftAmount; }
}; /* struct BitVectorRotateLeft */

struct BitVectorRotateRight
{
  unsigned d_rotateRightAmount;
  BitVectorRotateRight(unsigned rotateRightAmount)
      : d_rotateRightAmount(rotateRightAmount)
  {
  }
  operator unsigned() const { return d_rotateRightAmount; }
}; /* struct BitVectorRotateRight */

struct IntToBitVector
{
  unsigned d_size;
  IntToBitVector(unsigned size) : d_size(size) {}
  operator unsigned() const { return d_size; }
}; /* struct IntToBitVector */

/* -----------------------------------------------------------------------
 * Hash Function structs
 * ----------------------------------------------------------------------- */

/*
 * Hash function for the BitVector constants.
 */
struct BitVectorHashFunction
{
  inline size_t operator()(const BitVector& bv) const { return bv.hash(); }
}; /* struct BitVectorHashFunction */

/**
 * Hash function for the BitVectorExtract objects.
 */
struct BitVectorExtractHashFunction
{
  size_t operator()(const BitVectorExtract& extract) const
  {
    size_t hash = extract.d_low;
    hash ^= extract.d_high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
    return hash;
  }
}; /* struct BitVectorExtractHashFunction */

/**
 * Hash function for the BitVectorBitOf objects.
 */
struct BitVectorBitOfHashFunction
{
  size_t operator()(const BitVectorBitOf& b) const { return b.d_bitIndex; }
}; /* struct BitVectorBitOfHashFunction */

template <typename T>
struct UnsignedHashFunction
{
  inline size_t operator()(const T& x) const { return (size_t)x; }
}; /* struct UnsignedHashFunction */

/* -----------------------------------------------------------------------
 * Output stream
 * ----------------------------------------------------------------------- */

inline std::ostream& operator<<(std::ostream& os, const BitVector& bv);
inline std::ostream& operator<<(std::ostream& os, const BitVector& bv)
{
  return os << bv.toString();
}

inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv);
inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv)
{
  return os << "[" << bv.d_high << ":" << bv.d_low << "]";
}

inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv);
inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv)
{
  return os << "[" << bv.d_bitIndex << "]";
}

inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv);
inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv)
{
  return os << "[" << bv.d_size << "]";
}

}  // namespace cvc5

#endif /* CVC5__BITVECTOR_H */


Generated by: GCOVR (Version 3.2)

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