Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Liana Hadarean, Christopher L. Conway
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 "util/bitvector.h"
17 : :
18 : : #include "base/check.h"
19 : : #include "util/hash.h"
20 : :
21 : : namespace cvc5::internal {
22 : :
23 : 272705 : BitVector::BitVector(const std::string& num, uint32_t base)
24 : : {
25 [ + + ][ + + ]: 272705 : Assert(base == 2 || base == 10 || base == 16);
[ - + ][ - + ]
[ - - ]
26 [ - + ][ - + ]: 272705 : Assert(num[0] != '-');
[ - - ]
27 : 272705 : d_value = Integer(num, base);
28 [ - + ][ - + ]: 272705 : Assert(d_value == d_value.abs());
[ - - ]
29 : : // Compute the length, *without* any negative sign.
30 [ + + ][ + ]: 272705 : switch (base)
31 : : {
32 : 1 : case 10: d_size = d_value.length(); break;
33 : 2 : case 16: d_size = num.size() * 4; break;
34 : 272702 : default: d_size = num.size();
35 : : }
36 : 272705 : }
37 : :
38 : 180800000 : unsigned BitVector::getSize() const { return d_size; }
39 : :
40 : 110763000 : const Integer& BitVector::getValue() const { return d_value; }
41 : :
42 : 20482 : Integer BitVector::toInteger() const { return d_value; }
43 : :
44 : 11366400 : Integer BitVector::toSignedInteger() const
45 : : {
46 : 11366400 : unsigned size = d_size;
47 : 22732800 : Integer sign_bit = d_value.extractBitRange(1, size - 1);
48 : 22732800 : Integer val = d_value.extractBitRange(size - 1, 0);
49 : 22732800 : Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
50 : 22732800 : return res;
51 : : }
52 : :
53 : 56844 : std::string BitVector::toString(unsigned int base) const
54 : : {
55 : 113688 : std::string str = d_value.toString(base);
56 [ + + ][ + + ]: 56844 : if (base == 2 && d_size > str.size())
[ + + ]
57 : : {
58 : 47484 : std::string zeroes;
59 [ + + ]: 446291 : for (unsigned int i = 0; i < d_size - str.size(); ++i)
60 : : {
61 : 422549 : zeroes.append("0");
62 : : }
63 : 23742 : return zeroes + str;
64 : : }
65 : : else
66 : : {
67 : 33102 : return str;
68 : : }
69 : : }
70 : :
71 : 4376450 : size_t BitVector::hash() const
72 : : {
73 : : PairHashFunction<size_t, size_t> h;
74 : 4376450 : return h(std::make_pair(d_value.hash(), d_size));
75 : : }
76 : :
77 : 2019 : BitVector& BitVector::setBit(uint32_t i, bool value)
78 : : {
79 [ - + ][ - + ]: 2019 : Assert(i < d_size);
[ - - ]
80 : 2019 : d_value.setBit(i, value);
81 : 2019 : return *this;
82 : : }
83 : :
84 : 107569 : bool BitVector::isBitSet(uint32_t i) const
85 : : {
86 [ - + ][ - + ]: 107569 : Assert(i < d_size);
[ - - ]
87 : 107569 : return d_value.isBitSet(i);
88 : : }
89 : :
90 : 656291 : unsigned BitVector::isPow2() const
91 : : {
92 : 656291 : return d_value.isPow2();
93 : : }
94 : :
95 : : /* -----------------------------------------------------------------------
96 : : * Operators
97 : : * ----------------------------------------------------------------------- */
98 : :
99 : : /* String Operations ----------------------------------------------------- */
100 : :
101 : 771529 : BitVector BitVector::concat(const BitVector& other) const
102 : : {
103 : 771529 : return BitVector(d_size + other.d_size,
104 : 1543060 : (d_value.multiplyByPow2(other.d_size)) + other.d_value);
105 : : }
106 : :
107 : 2096490 : BitVector BitVector::extract(unsigned high, unsigned low) const
108 : : {
109 [ - + ][ - + ]: 2096490 : Assert(high < d_size);
[ - - ]
110 [ - + ][ - + ]: 2096490 : Assert(low <= high);
[ - - ]
111 : 2096490 : return BitVector(high - low + 1,
112 : 4192980 : d_value.extractBitRange(high - low + 1, low));
113 : : }
114 : :
115 : : /* (Dis)Equality --------------------------------------------------------- */
116 : :
117 : 20936700 : bool operator==(const BitVector& a, const BitVector& b)
118 : : {
119 [ - + ]: 20936700 : if (a.getSize() != b.getSize()) return false;
120 : 20936700 : return a.getValue() == b.getValue();
121 : : }
122 : :
123 : 990711 : bool operator!=(const BitVector& a, const BitVector& b)
124 : : {
125 [ - + ]: 990711 : if (a.getSize() != b.getSize()) return true;
126 : 990711 : return a.getValue() != b.getValue();
127 : : }
128 : :
129 : : /* Unsigned Inequality --------------------------------------------------- */
130 : :
131 : 1108 : bool operator<(const BitVector& a, const BitVector& b)
132 : : {
133 : 1108 : return a.getValue() < b.getValue();
134 : : }
135 : :
136 : 2207 : bool operator<=(const BitVector& a, const BitVector& b)
137 : : {
138 : 2207 : return a.getValue() <= b.getValue();
139 : : }
140 : :
141 : 455 : bool operator>(const BitVector& a, const BitVector& b)
142 : : {
143 : 455 : return a.getValue() > b.getValue();
144 : : }
145 : :
146 : 864 : bool operator>=(const BitVector& a, const BitVector& b)
147 : : {
148 : 864 : return a.getValue() >= b.getValue();
149 : : }
150 : :
151 : 156305 : bool BitVector::unsignedLessThan(const BitVector& y) const
152 : : {
153 [ - + ][ - + ]: 156305 : Assert(d_size == y.d_size);
[ - - ]
154 [ - + ][ - + ]: 156305 : Assert(d_value >= 0);
[ - - ]
155 [ - + ][ - + ]: 156305 : Assert(y.d_value >= 0);
[ - - ]
156 : 156305 : return d_value < y.d_value;
157 : : }
158 : :
159 : 39899 : bool BitVector::unsignedLessThanEq(const BitVector& y) const
160 : : {
161 [ - + ][ - + ]: 39899 : Assert(d_size == y.d_size);
[ - - ]
162 [ - + ][ - + ]: 39899 : Assert(d_value >= 0);
[ - - ]
163 [ - + ][ - + ]: 39899 : Assert(y.d_value >= 0);
[ - - ]
164 : 39899 : return d_value <= y.d_value;
165 : : }
166 : :
167 : : /* Signed Inequality ----------------------------------------------------- */
168 : :
169 : 240651 : bool BitVector::signedLessThan(const BitVector& y) const
170 : : {
171 [ - + ][ - + ]: 240651 : Assert(d_size == y.d_size);
[ - - ]
172 [ - + ][ - + ]: 240651 : Assert(d_value >= 0);
[ - - ]
173 [ - + ][ - + ]: 240651 : Assert(y.d_value >= 0);
[ - - ]
174 : 481302 : Integer a = (*this).toSignedInteger();
175 : 481302 : Integer b = y.toSignedInteger();
176 : :
177 : 481302 : return a < b;
178 : : }
179 : :
180 : 5442520 : bool BitVector::signedLessThanEq(const BitVector& y) const
181 : : {
182 [ - + ][ - + ]: 5442520 : Assert(d_size == y.d_size);
[ - - ]
183 [ - + ][ - + ]: 5442520 : Assert(d_value >= 0);
[ - - ]
184 [ - + ][ - + ]: 5442520 : Assert(y.d_value >= 0);
[ - - ]
185 : 10885000 : Integer a = (*this).toSignedInteger();
186 : 10885000 : Integer b = y.toSignedInteger();
187 : :
188 : 10885000 : return a <= b;
189 : : }
190 : :
191 : : /* Bit-wise operations --------------------------------------------------- */
192 : :
193 : 3474 : BitVector operator^(const BitVector& a, const BitVector& b)
194 : : {
195 [ - + ][ - + ]: 3474 : Assert(a.getSize() == b.getSize());
[ - - ]
196 : 6948 : return BitVector(a.getSize(), a.getValue().bitwiseXor(b.getValue()));
197 : : }
198 : :
199 : 506560 : BitVector operator|(const BitVector& a, const BitVector& b)
200 : : {
201 [ - + ][ - + ]: 506560 : Assert(a.getSize() == b.getSize());
[ - - ]
202 : 1013120 : return BitVector(a.getSize(), a.getValue().bitwiseOr(b.getValue()));
203 : : }
204 : :
205 : 1721290 : BitVector operator&(const BitVector& a, const BitVector& b)
206 : : {
207 [ - + ][ - + ]: 1721290 : Assert(a.getSize() == b.getSize());
[ - - ]
208 : 3442580 : return BitVector(a.getSize(), a.getValue().bitwiseAnd(b.getValue()));
209 : : }
210 : :
211 : 14553500 : BitVector operator~(const BitVector& a)
212 : : {
213 : 29107000 : return BitVector(a.getSize(), a.getValue().bitwiseNot());
214 : : }
215 : :
216 : : /* Arithmetic operations ------------------------------------------------- */
217 : :
218 : 23310400 : BitVector operator+(const BitVector& a, const BitVector& b)
219 : : {
220 [ - + ][ - + ]: 23310400 : Assert(a.getSize() == b.getSize());
[ - - ]
221 : 46620700 : Integer sum = a.getValue() + b.getValue();
222 : 46620700 : return BitVector(a.getSize(), sum);
223 : : }
224 : :
225 : 9216110 : BitVector operator-(const BitVector& a, const BitVector& b)
226 : : {
227 [ - + ][ - + ]: 9216110 : Assert(a.getSize() == b.getSize());
[ - - ]
228 : : // to maintain the invariant that we are only adding BitVectors of the
229 : : // same size
230 : 9216110 : BitVector one(a.getSize(), Integer(1));
231 : 27648300 : return a + ~b + one;
232 : : }
233 : :
234 : 4406260 : BitVector operator-(const BitVector& a)
235 : : {
236 : 4406260 : BitVector one(a.getSize(), Integer(1));
237 : 13218800 : return ~a + one;
238 : : }
239 : :
240 : 489858 : BitVector operator*(const BitVector& a, const BitVector& b)
241 : : {
242 [ - + ][ - + ]: 489858 : Assert(a.getSize() == b.getSize());
[ - - ]
243 : 979716 : Integer prod = a.getValue() * b.getValue();
244 : 979716 : return BitVector(a.getSize(), prod);
245 : : }
246 : :
247 : 68958 : BitVector BitVector::unsignedDivTotal(const BitVector& y) const
248 : : {
249 [ - + ][ - + ]: 68958 : Assert(d_size == y.d_size);
[ - - ]
250 : : /* d_value / 0 = -1 = 2^d_size - 1 */
251 [ + + ]: 68958 : if (y.d_value == 0)
252 : : {
253 : 16132 : return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
254 : : }
255 [ - + ][ - + ]: 60892 : Assert(d_value >= 0);
[ - - ]
256 [ - + ][ - + ]: 60892 : Assert(y.d_value > 0);
[ - - ]
257 : 121784 : return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
258 : : }
259 : :
260 : 73246 : BitVector BitVector::unsignedRemTotal(const BitVector& y) const
261 : : {
262 [ - + ][ - + ]: 73246 : Assert(d_size == y.d_size);
[ - - ]
263 [ + + ]: 73246 : if (y.d_value == 0)
264 : : {
265 : 8099 : return BitVector(d_size, d_value);
266 : : }
267 [ - + ][ - + ]: 65147 : Assert(d_value >= 0);
[ - - ]
268 [ - + ][ - + ]: 65147 : Assert(y.d_value > 0);
[ - - ]
269 : 130294 : return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
270 : : }
271 : :
272 : : /* Extend operations ----------------------------------------------------- */
273 : :
274 : 1890770 : BitVector BitVector::zeroExtend(unsigned n) const
275 : : {
276 : 1890770 : return BitVector(d_size + n, d_value);
277 : : }
278 : :
279 : 1656510 : BitVector BitVector::signExtend(unsigned n) const
280 : : {
281 : 3313010 : Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
282 [ + + ]: 1656510 : if (sign_bit == Integer(0))
283 : : {
284 : 276433 : return BitVector(d_size + n, d_value);
285 : : }
286 : 2760150 : Integer val = d_value.oneExtend(d_size, n);
287 : 1380070 : return BitVector(d_size + n, val);
288 : : }
289 : :
290 : : /* Shift operations ------------------------------------------------------ */
291 : :
292 : 7468420 : BitVector BitVector::leftShift(const BitVector& y) const
293 : : {
294 [ + + ]: 7468420 : if (y.d_value > Integer(d_size))
295 : : {
296 : 74714 : return BitVector(d_size, Integer(0));
297 : : }
298 [ + + ]: 7431070 : if (y.d_value == 0)
299 : : {
300 : 603605 : return *this;
301 : : }
302 : : // making sure we don't lose information casting
303 [ - + ][ - + ]: 6827460 : Assert(y.d_value < Integer(1).multiplyByPow2(32));
[ - - ]
304 : 6827460 : uint32_t amount = y.d_value.toUnsignedInt();
305 : 13654900 : Integer res = d_value.multiplyByPow2(amount);
306 : 6827460 : return BitVector(d_size, res);
307 : : }
308 : :
309 : 169188 : BitVector BitVector::logicalRightShift(const BitVector& y) const
310 : : {
311 [ + + ]: 169188 : if (y.d_value > Integer(d_size))
312 : : {
313 : 2 : return BitVector(d_size, Integer(0));
314 : : }
315 : : // making sure we don't lose information casting
316 [ - + ][ - + ]: 169187 : Assert(y.d_value < Integer(1).multiplyByPow2(32));
[ - - ]
317 : 169187 : uint32_t amount = y.d_value.toUnsignedInt();
318 : 338374 : Integer res = d_value.divByPow2(amount);
319 : 169187 : return BitVector(d_size, res);
320 : : }
321 : :
322 : 60291 : BitVector BitVector::arithRightShift(const BitVector& y) const
323 : : {
324 : 120582 : Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
325 [ + + ]: 60291 : if (y.d_value > Integer(d_size))
326 : : {
327 [ + + ]: 2182 : if (sign_bit == Integer(0))
328 : : {
329 : 2298 : return BitVector(d_size, Integer(0));
330 : : }
331 : : else
332 : : {
333 : 2066 : return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) - 1);
334 : : }
335 : : }
336 : :
337 [ + + ]: 58109 : if (y.d_value == 0)
338 : : {
339 : 1672 : return *this;
340 : : }
341 : :
342 : : // making sure we don't lose information casting
343 [ - + ][ - + ]: 56437 : Assert(y.d_value < Integer(1).multiplyByPow2(32));
[ - - ]
344 : :
345 : 56437 : uint32_t amount = y.d_value.toUnsignedInt();
346 : 112874 : Integer rest = d_value.divByPow2(amount);
347 : :
348 [ + + ]: 56437 : if (sign_bit == Integer(0))
349 : : {
350 : 39030 : return BitVector(d_size, rest);
351 : : }
352 : 34814 : Integer res = rest.oneExtend(d_size - amount, amount);
353 : 17407 : return BitVector(d_size, res);
354 : : }
355 : :
356 : : /* -----------------------------------------------------------------------
357 : : * Static helpers.
358 : : * ----------------------------------------------------------------------- */
359 : :
360 : 41 : BitVector BitVector::mkZero(unsigned size)
361 : : {
362 [ - + ][ - + ]: 41 : Assert(size > 0);
[ - - ]
363 : 41 : return BitVector(size);
364 : : }
365 : :
366 : 919 : BitVector BitVector::mkOne(unsigned size)
367 : : {
368 [ - + ][ - + ]: 919 : Assert(size > 0);
[ - - ]
369 : 919 : return BitVector(size, 1u);
370 : : }
371 : :
372 : 1034810 : BitVector BitVector::mkOnes(unsigned size)
373 : : {
374 [ - + ][ - + ]: 1034810 : Assert(size > 0);
[ - - ]
375 : 2069620 : return BitVector(1, Integer(1)).signExtend(size - 1);
376 : : }
377 : :
378 : 95 : BitVector BitVector::mkMinSigned(unsigned size)
379 : : {
380 [ - + ][ - + ]: 95 : Assert(size > 0);
[ - - ]
381 : 95 : BitVector res(size);
382 : 95 : res.setBit(size - 1, true);
383 : 95 : return res;
384 : : }
385 : :
386 : 39 : BitVector BitVector::mkMaxSigned(unsigned size)
387 : : {
388 [ - + ][ - + ]: 39 : Assert(size > 0);
[ - - ]
389 : 78 : return ~BitVector::mkMinSigned(size);
390 : : }
391 : :
392 : : } // namespace cvc5::internal
|
