1 /********************* */
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Andres Noetzli, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief A fixed-size bit-vector.
14 ** A fixed-size bit-vector, implemented as a wrapper around Integer.
17 #include "cvc4_public.h"
19 #ifndef CVC4__BITVECTOR_H
20 #define CVC4__BITVECTOR_H
25 #include "base/exception.h"
26 #include "util/integer.h"
30 class CVC4_PUBLIC BitVector
33 BitVector(unsigned size
, const Integer
& val
)
34 : d_size(size
), d_value(val
.modByPow2(size
))
38 BitVector(unsigned size
= 0) : d_size(size
), d_value(0) {}
41 * BitVector constructor using a 32-bit unsigned integer for the value.
43 * Note: we use an explicit bit-width here to be consistent across
44 * platforms (long is 32-bit when compiling 64-bit binaries on
45 * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
47 BitVector(unsigned size
, uint32_t z
) : d_size(size
), d_value(z
)
49 d_value
= d_value
.modByPow2(size
);
53 * BitVector constructor using a 64-bit unsigned integer for the value.
55 * Note: we use an explicit bit-width here to be consistent across
56 * platforms (long is 32-bit when compiling 64-bit binaries on
57 * Windows but 64-bit on Linux) and to prevent ambiguous overloads.
59 BitVector(unsigned size
, uint64_t z
) : d_size(size
), d_value(z
)
61 d_value
= d_value
.modByPow2(size
);
64 BitVector(unsigned size
, const BitVector
& q
)
65 : d_size(size
), d_value(q
.d_value
)
70 * BitVector constructor.
72 * The value of the bit-vector is passed in as string of base 2, 10 or 16.
73 * The size of resulting bit-vector is
74 * - base 2: the size of the binary string
75 * - base 10: the min. size required to represent the decimal as a bit-vector
76 * - base 16: the max. size required to represent the hexadecimal as a
77 * bit-vector (4 * size of the given value string)
79 * @param num The value of the bit-vector in string representation.
80 * @param base The base of the string representation.
82 BitVector(const std::string
& num
, unsigned base
= 2)
84 CheckArgument(base
== 2 || base
== 10 || base
== 16, base
);
85 d_value
= Integer(num
, base
);
88 case 10: d_size
= d_value
.length(); break;
89 case 16: d_size
= num
.size() * 4; break;
90 default: d_size
= num
.size();
96 BitVector
& operator=(const BitVector
& x
)
98 if (this == &x
) return *this;
104 /* Get size (bit-width). */
105 unsigned getSize() const;
107 const Integer
& getValue() const;
110 Integer
toInteger() const;
111 /* Return Integer corresponding to two's complement interpretation of this. */
112 Integer
toSignedInteger() const;
113 /* Return (binary) string representation. */
114 std::string
toString(unsigned int base
= 2) const;
116 /* Return hash value. */
119 /* Set bit at index 'i'. */
120 BitVector
setBit(uint32_t i
) const;
121 /* Return true if bit at index 'i' is set. */
122 bool isBitSet(uint32_t i
) const;
124 /* Return k if the value of this is equal to 2^{k-1}, and zero otherwise. */
125 unsigned isPow2() const;
127 /* -----------------------------------------------------------------------
129 * ----------------------------------------------------------------------- */
131 /* String Operations ----------------------------------------------------- */
133 /* Return the concatenation of this and bit-vector 'other'. */
134 BitVector
concat(const BitVector
& other
) const;
136 /* Return the bit range from index 'high' to index 'low'. */
137 BitVector
extract(unsigned high
, unsigned low
) const;
139 /* (Dis)Equality --------------------------------------------------------- */
141 /* Return true if this is equal to 'y'. */
142 bool operator==(const BitVector
& y
) const;
144 /* Return true if this is not equal to 'y'. */
145 bool operator!=(const BitVector
& y
) const;
147 /* Unsigned Inequality --------------------------------------------------- */
149 /* Return true if this is unsigned less than bit-vector 'y'. */
150 bool operator<(const BitVector
& y
) const;
152 /* Return true if this is unsigned less than or equal to bit-vector 'y'. */
153 bool operator<=(const BitVector
& y
) const;
155 /* Return true if this is unsigned greater than bit-vector 'y'. */
156 bool operator>(const BitVector
& y
) const;
158 /* Return true if this is unsigned greater than or equal to bit-vector 'y'. */
159 bool operator>=(const BitVector
& y
) const;
161 /* Return true if this is unsigned less than bit-vector 'y'.
162 * This function is a synonym for operator < but performs additional
164 bool unsignedLessThan(const BitVector
& y
) const;
166 /* Return true if this is unsigned less than or equal to bit-vector 'y'.
167 * This function is a synonym for operator >= but performs additional
169 bool unsignedLessThanEq(const BitVector
& y
) const;
171 /* Signed Inequality ----------------------------------------------------- */
173 /* Return true if this is signed less than bit-vector 'y'. */
174 bool signedLessThan(const BitVector
& y
) const;
176 /* Return true if this is signed less than or equal to bit-vector 'y'. */
177 bool signedLessThanEq(const BitVector
& y
) const;
179 /* Bit-wise operations --------------------------------------------------- */
181 /* Return a bit-vector representing the bit-wise xor (this ^ y). */
182 BitVector
operator^(const BitVector
& y
) const;
184 /* Return a bit-vector representing the bit-wise or (this | y). */
185 BitVector
operator|(const BitVector
& y
) const;
187 /* Return a bit-vector representing the bit-wise and (this & y). */
188 BitVector
operator&(const BitVector
& y
) const;
190 /* Return a bit-vector representing the bit-wise not of this. */
191 BitVector
operator~() const;
193 /* Arithmetic operations ------------------------------------------------- */
195 /* Return a bit-vector representing the addition (this + y). */
196 BitVector
operator+(const BitVector
& y
) const;
198 /* Return a bit-vector representing the subtraction (this - y). */
199 BitVector
operator-(const BitVector
& y
) const;
201 /* Return a bit-vector representing the negation of this. */
202 BitVector
operator-() const;
204 /* Return a bit-vector representing the multiplication (this * y). */
205 BitVector
operator*(const BitVector
& y
) const;
207 /* Total division function.
208 * Returns a bit-vector representing 2^d_size-1 (signed: -1) when the
209 * denominator is zero, and a bit-vector representing the unsigned division
210 * (this / y), otherwise. */
211 BitVector
unsignedDivTotal(const BitVector
& y
) const;
213 /* Total remainder function.
214 * Returns this when the denominator is zero, and the unsigned remainder
215 * (this % y), otherwise. */
216 BitVector
unsignedRemTotal(const BitVector
& y
) const;
218 /* Extend operations ----------------------------------------------------- */
220 /* Return a bit-vector representing this extended by 'n' zero bits. */
221 BitVector
zeroExtend(unsigned n
) const;
223 /* Return a bit-vector representing this extended by 'n' bits of the value
224 * of the signed bit. */
225 BitVector
signExtend(unsigned n
) const;
227 /* Shift operations ------------------------------------------------------ */
229 /* Return a bit-vector representing a left shift of this by 'y'. */
230 BitVector
leftShift(const BitVector
& y
) const;
232 /* Return a bit-vector representing a logical right shift of this by 'y'. */
233 BitVector
logicalRightShift(const BitVector
& y
) const;
235 /* Return a bit-vector representing an arithmetic right shift of this
237 BitVector
arithRightShift(const BitVector
& y
) const;
239 /* -----------------------------------------------------------------------
241 * ----------------------------------------------------------------------- */
243 /* Create zero bit-vector of given size. */
244 static BitVector
mkZero(unsigned size
);
246 /* Create bit-vector representing value 1 of given size. */
247 static BitVector
mkOne(unsigned size
);
249 /* Create bit-vector of ones of given size. */
250 static BitVector
mkOnes(unsigned size
);
252 /* Create bit-vector representing the minimum signed value of given size. */
253 static BitVector
mkMinSigned(unsigned size
);
255 /* Create bit-vector representing the maximum signed value of given size. */
256 static BitVector
mkMaxSigned(unsigned size
);
261 * - no overflows: 2^d_size < d_value
262 * - no negative numbers: d_value >= 0
268 }; /* class BitVector */
270 /* -----------------------------------------------------------------------
272 * ----------------------------------------------------------------------- */
275 * The structure representing the extraction operation for bit-vectors. The
276 * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
277 * by taking the bits at indices <code>high ... low</code>
279 struct CVC4_PUBLIC BitVectorExtract
281 /** The high bit of the range for this extract */
283 /** The low bit of the range for this extract */
286 BitVectorExtract(unsigned high
, unsigned low
) : d_high(high
), d_low(low
) {}
288 bool operator==(const BitVectorExtract
& extract
) const
290 return d_high
== extract
.d_high
&& d_low
== extract
.d_low
;
292 }; /* struct BitVectorExtract */
295 * The structure representing the extraction of one Boolean bit.
297 struct CVC4_PUBLIC BitVectorBitOf
299 /** The index of the bit */
301 BitVectorBitOf(unsigned i
) : d_bitIndex(i
) {}
303 bool operator==(const BitVectorBitOf
& other
) const
305 return d_bitIndex
== other
.d_bitIndex
;
307 }; /* struct BitVectorBitOf */
309 struct CVC4_PUBLIC BitVectorSize
312 BitVectorSize(unsigned size
) : d_size(size
) {}
313 operator unsigned() const { return d_size
; }
314 }; /* struct BitVectorSize */
316 struct CVC4_PUBLIC BitVectorRepeat
318 unsigned d_repeatAmount
;
319 BitVectorRepeat(unsigned repeatAmount
) : d_repeatAmount(repeatAmount
) {}
320 operator unsigned() const { return d_repeatAmount
; }
321 }; /* struct BitVectorRepeat */
323 struct CVC4_PUBLIC BitVectorZeroExtend
325 unsigned d_zeroExtendAmount
;
326 BitVectorZeroExtend(unsigned zeroExtendAmount
)
327 : d_zeroExtendAmount(zeroExtendAmount
)
330 operator unsigned() const { return d_zeroExtendAmount
; }
331 }; /* struct BitVectorZeroExtend */
333 struct CVC4_PUBLIC BitVectorSignExtend
335 unsigned d_signExtendAmount
;
336 BitVectorSignExtend(unsigned signExtendAmount
)
337 : d_signExtendAmount(signExtendAmount
)
340 operator unsigned() const { return d_signExtendAmount
; }
341 }; /* struct BitVectorSignExtend */
343 struct CVC4_PUBLIC BitVectorRotateLeft
345 unsigned d_rotateLeftAmount
;
346 BitVectorRotateLeft(unsigned rotateLeftAmount
)
347 : d_rotateLeftAmount(rotateLeftAmount
)
350 operator unsigned() const { return d_rotateLeftAmount
; }
351 }; /* struct BitVectorRotateLeft */
353 struct CVC4_PUBLIC BitVectorRotateRight
355 unsigned d_rotateRightAmount
;
356 BitVectorRotateRight(unsigned rotateRightAmount
)
357 : d_rotateRightAmount(rotateRightAmount
)
360 operator unsigned() const { return d_rotateRightAmount
; }
361 }; /* struct BitVectorRotateRight */
363 struct CVC4_PUBLIC IntToBitVector
366 IntToBitVector(unsigned size
) : d_size(size
) {}
367 operator unsigned() const { return d_size
; }
368 }; /* struct IntToBitVector */
370 /* -----------------------------------------------------------------------
371 ** Hash Function structs
372 * ----------------------------------------------------------------------- */
375 * Hash function for the BitVector constants.
377 struct CVC4_PUBLIC BitVectorHashFunction
379 inline size_t operator()(const BitVector
& bv
) const { return bv
.hash(); }
380 }; /* struct BitVectorHashFunction */
383 * Hash function for the BitVectorExtract objects.
385 struct CVC4_PUBLIC BitVectorExtractHashFunction
387 size_t operator()(const BitVectorExtract
& extract
) const
389 size_t hash
= extract
.d_low
;
390 hash
^= extract
.d_high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
393 }; /* struct BitVectorExtractHashFunction */
396 * Hash function for the BitVectorBitOf objects.
398 struct CVC4_PUBLIC BitVectorBitOfHashFunction
400 size_t operator()(const BitVectorBitOf
& b
) const { return b
.d_bitIndex
; }
401 }; /* struct BitVectorBitOfHashFunction */
403 template <typename T
>
404 struct CVC4_PUBLIC UnsignedHashFunction
406 inline size_t operator()(const T
& x
) const { return (size_t)x
; }
407 }; /* struct UnsignedHashFunction */
409 /* -----------------------------------------------------------------------
411 * ----------------------------------------------------------------------- */
413 inline std::ostream
& operator<<(std::ostream
& os
,
414 const BitVector
& bv
) CVC4_PUBLIC
;
415 inline std::ostream
& operator<<(std::ostream
& os
, const BitVector
& bv
)
417 return os
<< bv
.toString();
420 inline std::ostream
& operator<<(std::ostream
& os
,
421 const BitVectorExtract
& bv
) CVC4_PUBLIC
;
422 inline std::ostream
& operator<<(std::ostream
& os
, const BitVectorExtract
& bv
)
424 return os
<< "[" << bv
.d_high
<< ":" << bv
.d_low
<< "]";
427 inline std::ostream
& operator<<(std::ostream
& os
,
428 const BitVectorBitOf
& bv
) CVC4_PUBLIC
;
429 inline std::ostream
& operator<<(std::ostream
& os
, const BitVectorBitOf
& bv
)
431 return os
<< "[" << bv
.d_bitIndex
<< "]";
434 inline std::ostream
& operator<<(std::ostream
& os
,
435 const IntToBitVector
& bv
) CVC4_PUBLIC
;
436 inline std::ostream
& operator<<(std::ostream
& os
, const IntToBitVector
& bv
)
438 return os
<< "[" << bv
.d_size
<< "]";
443 #endif /* CVC4__BITVECTOR_H */