Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/util/rational_white.cpp	Lines:	288	288	100.0 %
Date:	2021-08-15	Branches:	770	2528	30.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Tim King
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * White box testing of cvc5::Rational.
 */

#include <sstream>

#include "test.h"
#include "util/rational.h"

namespace cvc5 {
namespace test {

class TestUtilWhiteRational : public TestInternal
{
 protected:
  static const char* s_can_reduce;
};

const char* TestUtilWhiteRational::s_can_reduce =
    "4547897890548754897897897897890789078907890/54878902347890234";

TEST_F(TestUtilWhiteRational, constructors)
{
  Rational zero;  // Default constructor
  ASSERT_EQ(0L, zero.getNumerator().getLong());
  ASSERT_EQ(1L, zero.getDenominator().getLong());

  Rational reduced_cstring_base_10(s_can_reduce);
  Integer tmp0("2273948945274377448948948948945394539453945");
  Integer tmp1("27439451173945117");
  ASSERT_EQ(reduced_cstring_base_10.getNumerator(), tmp0);
  ASSERT_EQ(reduced_cstring_base_10.getDenominator(), tmp1);

  Rational reduced_cstring_base_16(s_can_reduce, 16);
  Integer tmp2("405008068100961292527303019616635131091442462891556", 10);
  Integer tmp3("24363950654420566157", 10);
  ASSERT_EQ(tmp2, reduced_cstring_base_16.getNumerator());
  ASSERT_EQ(tmp3, reduced_cstring_base_16.getDenominator());

  std::string stringCanReduce(s_can_reduce);
  Rational reduced_cppstring_base_10(stringCanReduce);
  ASSERT_EQ(reduced_cppstring_base_10.getNumerator(), tmp0);
  ASSERT_EQ(reduced_cppstring_base_10.getDenominator(), tmp1);
  Rational reduced_cppstring_base_16(stringCanReduce, 16);
  ASSERT_EQ(tmp2, reduced_cppstring_base_16.getNumerator());
  ASSERT_EQ(tmp3, reduced_cppstring_base_16.getDenominator());

  Rational cpy_cnstr(zero);
  ASSERT_EQ(0L, cpy_cnstr.getNumerator().getLong());
  ASSERT_EQ(1L, cpy_cnstr.getDenominator().getLong());
  // Check that zero is unaffected
  ASSERT_EQ(0L, zero.getNumerator().getLong());
  ASSERT_EQ(1L, zero.getDenominator().getLong());

  signed int nsi = -5478, dsi = 34783;
  unsigned int nui = 5478u, dui = 347589u;
  signed long int nsli = 1489054690l, dsli = -347576678l;
  unsigned long int nuli = 2434689476ul, duli = 323447523ul;

  Rational qsi(nsi, dsi);
  Rational qui(nui, dui);
  Rational qsli(nsli, dsli);
  Rational quli(nuli, duli);

  ASSERT_EQ(nsi, qsi.getNumerator().getLong());
  ASSERT_EQ(dsi, qsi.getDenominator().getLong());

  ASSERT_EQ(nui / 33, qui.getNumerator().getUnsignedLong());
  ASSERT_EQ(dui / 33, qui.getDenominator().getUnsignedLong());

  ASSERT_EQ(-nsli / 2, qsli.getNumerator().getLong());
  ASSERT_EQ(-dsli / 2, qsli.getDenominator().getLong());

  ASSERT_EQ(nuli, quli.getNumerator().getUnsignedLong());
  ASSERT_EQ(duli, quli.getDenominator().getUnsignedLong());

  Integer nz("942358903458908903485");
  Integer dz("547890579034790793457934807");
  Rational qz(nz, dz);
  ASSERT_EQ(nz, qz.getNumerator());
  ASSERT_EQ(dz, qz.getDenominator());

  // Not sure how to catch this...
  // ASSERT_THROW(Rational div_0(0,0),__gmp_exception );
}

TEST_F(TestUtilWhiteRational, destructor)
{
  Rational* q = new Rational(s_can_reduce);
  ASSERT_NO_THROW(delete q);
}

TEST_F(TestUtilWhiteRational, compare_against_zero)
{
  Rational q(0);
  ASSERT_NO_THROW(q == 0;);
  ASSERT_EQ(q, 0);
}

TEST_F(TestUtilWhiteRational, operator_assign)
{
  Rational x(0, 1);
  Rational y(78, 6);
  Rational z(45789, 1);

  ASSERT_EQ(x.getNumerator().getUnsignedLong(), 0ul);
  ASSERT_EQ(y.getNumerator().getUnsignedLong(), 13ul);
  ASSERT_EQ(z.getNumerator().getUnsignedLong(), 45789ul);

  x = y = z;

  ASSERT_EQ(x.getNumerator().getUnsignedLong(), 45789ul);
  ASSERT_EQ(y.getNumerator().getUnsignedLong(), 45789ul);
  ASSERT_EQ(z.getNumerator().getUnsignedLong(), 45789ul);

  Rational a(78, 91);

  y = a;

  ASSERT_EQ(a.getNumerator().getUnsignedLong(), 6ul);
  ASSERT_EQ(a.getDenominator().getUnsignedLong(), 7ul);
  ASSERT_EQ(y.getNumerator().getUnsignedLong(), 6ul);
  ASSERT_EQ(y.getDenominator().getUnsignedLong(), 7ul);
  ASSERT_EQ(x.getNumerator().getUnsignedLong(), 45789ul);
  ASSERT_EQ(z.getNumerator().getUnsignedLong(), 45789ul);
}

TEST_F(TestUtilWhiteRational, toString)
{
  std::stringstream ss;
  Rational large(s_can_reduce);
  ss << large;
  std::string res = ss.str();

  ASSERT_EQ(res, large.toString());
}

TEST_F(TestUtilWhiteRational, operator_equals)
{
  Rational a;
  Rational b(s_can_reduce);
  Rational c("2273948945274377448948948948945394539453945/27439451173945117");
  Rational d(0, -237489);

  ASSERT_TRUE(a == a);
  ASSERT_FALSE(a == b);
  ASSERT_FALSE(a == c);
  ASSERT_TRUE(a == d);

  ASSERT_FALSE(b == a);
  ASSERT_TRUE(b == b);
  ASSERT_TRUE(b == c);
  ASSERT_FALSE(b == d);

  ASSERT_FALSE(c == a);
  ASSERT_TRUE(c == b);
  ASSERT_TRUE(c == c);
  ASSERT_FALSE(c == d);

  ASSERT_TRUE(d == a);
  ASSERT_FALSE(d == b);
  ASSERT_FALSE(d == c);
  ASSERT_TRUE(d == d);
}

TEST_F(TestUtilWhiteRational, operator_not_equals)
{
  Rational a;
  Rational b(s_can_reduce);
  Rational c("2273948945274377448948948948945394539453945/27439451173945117");
  Rational d(0, -237489);

  ASSERT_FALSE(a != a);
  ASSERT_TRUE(a != b);
  ASSERT_TRUE(a != c);
  ASSERT_FALSE(a != d);

  ASSERT_TRUE(b != a);
  ASSERT_FALSE(b != b);
  ASSERT_FALSE(b != c);
  ASSERT_TRUE(b != d);

  ASSERT_TRUE(c != a);
  ASSERT_FALSE(c != b);
  ASSERT_FALSE(c != c);
  ASSERT_TRUE(c != d);

  ASSERT_FALSE(d != a);
  ASSERT_TRUE(d != b);
  ASSERT_TRUE(d != c);
  ASSERT_FALSE(d != d);
}

TEST_F(TestUtilWhiteRational, operator_subtract)
{
  Rational x(3, 2);
  Rational y(7, 8);
  Rational z(-3, 33);

  Rational act0 = x - x;
  Rational act1 = x - y;
  Rational act2 = x - z;
  Rational exp0(0, 1);
  Rational exp1(5, 8);
  Rational exp2(35, 22);

  Rational act3 = y - x;
  Rational act4 = y - y;
  Rational act5 = y - z;
  Rational exp3(-5, 8);
  Rational exp4(0, 1);
  Rational exp5(85, 88);

  Rational act6 = z - x;
  Rational act7 = z - y;
  Rational act8 = z - z;
  Rational exp6(-35, 22);
  Rational exp7(-85, 88);
  Rational exp8(0, 1);

  ASSERT_EQ(act0, exp0);
  ASSERT_EQ(act1, exp1);
  ASSERT_EQ(act2, exp2);
  ASSERT_EQ(act3, exp3);
  ASSERT_EQ(act4, exp4);
  ASSERT_EQ(act5, exp5);
  ASSERT_EQ(act6, exp6);
  ASSERT_EQ(act7, exp7);
  ASSERT_EQ(act8, exp8);
}

TEST_F(TestUtilWhiteRational, operator_add)
{
  Rational x(3, 2);
  Rational y(7, 8);
  Rational z(-3, 33);

  Rational act0 = x + x;
  Rational act1 = x + y;
  Rational act2 = x + z;
  Rational exp0(3, 1);
  Rational exp1(19, 8);
  Rational exp2(31, 22);

  Rational act3 = y + x;
  Rational act4 = y + y;
  Rational act5 = y + z;
  Rational exp3(19, 8);
  Rational exp4(7, 4);
  Rational exp5(69, 88);

  Rational act6 = z + x;
  Rational act7 = z + y;
  Rational act8 = z + z;
  Rational exp6(31, 22);
  Rational exp7(69, 88);
  Rational exp8(-2, 11);

  ASSERT_EQ(act0, exp0);
  ASSERT_EQ(act1, exp1);
  ASSERT_EQ(act2, exp2);
  ASSERT_EQ(act3, exp3);
  ASSERT_EQ(act4, exp4);
  ASSERT_EQ(act5, exp5);
  ASSERT_EQ(act6, exp6);
  ASSERT_EQ(act7, exp7);
  ASSERT_EQ(act8, exp8);
}

TEST_F(TestUtilWhiteRational, operator_mult)
{
  Rational x(3, 2);
  Rational y(7, 8);
  Rational z(-3, 33);

  Rational act0 = x * x;
  Rational act1 = x * y;
  Rational act2 = x * z;
  Rational exp0(9, 4);
  Rational exp1(21, 16);
  Rational exp2(-3, 22);

  Rational act3 = y * x;
  Rational act4 = y * y;
  Rational act5 = y * z;
  Rational exp3(21, 16);
  Rational exp4(49, 64);
  Rational exp5(-7, 88);

  Rational act6 = z * x;
  Rational act7 = z * y;
  Rational act8 = z * z;
  Rational exp6(-3, 22);
  Rational exp7(-7, 88);
  Rational exp8(1, 121);

  ASSERT_EQ(act0, exp0);
  ASSERT_EQ(act1, exp1);
  ASSERT_EQ(act2, exp2);
  ASSERT_EQ(act3, exp3);
  ASSERT_EQ(act4, exp4);
  ASSERT_EQ(act5, exp5);
  ASSERT_EQ(act6, exp6);
  ASSERT_EQ(act7, exp7);
  ASSERT_EQ(act8, exp8);
}

TEST_F(TestUtilWhiteRational, operator_div)
{
  Rational x(3, 2);
  Rational y(7, 8);
  Rational z(-3, 33);

  Rational act0 = x / x;
  Rational act1 = x / y;
  Rational act2 = x / z;
  Rational exp0(1, 1);
  Rational exp1(12, 7);
  Rational exp2(-33, 2);

  Rational act3 = y / x;
  Rational act4 = y / y;
  Rational act5 = y / z;
  Rational exp3(7, 12);
  Rational exp4(1, 1);
  Rational exp5(-77, 8);

  Rational act6 = z / x;
  Rational act7 = z / y;
  Rational act8 = z / z;
  Rational exp6(-2, 33);
  Rational exp7(-8, 77);
  Rational exp8(1, 1);

  ASSERT_EQ(act0, exp0);
  ASSERT_EQ(act1, exp1);
  ASSERT_EQ(act2, exp2);
  ASSERT_EQ(act3, exp3);
  ASSERT_EQ(act4, exp4);
  ASSERT_EQ(act5, exp5);
  ASSERT_EQ(act6, exp6);
  ASSERT_EQ(act7, exp7);
  ASSERT_EQ(act8, exp8);
}

TEST_F(TestUtilWhiteRational, reduction_at_construction_time)
{
  Rational reduce0(s_can_reduce);
  Integer num0("2273948945274377448948948948945394539453945");
  Integer den0("27439451173945117");

  ASSERT_EQ(reduce0.getNumerator(), num0);
  ASSERT_EQ(reduce0.getDenominator(), den0);

  Rational reduce1(0, 454789);
  Integer num1(0);
  Integer den1(1);

  ASSERT_EQ(reduce1.getNumerator(), num1);
  ASSERT_EQ(reduce1.getDenominator(), den1);

  Rational reduce2(0, -454789);
  Integer num2(0);
  Integer den2(1);

  ASSERT_EQ(reduce2.getNumerator(), num2);
  ASSERT_EQ(reduce2.getDenominator(), den2);

  Rational reduce3(822898902L, 273L);
  Integer num3(39185662L);
  Integer den3(13);

  ASSERT_EQ(reduce2.getNumerator(), num2);
  ASSERT_EQ(reduce2.getDenominator(), den2);

  Rational reduce4(822898902L, -273L);
  Integer num4(-39185662L);
  Integer den4(13);

  ASSERT_EQ(reduce4.getNumerator(), num4);
  ASSERT_EQ(reduce4.getDenominator(), den4);

  Rational reduce5(-822898902L, 273L);
  Integer num5(-39185662L);
  Integer den5(13);

  ASSERT_EQ(reduce5.getNumerator(), num5);
  ASSERT_EQ(reduce5.getDenominator(), den5);

  Rational reduce6(-822898902L, -273L);
  Integer num6(39185662L);
  Integer den6(13);

  ASSERT_EQ(reduce6.getNumerator(), num6);
  ASSERT_EQ(reduce6.getDenominator(), den6);
}

/** Make sure we can handle: http://www.ginac.de/CLN/cln_3.html#SEC15 */
TEST_F(TestUtilWhiteRational, constructrion)
{
  const int32_t i = (1 << 29) + 1;
  const uint32_t u = (1 << 29) + 1;
  ASSERT_EQ(Rational(i), Rational(i));
  ASSERT_EQ(Rational(u), Rational(u));
}
}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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