1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 tst_rational.cpp
7
8 Abstract:
9
10 Test rationals
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2006-09-26.
15
16 Revision History:
17
18 --*/
19 #include<iostream>
20 #include "util/vector.h"
21 #include "util/rational.h"
22 #include "util/trace.h"
23 #include "util/ext_gcd.h"
24 #include "util/timeit.h"
25
tst1()26 static void tst1() {
27 rational r1(1);
28 rational r2(1,2);
29 rational r3(2,4);
30 ENSURE(r2 == r3);
31 ENSURE(r1 != r2);
32 ENSURE(r2 + r3 == r1);
33 ENSURE(r1.is_pos());
34 ENSURE((r2 - r1).is_neg());
35 ENSURE((r2 - r3).is_zero());
36 ENSURE(floor(r2).is_zero());
37 ENSURE(ceil(r2).is_one());
38 // std::cout << "-r2: " << (-r2) << ", floor(-r2):" << floor(-r2) << "\n";
39 ENSURE(floor(-r2).is_minus_one());
40 ENSURE(ceil(-r2).is_zero());
41 ENSURE(floor(r1) == r1);
42 ENSURE(ceil(r1) == r1);
43 rational r4(3,5);
44 ENSURE(r3 * r4 == rational(3, 10));
45 ENSURE(r3 / r4 == rational(5, 6));
46 rational r5(2,3);
47 ENSURE(r4 * r5 == rational(2, 5));
48 --r2;
49 ENSURE(r2 == -r3);
50 r2.neg();
51 ENSURE(r2 == r3);
52 --r2;
53 r2 = abs(r2);
54 ENSURE(r2 == r3);
55 --r2;
56 ++r2;
57 ENSURE(r2 == r3);
58 ENSURE(r2 == abs(r2));
59 ENSURE(r4 * rational(1) == r4);
60 ENSURE((r4 * rational(0)).is_zero());
61 ENSURE(r4 * rational(-1) == -r4);
62 ENSURE(rational(1) * r4 == r4);
63 ENSURE((rational(0) * r4).is_zero());
64 ENSURE(rational(-1) * r4 == -r4);
65 ENSURE(r4 + rational(0) == r4);
66 ENSURE(ceil(r4).is_one());
67 // std::cout << "r3: " << r3 << ", r4: " << r4 << ", -r4: " << -r4 << ", r3 / (-r4): " << (r3 / (-r4)) << "\n";
68 ENSURE(r3 / (-r4) == rational(5,-6));
69 ENSURE(div(rational(7), rational(2)) == rational(3));
70 ENSURE(rational(7) % rational(4) == rational(3));
71 ENSURE(div(rational(7), rational(-2)) == rational(-3));
72 ENSURE(rational(3) + rational(5) == rational(8));
73 ENSURE(rational("13/10") + rational("7/10") == rational(2));
74 ENSURE(rational("100/20") == rational(5));
75 ENSURE(gcd(rational(12), rational(8)) == rational(4));
76 ENSURE(ceil(rational(-3,2)) == rational(-1));
77 ENSURE(floor(rational(-3,2)) == rational(-2));
78 ENSURE(ceil(rational(3,2)) == rational(2));
79 ENSURE(floor(rational(3,2)) == rational(1));
80 ENSURE(rational(3).is_pos());
81 ENSURE(rational(0).is_nonneg());
82 ENSURE(rational(3).is_pos());
83 ENSURE(rational(3).is_nonneg());
84 ENSURE(rational(0).is_nonneg());
85 ENSURE(!rational(3).is_zero());
86 ENSURE(!rational(-3).is_zero());
87 ENSURE(rational(0).is_zero());
88 ENSURE(rational(1).is_one());
89 ENSURE(!rational(2).is_one());
90 ENSURE(rational(3,4) >= rational(2,8));
91 ENSURE(rational(3,4) <= rational(7,8));
92 ENSURE(rational(3,4) <= rational(3,4));
93 ENSURE(rational(3,4) >= rational(3,4));
94 ENSURE(rational(3,4) > rational(2,8));
95 ENSURE(rational(3,4) < rational(7,8));
96 TRACE("rational", tout << rational(3,4) << "\n";);
97 TRACE("rational", tout << rational(7,9) << "\n";);
98 TRACE("rational", tout << rational(-3,7) << "\n";);
99 TRACE("rational", tout << rational(5,8) << "\n";);
100 TRACE("rational", tout << rational(4,2) << "\n";);
101 ENSURE(rational(3) + rational(2) == rational(5));
102 ENSURE(rational(3) - rational(2) == rational(1));
103 ENSURE(rational(3) * rational(2) == rational(6));
104 ENSURE(rational(6) / rational(2) == rational(3));
105 ENSURE(rational(6) % rational(4) == rational(2));
106 ENSURE(power(rational(2),0) == rational(1));
107 ENSURE(power(rational(2),1) == rational(2));
108 ENSURE(power(rational(2),3) == rational(8));
109 }
110
tst2()111 static void tst2() {
112 rational r1("10000000000000000000000000000000000");
113 rational r2("10000000000000000000000000000000000/3");
114 rational r3("20000000000000000000000000000000000/6");
115 TRACE("rational", tout << r1 << std::endl;);
116 TRACE("rational", tout << r2 << std::endl;);
117 TRACE("rational", tout << r3 << std::endl;);
118
119 ENSURE(r2 == r3);
120 ENSURE(r1 != r2);
121 ENSURE(rational(2)*r2 + r3 == r1);
122 ENSURE(r1.is_pos());
123 ENSURE((r2 - r1).is_neg());
124 ENSURE((r2 - r3).is_zero());
125 // std::cout << "===> " << floor(r2) << "\n";
126 {
127 rational r0("1/3000000000000000000000000");
128 ENSURE(ceil(r0).is_one());
129 ENSURE(floor(-r0).is_minus_one());
130 ENSURE(ceil(-r0).is_zero());
131 }
132 ENSURE(floor(r1) == r1);
133 ENSURE(ceil(r1) == r1);
134 rational r4("300000000/5");
135 ENSURE(rational(1,2) * r4 == rational("300000000/10"));
136 ENSURE(rational(1,2) / r4 == rational("5/600000000"));
137 rational r5(2,3);
138 ENSURE(r4 * r5 == rational("200000000/5"));
139 rational r6("10000000000000000000000000000000003/3");
140 --r6;
141 ENSURE(r6 == r2);
142 r6.neg();
143 ENSURE(r6 != r2);
144 ENSURE(abs(r6) == r2);
145 --r2;
146 ++r2;
147 r2.neg();
148 ENSURE(r2 == r6);
149 ENSURE(r6 * rational(1) == r6);
150 ENSURE((r6 * rational(0)).is_zero());
151 ENSURE(r6 * rational(-1) == -r6);
152 ENSURE(rational(1) * r6 == r6);
153 ENSURE((rational(0) * r6).is_zero());
154 ENSURE(rational(-1) * r6 == -r6);
155 ENSURE(r6 + rational(0) == r6);
156
157 ENSURE(rational("300000000000000").is_pos());
158 ENSURE(rational("0000000000000000000").is_nonneg());
159 ENSURE(rational("0000000000000000000").is_nonpos());
160 ENSURE(rational("3000000000000000000/2").is_pos());
161 ENSURE(rational("3000000000000000000/2").is_nonneg());
162 ENSURE((-rational("3000000000000000000/2")).is_neg());
163 ENSURE(!rational("3000000000000000000/2").is_neg());
164 ENSURE(!rational("3000000000000000000/2").is_zero());
165 ENSURE(!rational("3000000000000000000/2").is_one());
166 ENSURE(rational("99999999999/2") >= rational("23/2"));
167 ENSURE(rational("99999999999/2") > rational("23/2"));
168 ENSURE(rational("23/2") <= rational("99999999999/2"));
169 ENSURE(rational("23/2") < rational("99999999999/2"));
170 ENSURE(!(rational("99999999999/2") < rational("23/2")));
171
172
173 rational int64_max("9223372036854775807");
174 rational int64_min((-int64_max) - rational(1));
175 // is_int64
176 ENSURE(int64_max.is_int64());
177 ENSURE(int64_min.is_int64());
178 ENSURE(rational(0).is_int64());
179 ENSURE(rational(1).is_int64());
180 ENSURE(rational(-1).is_int64());
181 ENSURE(!(int64_max + rational(1)).is_int64());
182 ENSURE(!(int64_min - rational(1)).is_int64());
183
184 // is_uint64
185 ENSURE(int64_max.is_uint64());
186 ENSURE(!int64_min.is_uint64());
187 ENSURE(rational(0).is_uint64());
188 ENSURE(rational(1).is_uint64());
189 ENSURE(!rational(-1).is_uint64());
190 ENSURE((int64_max + rational(1)).is_uint64());
191 ENSURE(!(int64_min - rational(1)).is_uint64());
192
193 rational uint64_max(rational(1) + (rational(2) * int64_max));
194 ENSURE(uint64_max.is_uint64());
195
196 // get_int64, get_uint64
197 uint64_t u1 = uint64_max.get_uint64();
198 uint64_t u2 = UINT64_MAX;
199 VERIFY(u1 == u2);
200 std::cout << "int64_max: " << int64_max << ", INT64_MAX: " << INT64_MAX << ", int64_max.get_int64(): " << int64_max.get_int64() << ", int64_max.get_uint64(): " << int64_max.get_uint64() << "\n";
201 ENSURE(int64_max.get_int64() == INT64_MAX);
202 ENSURE(int64_min.get_int64() == INT64_MIN);
203
204 // extended Euclid:
205
206 }
207
tst3()208 void tst3() {
209 rational n1 = power(rational(2), 32);
210 TRACE("rational", tout << "n1: " << n1 << "\n";);
211 rational n2 = div(n1, rational(2));
212 rational n3 = div(rational(2), n2);
213 TRACE("rational",
214 tout << "n1: " << n1 << "\n";
215 tout << "n2: " << n2 << "\n";
216 tout << "n3: " << n3 << "\n";);
217 rational n4 = n1 - rational(3);
218 rational n5 = div(n4, rational(2));
219 TRACE("rational",
220 tout << "n4: " << n4 << "\n";
221 tout << "n5: " << n5 << "\n";);
222 ENSURE(n5 == rational("2147483646"));
223 }
224
tst4()225 void tst4() {
226 rational n1("4294967293");
227 TRACE("rational", tout << "n1: " << n1 << "\n";);
228 rational n2 = div(n1, rational(2));
229 }
230
tst5()231 void tst5() {
232 rational n1(1);
233 n1.neg();
234 rational n2("4294967295");
235 n1 /= n2;
236 TRACE("rational", tout << n1 << " " << n2 << " " << n1.is_big() << " " << n2.is_big() << "\n";);
237 n1 *= n2;
238 TRACE("rational", tout << "after: " << n1 << " " << n2 << "\n";);
239 ENSURE(n1.is_minus_one());
240 }
241
tst6()242 void tst6() {
243 rational t1(5);
244 rational t2(3);
245 rational a, b, g;
246
247 g = gcd(t1, t2, a, b);
248
249 t1 = rational(15);
250 t2 = rational(25);
251
252 g = gcd(t1, t2, a, b);
253 t1.neg();
254 g = gcd(t1, t2, a, b);
255 t2.neg();
256 g = gcd(t1, t2, a, b);
257 t1.neg();
258 g = gcd(t1, t2, a, b);
259
260 std::swap(t1, t2);
261
262 g = gcd(t1, t2, a, b);
263 t1.neg();
264 g = gcd(t1, t2, a, b);
265 t2.neg();
266 g = gcd(t1, t2, a, b);
267 t1.neg();
268 g = gcd(t1, t2, a, b);
269
270 }
271
272 class rational_tester {
273 public:
tst1()274 static void tst1() {
275 rational n1(-1);
276 rational n2(8);
277 ENSURE((n1 % n2).is_minus_one());
278 ENSURE(mod(n1, n2) == rational(7));
279 }
280
tst_hash(int val)281 static void tst_hash(int val) {
282 rational n1(val);
283 rational n2("10203939394995449949494394932929");
284 rational n3(val);
285 n2 = n3;
286 ENSURE(n1.hash() == n2.hash());
287 }
288
tst2()289 static void tst2() {
290 tst_hash(0);
291 for (int i = 0; i <= 10000; i++) {
292 int r = rand() % INT_MAX;
293 if (rand()%2 == 1) r = -r;
294 tst_hash(r);
295 }
296 }
297 };
298
tst7()299 static void tst7() {
300 rational p;
301 p = power(rational(2), 32);
302 for (unsigned i = 1; i < 1000; i++) {
303 rational n(i);
304 rational x;
305 rational y;
306 rational gcd;
307 extended_gcd(n, p, gcd, x, y);
308 TRACE("gcd", tout << n << " " << p << ": " << gcd << " " << x << " " << y << "\n";);
309 ENSURE(!mod(n, rational(2)).is_one() || mod(n * x, p).is_one());
310 }
311 }
312
tst8()313 static void tst8() {
314 rational r;
315 ENSURE(!rational(-4).is_int_perfect_square(r) && r.is_zero());
316 ENSURE(!rational(-3).is_int_perfect_square(r) && r.is_zero());
317 ENSURE(!rational(-2).is_int_perfect_square(r) && r.is_zero());
318 ENSURE(!rational(-1).is_int_perfect_square(r) && r.is_zero());
319 ENSURE(rational(0).is_int_perfect_square(r) && r.is_zero());
320 ENSURE(rational(1).is_int_perfect_square(r) && r.is_one());
321 ENSURE(!rational(2).is_int_perfect_square(r) && r == rational(2));
322 ENSURE(!rational(3).is_int_perfect_square(r) && r == rational(2));
323 ENSURE(rational(4).is_int_perfect_square(r) && r == rational(2));
324 ENSURE(!rational(5).is_int_perfect_square(r) && r == rational(3));
325 ENSURE(!rational(6).is_int_perfect_square(r) && r == rational(3));
326 ENSURE(!rational(7).is_int_perfect_square(r) && r == rational(3));
327 ENSURE(!rational(8).is_int_perfect_square(r) && r == rational(3));
328 ENSURE(rational(9).is_int_perfect_square(r) && r == rational(3));
329 ENSURE(!rational(10).is_int_perfect_square(r) && r == rational(4));
330 ENSURE(!rational(11).is_int_perfect_square(r) && r == rational(4));
331 ENSURE(!rational(12).is_int_perfect_square(r) && r == rational(4));
332 ENSURE(!rational(13).is_int_perfect_square(r) && r == rational(4));
333 ENSURE(!rational(14).is_int_perfect_square(r) && r == rational(4));
334 ENSURE(!rational(15).is_int_perfect_square(r) && r == rational(4));
335 ENSURE(rational(16).is_int_perfect_square(r) && r == rational(4));
336 ENSURE(!rational(17).is_int_perfect_square(r) && r == rational(5));
337 ENSURE(!rational(18).is_int_perfect_square(r) && r == rational(5));
338 ENSURE(!rational(19).is_int_perfect_square(r) && r == rational(5));
339 ENSURE(!rational(20).is_int_perfect_square(r) && r == rational(5));
340 ENSURE(!rational(21).is_int_perfect_square(r) && r == rational(5));
341 ENSURE(!rational(22).is_int_perfect_square(r) && r == rational(5));
342 ENSURE(!rational(23).is_int_perfect_square(r) && r == rational(5));
343 ENSURE(!rational(24).is_int_perfect_square(r) && r == rational(5));
344 ENSURE(rational(25).is_int_perfect_square(r) && r == rational(5));
345 ENSURE(!rational(26).is_int_perfect_square(r) && r == rational(6));
346 ENSURE(rational(36).is_int_perfect_square(r) && r == rational(6));
347
348 ENSURE(rational(1,9).is_perfect_square(r) && r == rational(1,3));
349 ENSURE(rational(4,9).is_perfect_square(r) && r == rational(2,3));
350 }
351
352
tstmod(rational const & m,rational const & n)353 static void tstmod(rational const& m, rational const& n) {
354 //
355 // (=> (distinct n 0)
356 // (let ((q (div m n)) (r (mod m n)))
357 // (and (= m (+ (* n q) r))
358 // (<= 0 r (- (abs n) 1))))))
359 //
360
361 rational q = div(m,n);
362 rational r = mod(m,n);
363 std::cout << m << " " << n << " " << q << " " << r << "\n";
364 std::cout << m << " == " << n*q+r << "\n";
365
366 ENSURE(m == (n * q) + r);
367 ENSURE(rational::zero() <= r);
368 ENSURE(r < abs(n));
369
370 }
371
tst9()372 static void tst9() {
373 // record semantics of rational div/mod.
374 tstmod(rational("41000000000000"),rational("-7000000000000"));
375 tstmod(rational("-41000000000000"),rational("-7000000000000"));
376 tstmod(rational("-41000000000000"),rational("7000000000000"));
377 tstmod(rational("41000000000000"),rational("7000000000000"));
378
379 tstmod(rational(41),rational(-7));
380 tstmod(rational(-41),rational(-7));
381 tstmod(rational(-41),rational(7));
382 tstmod(rational(41),rational(7));
383 }
384
385 #define NUM_RATIONALS 1000000
386 #define MAGNITUDE 10000
387
tst10(bool use_ints)388 static void tst10(bool use_ints) {
389 if (use_ints)
390 std::cout << "Testing multiplication performance using small ints\n";
391 else
392 std::cout << "Testing multiplication performance using small rationals\n";
393 vector<rational> vals;
394 vector<rational> vals2;
395 vector<float> fvals;
396 vals.resize(NUM_RATIONALS);
397 vals2.resize(NUM_RATIONALS);
398 fvals.resize(NUM_RATIONALS);
399 for (unsigned i = 0; i < NUM_RATIONALS; i++) {
400 int r1 = rand() % MAGNITUDE;
401 int r2 = use_ints ? 1 : rand() % MAGNITUDE;
402 if (r2 == 0) r2 = 1;
403 if (rand() % 2 == 0) r1 = -r1;
404 vals[i] = rational(r1, r2);
405 vals2[i] = rational(r1, r2);
406 fvals[i] = ((float)r1) / ((float)r2);
407 }
408 {
409 timeit t(true, "multiplication with rationals");
410 for (unsigned i = 0; i < NUM_RATIONALS - 1; i++) {
411 vals[i] *= vals[i+1];
412 }
413 }
414 {
415 timeit t(true, "multiplication with floats: ");
416 for (unsigned i = 0; i < NUM_RATIONALS - 1; i++) {
417 fvals[i] *= fvals[i+1];
418 }
419 }
420 std::cout << "\n";
421 }
422
423 #define NUM_RATIONALS2 10000
424 #define MAGNITUDE2 100000000
425
tst11(bool use_ints)426 static void tst11(bool use_ints) {
427 vector<rational> vals;
428 vector<float> fvals;
429 vals.resize(NUM_RATIONALS2);
430 fvals.resize(NUM_RATIONALS2);
431 for (unsigned i = 0; i < NUM_RATIONALS2; i++) {
432 int r1 = rand() % MAGNITUDE2;
433 int r2 = use_ints ? 1 : rand() % MAGNITUDE2;
434 if (r2 == 0) r2 = 1;
435 if (rand() % 2 == 0) r1 = -r1;
436 vals[i] = rational(r1, r2);
437 fvals[i] = ((float)r1) / ((float)r2);
438 }
439 {
440 timeit t(true, "multiplication with big rationals");
441 for (unsigned j = 0; j < 10; j++)
442 for (unsigned i = 0; i < NUM_RATIONALS2-1; i++) {
443 vals[i] *= vals[i+1];
444 }
445 }
446 {
447 timeit t(true, "multiplication with floats: ");
448 for (unsigned j = 0; j < 10; j++)
449 for (unsigned i = 0; i < NUM_RATIONALS2-1; i++) {
450 fvals[i] *= fvals[i+1];
451 }
452 }
453 std::cout << "\n";
454 }
455
tst12()456 static void tst12() {
457 std::cout << "test12\n";
458 rational r;
459 r = 5;
460 SASSERT(r.get_bit(0));
461 SASSERT(!r.get_bit(1));
462 SASSERT(r.get_bit(2));
463 SASSERT(!r.get_bit(3));
464 r = rational("10000000000000000000000000000000001");
465 for (unsigned i = 0; i < r.get_num_bits(); ++i)
466 std::cout << i << ": " << r.get_bit(i) << "\n";
467 }
468
469
tst_rational()470 void tst_rational() {
471 TRACE("rational", tout << "starting rational test...\n";);
472 std::cout << "sizeof(rational): " << sizeof(rational) << "\n";
473 rational r1("10000000000000000000000000000000001");
474 r1.hash();
475 tst1();
476 tst2();
477 tst3();
478 tst4();
479 tst5();
480 std::cout << "running tst6" << std::endl;
481 tst6();
482 std::cout << "running tst7" << std::endl;
483 tst7();
484 std::cout << "running tst8" << std::endl;
485 tst8();
486 std::cout << "running tst9" << std::endl;
487 tst9();
488 std::cout << "running rational_tester::tst1" << std::endl;
489 rational_tester::tst1();
490 rational_tester::tst2();
491 tst11(true);
492 tst10(true);
493 tst10(false);
494 tst12();
495 }
496