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