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 : : * Black box testing of cvc5::Integer.
11 : : */
12 : :
13 : : #include <limits>
14 : : #include <sstream>
15 : : #include <unordered_set>
16 : :
17 : : #include "base/exception.h"
18 : : #include "test.h"
19 : : #include "util/integer.h"
20 : : #include "util/random.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace test {
24 : :
25 : : class TestUtilBlackInteger : public TestInternal
26 : : {
27 : : protected:
28 : 35 : uint32_t internalLength(int32_t i)
29 : : {
30 [ + + ]: 35 : if (i == 0)
31 : : {
32 : 1 : return 1;
33 : : }
34 : : else
35 : : {
36 : 34 : int32_t absi = i < 0 ? -i : i;
37 : 34 : uint32_t n = 0;
38 : 34 : int32_t powN = 1;
39 : : do
40 : : {
41 : 118 : powN <<= 1;
42 : 118 : ++n;
43 [ + + ]: 118 : } while (absi >= powN);
44 : 34 : return n;
45 : : }
46 : : }
47 : : static const char* s_large_val;
48 : : static const char* s_lots_of_leading_zeros;
49 : : };
50 : :
51 : : const char* TestUtilBlackInteger::s_large_val =
52 : : "4547897890548754897897897897890789078907890";
53 : : const char* TestUtilBlackInteger::s_lots_of_leading_zeros =
54 : : "00000000000000000000000000000000000000000000000000000000000000000000000000"
55 : : "000000000000000000000000000000000000000000000000000000000000000000000001";
56 : :
57 : 4 : TEST_F(TestUtilBlackInteger, constructors)
58 : : {
59 : 1 : Integer z0(1);
60 [ - + ][ + - ]: 1 : ASSERT_EQ(z0.getLong(), 1);
61 : :
62 : 1 : Integer z1(0);
63 [ - + ][ + - ]: 1 : ASSERT_EQ(z1.getLong(), 0);
64 : :
65 : 1 : Integer z2(-1);
66 [ - + ][ + - ]: 1 : ASSERT_EQ(z2.getLong(), -1);
67 : :
68 : 1 : Integer z3(0x890UL);
69 [ - + ][ + - ]: 1 : ASSERT_EQ(z3.getUnsignedLong(), 0x890UL);
70 : :
71 : 1 : Integer z4;
72 [ - + ][ + - ]: 1 : ASSERT_EQ(z4.getLong(), 0);
73 : :
74 : 1 : Integer z5("7896890");
75 [ - + ][ + - ]: 1 : ASSERT_EQ(z5.getUnsignedLong(), 7896890ul);
76 : :
77 : 1 : Integer z6(z5);
78 [ - + ][ + - ]: 1 : ASSERT_EQ(z5.getUnsignedLong(), 7896890ul);
79 [ - + ][ + - ]: 1 : ASSERT_EQ(z6.getUnsignedLong(), 7896890ul);
80 : :
81 : 1 : std::string bigValue("1536729");
82 : 1 : Integer z7(bigValue);
83 [ - + ][ + - ]: 1 : ASSERT_EQ(z7.getUnsignedLong(), 1536729ul);
84 [ + - ]: 1 : }
85 : :
86 : 4 : TEST_F(TestUtilBlackInteger, compare_against_zero)
87 : : {
88 : 1 : Integer z(0);
89 [ + - ][ + - ]: 1 : ASSERT_NO_THROW((void)(z == 0););
[ + - ][ - - ]
90 [ - + ][ + - ]: 1 : ASSERT_EQ(z, 0);
91 [ + - ]: 1 : }
92 : :
93 : 4 : TEST_F(TestUtilBlackInteger, operator_assign)
94 : : {
95 : 1 : Integer x(0);
96 : 1 : Integer y(79);
97 : 1 : Integer z(45789);
98 : :
99 [ - + ][ + - ]: 1 : ASSERT_EQ(x.getUnsignedLong(), 0ul);
100 [ - + ][ + - ]: 1 : ASSERT_EQ(y.getUnsignedLong(), 79ul);
101 [ - + ][ + - ]: 1 : ASSERT_EQ(z.getUnsignedLong(), 45789ul);
102 : :
103 : 1 : x = y = z;
104 : :
105 [ - + ][ + - ]: 1 : ASSERT_EQ(x.getUnsignedLong(), 45789ul);
106 [ - + ][ + - ]: 1 : ASSERT_EQ(y.getUnsignedLong(), 45789ul);
107 [ - + ][ + - ]: 1 : ASSERT_EQ(z.getUnsignedLong(), 45789ul);
108 : :
109 : 1 : Integer a(2);
110 : :
111 : 1 : y = a;
112 : :
113 [ - + ][ + - ]: 1 : ASSERT_EQ(a.getUnsignedLong(), 2ul);
114 [ - + ][ + - ]: 1 : ASSERT_EQ(y.getUnsignedLong(), 2ul);
115 [ - + ][ + - ]: 1 : ASSERT_EQ(x.getUnsignedLong(), 45789ul);
116 [ - + ][ + - ]: 1 : ASSERT_EQ(z.getUnsignedLong(), 45789ul);
117 [ + - ][ + - ]: 1 : }
[ + - ]
118 : :
119 : 4 : TEST_F(TestUtilBlackInteger, operator_equals)
120 : : {
121 : 1 : Integer a(0);
122 : 1 : Integer b(79);
123 : 1 : Integer c("79");
124 : 1 : Integer d;
125 : :
126 [ - + ][ + - ]: 1 : ASSERT_TRUE(a == a);
127 [ - + ][ + - ]: 1 : ASSERT_FALSE(a == b);
128 [ - + ][ + - ]: 1 : ASSERT_FALSE(a == c);
129 [ - + ][ + - ]: 1 : ASSERT_TRUE(a == d);
130 : :
131 [ - + ][ + - ]: 1 : ASSERT_FALSE(b == a);
132 [ - + ][ + - ]: 1 : ASSERT_TRUE(b == b);
133 [ - + ][ + - ]: 1 : ASSERT_TRUE(b == c);
134 [ - + ][ + - ]: 1 : ASSERT_FALSE(b == d);
135 : :
136 [ - + ][ + - ]: 1 : ASSERT_FALSE(c == a);
137 [ - + ][ + - ]: 1 : ASSERT_TRUE(c == b);
138 [ - + ][ + - ]: 1 : ASSERT_TRUE(c == c);
139 [ - + ][ + - ]: 1 : ASSERT_FALSE(c == d);
140 : :
141 [ - + ][ + - ]: 1 : ASSERT_TRUE(d == a);
142 [ - + ][ + - ]: 1 : ASSERT_FALSE(d == b);
143 [ - + ][ + - ]: 1 : ASSERT_FALSE(d == c);
144 [ - + ][ + - ]: 1 : ASSERT_TRUE(d == d);
145 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
146 : :
147 : 4 : TEST_F(TestUtilBlackInteger, operator_not_equals)
148 : : {
149 : 1 : Integer a(0);
150 : 1 : Integer b(79);
151 : 1 : Integer c("79");
152 : 1 : Integer d;
153 : :
154 [ - + ][ + - ]: 1 : ASSERT_FALSE(a != a);
155 [ - + ][ + - ]: 1 : ASSERT_TRUE(a != b);
156 [ - + ][ + - ]: 1 : ASSERT_TRUE(a != c);
157 [ - + ][ + - ]: 1 : ASSERT_FALSE(a != d);
158 : :
159 [ - + ][ + - ]: 1 : ASSERT_TRUE(b != a);
160 [ - + ][ + - ]: 1 : ASSERT_FALSE(b != b);
161 [ - + ][ + - ]: 1 : ASSERT_FALSE(b != c);
162 [ - + ][ + - ]: 1 : ASSERT_TRUE(b != d);
163 : :
164 [ - + ][ + - ]: 1 : ASSERT_TRUE(c != a);
165 [ - + ][ + - ]: 1 : ASSERT_FALSE(c != b);
166 [ - + ][ + - ]: 1 : ASSERT_FALSE(c != c);
167 [ - + ][ + - ]: 1 : ASSERT_TRUE(c != d);
168 : :
169 [ - + ][ + - ]: 1 : ASSERT_FALSE(d != a);
170 [ - + ][ + - ]: 1 : ASSERT_TRUE(d != b);
171 [ - + ][ + - ]: 1 : ASSERT_TRUE(d != c);
172 [ - + ][ + - ]: 1 : ASSERT_FALSE(d != d);
173 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
174 : :
175 : 4 : TEST_F(TestUtilBlackInteger, operator_subtract)
176 : : {
177 : 1 : Integer x(0);
178 : 1 : Integer y(79);
179 : 1 : Integer z(-34);
180 : :
181 : 1 : Integer act0 = x - x;
182 : 1 : Integer act1 = x - y;
183 : 1 : Integer act2 = x - z;
184 : 1 : Integer exp0(0);
185 : 1 : Integer exp1(-79);
186 : 1 : Integer exp2(34);
187 : :
188 : 1 : Integer act3 = y - x;
189 : 1 : Integer act4 = y - y;
190 : 1 : Integer act5 = y - z;
191 : 1 : Integer exp3(79);
192 : 1 : Integer exp4(0);
193 : 1 : Integer exp5(113);
194 : :
195 : 1 : Integer act6 = z - x;
196 : 1 : Integer act7 = z - y;
197 : 1 : Integer act8 = z - z;
198 : 1 : Integer exp6(-34);
199 : 1 : Integer exp7(-113);
200 : 1 : Integer exp8(0);
201 : :
202 [ - + ][ + - ]: 1 : ASSERT_EQ(act0, exp0);
203 [ - + ][ + - ]: 1 : ASSERT_EQ(act1, exp1);
204 [ - + ][ + - ]: 1 : ASSERT_EQ(act2, exp2);
205 [ - + ][ + - ]: 1 : ASSERT_EQ(act3, exp3);
206 [ - + ][ + - ]: 1 : ASSERT_EQ(act4, exp4);
207 [ - + ][ + - ]: 1 : ASSERT_EQ(act5, exp5);
208 [ - + ][ + - ]: 1 : ASSERT_EQ(act6, exp6);
209 [ - + ][ + - ]: 1 : ASSERT_EQ(act7, exp7);
210 [ - + ][ + - ]: 1 : ASSERT_EQ(act8, exp8);
211 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
212 : :
213 : 4 : TEST_F(TestUtilBlackInteger, operator_add)
214 : : {
215 : 1 : Integer x(0);
216 : 1 : Integer y(79);
217 : 1 : Integer z(-34);
218 : :
219 : 1 : Integer act0 = x + x;
220 : 1 : Integer act1 = x + y;
221 : 1 : Integer act2 = x + z;
222 : 1 : Integer exp0(0);
223 : 1 : Integer exp1(79);
224 : 1 : Integer exp2(-34);
225 : :
226 : 1 : Integer act3 = y + x;
227 : 1 : Integer act4 = y + y;
228 : 1 : Integer act5 = y + z;
229 : 1 : Integer exp3(79);
230 : 1 : Integer exp4(158);
231 : 1 : Integer exp5(45);
232 : :
233 : 1 : Integer act6 = z + x;
234 : 1 : Integer act7 = z + y;
235 : 1 : Integer act8 = z + z;
236 : 1 : Integer exp6(-34);
237 : 1 : Integer exp7(45);
238 : 1 : Integer exp8(-68);
239 : :
240 [ - + ][ + - ]: 1 : ASSERT_EQ(act0, exp0);
241 [ - + ][ + - ]: 1 : ASSERT_EQ(act1, exp1);
242 [ - + ][ + - ]: 1 : ASSERT_EQ(act2, exp2);
243 [ - + ][ + - ]: 1 : ASSERT_EQ(act3, exp3);
244 [ - + ][ + - ]: 1 : ASSERT_EQ(act4, exp4);
245 [ - + ][ + - ]: 1 : ASSERT_EQ(act5, exp5);
246 [ - + ][ + - ]: 1 : ASSERT_EQ(act6, exp6);
247 [ - + ][ + - ]: 1 : ASSERT_EQ(act7, exp7);
248 [ - + ][ + - ]: 1 : ASSERT_EQ(act8, exp8);
249 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
250 : :
251 : 4 : TEST_F(TestUtilBlackInteger, operator_mult)
252 : : {
253 : 1 : Integer x(0);
254 : 1 : Integer y(79);
255 : 1 : Integer z(-34);
256 : :
257 : 1 : Integer act0 = x * x;
258 : 1 : Integer act1 = x * y;
259 : 1 : Integer act2 = x * z;
260 : 1 : Integer exp0(0);
261 : 1 : Integer exp1(0);
262 : 1 : Integer exp2(0);
263 : :
264 : 1 : Integer act3 = y * x;
265 : 1 : Integer act4 = y * y;
266 : 1 : Integer act5 = y * z;
267 : 1 : Integer exp3(0);
268 : 1 : Integer exp4(6241);
269 : 1 : Integer exp5(-2686);
270 : :
271 : 1 : Integer act6 = z * x;
272 : 1 : Integer act7 = z * y;
273 : 1 : Integer act8 = z * z;
274 : 1 : Integer exp6(0);
275 : 1 : Integer exp7(-2686);
276 : 1 : Integer exp8(1156);
277 : :
278 [ - + ][ + - ]: 1 : ASSERT_EQ(act0, exp0);
279 [ - + ][ + - ]: 1 : ASSERT_EQ(act1, exp1);
280 [ - + ][ + - ]: 1 : ASSERT_EQ(act2, exp2);
281 [ - + ][ + - ]: 1 : ASSERT_EQ(act3, exp3);
282 [ - + ][ + - ]: 1 : ASSERT_EQ(act4, exp4);
283 [ - + ][ + - ]: 1 : ASSERT_EQ(act5, exp5);
284 [ - + ][ + - ]: 1 : ASSERT_EQ(act6, exp6);
285 [ - + ][ + - ]: 1 : ASSERT_EQ(act7, exp7);
286 [ - + ][ + - ]: 1 : ASSERT_EQ(act8, exp8);
287 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
288 : :
289 : 4 : TEST_F(TestUtilBlackInteger, to_string)
290 : : {
291 : 1 : std::stringstream ss;
292 : 1 : Integer large(s_large_val);
293 : 1 : ss << large;
294 : 1 : std::string res = ss.str();
295 : :
296 [ - + ][ + - ]: 2 : ASSERT_EQ(res, large.toString());
297 [ + - ][ + - ]: 1 : }
[ + - ]
298 : :
299 : 4 : TEST_F(TestUtilBlackInteger, base_inference)
300 : : {
301 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer("0xa", 0), 10);
302 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer("0xff", 0), 255);
303 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer("011", 0), 9);
304 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer("0b1010", 0), 10);
305 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer("-1", 0), -1);
306 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer("42", 0), 42);
307 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer("0", 0), 0);
308 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer("-0", 0), 0);
309 : : }
310 : :
311 : 4 : TEST_F(TestUtilBlackInteger, fits_signed_int)
312 : : {
313 : 1 : Integer imin(std::numeric_limits<int>::min());
314 : 1 : Integer imax(std::numeric_limits<int>::max());
315 : 1 : Integer too_small(std::numeric_limits<int64_t>::min());
316 [ - + ][ + - ]: 1 : ASSERT_TRUE(imin.fitsSignedInt());
317 [ - + ][ + - ]: 1 : ASSERT_TRUE(imax.fitsSignedInt());
318 [ - + ][ + - ]: 1 : ASSERT_FALSE(too_small.fitsSignedInt());
319 [ - + ][ + - ]: 1 : ASSERT_EQ(imin.getSignedInt(), std::numeric_limits<int>::min());
320 [ - + ][ + - ]: 1 : ASSERT_EQ(imax.getSignedInt(), std::numeric_limits<int>::max());
321 [ + - ][ + - ]: 1 : }
[ + - ]
322 : :
323 : 4 : TEST_F(TestUtilBlackInteger, parse_errors)
324 : : {
325 : 1 : ASSERT_THROW(Integer("abracadabra"), std::invalid_argument);
326 : 1 : ASSERT_THROW(Integer("+-1"), std::invalid_argument);
327 : 1 : ASSERT_THROW(Integer("-+1"), std::invalid_argument);
328 : 1 : ASSERT_THROW(Integer("5i"), std::invalid_argument);
329 : 1 : ASSERT_THROW(Integer("10xyz"), std::invalid_argument);
330 : 1 : ASSERT_THROW(Integer("0xff", 10), std::invalid_argument);
331 : 1 : ASSERT_THROW(Integer("#x5", 0), std::invalid_argument);
332 : 1 : ASSERT_THROW(Integer("0b123", 0), std::invalid_argument);
333 : : }
334 : :
335 : 4 : TEST_F(TestUtilBlackInteger, pow)
336 : : {
337 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(1), Integer(1).pow(0));
338 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(1), Integer(5).pow(0));
339 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(1), Integer(-1).pow(0));
340 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(0), Integer(0).pow(1));
341 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(5), Integer(5).pow(1));
342 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(-5), Integer(-5).pow(1));
343 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(16), Integer(2).pow(4));
344 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(16), Integer(-2).pow(4));
345 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(1000), Integer(10).pow(3));
346 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(-1000), Integer(-10).pow(3));
347 : : }
348 : :
349 : 4 : TEST_F(TestUtilBlackInteger, overly_long_signed)
350 : : {
351 : 1 : int64_t sl = std::numeric_limits<int64_t>::max();
352 : 1 : Integer i(sl);
353 : : if constexpr (sizeof(unsigned long) == sizeof(uint64_t))
354 : : {
355 [ - + ][ + - ]: 1 : ASSERT_EQ(i.getLong(), sl);
356 : : }
357 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(i.getSigned64());
[ + - ][ - - ]
358 [ - + ][ + - ]: 1 : ASSERT_EQ(i.getSigned64(), sl);
359 : 1 : i = i + 1;
360 : 1 : ASSERT_DEATH(i.getSigned64(), "Overflow detected");
361 [ + - ]: 1 : }
362 : :
363 : 4 : TEST_F(TestUtilBlackInteger, overly_long_unsigned)
364 : : {
365 : 1 : uint64_t ul = std::numeric_limits<uint64_t>::max();
366 : 1 : Integer i(ul);
367 : : if constexpr (sizeof(unsigned long) == sizeof(uint64_t))
368 : : {
369 [ - + ][ + - ]: 1 : ASSERT_EQ(i.getUnsignedLong(), ul);
370 : : }
371 : 1 : ASSERT_DEATH(i.getLong(), "Overflow detected");
372 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(i.getUnsigned64());
[ + - ][ - - ]
373 [ - + ][ + - ]: 1 : ASSERT_EQ(i.getUnsigned64(), ul);
374 : 1 : uint64_t ulplus1 = ul + 1;
375 [ - + ][ + - ]: 1 : ASSERT_EQ(ulplus1, 0);
376 : 1 : i = i + 1;
377 : 1 : ASSERT_DEATH(i.getUnsignedLong(), "Overflow detected");
378 [ + - ]: 1 : }
379 : :
380 : 4 : TEST_F(TestUtilBlackInteger, getSigned64)
381 : : {
382 : : {
383 : 1 : int64_t i = std::numeric_limits<int64_t>::max();
384 : 1 : Integer a(i);
385 [ - + ][ + - ]: 1 : ASSERT_EQ(a.getSigned64(), i);
386 : 1 : ASSERT_DEATH((a + 1).getSigned64(), "Overflow detected");
387 [ + - ]: 1 : }
388 : : {
389 : 1 : int64_t i = std::numeric_limits<int64_t>::min();
390 : 1 : Integer a(i);
391 [ - + ][ + - ]: 1 : ASSERT_EQ(a.getSigned64(), i);
392 : 1 : ASSERT_DEATH((a - 1).getSigned64(), "Overflow detected");
393 [ + - ]: 1 : }
394 : : }
395 : :
396 : 4 : TEST_F(TestUtilBlackInteger, getUnsigned64)
397 : : {
398 : : {
399 : 1 : uint64_t i = std::numeric_limits<uint64_t>::max();
400 : 1 : Integer a(i);
401 [ - + ][ + - ]: 1 : ASSERT_EQ(a.getUnsigned64(), i);
402 : 1 : ASSERT_DEATH((a + 1).getUnsigned64(), "Overflow detected");
403 [ + - ]: 1 : }
404 : : {
405 : 1 : uint64_t i = std::numeric_limits<uint64_t>::min();
406 : 1 : Integer a(i);
407 [ - + ][ + - ]: 1 : ASSERT_EQ(a.getUnsigned64(), i);
408 : 1 : ASSERT_DEATH((a - 1).getUnsigned64(), "Overflow detected");
409 [ + - ]: 1 : }
410 : : }
411 : :
412 : 4 : TEST_F(TestUtilBlackInteger, testBit)
413 : : {
414 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(6));
415 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(5));
416 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(4));
417 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(3));
418 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(2));
419 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(1));
420 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(0));
421 : :
422 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(6));
423 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(5));
424 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(4));
425 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(3));
426 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(2));
427 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(1));
428 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(0));
429 : :
430 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(10).testBit(6));
431 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(10).testBit(5));
432 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(10).testBit(4));
433 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(10).testBit(3));
434 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(10).testBit(2));
435 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(10).testBit(1));
436 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(10).testBit(0));
437 : :
438 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(14).testBit(6));
439 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(14).testBit(5));
440 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(14).testBit(4));
441 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(14).testBit(3));
442 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(14).testBit(2));
443 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(14).testBit(1));
444 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(14).testBit(0));
445 : :
446 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(64).testBit(6));
447 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(5));
448 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(4));
449 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(3));
450 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(2));
451 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(1));
452 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(0));
453 : : }
454 : :
455 : 4 : TEST_F(TestUtilBlackInteger, length)
456 : : {
457 [ + + ]: 36 : for (int32_t i = -17; i <= 17; ++i)
458 : : {
459 [ - + ][ + - ]: 35 : ASSERT_EQ(Integer(i).length(), internalLength(i));
460 : : }
461 : : }
462 : :
463 : 4 : TEST_F(TestUtilBlackInteger, euclidianQR)
464 : : {
465 : 1 : Integer q, r;
466 : :
467 : 1 : Integer::euclidianQR(q, r, 1, 4);
468 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(0));
469 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
470 : :
471 : 1 : Integer::euclidianQR(q, r, 1, -4);
472 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(0));
473 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
474 : :
475 : 1 : Integer::euclidianQR(q, r, -1, 4);
476 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-1));
477 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
478 : :
479 : 1 : Integer::euclidianQR(q, r, -1, -4);
480 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(1));
481 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
482 : :
483 : 1 : Integer::euclidianQR(q, r, 5, 4);
484 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(1));
485 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
486 : :
487 : 1 : Integer::euclidianQR(q, r, 5, -4);
488 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-1));
489 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
490 : :
491 : 1 : Integer::euclidianQR(q, r, -5, 4);
492 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-2));
493 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
494 : :
495 : 1 : Integer::euclidianQR(q, r, -5, -4);
496 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(2));
497 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
498 [ + - ][ + - ]: 1 : }
499 : :
500 : 4 : TEST_F(TestUtilBlackInteger, floorQR)
501 : : {
502 : 1 : Integer q, r;
503 : :
504 : 1 : Integer::floorQR(q, r, 1, 4);
505 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(0));
506 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
507 : :
508 : 1 : Integer::floorQR(q, r, 1, -4);
509 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-1));
510 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(-3));
511 : :
512 : 1 : Integer::floorQR(q, r, -1, 4);
513 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-1));
514 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
515 : :
516 : 1 : Integer::floorQR(q, r, -1, -4);
517 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(0));
518 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(-1));
519 : :
520 : 1 : Integer::floorQR(q, r, 5, 4);
521 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(1));
522 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
523 : :
524 : 1 : Integer::floorQR(q, r, 5, -4);
525 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-2));
526 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(-3));
527 : :
528 : 1 : Integer::floorQR(q, r, -5, 4);
529 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-2));
530 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
531 : :
532 : 1 : Integer::floorQR(q, r, -5, -4);
533 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(1));
534 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(-1));
535 [ + - ][ + - ]: 1 : }
536 : :
537 : 4 : TEST_F(TestUtilBlackInteger, leadingZeros)
538 : : {
539 : 1 : std::string leadingZeros(s_lots_of_leading_zeros);
540 : 1 : Integer one(1u);
541 : 1 : Integer one_from_string(leadingZeros, 2);
542 [ - + ][ + - ]: 1 : ASSERT_EQ(one, one_from_string);
543 [ + - ][ + - ]: 1 : }
[ + - ]
544 : :
545 : 4 : TEST_F(TestUtilBlackInteger, modAdd)
546 : : {
547 [ + + ]: 12 : for (uint32_t i = 0; i <= 10; ++i)
548 : : {
549 [ + + ]: 132 : for (uint32_t j = 0; j <= 10; ++j)
550 : : {
551 : 121 : Integer yy;
552 : 121 : Integer x(i);
553 : 121 : Integer y = x + j;
554 : 242 : Integer yp = x.modAdd(j, 3);
555 [ + + ]: 484 : for (yy = y; yy >= 3; yy -= 3);
556 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
557 : 121 : yp = x.modAdd(j, 7);
558 [ + + ]: 242 : for (yy = y; yy >= 7; yy -= 7);
559 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
560 : 121 : yp = x.modAdd(j, 11);
561 [ + + ]: 176 : for (yy = y; yy >= 11; yy -= 11);
562 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
563 [ + - ][ + - ]: 121 : }
[ + - ][ + - ]
564 : : }
565 : : }
566 : :
567 : 4 : TEST_F(TestUtilBlackInteger, modMultiply)
568 : : {
569 [ + + ]: 12 : for (uint32_t i = 0; i <= 10; ++i)
570 : : {
571 [ + + ]: 132 : for (uint32_t j = 0; j <= 10; ++j)
572 : : {
573 : 121 : Integer yy;
574 : 121 : Integer x(i);
575 : 121 : Integer y = x * j;
576 : 242 : Integer yp = x.modMultiply(j, 3);
577 [ + + ]: 1105 : for (yy = y; yy >= 3; yy -= 3);
578 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
579 : 121 : yp = x.modMultiply(j, 7);
580 [ + + ]: 513 : for (yy = y; yy >= 7; yy -= 7);
581 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
582 : 121 : yp = x.modMultiply(j, 11);
583 [ + + ]: 346 : for (yy = y; yy >= 11; yy -= 11);
584 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
585 [ + - ][ + - ]: 121 : }
[ + - ][ + - ]
586 : : }
587 : : }
588 : :
589 : 4 : TEST_F(TestUtilBlackInteger, modInverse)
590 : : {
591 [ + + ]: 12 : for (uint32_t i = 0; i <= 10; ++i)
592 : : {
593 : 11 : Integer x(i);
594 : 11 : Integer inv = x.modInverse(3);
595 [ + + ][ + + ]: 11 : if (i == 0 || i == 3 || i == 6 || i == 9)
[ + + ][ + + ]
596 : : {
597 [ - + ][ + - ]: 4 : ASSERT_EQ(inv, -1); /* no inverse */
598 : 4 : }
599 : : else
600 : : {
601 [ - + ][ + - ]: 14 : ASSERT_EQ(x.modMultiply(inv, 3), 1);
602 : : }
603 : 11 : inv = x.modInverse(7);
604 [ + + ][ + + ]: 11 : if (i == 0 || i == 7)
605 : : {
606 [ - + ][ + - ]: 2 : ASSERT_EQ(inv, -1); /* no inverse */
607 : 2 : }
608 : : else
609 : : {
610 [ - + ][ + - ]: 18 : ASSERT_EQ(x.modMultiply(inv, 7), 1);
611 : : }
612 : 11 : inv = x.modInverse(11);
613 [ + + ]: 11 : if (i == 0)
614 : : {
615 [ - + ][ + - ]: 1 : ASSERT_EQ(inv, -1); /* no inverse */
616 : : }
617 : : else
618 : : {
619 [ - + ][ + - ]: 20 : ASSERT_EQ(x.modMultiply(inv, 11), 1);
620 : : }
621 [ + - ][ + - ]: 11 : }
622 : : }
623 : :
624 : 4 : TEST_F(TestUtilBlackInteger, mkRandom_bound)
625 : : {
626 : : // Result must be in [0, 2^nbits) for various bit widths
627 : 1 : uint32_t sizes[] = {1, 2, 7, 8, 16, 32, 63, 64, 65, 100, 128, 256};
628 [ + + ]: 13 : for (uint32_t nbits : sizes)
629 : : {
630 : 12 : Integer bound = Integer(1).multiplyByPow2(nbits);
631 : 12 : std::unordered_set<Integer> values;
632 [ + + ]: 252 : for (size_t i = 0; i < 20; ++i)
633 : : {
634 : 240 : Integer v = Integer::mkRandom(nbits);
635 : 240 : values.insert(v);
636 [ - + ][ + - ]: 240 : ASSERT_TRUE(v >= 0);
637 [ - + ][ + - ]: 240 : ASSERT_TRUE(v < bound);
638 [ + - ]: 240 : }
639 [ - + ][ + - ]: 12 : ASSERT_GT(values.size(), 1);
640 [ + - ][ + - ]: 12 : }
641 : : }
642 : :
643 : 4 : TEST_F(TestUtilBlackInteger, mkRandom_deterministic)
644 : : {
645 : : // Same seed should produce the same sequence
646 : 1 : Random::getRandom().setSeed(42);
647 : 1 : Integer a1 = Integer::mkRandom(128);
648 : 1 : Integer a2 = Integer::mkRandom(128);
649 : :
650 : 1 : Random::getRandom().setSeed(42);
651 : 1 : Integer b1 = Integer::mkRandom(128);
652 : 1 : Integer b2 = Integer::mkRandom(128);
653 : :
654 [ - + ][ + - ]: 1 : ASSERT_EQ(a1, b1);
655 [ - + ][ + - ]: 1 : ASSERT_EQ(a2, b2);
656 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
657 : :
658 : 4 : TEST_F(TestUtilBlackInteger, mkRandom_not_always_zero)
659 : : {
660 : : // With 128 bits, getting all zeros 10 times in a row is unlikely.
661 : 1 : Random::getRandom().setSeed(0);
662 : 1 : bool nonZero = false;
663 [ + - ]: 1 : for (int i = 0; i < 10; ++i)
664 : : {
665 [ + - ]: 1 : if (!Integer::mkRandom(128).isZero())
666 : : {
667 : 1 : nonZero = true;
668 : 1 : break;
669 : : }
670 : : }
671 [ - + ][ + - ]: 1 : ASSERT_TRUE(nonZero);
672 : : }
673 : :
674 : : } // namespace test
675 : : } // namespace cvc5::internal
|
