Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Tim King
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * White box testing of cvc5::Rational.
14 : : */
15 : :
16 : : #include <sstream>
17 : :
18 : : #include "test.h"
19 : : #include "util/rational.h"
20 : :
21 : : namespace cvc5::internal {
22 : : namespace test {
23 : :
24 : : class TestUtilWhiteRational : public TestInternal
25 : : {
26 : : protected:
27 : : static const char* s_can_reduce;
28 : : };
29 : :
30 : : const char* TestUtilWhiteRational::s_can_reduce =
31 : : "4547897890548754897897897897890789078907890/54878902347890234";
32 : :
33 : 2 : TEST_F(TestUtilWhiteRational, constructors)
34 : : {
35 : 1 : Rational zero; // Default constructor
36 [ - + ]: 1 : ASSERT_EQ(0L, zero.getNumerator().getLong());
37 [ - + ]: 1 : ASSERT_EQ(1L, zero.getDenominator().getLong());
38 : :
39 : 1 : Rational reduced_cstring_base_10(s_can_reduce);
40 : 1 : Integer tmp0("2273948945274377448948948948945394539453945");
41 : 1 : Integer tmp1("27439451173945117");
42 [ - + ]: 2 : ASSERT_EQ(reduced_cstring_base_10.getNumerator(), tmp0);
43 [ - + ]: 2 : ASSERT_EQ(reduced_cstring_base_10.getDenominator(), tmp1);
44 : :
45 : 1 : Rational reduced_cstring_base_16(s_can_reduce, 16);
46 : 1 : Integer tmp2("405008068100961292527303019616635131091442462891556", 10);
47 : 1 : Integer tmp3("24363950654420566157", 10);
48 [ - + ]: 2 : ASSERT_EQ(tmp2, reduced_cstring_base_16.getNumerator());
49 [ - + ]: 2 : ASSERT_EQ(tmp3, reduced_cstring_base_16.getDenominator());
50 : :
51 : 1 : std::string stringCanReduce(s_can_reduce);
52 : 1 : Rational reduced_cppstring_base_10(stringCanReduce);
53 [ - + ]: 2 : ASSERT_EQ(reduced_cppstring_base_10.getNumerator(), tmp0);
54 [ - + ]: 2 : ASSERT_EQ(reduced_cppstring_base_10.getDenominator(), tmp1);
55 : 1 : Rational reduced_cppstring_base_16(stringCanReduce, 16);
56 [ - + ]: 2 : ASSERT_EQ(tmp2, reduced_cppstring_base_16.getNumerator());
57 [ - + ]: 2 : ASSERT_EQ(tmp3, reduced_cppstring_base_16.getDenominator());
58 : :
59 : 1 : Rational cpy_cnstr(zero);
60 [ - + ]: 1 : ASSERT_EQ(0L, cpy_cnstr.getNumerator().getLong());
61 [ - + ]: 1 : ASSERT_EQ(1L, cpy_cnstr.getDenominator().getLong());
62 : : // Check that zero is unaffected
63 [ - + ]: 1 : ASSERT_EQ(0L, zero.getNumerator().getLong());
64 [ - + ]: 1 : ASSERT_EQ(1L, zero.getDenominator().getLong());
65 : :
66 : 1 : signed int nsi = -5478, dsi = 34783;
67 : 1 : unsigned int nui = 5478u, dui = 347589u;
68 : 1 : signed long int nsli = 1489054690l, dsli = -347576678l;
69 : 1 : unsigned long int nuli = 2434689476ul, duli = 323447523ul;
70 : :
71 : 1 : Rational qsi(nsi, dsi);
72 : 1 : Rational qui(nui, dui);
73 : 1 : Rational qsli(nsli, dsli);
74 : 1 : Rational quli(nuli, duli);
75 : :
76 [ - + ]: 1 : ASSERT_EQ(nsi, qsi.getNumerator().getLong());
77 [ - + ]: 1 : ASSERT_EQ(dsi, qsi.getDenominator().getLong());
78 : :
79 [ - + ]: 1 : ASSERT_EQ(nui / 33, qui.getNumerator().getUnsignedLong());
80 [ - + ]: 1 : ASSERT_EQ(dui / 33, qui.getDenominator().getUnsignedLong());
81 : :
82 [ - + ]: 1 : ASSERT_EQ(-nsli / 2, qsli.getNumerator().getLong());
83 [ - + ]: 1 : ASSERT_EQ(-dsli / 2, qsli.getDenominator().getLong());
84 : :
85 [ - + ]: 1 : ASSERT_EQ(nuli, quli.getNumerator().getUnsignedLong());
86 [ - + ]: 1 : ASSERT_EQ(duli, quli.getDenominator().getUnsignedLong());
87 : :
88 : 1 : Integer nz("942358903458908903485");
89 : 1 : Integer dz("547890579034790793457934807");
90 : 1 : Rational qz(nz, dz);
91 [ - + ]: 2 : ASSERT_EQ(nz, qz.getNumerator());
92 [ - + ]: 2 : ASSERT_EQ(dz, qz.getDenominator());
93 : :
94 : : // Not sure how to catch this...
95 : : // ASSERT_THROW(Rational div_0(0,0),__gmp_exception );
96 : : }
97 : :
98 : 2 : TEST_F(TestUtilWhiteRational, destructor)
99 : : {
100 : 1 : Rational* q = new Rational(s_can_reduce);
101 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(delete q);
[ + - ]
102 : : }
103 : :
104 : 2 : TEST_F(TestUtilWhiteRational, compare_against_zero)
105 : : {
106 : 1 : Rational q(0);
107 [ + - ][ + - ]: 1 : ASSERT_NO_THROW(q == 0;);
108 [ - + ]: 1 : ASSERT_EQ(q, 0);
109 : : }
110 : :
111 : 2 : TEST_F(TestUtilWhiteRational, operator_assign)
112 : : {
113 : 1 : Rational x(0, 1);
114 : 1 : Rational y(78, 6);
115 : 1 : Rational z(45789, 1);
116 : :
117 [ - + ]: 1 : ASSERT_EQ(x.getNumerator().getUnsignedLong(), 0ul);
118 [ - + ]: 1 : ASSERT_EQ(y.getNumerator().getUnsignedLong(), 13ul);
119 [ - + ]: 1 : ASSERT_EQ(z.getNumerator().getUnsignedLong(), 45789ul);
120 : :
121 : 1 : x = y = z;
122 : :
123 [ - + ]: 1 : ASSERT_EQ(x.getNumerator().getUnsignedLong(), 45789ul);
124 [ - + ]: 1 : ASSERT_EQ(y.getNumerator().getUnsignedLong(), 45789ul);
125 [ - + ]: 1 : ASSERT_EQ(z.getNumerator().getUnsignedLong(), 45789ul);
126 : :
127 : 1 : Rational a(78, 91);
128 : :
129 : 1 : y = a;
130 : :
131 [ - + ]: 1 : ASSERT_EQ(a.getNumerator().getUnsignedLong(), 6ul);
132 [ - + ]: 1 : ASSERT_EQ(a.getDenominator().getUnsignedLong(), 7ul);
133 [ - + ]: 1 : ASSERT_EQ(y.getNumerator().getUnsignedLong(), 6ul);
134 [ - + ]: 1 : ASSERT_EQ(y.getDenominator().getUnsignedLong(), 7ul);
135 [ - + ]: 1 : ASSERT_EQ(x.getNumerator().getUnsignedLong(), 45789ul);
136 [ - + ]: 1 : ASSERT_EQ(z.getNumerator().getUnsignedLong(), 45789ul);
137 : : }
138 : :
139 : 2 : TEST_F(TestUtilWhiteRational, toString)
140 : : {
141 : 1 : std::stringstream ss;
142 : 1 : Rational large(s_can_reduce);
143 : 1 : ss << large;
144 : 1 : std::string res = ss.str();
145 : :
146 [ - + ]: 2 : ASSERT_EQ(res, large.toString());
147 : : }
148 : :
149 : 2 : TEST_F(TestUtilWhiteRational, operator_equals)
150 : : {
151 : 1 : Rational a;
152 : 1 : Rational b(s_can_reduce);
153 : 1 : Rational c("2273948945274377448948948948945394539453945/27439451173945117");
154 : 1 : Rational d(0, -237489);
155 : :
156 [ - + ]: 1 : ASSERT_TRUE(a == a);
157 [ - + ]: 1 : ASSERT_FALSE(a == b);
158 [ - + ]: 1 : ASSERT_FALSE(a == c);
159 [ - + ]: 1 : ASSERT_TRUE(a == d);
160 : :
161 [ - + ]: 1 : ASSERT_FALSE(b == a);
162 [ - + ]: 1 : ASSERT_TRUE(b == b);
163 [ - + ]: 1 : ASSERT_TRUE(b == c);
164 [ - + ]: 1 : ASSERT_FALSE(b == d);
165 : :
166 [ - + ]: 1 : ASSERT_FALSE(c == a);
167 [ - + ]: 1 : ASSERT_TRUE(c == b);
168 [ - + ]: 1 : ASSERT_TRUE(c == c);
169 [ - + ]: 1 : ASSERT_FALSE(c == d);
170 : :
171 [ - + ]: 1 : ASSERT_TRUE(d == a);
172 [ - + ]: 1 : ASSERT_FALSE(d == b);
173 [ - + ]: 1 : ASSERT_FALSE(d == c);
174 [ - + ]: 1 : ASSERT_TRUE(d == d);
175 : : }
176 : :
177 : 2 : TEST_F(TestUtilWhiteRational, operator_not_equals)
178 : : {
179 : 1 : Rational a;
180 : 1 : Rational b(s_can_reduce);
181 : 1 : Rational c("2273948945274377448948948948945394539453945/27439451173945117");
182 : 1 : Rational d(0, -237489);
183 : :
184 [ - + ]: 1 : ASSERT_FALSE(a != a);
185 [ - + ]: 1 : ASSERT_TRUE(a != b);
186 [ - + ]: 1 : ASSERT_TRUE(a != c);
187 [ - + ]: 1 : ASSERT_FALSE(a != d);
188 : :
189 [ - + ]: 1 : ASSERT_TRUE(b != a);
190 [ - + ]: 1 : ASSERT_FALSE(b != b);
191 [ - + ]: 1 : ASSERT_FALSE(b != c);
192 [ - + ]: 1 : ASSERT_TRUE(b != d);
193 : :
194 [ - + ]: 1 : ASSERT_TRUE(c != a);
195 [ - + ]: 1 : ASSERT_FALSE(c != b);
196 [ - + ]: 1 : ASSERT_FALSE(c != c);
197 [ - + ]: 1 : ASSERT_TRUE(c != d);
198 : :
199 [ - + ]: 1 : ASSERT_FALSE(d != a);
200 [ - + ]: 1 : ASSERT_TRUE(d != b);
201 [ - + ]: 1 : ASSERT_TRUE(d != c);
202 [ - + ]: 1 : ASSERT_FALSE(d != d);
203 : : }
204 : :
205 : 2 : TEST_F(TestUtilWhiteRational, operator_subtract)
206 : : {
207 : 1 : Rational x(3, 2);
208 : 1 : Rational y(7, 8);
209 : 1 : Rational z(-3, 33);
210 : :
211 : 1 : Rational act0 = x - x;
212 : 1 : Rational act1 = x - y;
213 : 1 : Rational act2 = x - z;
214 : 1 : Rational exp0(0, 1);
215 : 1 : Rational exp1(5, 8);
216 : 1 : Rational exp2(35, 22);
217 : :
218 : 1 : Rational act3 = y - x;
219 : 1 : Rational act4 = y - y;
220 : 1 : Rational act5 = y - z;
221 : 1 : Rational exp3(-5, 8);
222 : 1 : Rational exp4(0, 1);
223 : 1 : Rational exp5(85, 88);
224 : :
225 : 1 : Rational act6 = z - x;
226 : 1 : Rational act7 = z - y;
227 : 1 : Rational act8 = z - z;
228 : 1 : Rational exp6(-35, 22);
229 : 1 : Rational exp7(-85, 88);
230 : 1 : Rational exp8(0, 1);
231 : :
232 [ - + ]: 1 : ASSERT_EQ(act0, exp0);
233 [ - + ]: 1 : ASSERT_EQ(act1, exp1);
234 [ - + ]: 1 : ASSERT_EQ(act2, exp2);
235 [ - + ]: 1 : ASSERT_EQ(act3, exp3);
236 [ - + ]: 1 : ASSERT_EQ(act4, exp4);
237 [ - + ]: 1 : ASSERT_EQ(act5, exp5);
238 [ - + ]: 1 : ASSERT_EQ(act6, exp6);
239 [ - + ]: 1 : ASSERT_EQ(act7, exp7);
240 [ - + ]: 1 : ASSERT_EQ(act8, exp8);
241 : : }
242 : :
243 : 2 : TEST_F(TestUtilWhiteRational, operator_add)
244 : : {
245 : 1 : Rational x(3, 2);
246 : 1 : Rational y(7, 8);
247 : 1 : Rational z(-3, 33);
248 : :
249 : 1 : Rational act0 = x + x;
250 : 1 : Rational act1 = x + y;
251 : 1 : Rational act2 = x + z;
252 : 1 : Rational exp0(3, 1);
253 : 1 : Rational exp1(19, 8);
254 : 1 : Rational exp2(31, 22);
255 : :
256 : 1 : Rational act3 = y + x;
257 : 1 : Rational act4 = y + y;
258 : 1 : Rational act5 = y + z;
259 : 1 : Rational exp3(19, 8);
260 : 1 : Rational exp4(7, 4);
261 : 1 : Rational exp5(69, 88);
262 : :
263 : 1 : Rational act6 = z + x;
264 : 1 : Rational act7 = z + y;
265 : 1 : Rational act8 = z + z;
266 : 1 : Rational exp6(31, 22);
267 : 1 : Rational exp7(69, 88);
268 : 1 : Rational exp8(-2, 11);
269 : :
270 [ - + ]: 1 : ASSERT_EQ(act0, exp0);
271 [ - + ]: 1 : ASSERT_EQ(act1, exp1);
272 [ - + ]: 1 : ASSERT_EQ(act2, exp2);
273 [ - + ]: 1 : ASSERT_EQ(act3, exp3);
274 [ - + ]: 1 : ASSERT_EQ(act4, exp4);
275 [ - + ]: 1 : ASSERT_EQ(act5, exp5);
276 [ - + ]: 1 : ASSERT_EQ(act6, exp6);
277 [ - + ]: 1 : ASSERT_EQ(act7, exp7);
278 [ - + ]: 1 : ASSERT_EQ(act8, exp8);
279 : : }
280 : :
281 : 2 : TEST_F(TestUtilWhiteRational, operator_mult)
282 : : {
283 : 1 : Rational x(3, 2);
284 : 1 : Rational y(7, 8);
285 : 1 : Rational z(-3, 33);
286 : :
287 : 1 : Rational act0 = x * x;
288 : 1 : Rational act1 = x * y;
289 : 1 : Rational act2 = x * z;
290 : 1 : Rational exp0(9, 4);
291 : 1 : Rational exp1(21, 16);
292 : 1 : Rational exp2(-3, 22);
293 : :
294 : 1 : Rational act3 = y * x;
295 : 1 : Rational act4 = y * y;
296 : 1 : Rational act5 = y * z;
297 : 1 : Rational exp3(21, 16);
298 : 1 : Rational exp4(49, 64);
299 : 1 : Rational exp5(-7, 88);
300 : :
301 : 1 : Rational act6 = z * x;
302 : 1 : Rational act7 = z * y;
303 : 1 : Rational act8 = z * z;
304 : 1 : Rational exp6(-3, 22);
305 : 1 : Rational exp7(-7, 88);
306 : 1 : Rational exp8(1, 121);
307 : :
308 [ - + ]: 1 : ASSERT_EQ(act0, exp0);
309 [ - + ]: 1 : ASSERT_EQ(act1, exp1);
310 [ - + ]: 1 : ASSERT_EQ(act2, exp2);
311 [ - + ]: 1 : ASSERT_EQ(act3, exp3);
312 [ - + ]: 1 : ASSERT_EQ(act4, exp4);
313 [ - + ]: 1 : ASSERT_EQ(act5, exp5);
314 [ - + ]: 1 : ASSERT_EQ(act6, exp6);
315 [ - + ]: 1 : ASSERT_EQ(act7, exp7);
316 [ - + ]: 1 : ASSERT_EQ(act8, exp8);
317 : : }
318 : :
319 : 2 : TEST_F(TestUtilWhiteRational, operator_div)
320 : : {
321 : 1 : Rational x(3, 2);
322 : 1 : Rational y(7, 8);
323 : 1 : Rational z(-3, 33);
324 : :
325 : 1 : Rational act0 = x / x;
326 : 1 : Rational act1 = x / y;
327 : 1 : Rational act2 = x / z;
328 : 1 : Rational exp0(1, 1);
329 : 1 : Rational exp1(12, 7);
330 : 1 : Rational exp2(-33, 2);
331 : :
332 : 1 : Rational act3 = y / x;
333 : 1 : Rational act4 = y / y;
334 : 1 : Rational act5 = y / z;
335 : 1 : Rational exp3(7, 12);
336 : 1 : Rational exp4(1, 1);
337 : 1 : Rational exp5(-77, 8);
338 : :
339 : 1 : Rational act6 = z / x;
340 : 1 : Rational act7 = z / y;
341 : 1 : Rational act8 = z / z;
342 : 1 : Rational exp6(-2, 33);
343 : 1 : Rational exp7(-8, 77);
344 : 1 : Rational exp8(1, 1);
345 : :
346 [ - + ]: 1 : ASSERT_EQ(act0, exp0);
347 [ - + ]: 1 : ASSERT_EQ(act1, exp1);
348 [ - + ]: 1 : ASSERT_EQ(act2, exp2);
349 [ - + ]: 1 : ASSERT_EQ(act3, exp3);
350 [ - + ]: 1 : ASSERT_EQ(act4, exp4);
351 [ - + ]: 1 : ASSERT_EQ(act5, exp5);
352 [ - + ]: 1 : ASSERT_EQ(act6, exp6);
353 [ - + ]: 1 : ASSERT_EQ(act7, exp7);
354 [ - + ]: 1 : ASSERT_EQ(act8, exp8);
355 : : }
356 : :
357 : 2 : TEST_F(TestUtilWhiteRational, reduction_at_construction_time)
358 : : {
359 : 1 : Rational reduce0(s_can_reduce);
360 : 1 : Integer num0("2273948945274377448948948948945394539453945");
361 : 1 : Integer den0("27439451173945117");
362 : :
363 [ - + ]: 2 : ASSERT_EQ(reduce0.getNumerator(), num0);
364 [ - + ]: 2 : ASSERT_EQ(reduce0.getDenominator(), den0);
365 : :
366 : 1 : Rational reduce1(0, 454789);
367 : 1 : Integer num1(0);
368 : 1 : Integer den1(1);
369 : :
370 [ - + ]: 2 : ASSERT_EQ(reduce1.getNumerator(), num1);
371 [ - + ]: 2 : ASSERT_EQ(reduce1.getDenominator(), den1);
372 : :
373 : 1 : Rational reduce2(0, -454789);
374 : 1 : Integer num2(0);
375 : 1 : Integer den2(1);
376 : :
377 [ - + ]: 2 : ASSERT_EQ(reduce2.getNumerator(), num2);
378 [ - + ]: 2 : ASSERT_EQ(reduce2.getDenominator(), den2);
379 : :
380 : 1 : Rational reduce3(822898902L, 273L);
381 : 1 : Integer num3(39185662L);
382 : 1 : Integer den3(13);
383 : :
384 [ - + ]: 2 : ASSERT_EQ(reduce2.getNumerator(), num2);
385 [ - + ]: 2 : ASSERT_EQ(reduce2.getDenominator(), den2);
386 : :
387 : 1 : Rational reduce4(822898902L, -273L);
388 : 1 : Integer num4(-39185662L);
389 : 1 : Integer den4(13);
390 : :
391 [ - + ]: 2 : ASSERT_EQ(reduce4.getNumerator(), num4);
392 [ - + ]: 2 : ASSERT_EQ(reduce4.getDenominator(), den4);
393 : :
394 : 1 : Rational reduce5(-822898902L, 273L);
395 : 1 : Integer num5(-39185662L);
396 : 1 : Integer den5(13);
397 : :
398 [ - + ]: 2 : ASSERT_EQ(reduce5.getNumerator(), num5);
399 [ - + ]: 2 : ASSERT_EQ(reduce5.getDenominator(), den5);
400 : :
401 : 1 : Rational reduce6(-822898902L, -273L);
402 : 1 : Integer num6(39185662L);
403 : 1 : Integer den6(13);
404 : :
405 [ - + ]: 2 : ASSERT_EQ(reduce6.getNumerator(), num6);
406 [ - + ]: 2 : ASSERT_EQ(reduce6.getDenominator(), den6);
407 : : }
408 : :
409 : : /** Make sure we can handle: http://www.ginac.de/CLN/cln_3.html#SEC15 */
410 : 2 : TEST_F(TestUtilWhiteRational, constructrion)
411 : : {
412 : 1 : const int32_t i = (1 << 29) + 1;
413 : 1 : const uint32_t u = (1 << 29) + 1;
414 [ - + ]: 2 : ASSERT_EQ(Rational(i), Rational(i));
415 [ - + ]: 2 : ASSERT_EQ(Rational(u), Rational(u));
416 : : }
417 : : } // namespace test
418 : : } // namespace cvc5::internal
|
