Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * A fixed-size bit-vector, implemented as a wrapper around Integer.
11 : : */
12 : :
13 : : #include "util/bitvector.h"
14 : :
15 : : #include "base/check.h"
16 : : #include "util/hash.h"
17 : :
18 : : namespace cvc5::internal {
19 : :
20 : 129528 : BitVector::BitVector(const std::string& num, uint32_t base)
21 : : {
22 [ + + ][ + + ]: 129528 : Assert(base == 2 || base == 10 || base == 16);
[ + + ][ + - ]
[ - + ][ - + ]
[ - - ]
23 [ - + ][ - + ]: 129528 : Assert(num[0] != '-');
[ - - ]
24 : 129528 : d_value = Integer(num, base);
25 [ - + ][ - + ]: 129528 : Assert(d_value == d_value.abs());
[ - - ]
26 : : // Compute the length, *without* any negative sign.
27 [ + + ][ + ]: 129528 : switch (base)
28 : : {
29 : 1 : case 10: d_size = d_value.length(); break;
30 : 2 : case 16: d_size = num.size() * 4; break;
31 : 129525 : default: d_size = num.size();
32 : : }
33 : 129528 : }
34 : :
35 : 90782738 : uint32_t BitVector::getSize() const { return d_size; }
36 : :
37 : 66174599 : const Integer& BitVector::getValue() const { return d_value; }
38 : :
39 : 41699 : Integer BitVector::toInteger() const { return d_value; }
40 : :
41 : 3527007 : Integer BitVector::toSignedInteger() const
42 : : {
43 : 3527007 : uint32_t size = d_size;
44 : 3527007 : Integer sign_bit = d_value.extractBitRange(1, size - 1);
45 : 3527007 : Integer val = d_value.extractBitRange(size - 1, 0);
46 : 7054014 : Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
47 : 7054014 : return res;
48 : 3527007 : }
49 : :
50 : 73849 : std::string BitVector::toString(uint32_t base) const
51 : : {
52 : 73849 : std::string str = d_value.toString(base);
53 [ + + ][ + + ]: 73849 : if (base == 2 && d_size > str.size())
[ + + ]
54 : : {
55 : 36153 : std::string zeroes;
56 [ + + ]: 573926 : for (uint32_t i = 0; i < d_size - str.size(); ++i)
57 : : {
58 : 537773 : zeroes.append("0");
59 : : }
60 : 36153 : return zeroes + str;
61 : 36153 : }
62 : : else
63 : : {
64 : 37696 : return str;
65 : : }
66 : 73849 : }
67 : :
68 : 4946567 : size_t BitVector::hash() const
69 : : {
70 : : PairHashFunction<size_t, size_t> h;
71 : 4946567 : return h(std::make_pair(d_value.hash(), d_size));
72 : : }
73 : :
74 : 2344 : BitVector& BitVector::setBit(uint32_t i, bool value)
75 : : {
76 [ - + ][ - + ]: 2344 : Assert(i < d_size);
[ - - ]
77 : 2344 : d_value.setBit(i, value);
78 : 2344 : return *this;
79 : : }
80 : :
81 : 151438 : bool BitVector::isBitSet(uint32_t i) const
82 : : {
83 [ - + ][ - + ]: 151438 : Assert(i < d_size);
[ - - ]
84 : 151438 : return d_value.isBitSet(i);
85 : : }
86 : :
87 : 195986 : unsigned BitVector::isPow2() const { return d_value.isPow2(); }
88 : :
89 : 2 : bool BitVector::is_one() const { return d_value == Integer(1); }
90 : :
91 : : /* -----------------------------------------------------------------------
92 : : * Operators
93 : : * ----------------------------------------------------------------------- */
94 : :
95 : : /* String Operations ----------------------------------------------------- */
96 : :
97 : 304937 : BitVector BitVector::concat(const BitVector& other) const
98 : : {
99 : 304937 : return BitVector(d_size + other.d_size,
100 : 609874 : (d_value.multiplyByPow2(other.d_size)) + other.d_value);
101 : : }
102 : :
103 : 897646 : BitVector BitVector::extract(uint32_t high, uint32_t low) const
104 : : {
105 [ - + ][ - + ]: 897646 : Assert(high < d_size);
[ - - ]
106 [ - + ][ - + ]: 897646 : Assert(low <= high);
[ - - ]
107 : 897646 : return BitVector(high - low + 1,
108 : 1795292 : d_value.extractBitRange(high - low + 1, low));
109 : : }
110 : :
111 : : /* (Dis)Equality --------------------------------------------------------- */
112 : :
113 : 20011105 : bool operator==(const BitVector& a, const BitVector& b)
114 : : {
115 [ - + ]: 20011105 : if (a.getSize() != b.getSize()) return false;
116 : 20011105 : return a.getValue() == b.getValue();
117 : : }
118 : :
119 : 1212592 : bool operator!=(const BitVector& a, const BitVector& b)
120 : : {
121 [ - + ]: 1212592 : if (a.getSize() != b.getSize()) return true;
122 : 1212592 : return a.getValue() != b.getValue();
123 : : }
124 : :
125 : : /* Unsigned Inequality --------------------------------------------------- */
126 : :
127 : 1336 : bool operator<(const BitVector& a, const BitVector& b)
128 : : {
129 : 1336 : return a.getValue() < b.getValue();
130 : : }
131 : :
132 : 2667 : bool operator<=(const BitVector& a, const BitVector& b)
133 : : {
134 : 2667 : return a.getValue() <= b.getValue();
135 : : }
136 : :
137 : 474 : bool operator>(const BitVector& a, const BitVector& b)
138 : : {
139 : 474 : return a.getValue() > b.getValue();
140 : : }
141 : :
142 : 1028 : bool operator>=(const BitVector& a, const BitVector& b)
143 : : {
144 : 1028 : return a.getValue() >= b.getValue();
145 : : }
146 : :
147 : 58592 : bool BitVector::unsignedLessThan(const BitVector& y) const
148 : : {
149 [ - + ][ - + ]: 58592 : Assert(d_size == y.d_size);
[ - - ]
150 [ - + ][ - + ]: 58592 : Assert(d_value >= 0);
[ - - ]
151 [ - + ][ - + ]: 58592 : Assert(y.d_value >= 0);
[ - - ]
152 : 58592 : return d_value < y.d_value;
153 : : }
154 : :
155 : 13761 : bool BitVector::unsignedLessThanEq(const BitVector& y) const
156 : : {
157 [ - + ][ - + ]: 13761 : Assert(d_size == y.d_size);
[ - - ]
158 [ - + ][ - + ]: 13761 : Assert(d_value >= 0);
[ - - ]
159 [ - + ][ - + ]: 13761 : Assert(y.d_value >= 0);
[ - - ]
160 : 13761 : return d_value <= y.d_value;
161 : : }
162 : :
163 : : /* Signed Inequality ----------------------------------------------------- */
164 : :
165 : 75487 : bool BitVector::signedLessThan(const BitVector& y) const
166 : : {
167 [ - + ][ - + ]: 75487 : Assert(d_size == y.d_size);
[ - - ]
168 [ - + ][ - + ]: 75487 : Assert(d_value >= 0);
[ - - ]
169 [ - + ][ - + ]: 75487 : Assert(y.d_value >= 0);
[ - - ]
170 : 75487 : Integer a = (*this).toSignedInteger();
171 : 75487 : Integer b = y.toSignedInteger();
172 : :
173 : 150974 : return a < b;
174 : 75487 : }
175 : :
176 : 1687986 : bool BitVector::signedLessThanEq(const BitVector& y) const
177 : : {
178 [ - + ][ - + ]: 1687986 : Assert(d_size == y.d_size);
[ - - ]
179 [ - + ][ - + ]: 1687986 : Assert(d_value >= 0);
[ - - ]
180 [ - + ][ - + ]: 1687986 : Assert(y.d_value >= 0);
[ - - ]
181 : 1687986 : Integer a = (*this).toSignedInteger();
182 : 1687986 : Integer b = y.toSignedInteger();
183 : :
184 : 3375972 : return a <= b;
185 : 1687986 : }
186 : :
187 : : /* Bit-wise operations --------------------------------------------------- */
188 : :
189 : 3383 : BitVector operator^(const BitVector& a, const BitVector& b)
190 : : {
191 [ - + ][ - + ]: 3383 : Assert(a.getSize() == b.getSize());
[ - - ]
192 : 6766 : return BitVector(a.getSize(), a.getValue().bitwiseXor(b.getValue()));
193 : : }
194 : :
195 : 328769 : BitVector operator|(const BitVector& a, const BitVector& b)
196 : : {
197 [ - + ][ - + ]: 328769 : Assert(a.getSize() == b.getSize());
[ - - ]
198 : 657538 : return BitVector(a.getSize(), a.getValue().bitwiseOr(b.getValue()));
199 : : }
200 : :
201 : 662683 : BitVector operator&(const BitVector& a, const BitVector& b)
202 : : {
203 [ - + ][ - + ]: 662683 : Assert(a.getSize() == b.getSize());
[ - - ]
204 : 1325366 : return BitVector(a.getSize(), a.getValue().bitwiseAnd(b.getValue()));
205 : : }
206 : :
207 : 4996942 : BitVector operator~(const BitVector& a)
208 : : {
209 : 9993884 : return BitVector(a.getSize(), a.getValue().bitwiseNot());
210 : : }
211 : :
212 : : /* Arithmetic operations ------------------------------------------------- */
213 : :
214 : 7742604 : BitVector operator+(const BitVector& a, const BitVector& b)
215 : : {
216 [ - + ][ - + ]: 7742604 : Assert(a.getSize() == b.getSize());
[ - - ]
217 : 7742604 : Integer sum = a.getValue() + b.getValue();
218 : 15485208 : return BitVector(a.getSize(), sum);
219 : 7742604 : }
220 : :
221 : 2838574 : BitVector operator-(const BitVector& a, const BitVector& b)
222 : : {
223 [ - + ][ - + ]: 2838574 : Assert(a.getSize() == b.getSize());
[ - - ]
224 : : // to maintain the invariant that we are only adding BitVectors of the
225 : : // same size
226 : 2838574 : BitVector one(a.getSize(), Integer(1));
227 : 8515722 : return a + ~b + one;
228 : 2838574 : }
229 : :
230 : 1802437 : BitVector operator-(const BitVector& a)
231 : : {
232 : 1802437 : BitVector one(a.getSize(), Integer(1));
233 : 5407311 : return ~a + one;
234 : 1802437 : }
235 : :
236 : 476454 : BitVector operator*(const BitVector& a, const BitVector& b)
237 : : {
238 [ - + ][ - + ]: 476454 : Assert(a.getSize() == b.getSize());
[ - - ]
239 : 476454 : Integer prod = a.getValue() * b.getValue();
240 : 952908 : return BitVector(a.getSize(), prod);
241 : 476454 : }
242 : :
243 : 62483 : BitVector BitVector::unsignedDivTotal(const BitVector& y) const
244 : : {
245 [ - + ][ - + ]: 62483 : Assert(d_size == y.d_size);
[ - - ]
246 : : /* d_value / 0 = -1 = 2^d_size - 1 */
247 [ + + ]: 62483 : if (y.d_value == 0)
248 : : {
249 : 16316 : return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
250 : : }
251 [ - + ][ - + ]: 54325 : Assert(d_value >= 0);
[ - - ]
252 [ - + ][ - + ]: 54325 : Assert(y.d_value > 0);
[ - - ]
253 : 108650 : return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
254 : : }
255 : :
256 : 67376 : BitVector BitVector::unsignedRemTotal(const BitVector& y) const
257 : : {
258 [ - + ][ - + ]: 67376 : Assert(d_size == y.d_size);
[ - - ]
259 [ + + ]: 67376 : if (y.d_value == 0)
260 : : {
261 : 8135 : return BitVector(d_size, d_value);
262 : : }
263 [ - + ][ - + ]: 59241 : Assert(d_value >= 0);
[ - - ]
264 [ - + ][ - + ]: 59241 : Assert(y.d_value > 0);
[ - - ]
265 : 118482 : return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
266 : : }
267 : :
268 : : /* Extend operations ----------------------------------------------------- */
269 : :
270 : 591092 : BitVector BitVector::zeroExtend(uint32_t n) const
271 : : {
272 : 591092 : return BitVector(d_size + n, d_value);
273 : : }
274 : :
275 : 1597854 : BitVector BitVector::signExtend(uint32_t n) const
276 : : {
277 : 1597854 : Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
278 [ + + ]: 1597854 : if (sign_bit == Integer(0))
279 : : {
280 : 91127 : return BitVector(d_size + n, d_value);
281 : : }
282 : 1506727 : Integer val = d_value.oneExtend(d_size, n);
283 : 1506727 : return BitVector(d_size + n, val);
284 : 1597854 : }
285 : :
286 : : /* Shift operations ------------------------------------------------------ */
287 : :
288 : 2342868 : BitVector BitVector::leftShift(const BitVector& y) const
289 : : {
290 [ + + ]: 2342868 : if (y.d_value > Integer(d_size))
291 : : {
292 : 22262 : return BitVector(d_size, Integer(0));
293 : : }
294 [ + + ]: 2331737 : if (y.d_value == 0)
295 : : {
296 : 182548 : return *this;
297 : : }
298 : : // making sure we don't lose information casting
299 [ - + ][ - + ]: 2149189 : Assert(y.d_value < Integer(1).multiplyByPow2(32));
[ - - ]
300 : 2149189 : uint32_t amount = y.d_value.toUnsignedInt();
301 : 2149189 : Integer res = d_value.multiplyByPow2(amount);
302 : 2149189 : return BitVector(d_size, res);
303 : 2149189 : }
304 : :
305 : 57962 : BitVector BitVector::logicalRightShift(const BitVector& y) const
306 : : {
307 [ + + ]: 57962 : if (y.d_value > Integer(d_size))
308 : : {
309 : 2 : return BitVector(d_size, Integer(0));
310 : : }
311 : : // making sure we don't lose information casting
312 [ - + ][ - + ]: 57961 : Assert(y.d_value < Integer(1).multiplyByPow2(32));
[ - - ]
313 : 57961 : uint32_t amount = y.d_value.toUnsignedInt();
314 : 57961 : Integer res = d_value.divByPow2(amount);
315 : 57961 : return BitVector(d_size, res);
316 : 57961 : }
317 : :
318 : 20758 : BitVector BitVector::arithRightShift(const BitVector& y) const
319 : : {
320 : 20758 : Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
321 [ + + ]: 20758 : if (y.d_value > Integer(d_size))
322 : : {
323 [ + + ]: 983 : if (sign_bit == Integer(0))
324 : : {
325 : 1336 : return BitVector(d_size, Integer(0));
326 : : }
327 : : else
328 : : {
329 : 630 : return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) - 1);
330 : : }
331 : : }
332 : :
333 [ + + ]: 19775 : if (y.d_value == 0)
334 : : {
335 : 755 : return *this;
336 : : }
337 : :
338 : : // making sure we don't lose information casting
339 [ - + ][ - + ]: 19020 : Assert(y.d_value < Integer(1).multiplyByPow2(32));
[ - - ]
340 : :
341 : 19020 : uint32_t amount = y.d_value.toUnsignedInt();
342 : 19020 : Integer rest = d_value.divByPow2(amount);
343 : :
344 [ + + ]: 19020 : if (sign_bit == Integer(0))
345 : : {
346 : 12865 : return BitVector(d_size, rest);
347 : : }
348 : 6155 : Integer res = rest.oneExtend(d_size - amount, amount);
349 : 6155 : return BitVector(d_size, res);
350 : 20758 : }
351 : :
352 : : /* -----------------------------------------------------------------------
353 : : * Static helpers.
354 : : * ----------------------------------------------------------------------- */
355 : :
356 : 41 : BitVector BitVector::mkZero(uint32_t size)
357 : : {
358 [ - + ][ - + ]: 41 : Assert(size > 0);
[ - - ]
359 : 41 : return BitVector(size);
360 : : }
361 : :
362 : 45 : BitVector BitVector::mkOne(uint32_t size)
363 : : {
364 [ - + ][ - + ]: 45 : Assert(size > 0);
[ - - ]
365 : 45 : return BitVector(size, 1u);
366 : : }
367 : :
368 : 1398605 : BitVector BitVector::mkOnes(uint32_t size)
369 : : {
370 [ - + ][ - + ]: 1398605 : Assert(size > 0);
[ - - ]
371 : 2797210 : return BitVector(1, Integer(1)).signExtend(size - 1);
372 : : }
373 : :
374 : 127 : BitVector BitVector::mkMinSigned(uint32_t size)
375 : : {
376 [ - + ][ - + ]: 127 : Assert(size > 0);
[ - - ]
377 : 127 : BitVector res(size);
378 : 127 : res.setBit(size - 1, true);
379 : 127 : return res;
380 : 0 : }
381 : :
382 : 39 : BitVector BitVector::mkMaxSigned(uint32_t size)
383 : : {
384 [ - + ][ - + ]: 39 : Assert(size > 0);
[ - - ]
385 : 78 : return ~BitVector::mkMinSigned(size);
386 : : }
387 : :
388 : 2 : BitVector BitVector::mkRandom(uint32_t size)
389 : : {
390 [ - + ][ - + ]: 2 : Assert(size > 0);
[ - - ]
391 : 4 : return BitVector(size, Integer::mkRandom(size));
392 : : }
393 : :
394 : : } // namespace cvc5::internal
|
