1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 mpq.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2010-06-21.
15
16 Revision History:
17
18 --*/
19
20 #include "util/mpq.h"
21 #include "util/rational.h"
22 #include "util/timeit.h"
23
tst0()24 static void tst0() {
25 synch_mpq_manager m;
26 mpq a, b;
27 m.set(a, 2, 3);
28 m.set(b, 4, 3);
29 m.div(a, b, b);
30 ENSURE(m.eq(b, m.mk_q(1, 2)));
31 }
32
tst1()33 static void tst1() {
34 synch_mpq_manager m;
35 char const * str = "1002034040050606089383838288182";
36 mpz v;
37 m.set(v, str);
38 std::cout << str << "\n" << m.to_string(v) << "\n";
39 mpz v2, v3;
40 m.mul(v, m.mk_z(-2), v2);
41 std::cout << "*-2 = \n" << m.to_string(v2) << "\n";
42 m.add(v, v2, v3);
43 m.neg(v3);
44 ENSURE(m.eq(v, v3));
45 ENSURE(m.le(v, v3));
46 ENSURE(m.ge(v, v3));
47 ENSURE(m.lt(v2, v));
48 ENSURE(m.le(v2, v));
49 ENSURE(m.gt(v, v2));
50 ENSURE(m.ge(v, v2));
51 ENSURE(m.neq(v, v2));
52 ENSURE(!m.neq(v, v3));
53 m.del(v);
54 m.del(v2);
55 m.del(v3);
56 }
57
58 #if 0
59 static void mk_random_num_str(unsigned buffer_sz, char * buffer) {
60 unsigned div_pos;
61 unsigned sz = (rand() % (buffer_sz-2)) + 1;
62 if (rand() % 2 == 0) {
63 // integer
64 div_pos = sz + 1;
65 }
66 else {
67 div_pos = rand() % sz;
68 if (div_pos == 0)
69 div_pos++;
70 }
71 ENSURE(sz < buffer_sz);
72 for (unsigned i = 0; i < sz-1; i++) {
73 if (i == div_pos && i < sz-2) {
74 buffer[i] = '/';
75 i++;
76 buffer[i] = '1' + (rand() % 9);
77 }
78 else {
79 buffer[i] = '0' + (rand() % 10);
80 }
81 }
82 buffer[sz-1] = 0;
83 }
84 #endif
85
bug1()86 static void bug1() {
87 synch_mpq_manager m;
88 mpq a;
89 mpq b;
90 m.set(a, 2);
91 m.set(b, 1, 2);
92 m.inv(a, a);
93 ENSURE(m.eq(a, b));
94 }
95
bug2()96 static void bug2() {
97 synch_mpq_manager m;
98 mpq a;
99 mpq b;
100 m.set(a, -2);
101 m.set(b, -1, 2);
102 m.inv(a, a);
103 ENSURE(m.eq(a, b));
104 }
105
tst2()106 static void tst2() {
107 unsynch_mpq_manager m;
108 scoped_mpq a(m);
109 m.set(a, 1, 3);
110 std::cout << "1/3: ";
111 m.display_decimal(std::cout, a, 10);
112 std::cout << "\n1/4: ";
113 m.set(a, 1, 4);
114 m.display_decimal(std::cout, a, 10);
115 std::cout << "\n";
116 }
117
set_str_bug()118 static void set_str_bug() {
119 unsynch_mpq_manager m;
120 scoped_mpq a(m);
121 scoped_mpq b(m);
122 m.set(a, "1.0");
123 std::cout << a << "\n";
124 m.set(b, 1);
125 ENSURE(a == b);
126 m.set(a, "1.1");
127 std::cout << a << "\n";
128 m.set(b, 11, 10);
129 ENSURE(a == b);
130 m.set(a, "1/3");
131 m.set(b, 1, 3);
132 std::cout << a << "\n";
133 ENSURE(a == b);
134 }
135
tst_prev_power_2(int64_t n,uint64_t d,unsigned expected)136 static void tst_prev_power_2(int64_t n, uint64_t d, unsigned expected) {
137 unsynch_mpq_manager m;
138 scoped_mpq a(m);
139 m.set(a, n, d);
140 ENSURE(m.prev_power_of_two(a) == expected);
141 }
142
tst_prev_power_2()143 static void tst_prev_power_2() {
144 tst_prev_power_2(-10, 1, 0);
145 tst_prev_power_2(0, 1, 0);
146 tst_prev_power_2(1, 1, 0);
147 tst_prev_power_2(2, 1, 1);
148 tst_prev_power_2(3, 1, 1);
149 tst_prev_power_2(4, 1, 2);
150 tst_prev_power_2(5, 1, 2);
151 tst_prev_power_2(8, 1, 3);
152 tst_prev_power_2(9, 1, 3);
153 tst_prev_power_2(9, 2, 2);
154 tst_prev_power_2(9, 4, 1);
155 tst_prev_power_2(9, 5, 0);
156 tst_prev_power_2((1ll << 60) + 1, 1, 60);
157 tst_prev_power_2((1ll << 60), 1, 60);
158 tst_prev_power_2((1ll << 60) - 1, 1, 59);
159 tst_prev_power_2((1ll << 60), 3, 58);
160 }
161
tst_mpq()162 void tst_mpq() {
163 tst_prev_power_2();
164 set_str_bug();
165 bug2();
166 bug1();
167 tst0();
168 tst1();
169 tst2();
170 }
171
172
173