1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 inf_rational.h
7
8 Abstract:
9
10 Rational numbers with infenitesimals
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2006-09-18.
15 Nikolaj Bjorner (nbjorner) 2006-10-24.
16
17 Revision History:
18
19 --*/
20 #pragma once
21
22 #include<stdlib.h>
23 #include<string>
24 #include "util/debug.h"
25 #include "util/vector.h"
26 #include "util/rational.h"
27
28
29 class inf_rational {
30 static inf_rational m_zero;
31 static inf_rational m_one;
32 static inf_rational m_minus_one;
33 rational m_first;
34 rational m_second;
35 public:
36 static void init(); // called from rational::initialize() only
37 static void finalize(); // called from rational::finalize() only
38
hash()39 unsigned hash() const {
40 return m_first.hash() ^ (m_second.hash()+1);
41 }
42
operatorhash_proc43 struct hash_proc { unsigned operator()(inf_rational const& r) const { return r.hash(); } };
44
operatoreq_proc45 struct eq_proc { bool operator()(inf_rational const& r1, inf_rational const& r2) const { return r1 == r2; } };
46
swap(inf_rational & n)47 void swap(inf_rational & n) {
48 m_first.swap(n.m_first);
49 m_second.swap(n.m_second);
50 }
to_string()51 std::string to_string() const {
52 if (m_second.is_zero()) {
53 return m_first.to_string();
54 }
55 std::string s = "(";
56 s += m_first.to_string();
57 if (m_second.is_neg()) {
58 s += " -e*";
59 }
60 else {
61 s += " +e*";
62 }
63 s += abs(m_second).to_string();
64 s += ")";
65 return s;
66 }
67
inf_rational()68 inf_rational() {}
69
inf_rational(int n)70 explicit inf_rational(int n):
71 m_first(rational(n)),
72 m_second(rational())
73 {}
74
inf_rational(int n,int d)75 explicit inf_rational(int n, int d):
76 m_first(rational(n,d)),
77 m_second(rational())
78 {}
79
inf_rational(rational const & r,bool pos_inf)80 explicit inf_rational(rational const& r, bool pos_inf):
81 m_first(r),
82 m_second(pos_inf ? rational::one() : rational::minus_one())
83 {}
84
inf_rational(rational const & r)85 inf_rational(rational const& r):
86 m_first(r)
87 {
88 m_second.reset();
89 }
90
inf_rational(rational const & r,rational const & i)91 inf_rational(rational const& r, rational const& i):
92 m_first(r),
93 m_second(i) {
94 }
95
96 /**
97 \brief Set inf_rational to 0.
98 */
reset()99 void reset() {
100 m_first.reset();
101 m_second.reset();
102 }
103
is_int()104 bool is_int() const {
105 return m_first.is_int() && m_second.is_zero();
106 }
107
is_int64()108 bool is_int64() const {
109 return m_first.is_int64() && m_second.is_zero();
110 }
111
is_uint64()112 bool is_uint64() const {
113 return m_first.is_uint64() && m_second.is_zero();
114 }
115
is_rational()116 bool is_rational() const { return m_second.is_zero(); }
117
get_int64()118 int64_t get_int64() const {
119 SASSERT(is_int64());
120 return m_first.get_int64();
121 }
122
get_uint64()123 uint64_t get_uint64() const {
124 SASSERT(is_uint64());
125 return m_first.get_uint64();
126 }
127
get_rational()128 rational const& get_rational() const {
129 return m_first;
130 }
131
get_infinitesimal()132 rational const& get_infinitesimal() const {
133 return m_second;
134 }
135
get_first()136 rational const & get_first() const { return m_first; }
137
138 inf_rational & operator=(const rational & r) {
139 m_first = r;
140 m_second.reset();
141 return *this;
142 }
143
numerator(const inf_rational & r)144 friend inline inf_rational numerator(const inf_rational & r) {
145 SASSERT(r.m_second.is_zero());
146 return inf_rational(numerator(r.m_first));
147 }
148
denominator(const inf_rational & r)149 friend inline inf_rational denominator(const inf_rational & r) {
150 SASSERT(r.m_second.is_zero());
151 return inf_rational(denominator(r.m_first));
152 }
153
154 inf_rational & operator+=(const inf_rational & r) {
155 m_first += r.m_first;
156 m_second += r.m_second;
157 return *this;
158 }
159
160 inf_rational & operator-=(const inf_rational & r) {
161 m_first -= r.m_first;
162 m_second -= r.m_second;
163 return *this;
164 }
165
166 inf_rational & operator+=(const rational & r) {
167 m_first += r;
168 return *this;
169 }
170
171 inf_rational & operator-=(const rational & r) {
172 m_first -= r;
173 return *this;
174 }
175
176 inf_rational & operator*=(const rational & r1) {
177 m_first *= r1;
178 m_second *= r1;
179 return *this;
180 }
181
182 //
183 // These operations get us out of the realm of inf_rational:
184 // (r1 + e*k1)*(r2 + e*k2) = (r1*r2 + (r1*k2 + r2*k1)*e)
185 //
186 // inf_rational & operator*=(const inf_rational & r)
187 // inf_rational & operator/=(const inf_rational & r)
188 // inf_rational & operator%=(const inf_rational & r)
189 // friend inline inf_rational div(const inf_rational & r1, const inf_rational & r2)
190 // inf_rational expt(int n)
191 // instead, we define operators that approximate some of these operations from above and below.
192
193 friend inf_rational inf_mult(inf_rational const& r1, inf_rational const& r2);
194 friend inf_rational sup_mult(inf_rational const& r1, inf_rational const& r2);
195
196 friend inf_rational inf_div(inf_rational const& r1, inf_rational const& r2);
197 friend inf_rational sup_div(inf_rational const& r1, inf_rational const& r2);
198
199 friend inf_rational inf_power(inf_rational const& r1, unsigned n);
200 friend inf_rational sup_power(inf_rational const& r1, unsigned n);
201
202 friend inf_rational inf_root(inf_rational const& r1, unsigned n);
203 friend inf_rational sup_root(inf_rational const& r1, unsigned n);
204
205 inf_rational & operator/=(const rational & r) {
206 m_first /= r;
207 m_second /= r;
208 return *this;
209 }
210
211 friend inline inf_rational operator*(const rational & r1, const inf_rational & r2);
212 friend inline inf_rational operator*(const inf_rational & r1, const rational & r2);
213 friend inline inf_rational operator/(const inf_rational & r1, const rational & r2);
214
215 inf_rational & operator++() {
216 ++m_first;
217 return *this;
218 }
219
220 const inf_rational operator++(int) { inf_rational tmp(*this); ++(*this); return tmp; }
221
222 inf_rational & operator--() {
223 --m_first;
224 return *this;
225 }
226
227 const inf_rational operator--(int) { inf_rational tmp(*this); --(*this); return tmp; }
228
229 friend inline bool operator==(const inf_rational & r1, const inf_rational & r2) {
230 return r1.m_first == r2.m_first && r1.m_second == r2.m_second;
231 }
232
233 friend inline bool operator==(const rational & r1, const inf_rational & r2) {
234 return r1 == r2.m_first && r2.m_second.is_zero();
235 }
236
237 friend inline bool operator==(const inf_rational & r1, const rational & r2) {
238 return r1.m_first == r2 && r1.m_second.is_zero();
239 }
240
241 friend inline bool operator<(const inf_rational & r1, const inf_rational & r2) {
242 return
243 (r1.m_first < r2.m_first) ||
244 (r1.m_first == r2.m_first && r1.m_second < r2.m_second);
245 }
246
247 friend inline bool operator<(const rational & r1, const inf_rational & r2) {
248 return
249 (r1 < r2.m_first) ||
250 (r1 == r2.m_first && r2.m_second.is_pos());
251 }
252
253 friend inline bool operator<(const inf_rational & r1, const rational & r2) {
254 return
255 (r1.m_first < r2) ||
256 (r1.m_first == r2 && r1.m_second.is_neg());
257 }
258
neg()259 void neg() {
260 m_first.neg();
261 m_second.neg();
262 }
263
is_zero()264 bool is_zero() const {
265 return m_first.is_zero() && m_second.is_zero();
266 }
267
is_one()268 bool is_one() const {
269 return m_first.is_one() && m_second.is_zero();
270 }
271
is_minus_one()272 bool is_minus_one() const {
273 return m_first.is_minus_one() && m_second.is_zero();
274 }
275
is_neg()276 bool is_neg() const {
277 return
278 m_first.is_neg() ||
279 (m_first.is_zero() && m_second.is_neg());
280 }
281
is_pos()282 bool is_pos() const {
283 return
284 m_first.is_pos() ||
285 (m_first.is_zero() && m_second.is_pos());
286 }
287
is_nonneg()288 bool is_nonneg() const {
289 return
290 m_first.is_pos() ||
291 (m_first.is_zero() && m_second.is_nonneg());
292 }
293
is_nonpos()294 bool is_nonpos() const {
295 return
296 m_first.is_neg() ||
297 (m_first.is_zero() && m_second.is_nonpos());
298 }
299
floor(const inf_rational & r)300 friend inline rational floor(const inf_rational & r) {
301 if (r.m_first.is_int()) {
302 if (r.m_second.is_nonneg()) {
303 return r.m_first;
304 }
305 return r.m_first - rational::one();
306 }
307
308 return floor(r.m_first);
309 }
310
ceil(const inf_rational & r)311 friend inline rational ceil(const inf_rational & r) {
312 if (r.m_first.is_int()) {
313 if (r.m_second.is_nonpos()) {
314 return r.m_first;
315 }
316 return r.m_first + rational::one();
317 }
318
319 return ceil(r.m_first);
320 }
321
zero()322 static const inf_rational & zero() {
323 return m_zero;
324 }
325
one()326 static const inf_rational & one() {
327 return m_one;
328 }
329
minus_one()330 static const inf_rational & minus_one() {
331 return m_minus_one;
332 }
333
334 // Perform: this += c * k
addmul(const rational & c,const inf_rational & k)335 void addmul(const rational & c, const inf_rational & k) {
336 m_first.addmul(c, k.m_first);
337 m_second.addmul(c, k.m_second);
338 }
339
340 // Perform: this += c * k
submul(const rational & c,const inf_rational & k)341 void submul(const rational & c, const inf_rational & k) {
342 m_first.submul(c, k.m_first);
343 m_second.submul(c, k.m_second);
344 }
345 };
346
347 inline bool operator!=(const inf_rational & r1, const inf_rational & r2) {
348 return !operator==(r1, r2);
349 }
350
351 inline bool operator!=(const rational & r1, const inf_rational & r2) {
352 return !operator==(r1, r2);
353 }
354
355 inline bool operator!=(const inf_rational & r1, const rational & r2) {
356 return !operator==(r1, r2);
357 }
358
359 inline bool operator>(const inf_rational & r1, const inf_rational & r2) {
360 return operator<(r2, r1);
361 }
362
363 inline bool operator>(const inf_rational & r1, const rational & r2) {
364 return operator<(r2, r1);
365 }
366
367 inline bool operator>(const rational & r1, const inf_rational & r2) {
368 return operator<(r2, r1);
369 }
370
371 inline bool operator<=(const inf_rational & r1, const inf_rational & r2) {
372 return !operator>(r1, r2);
373 }
374
375 inline bool operator<=(const rational & r1, const inf_rational & r2) {
376 return !operator>(r1, r2);
377 }
378
379 inline bool operator<=(const inf_rational & r1, const rational & r2) {
380 return !operator>(r1, r2);
381 }
382
383 inline bool operator>=(const inf_rational & r1, const inf_rational & r2) {
384 return !operator<(r1, r2);
385 }
386
387 inline bool operator>=(const rational & r1, const inf_rational & r2) {
388 return !operator<(r1, r2);
389 }
390
391 inline bool operator>=(const inf_rational & r1, const rational & r2) {
392 return !operator<(r1, r2);
393 }
394
395 inline inf_rational operator+(const inf_rational & r1, const inf_rational & r2) {
396 return inf_rational(r1) += r2;
397 }
398
399 inline inf_rational operator-(const inf_rational & r1, const inf_rational & r2) {
400 return inf_rational(r1) -= r2;
401 }
402
403 inline inf_rational operator-(const inf_rational & r) {
404 inf_rational result(r);
405 result.neg();
406 return result;
407 }
408
409 inline inf_rational operator*(const rational & r1, const inf_rational & r2) {
410 inf_rational result(r2);
411 result.m_first *= r1;
412 result.m_second *= r1;
413 return result;
414 }
415
416 inline inf_rational operator*(const inf_rational & r1, const rational & r2) {
417 return r2 * r1;
418 }
419
420 inline inf_rational operator/(const inf_rational & r1, const rational & r2) {
421 inf_rational result(r1);
422 result.m_first /= r2;
423 result.m_second /= r2;
424 return result;
425 }
426
427 #if 0
428 inf_rational inf_mult(inf_rational const& r1, inf_rational const& r2);
429 inf_rational sup_mult(inf_rational const& r1, inf_rational const& r2);
430
431 inf_rational inf_div(inf_rational const& r1, inf_rational const& r2);
432 inf_rational sup_div(inf_rational const& r1, inf_rational const& r2);
433
434 inf_rational inf_power(inf_rational const& r1, unsigned n);
435 inf_rational sup_power(inf_rational const& r1, unsigned n);
436
437 inf_rational inf_root(inf_rational const& r1, unsigned n);
438 inf_rational sup_root(inf_rational const& r1, unsigned n);
439 #endif
440 //
441 // inline inf_rational operator/(const inf_rational & r1, const inf_rational & r2)
442 // inline inf_rational operator%(const inf_rational & r1, const inf_rational & r2)
443 // inf_rational gcd(const inf_rational & r1, const inf_rational & r2);
444 // inf_rational lcm(const inf_rational & r1, const inf_rational & r2);
445
446 inline std::ostream & operator<<(std::ostream & target, const inf_rational & r)
447 {
448 target << r.to_string();
449 return target;
450 }
451
452
abs(const inf_rational & r)453 inline inf_rational abs(const inf_rational & r) {
454 inf_rational result(r);
455 if (result.is_neg()) {
456 result.neg();
457 }
458 return result;
459 }
460