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