1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Tim King, Christopher L. Conway, Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* A multi-precision rational constant. |
14 |
|
*/ |
15 |
|
#include <sstream> |
16 |
|
#include <string> |
17 |
|
|
18 |
|
#include "base/cvc5config.h" |
19 |
|
#include "util/rational.h" |
20 |
|
|
21 |
|
#ifndef CVC5_CLN_IMP |
22 |
|
#error "This source should only ever be built if CVC5_CLN_IMP is on !" |
23 |
|
#endif /* CVC5_CLN_IMP */ |
24 |
|
|
25 |
|
#include "base/check.h" |
26 |
|
|
27 |
|
using namespace std; |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
|
31 |
|
/* Computes a rational given a decimal string. The rational |
32 |
|
* version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. |
33 |
|
*/ |
34 |
386220 |
Rational Rational::fromDecimal(const std::string& dec) { |
35 |
|
// Find the decimal point, if there is one |
36 |
386220 |
string::size_type i( dec.find(".") ); |
37 |
386220 |
if( i != string::npos ) { |
38 |
|
/* Erase the decimal point, so we have just the numerator. */ |
39 |
44716 |
Integer numerator( string(dec).erase(i,1) ); |
40 |
|
|
41 |
|
/* Compute the denominator: 10 raise to the number of decimal places */ |
42 |
22354 |
int decPlaces = dec.size() - (i + 1); |
43 |
44708 |
Integer denominator( Integer(10).pow(decPlaces) ); |
44 |
|
|
45 |
22354 |
return Rational( numerator, denominator ); |
46 |
|
} else { |
47 |
|
/* No decimal point, assume it's just an integer. */ |
48 |
363862 |
return Rational( dec ); |
49 |
|
} |
50 |
|
} |
51 |
|
|
52 |
460054855 |
int Rational::sgn() const |
53 |
|
{ |
54 |
460054855 |
if (cln::zerop(d_value)) |
55 |
|
{ |
56 |
42556660 |
return 0; |
57 |
|
} |
58 |
417498195 |
else if (cln::minusp(d_value)) |
59 |
|
{ |
60 |
279492240 |
return -1; |
61 |
|
} |
62 |
|
else |
63 |
|
{ |
64 |
138005955 |
Assert(cln::plusp(d_value)); |
65 |
138005955 |
return 1; |
66 |
|
} |
67 |
|
} |
68 |
|
|
69 |
221306 |
std::ostream& operator<<(std::ostream& os, const Rational& q){ |
70 |
221306 |
return os << q.toString(); |
71 |
|
} |
72 |
|
|
73 |
|
|
74 |
|
|
75 |
|
/** Equivalent to calling (this->abs()).cmp(b.abs()) */ |
76 |
8776002 |
int Rational::absCmp(const Rational& q) const{ |
77 |
8776002 |
const Rational& r = *this; |
78 |
8776002 |
int rsgn = r.sgn(); |
79 |
8776002 |
int qsgn = q.sgn(); |
80 |
8776002 |
if(rsgn == 0){ |
81 |
|
return (qsgn == 0) ? 0 : -1; |
82 |
8776002 |
}else if(qsgn == 0){ |
83 |
|
Assert(rsgn != 0); |
84 |
|
return 1; |
85 |
8776002 |
}else if((rsgn > 0) && (qsgn > 0)){ |
86 |
6912396 |
return r.cmp(q); |
87 |
1863606 |
}else if((rsgn < 0) && (qsgn < 0)){ |
88 |
|
// if r < q < 0, q.cmp(r) = +1, (r.abs()).cmp(q.abs()) = +1 |
89 |
|
// if q < r < 0, q.cmp(r) = -1, (r.abs()).cmp(q.abs()) = -1 |
90 |
|
// if q = r < 0, q.cmp(r) = 0, (r.abs()).cmp(q.abs()) = 0 |
91 |
214344 |
return q.cmp(r); |
92 |
1649262 |
}else if((rsgn < 0) && (qsgn > 0)){ |
93 |
1908346 |
Rational rpos = -r; |
94 |
954173 |
return rpos.cmp(q); |
95 |
|
}else { |
96 |
695089 |
Assert(rsgn > 0 && (qsgn < 0)); |
97 |
1390178 |
Rational qpos = -q; |
98 |
695089 |
return r.cmp(qpos); |
99 |
|
} |
100 |
|
} |
101 |
|
|
102 |
|
Maybe<Rational> Rational::fromDouble(double d) |
103 |
|
{ |
104 |
|
try{ |
105 |
|
cln::cl_DF fromD = d; |
106 |
|
Rational q; |
107 |
|
q.d_value = cln::rationalize(fromD); |
108 |
|
return q; |
109 |
|
}catch(cln::floating_point_underflow_exception& fpue){ |
110 |
|
return Maybe<Rational>(); |
111 |
|
}catch(cln::floating_point_nan_exception& fpne){ |
112 |
|
return Maybe<Rational>(); |
113 |
|
}catch(cln::floating_point_overflow_exception& fpoe){ |
114 |
|
return Maybe<Rational>(); |
115 |
|
} |
116 |
|
} |
117 |
|
|
118 |
29322 |
} // namespace cvc5 |