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 : 129798 : BitVector::BitVector(const std::string& num, uint32_t base)
21 : : {
22 [ + + ][ + + ]: 129798 : Assert(base == 2 || base == 10 || base == 16);
[ + + ][ + - ]
[ - + ][ - + ]
[ - - ]
23 [ - + ][ - + ]: 129798 : Assert(num[0] != '-');
[ - - ]
24 : 129798 : d_value = Integer(num, base);
25 [ - + ][ - + ]: 129798 : Assert(d_value == d_value.abs());
[ - - ]
26 : : // Compute the length, *without* any negative sign.
27 [ + + ][ + ]: 129798 : switch (base)
28 : : {
29 : 1 : case 10: d_size = d_value.length(); break;
30 : 2 : case 16: d_size = num.size() * 4; break;
31 : 129795 : default: d_size = num.size();
32 : : }
33 : 129798 : }
34 : :
35 : 87667789 : unsigned BitVector::getSize() const { return d_size; }
36 : :
37 : 63481078 : const Integer& BitVector::getValue() const { return d_value; }
38 : :
39 : 31750 : Integer BitVector::toInteger() const { return d_value; }
40 : :
41 : 3522848 : Integer BitVector::toSignedInteger() const
42 : : {
43 : 3522848 : unsigned size = d_size;
44 : 3522848 : Integer sign_bit = d_value.extractBitRange(1, size - 1);
45 : 3522848 : Integer val = d_value.extractBitRange(size - 1, 0);
46 : 7045696 : Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
47 : 7045696 : return res;
48 : 3522848 : }
49 : :
50 : 174309 : std::string BitVector::toString(unsigned int base) const
51 : : {
52 : 174309 : std::string str = d_value.toString(base);
53 [ + + ][ + + ]: 174309 : if (base == 2 && d_size > str.size())
[ + + ]
54 : : {
55 : 125400 : std::string zeroes;
56 [ + + ]: 1308502 : for (unsigned int i = 0; i < d_size - str.size(); ++i)
57 : : {
58 : 1183102 : zeroes.append("0");
59 : : }
60 : 125400 : return zeroes + str;
61 : 125400 : }
62 : : else
63 : : {
64 : 48909 : return str;
65 : : }
66 : 174309 : }
67 : :
68 : 4530383 : size_t BitVector::hash() const
69 : : {
70 : : PairHashFunction<size_t, size_t> h;
71 : 4530383 : return h(std::make_pair(d_value.hash(), d_size));
72 : : }
73 : :
74 : 2269 : BitVector& BitVector::setBit(uint32_t i, bool value)
75 : : {
76 [ - + ][ - + ]: 2269 : Assert(i < d_size);
[ - - ]
77 : 2269 : d_value.setBit(i, value);
78 : 2269 : return *this;
79 : : }
80 : :
81 : 140634 : bool BitVector::isBitSet(uint32_t i) const
82 : : {
83 [ - + ][ - + ]: 140634 : Assert(i < d_size);
[ - - ]
84 : 140634 : return d_value.isBitSet(i);
85 : : }
86 : :
87 : 194988 : 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 : 307565 : BitVector BitVector::concat(const BitVector& other) const
98 : : {
99 : 307565 : return BitVector(d_size + other.d_size,
100 : 615130 : (d_value.multiplyByPow2(other.d_size)) + other.d_value);
101 : : }
102 : :
103 : 898272 : BitVector BitVector::extract(unsigned high, unsigned low) const
104 : : {
105 [ - + ][ - + ]: 898272 : Assert(high < d_size);
[ - - ]
106 [ - + ][ - + ]: 898272 : Assert(low <= high);
[ - - ]
107 : 898272 : return BitVector(high - low + 1,
108 : 1796544 : d_value.extractBitRange(high - low + 1, low));
109 : : }
110 : :
111 : : /* (Dis)Equality --------------------------------------------------------- */
112 : :
113 : 19028572 : bool operator==(const BitVector& a, const BitVector& b)
114 : : {
115 [ - + ]: 19028572 : if (a.getSize() != b.getSize()) return false;
116 : 19028572 : return a.getValue() == b.getValue();
117 : : }
118 : :
119 : 1162768 : bool operator!=(const BitVector& a, const BitVector& b)
120 : : {
121 [ - + ]: 1162768 : if (a.getSize() != b.getSize()) return true;
122 : 1162768 : return a.getValue() != b.getValue();
123 : : }
124 : :
125 : : /* Unsigned Inequality --------------------------------------------------- */
126 : :
127 : 1273 : bool operator<(const BitVector& a, const BitVector& b)
128 : : {
129 : 1273 : return a.getValue() < b.getValue();
130 : : }
131 : :
132 : 2560 : bool operator<=(const BitVector& a, const BitVector& b)
133 : : {
134 : 2560 : 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 : 986 : bool operator>=(const BitVector& a, const BitVector& b)
143 : : {
144 : 986 : return a.getValue() >= b.getValue();
145 : : }
146 : :
147 : 58117 : bool BitVector::unsignedLessThan(const BitVector& y) const
148 : : {
149 [ - + ][ - + ]: 58117 : Assert(d_size == y.d_size);
[ - - ]
150 [ - + ][ - + ]: 58117 : Assert(d_value >= 0);
[ - - ]
151 [ - + ][ - + ]: 58117 : Assert(y.d_value >= 0);
[ - - ]
152 : 58117 : return d_value < y.d_value;
153 : : }
154 : :
155 : 13604 : bool BitVector::unsignedLessThanEq(const BitVector& y) const
156 : : {
157 [ - + ][ - + ]: 13604 : Assert(d_size == y.d_size);
[ - - ]
158 [ - + ][ - + ]: 13604 : Assert(d_value >= 0);
[ - - ]
159 [ - + ][ - + ]: 13604 : Assert(y.d_value >= 0);
[ - - ]
160 : 13604 : return d_value <= y.d_value;
161 : : }
162 : :
163 : : /* Signed Inequality ----------------------------------------------------- */
164 : :
165 : 75292 : bool BitVector::signedLessThan(const BitVector& y) const
166 : : {
167 [ - + ][ - + ]: 75292 : Assert(d_size == y.d_size);
[ - - ]
168 [ - + ][ - + ]: 75292 : Assert(d_value >= 0);
[ - - ]
169 [ - + ][ - + ]: 75292 : Assert(y.d_value >= 0);
[ - - ]
170 : 75292 : Integer a = (*this).toSignedInteger();
171 : 75292 : Integer b = y.toSignedInteger();
172 : :
173 : 150584 : return a < b;
174 : 75292 : }
175 : :
176 : 1686102 : bool BitVector::signedLessThanEq(const BitVector& y) const
177 : : {
178 [ - + ][ - + ]: 1686102 : Assert(d_size == y.d_size);
[ - - ]
179 [ - + ][ - + ]: 1686102 : Assert(d_value >= 0);
[ - - ]
180 [ - + ][ - + ]: 1686102 : Assert(y.d_value >= 0);
[ - - ]
181 : 1686102 : Integer a = (*this).toSignedInteger();
182 : 1686102 : Integer b = y.toSignedInteger();
183 : :
184 : 3372204 : return a <= b;
185 : 1686102 : }
186 : :
187 : : /* Bit-wise operations --------------------------------------------------- */
188 : :
189 : 3211 : BitVector operator^(const BitVector& a, const BitVector& b)
190 : : {
191 [ - + ][ - + ]: 3211 : Assert(a.getSize() == b.getSize());
[ - - ]
192 : 6422 : return BitVector(a.getSize(), a.getValue().bitwiseXor(b.getValue()));
193 : : }
194 : :
195 : 327557 : BitVector operator|(const BitVector& a, const BitVector& b)
196 : : {
197 [ - + ][ - + ]: 327557 : Assert(a.getSize() == b.getSize());
[ - - ]
198 : 655114 : return BitVector(a.getSize(), a.getValue().bitwiseOr(b.getValue()));
199 : : }
200 : :
201 : 660812 : BitVector operator&(const BitVector& a, const BitVector& b)
202 : : {
203 [ - + ][ - + ]: 660812 : Assert(a.getSize() == b.getSize());
[ - - ]
204 : 1321624 : return BitVector(a.getSize(), a.getValue().bitwiseAnd(b.getValue()));
205 : : }
206 : :
207 : 4790630 : BitVector operator~(const BitVector& a)
208 : : {
209 : 9581260 : return BitVector(a.getSize(), a.getValue().bitwiseNot());
210 : : }
211 : :
212 : : /* Arithmetic operations ------------------------------------------------- */
213 : :
214 : 7537960 : BitVector operator+(const BitVector& a, const BitVector& b)
215 : : {
216 [ - + ][ - + ]: 7537960 : Assert(a.getSize() == b.getSize());
[ - - ]
217 : 7537960 : Integer sum = a.getValue() + b.getValue();
218 : 15075920 : return BitVector(a.getSize(), sum);
219 : 7537960 : }
220 : :
221 : 2835841 : BitVector operator-(const BitVector& a, const BitVector& b)
222 : : {
223 [ - + ][ - + ]: 2835841 : Assert(a.getSize() == b.getSize());
[ - - ]
224 : : // to maintain the invariant that we are only adding BitVectors of the
225 : : // same size
226 : 2835841 : BitVector one(a.getSize(), Integer(1));
227 : 8507523 : return a + ~b + one;
228 : 2835841 : }
229 : :
230 : 1600126 : BitVector operator-(const BitVector& a)
231 : : {
232 : 1600126 : BitVector one(a.getSize(), Integer(1));
233 : 4800378 : return ~a + one;
234 : 1600126 : }
235 : :
236 : 475649 : BitVector operator*(const BitVector& a, const BitVector& b)
237 : : {
238 [ - + ][ - + ]: 475649 : Assert(a.getSize() == b.getSize());
[ - - ]
239 : 475649 : Integer prod = a.getValue() * b.getValue();
240 : 951298 : return BitVector(a.getSize(), prod);
241 : 475649 : }
242 : :
243 : 62472 : BitVector BitVector::unsignedDivTotal(const BitVector& y) const
244 : : {
245 [ - + ][ - + ]: 62472 : Assert(d_size == y.d_size);
[ - - ]
246 : : /* d_value / 0 = -1 = 2^d_size - 1 */
247 [ + + ]: 62472 : if (y.d_value == 0)
248 : : {
249 : 16308 : return BitVector(d_size, Integer(1).oneExtend(1, d_size - 1));
250 : : }
251 [ - + ][ - + ]: 54318 : Assert(d_value >= 0);
[ - - ]
252 [ - + ][ - + ]: 54318 : Assert(y.d_value > 0);
[ - - ]
253 : 108636 : return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
254 : : }
255 : :
256 : 67332 : BitVector BitVector::unsignedRemTotal(const BitVector& y) const
257 : : {
258 [ - + ][ - + ]: 67332 : Assert(d_size == y.d_size);
[ - - ]
259 [ + + ]: 67332 : if (y.d_value == 0)
260 : : {
261 : 8113 : return BitVector(d_size, d_value);
262 : : }
263 [ - + ][ - + ]: 59219 : Assert(d_value >= 0);
[ - - ]
264 [ - + ][ - + ]: 59219 : Assert(y.d_value > 0);
[ - - ]
265 : 118438 : return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
266 : : }
267 : :
268 : : /* Extend operations ----------------------------------------------------- */
269 : :
270 : 588835 : BitVector BitVector::zeroExtend(unsigned n) const
271 : : {
272 : 588835 : return BitVector(d_size + n, d_value);
273 : : }
274 : :
275 : 1529468 : BitVector BitVector::signExtend(unsigned n) const
276 : : {
277 : 1529468 : Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
278 [ + + ]: 1529468 : if (sign_bit == Integer(0))
279 : : {
280 : 89975 : return BitVector(d_size + n, d_value);
281 : : }
282 : 1439493 : Integer val = d_value.oneExtend(d_size, n);
283 : 1439493 : return BitVector(d_size + n, val);
284 : 1529468 : }
285 : :
286 : : /* Shift operations ------------------------------------------------------ */
287 : :
288 : 2340578 : BitVector BitVector::leftShift(const BitVector& y) const
289 : : {
290 [ + + ]: 2340578 : if (y.d_value > Integer(d_size))
291 : : {
292 : 22218 : return BitVector(d_size, Integer(0));
293 : : }
294 [ + + ]: 2329469 : if (y.d_value == 0)
295 : : {
296 : 182274 : return *this;
297 : : }
298 : : // making sure we don't lose information casting
299 [ - + ][ - + ]: 2147195 : Assert(y.d_value < Integer(1).multiplyByPow2(32));
[ - - ]
300 : 2147195 : uint32_t amount = y.d_value.toUnsignedInt();
301 : 2147195 : Integer res = d_value.multiplyByPow2(amount);
302 : 2147195 : return BitVector(d_size, res);
303 : 2147195 : }
304 : :
305 : 57892 : BitVector BitVector::logicalRightShift(const BitVector& y) const
306 : : {
307 [ + + ]: 57892 : 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 [ - + ][ - + ]: 57891 : Assert(y.d_value < Integer(1).multiplyByPow2(32));
[ - - ]
313 : 57891 : uint32_t amount = y.d_value.toUnsignedInt();
314 : 57891 : Integer res = d_value.divByPow2(amount);
315 : 57891 : return BitVector(d_size, res);
316 : 57891 : }
317 : :
318 : 20623 : BitVector BitVector::arithRightShift(const BitVector& y) const
319 : : {
320 : 20623 : Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
321 [ + + ]: 20623 : if (y.d_value > Integer(d_size))
322 : : {
323 [ + + ]: 852 : if (sign_bit == Integer(0))
324 : : {
325 : 1074 : 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 [ + + ]: 19771 : if (y.d_value == 0)
334 : : {
335 : 754 : return *this;
336 : : }
337 : :
338 : : // making sure we don't lose information casting
339 [ - + ][ - + ]: 19017 : Assert(y.d_value < Integer(1).multiplyByPow2(32));
[ - - ]
340 : :
341 : 19017 : uint32_t amount = y.d_value.toUnsignedInt();
342 : 19017 : Integer rest = d_value.divByPow2(amount);
343 : :
344 [ + + ]: 19017 : if (sign_bit == Integer(0))
345 : : {
346 : 12862 : return BitVector(d_size, rest);
347 : : }
348 : 6155 : Integer res = rest.oneExtend(d_size - amount, amount);
349 : 6155 : return BitVector(d_size, res);
350 : 20623 : }
351 : :
352 : : /* -----------------------------------------------------------------------
353 : : * Static helpers.
354 : : * ----------------------------------------------------------------------- */
355 : :
356 : 41 : BitVector BitVector::mkZero(unsigned size)
357 : : {
358 [ - + ][ - + ]: 41 : Assert(size > 0);
[ - - ]
359 : 41 : return BitVector(size);
360 : : }
361 : :
362 : 45 : BitVector BitVector::mkOne(unsigned size)
363 : : {
364 [ - + ][ - + ]: 45 : Assert(size > 0);
[ - - ]
365 : 45 : return BitVector(size, 1u);
366 : : }
367 : :
368 : 1331928 : BitVector BitVector::mkOnes(unsigned size)
369 : : {
370 [ - + ][ - + ]: 1331928 : Assert(size > 0);
[ - - ]
371 : 2663856 : return BitVector(1, Integer(1)).signExtend(size - 1);
372 : : }
373 : :
374 : 127 : BitVector BitVector::mkMinSigned(unsigned 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(unsigned 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
|
