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