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