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 : : }
308 : :
309 : 4 : TEST_F(TestUtilBlackInteger, parse_errors)
310 : : {
311 : 1 : ASSERT_THROW(Integer("abracadabra"), std::invalid_argument);
312 : 1 : ASSERT_THROW(Integer("+-1"), std::invalid_argument);
313 : 1 : ASSERT_THROW(Integer("-+1"), std::invalid_argument);
314 : 1 : ASSERT_THROW(Integer("5i"), std::invalid_argument);
315 : 1 : ASSERT_THROW(Integer("10xyz"), std::invalid_argument);
316 : 1 : ASSERT_THROW(Integer("0xff", 10), std::invalid_argument);
317 : 1 : ASSERT_THROW(Integer("#x5", 0), std::invalid_argument);
318 : 1 : ASSERT_THROW(Integer("0b123", 0), std::invalid_argument);
319 : : }
320 : :
321 : 4 : TEST_F(TestUtilBlackInteger, pow)
322 : : {
323 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(1), Integer(1).pow(0));
324 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(1), Integer(5).pow(0));
325 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(1), Integer(-1).pow(0));
326 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(0), Integer(0).pow(1));
327 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(5), Integer(5).pow(1));
328 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(-5), Integer(-5).pow(1));
329 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(16), Integer(2).pow(4));
330 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(16), Integer(-2).pow(4));
331 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(1000), Integer(10).pow(3));
332 [ - + ][ + - ]: 2 : ASSERT_EQ(Integer(-1000), Integer(-10).pow(3));
333 : : }
334 : :
335 : 4 : TEST_F(TestUtilBlackInteger, overly_long_signed)
336 : : {
337 : 1 : int64_t sl = std::numeric_limits<int64_t>::max();
338 : 1 : Integer i(sl);
339 : : if constexpr (sizeof(unsigned long) == sizeof(uint64_t))
340 : : {
341 [ - + ][ + - ]: 1 : ASSERT_EQ(i.getLong(), sl);
342 : : }
343 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(i.getSigned64());
[ + - ][ - - ]
344 [ - + ][ + - ]: 1 : ASSERT_EQ(i.getSigned64(), sl);
345 : 1 : i = i + 1;
346 : 1 : ASSERT_DEATH(i.getSigned64(), "Overflow detected");
347 [ + - ]: 1 : }
348 : :
349 : 4 : TEST_F(TestUtilBlackInteger, overly_long_unsigned)
350 : : {
351 : 1 : uint64_t ul = std::numeric_limits<uint64_t>::max();
352 : 1 : Integer i(ul);
353 : : if constexpr (sizeof(unsigned long) == sizeof(uint64_t))
354 : : {
355 [ - + ][ + - ]: 1 : ASSERT_EQ(i.getUnsignedLong(), ul);
356 : : }
357 : 1 : ASSERT_DEATH(i.getLong(), "Overflow detected");
358 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(i.getUnsigned64());
[ + - ][ - - ]
359 [ - + ][ + - ]: 1 : ASSERT_EQ(i.getUnsigned64(), ul);
360 : 1 : uint64_t ulplus1 = ul + 1;
361 [ - + ][ + - ]: 1 : ASSERT_EQ(ulplus1, 0);
362 : 1 : i = i + 1;
363 : 1 : ASSERT_DEATH(i.getUnsignedLong(), "Overflow detected");
364 [ + - ]: 1 : }
365 : :
366 : 4 : TEST_F(TestUtilBlackInteger, getSigned64)
367 : : {
368 : : {
369 : 1 : int64_t i = std::numeric_limits<int64_t>::max();
370 : 1 : Integer a(i);
371 [ - + ][ + - ]: 1 : ASSERT_EQ(a.getSigned64(), i);
372 : 1 : ASSERT_DEATH((a + 1).getSigned64(), "Overflow detected");
373 [ + - ]: 1 : }
374 : : {
375 : 1 : int64_t i = std::numeric_limits<int64_t>::min();
376 : 1 : Integer a(i);
377 [ - + ][ + - ]: 1 : ASSERT_EQ(a.getSigned64(), i);
378 : 1 : ASSERT_DEATH((a - 1).getSigned64(), "Overflow detected");
379 [ + - ]: 1 : }
380 : : }
381 : :
382 : 4 : TEST_F(TestUtilBlackInteger, getUnsigned64)
383 : : {
384 : : {
385 : 1 : uint64_t i = std::numeric_limits<uint64_t>::max();
386 : 1 : Integer a(i);
387 [ - + ][ + - ]: 1 : ASSERT_EQ(a.getUnsigned64(), i);
388 : 1 : ASSERT_DEATH((a + 1).getUnsigned64(), "Overflow detected");
389 [ + - ]: 1 : }
390 : : {
391 : 1 : uint64_t i = std::numeric_limits<uint64_t>::min();
392 : 1 : Integer a(i);
393 [ - + ][ + - ]: 1 : ASSERT_EQ(a.getUnsigned64(), i);
394 : 1 : ASSERT_DEATH((a - 1).getUnsigned64(), "Overflow detected");
395 [ + - ]: 1 : }
396 : : }
397 : :
398 : 4 : TEST_F(TestUtilBlackInteger, testBit)
399 : : {
400 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(6));
401 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(5));
402 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(4));
403 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(3));
404 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(2));
405 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(1));
406 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(0).testBit(0));
407 : :
408 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(6));
409 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(5));
410 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(4));
411 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(3));
412 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(2));
413 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(1));
414 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(-1).testBit(0));
415 : :
416 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(10).testBit(6));
417 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(10).testBit(5));
418 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(10).testBit(4));
419 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(10).testBit(3));
420 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(10).testBit(2));
421 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(10).testBit(1));
422 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(10).testBit(0));
423 : :
424 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(14).testBit(6));
425 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(14).testBit(5));
426 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(14).testBit(4));
427 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(14).testBit(3));
428 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(14).testBit(2));
429 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(14).testBit(1));
430 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(14).testBit(0));
431 : :
432 [ - + ][ + - ]: 1 : ASSERT_TRUE(Integer(64).testBit(6));
433 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(5));
434 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(4));
435 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(3));
436 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(2));
437 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(1));
438 [ - + ][ + - ]: 1 : ASSERT_FALSE(Integer(64).testBit(0));
439 : : }
440 : :
441 : 4 : TEST_F(TestUtilBlackInteger, length)
442 : : {
443 [ + + ]: 36 : for (int32_t i = -17; i <= 17; ++i)
444 : : {
445 [ - + ][ + - ]: 35 : ASSERT_EQ(Integer(i).length(), internalLength(i));
446 : : }
447 : : }
448 : :
449 : 4 : TEST_F(TestUtilBlackInteger, euclidianQR)
450 : : {
451 : 1 : Integer q, r;
452 : :
453 : 1 : Integer::euclidianQR(q, r, 1, 4);
454 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(0));
455 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
456 : :
457 : 1 : Integer::euclidianQR(q, r, 1, -4);
458 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(0));
459 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
460 : :
461 : 1 : Integer::euclidianQR(q, r, -1, 4);
462 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-1));
463 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
464 : :
465 : 1 : Integer::euclidianQR(q, r, -1, -4);
466 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(1));
467 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
468 : :
469 : 1 : Integer::euclidianQR(q, r, 5, 4);
470 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(1));
471 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
472 : :
473 : 1 : Integer::euclidianQR(q, r, 5, -4);
474 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-1));
475 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
476 : :
477 : 1 : Integer::euclidianQR(q, r, -5, 4);
478 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-2));
479 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
480 : :
481 : 1 : Integer::euclidianQR(q, r, -5, -4);
482 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(2));
483 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
484 [ + - ][ + - ]: 1 : }
485 : :
486 : 4 : TEST_F(TestUtilBlackInteger, floorQR)
487 : : {
488 : 1 : Integer q, r;
489 : :
490 : 1 : Integer::floorQR(q, r, 1, 4);
491 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(0));
492 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
493 : :
494 : 1 : Integer::floorQR(q, r, 1, -4);
495 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-1));
496 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(-3));
497 : :
498 : 1 : Integer::floorQR(q, r, -1, 4);
499 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-1));
500 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
501 : :
502 : 1 : Integer::floorQR(q, r, -1, -4);
503 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(0));
504 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(-1));
505 : :
506 : 1 : Integer::floorQR(q, r, 5, 4);
507 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(1));
508 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(1));
509 : :
510 : 1 : Integer::floorQR(q, r, 5, -4);
511 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-2));
512 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(-3));
513 : :
514 : 1 : Integer::floorQR(q, r, -5, 4);
515 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(-2));
516 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(3));
517 : :
518 : 1 : Integer::floorQR(q, r, -5, -4);
519 [ - + ][ + - ]: 2 : ASSERT_EQ(q, Integer(1));
520 [ - + ][ + - ]: 2 : ASSERT_EQ(r, Integer(-1));
521 [ + - ][ + - ]: 1 : }
522 : :
523 : 4 : TEST_F(TestUtilBlackInteger, leadingZeros)
524 : : {
525 : 1 : std::string leadingZeros(s_lots_of_leading_zeros);
526 : 1 : Integer one(1u);
527 : 1 : Integer one_from_string(leadingZeros, 2);
528 [ - + ][ + - ]: 1 : ASSERT_EQ(one, one_from_string);
529 [ + - ][ + - ]: 1 : }
[ + - ]
530 : :
531 : 4 : TEST_F(TestUtilBlackInteger, modAdd)
532 : : {
533 [ + + ]: 12 : for (uint32_t i = 0; i <= 10; ++i)
534 : : {
535 [ + + ]: 132 : for (uint32_t j = 0; j <= 10; ++j)
536 : : {
537 : 121 : Integer yy;
538 : 121 : Integer x(i);
539 : 121 : Integer y = x + j;
540 : 242 : Integer yp = x.modAdd(j, 3);
541 [ + + ]: 484 : for (yy = y; yy >= 3; yy -= 3);
542 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
543 : 121 : yp = x.modAdd(j, 7);
544 [ + + ]: 242 : for (yy = y; yy >= 7; yy -= 7);
545 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
546 : 121 : yp = x.modAdd(j, 11);
547 [ + + ]: 176 : for (yy = y; yy >= 11; yy -= 11);
548 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
549 [ + - ][ + - ]: 121 : }
[ + - ][ + - ]
550 : : }
551 : : }
552 : :
553 : 4 : TEST_F(TestUtilBlackInteger, modMultiply)
554 : : {
555 [ + + ]: 12 : for (uint32_t i = 0; i <= 10; ++i)
556 : : {
557 [ + + ]: 132 : for (uint32_t j = 0; j <= 10; ++j)
558 : : {
559 : 121 : Integer yy;
560 : 121 : Integer x(i);
561 : 121 : Integer y = x * j;
562 : 242 : Integer yp = x.modMultiply(j, 3);
563 [ + + ]: 1105 : for (yy = y; yy >= 3; yy -= 3);
564 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
565 : 121 : yp = x.modMultiply(j, 7);
566 [ + + ]: 513 : for (yy = y; yy >= 7; yy -= 7);
567 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
568 : 121 : yp = x.modMultiply(j, 11);
569 [ + + ]: 346 : for (yy = y; yy >= 11; yy -= 11);
570 [ - + ][ + - ]: 121 : ASSERT_EQ(yp, yy);
571 [ + - ][ + - ]: 121 : }
[ + - ][ + - ]
572 : : }
573 : : }
574 : :
575 : 4 : TEST_F(TestUtilBlackInteger, modInverse)
576 : : {
577 [ + + ]: 12 : for (uint32_t i = 0; i <= 10; ++i)
578 : : {
579 : 11 : Integer x(i);
580 : 11 : Integer inv = x.modInverse(3);
581 [ + + ][ + + ]: 11 : if (i == 0 || i == 3 || i == 6 || i == 9)
[ + + ][ + + ]
582 : : {
583 [ - + ][ + - ]: 4 : ASSERT_EQ(inv, -1); /* no inverse */
584 : 4 : }
585 : : else
586 : : {
587 [ - + ][ + - ]: 14 : ASSERT_EQ(x.modMultiply(inv, 3), 1);
588 : : }
589 : 11 : inv = x.modInverse(7);
590 [ + + ][ + + ]: 11 : if (i == 0 || i == 7)
591 : : {
592 [ - + ][ + - ]: 2 : ASSERT_EQ(inv, -1); /* no inverse */
593 : 2 : }
594 : : else
595 : : {
596 [ - + ][ + - ]: 18 : ASSERT_EQ(x.modMultiply(inv, 7), 1);
597 : : }
598 : 11 : inv = x.modInverse(11);
599 [ + + ]: 11 : if (i == 0)
600 : : {
601 [ - + ][ + - ]: 1 : ASSERT_EQ(inv, -1); /* no inverse */
602 : : }
603 : : else
604 : : {
605 [ - + ][ + - ]: 20 : ASSERT_EQ(x.modMultiply(inv, 11), 1);
606 : : }
607 [ + - ][ + - ]: 11 : }
608 : : }
609 : :
610 : 4 : TEST_F(TestUtilBlackInteger, mkRandom_bound)
611 : : {
612 : : // Result must be in [0, 2^nbits) for various bit widths
613 : 1 : uint32_t sizes[] = {1, 2, 7, 8, 16, 32, 63, 64, 65, 100, 128, 256};
614 [ + + ]: 13 : for (uint32_t nbits : sizes)
615 : : {
616 : 12 : Integer bound = Integer(1).multiplyByPow2(nbits);
617 : 12 : std::unordered_set<Integer> values;
618 [ + + ]: 252 : for (size_t i = 0; i < 20; ++i)
619 : : {
620 : 240 : Integer v = Integer::mkRandom(nbits);
621 : 240 : values.insert(v);
622 [ - + ][ + - ]: 240 : ASSERT_TRUE(v >= 0);
623 [ - + ][ + - ]: 240 : ASSERT_TRUE(v < bound);
624 [ + - ]: 240 : }
625 [ - + ][ + - ]: 12 : ASSERT_GT(values.size(), 1);
626 [ + - ][ + - ]: 12 : }
627 : : }
628 : :
629 : 4 : TEST_F(TestUtilBlackInteger, mkRandom_deterministic)
630 : : {
631 : : // Same seed should produce the same sequence
632 : 1 : Random::getRandom().setSeed(42);
633 : 1 : Integer a1 = Integer::mkRandom(128);
634 : 1 : Integer a2 = Integer::mkRandom(128);
635 : :
636 : 1 : Random::getRandom().setSeed(42);
637 : 1 : Integer b1 = Integer::mkRandom(128);
638 : 1 : Integer b2 = Integer::mkRandom(128);
639 : :
640 [ - + ][ + - ]: 1 : ASSERT_EQ(a1, b1);
641 [ - + ][ + - ]: 1 : ASSERT_EQ(a2, b2);
642 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
643 : :
644 : 4 : TEST_F(TestUtilBlackInteger, mkRandom_not_always_zero)
645 : : {
646 : : // With 128 bits, getting all zeros 10 times in a row is unlikely.
647 : 1 : Random::getRandom().setSeed(0);
648 : 1 : bool nonZero = false;
649 [ + - ]: 1 : for (int i = 0; i < 10; ++i)
650 : : {
651 [ + - ]: 1 : if (!Integer::mkRandom(128).isZero())
652 : : {
653 : 1 : nonZero = true;
654 : 1 : break;
655 : : }
656 : : }
657 [ - + ][ + - ]: 1 : ASSERT_TRUE(nonZero);
658 : : }
659 : :
660 : : } // namespace test
661 : : } // namespace cvc5::internal
|
