Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/bitvector.h	Lines:	70	74	94.6 %
Date:	2021-08-14	Branches:	30	41	73.2 %


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