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