1 /********************* */
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Dejan Jovanovic, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
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 bit-vector of ones of given size. */
244 static BitVector
mkOnes(unsigned size
);
246 /* Create bit-vector representing the minimum signed value of given size. */
247 static BitVector
mkMinSigned(unsigned size
);
249 /* Create bit-vector representing the maximum signed value of given size. */
250 static BitVector
mkMaxSigned(unsigned size
);
255 * - no overflows: 2^d_size < d_value
256 * - no negative numbers: d_value >= 0
262 }; /* class BitVector */
264 /* -----------------------------------------------------------------------
266 * ----------------------------------------------------------------------- */
269 * The structure representing the extraction operation for bit-vectors. The
270 * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
271 * by taking the bits at indices <code>high ... low</code>
273 struct CVC4_PUBLIC BitVectorExtract
275 /** The high bit of the range for this extract */
277 /** The low bit of the range for this extract */
280 BitVectorExtract(unsigned high
, unsigned low
) : high(high
), low(low
) {}
282 bool operator==(const BitVectorExtract
& extract
) const
284 return high
== extract
.high
&& low
== extract
.low
;
286 }; /* struct BitVectorExtract */
289 * The structure representing the extraction of one Boolean bit.
291 struct CVC4_PUBLIC BitVectorBitOf
293 /** The index of the bit */
295 BitVectorBitOf(unsigned i
) : bitIndex(i
) {}
297 bool operator==(const BitVectorBitOf
& other
) const
299 return bitIndex
== other
.bitIndex
;
301 }; /* struct BitVectorBitOf */
303 struct CVC4_PUBLIC BitVectorSize
306 BitVectorSize(unsigned size
) : size(size
) {}
307 operator unsigned() const { return size
; }
308 }; /* struct BitVectorSize */
310 struct CVC4_PUBLIC BitVectorRepeat
312 unsigned repeatAmount
;
313 BitVectorRepeat(unsigned repeatAmount
) : repeatAmount(repeatAmount
) {}
314 operator unsigned() const { return repeatAmount
; }
315 }; /* struct BitVectorRepeat */
317 struct CVC4_PUBLIC BitVectorZeroExtend
319 unsigned zeroExtendAmount
;
320 BitVectorZeroExtend(unsigned zeroExtendAmount
)
321 : zeroExtendAmount(zeroExtendAmount
)
324 operator unsigned() const { return zeroExtendAmount
; }
325 }; /* struct BitVectorZeroExtend */
327 struct CVC4_PUBLIC BitVectorSignExtend
329 unsigned signExtendAmount
;
330 BitVectorSignExtend(unsigned signExtendAmount
)
331 : signExtendAmount(signExtendAmount
)
334 operator unsigned() const { return signExtendAmount
; }
335 }; /* struct BitVectorSignExtend */
337 struct CVC4_PUBLIC BitVectorRotateLeft
339 unsigned rotateLeftAmount
;
340 BitVectorRotateLeft(unsigned rotateLeftAmount
)
341 : rotateLeftAmount(rotateLeftAmount
)
344 operator unsigned() const { return rotateLeftAmount
; }
345 }; /* struct BitVectorRotateLeft */
347 struct CVC4_PUBLIC BitVectorRotateRight
349 unsigned rotateRightAmount
;
350 BitVectorRotateRight(unsigned rotateRightAmount
)
351 : rotateRightAmount(rotateRightAmount
)
354 operator unsigned() const { return rotateRightAmount
; }
355 }; /* struct BitVectorRotateRight */
357 struct CVC4_PUBLIC IntToBitVector
360 IntToBitVector(unsigned size
) : size(size
) {}
361 operator unsigned() const { return size
; }
362 }; /* struct IntToBitVector */
364 /* -----------------------------------------------------------------------
365 ** Hash Function structs
366 * ----------------------------------------------------------------------- */
369 * Hash function for the BitVector constants.
371 struct CVC4_PUBLIC BitVectorHashFunction
373 inline size_t operator()(const BitVector
& bv
) const { return bv
.hash(); }
374 }; /* struct BitVectorHashFunction */
377 * Hash function for the BitVectorExtract objects.
379 struct CVC4_PUBLIC BitVectorExtractHashFunction
381 size_t operator()(const BitVectorExtract
& extract
) const
383 size_t hash
= extract
.low
;
384 hash
^= extract
.high
+ 0x9e3779b9 + (hash
<< 6) + (hash
>> 2);
387 }; /* struct BitVectorExtractHashFunction */
390 * Hash function for the BitVectorBitOf objects.
392 struct CVC4_PUBLIC BitVectorBitOfHashFunction
394 size_t operator()(const BitVectorBitOf
& b
) const { return b
.bitIndex
; }
395 }; /* struct BitVectorBitOfHashFunction */
397 template <typename T
>
398 struct CVC4_PUBLIC UnsignedHashFunction
400 inline size_t operator()(const T
& x
) const { return (size_t)x
; }
401 }; /* struct UnsignedHashFunction */
403 /* -----------------------------------------------------------------------
405 * ----------------------------------------------------------------------- */
407 inline std::ostream
& operator<<(std::ostream
& os
,
408 const BitVector
& bv
) CVC4_PUBLIC
;
409 inline std::ostream
& operator<<(std::ostream
& os
, const BitVector
& bv
)
411 return os
<< bv
.toString();
414 inline std::ostream
& operator<<(std::ostream
& os
,
415 const BitVectorExtract
& bv
) CVC4_PUBLIC
;
416 inline std::ostream
& operator<<(std::ostream
& os
, const BitVectorExtract
& bv
)
418 return os
<< "[" << bv
.high
<< ":" << bv
.low
<< "]";
421 inline std::ostream
& operator<<(std::ostream
& os
,
422 const BitVectorBitOf
& bv
) CVC4_PUBLIC
;
423 inline std::ostream
& operator<<(std::ostream
& os
, const BitVectorBitOf
& bv
)
425 return os
<< "[" << bv
.bitIndex
<< "]";
428 inline std::ostream
& operator<<(std::ostream
& os
,
429 const IntToBitVector
& bv
) CVC4_PUBLIC
;
430 inline std::ostream
& operator<<(std::ostream
& os
, const IntToBitVector
& bv
)
432 return os
<< "[" << bv
.size
<< "]";
437 #endif /* CVC4__BITVECTOR_H */