cprover
rational.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_RATIONAL_H
11 #define CPROVER_UTIL_RATIONAL_H
12 
13 #include "mp_arith.h"
14 
15 class constant_exprt;
16 
17 class rationalt
18 {
19 protected:
20  mp_integer numerator; // Zaehler
22 
23  void normalize();
24  void same_denominator(rationalt &n);
25 
26 public:
27  // constructors
29  explicit rationalt(const mp_integer &i):numerator(i), denominator(1) { }
30  explicit rationalt(int i):numerator(i), denominator(1) { }
31 
32  rationalt &operator+=(const rationalt &n);
33  rationalt &operator-=(const rationalt &n);
35  rationalt &operator*=(const rationalt &n);
36  rationalt &operator/=(const rationalt &n);
37 
38  bool operator==(const rationalt &n) const
39  {
40  rationalt r1(*this), r2(n);
41  r1.same_denominator(r2);
42  return r1.numerator==r2.numerator;
43  }
44 
45  bool operator!=(const rationalt &n) const
46  {
47  rationalt r1(*this), r2(n);
48  r1.same_denominator(r2);
49  return r1.numerator!=r2.numerator;
50  }
51 
52  bool operator<(const rationalt &n) const
53  {
54  rationalt r1(*this), r2(n);
55  r1.same_denominator(r2);
56  return r1.numerator<r2.numerator;
57  }
58 
59  bool operator<=(const rationalt &n) const
60  {
61  rationalt r1(*this), r2(n);
62  r1.same_denominator(r2);
63  return r1.numerator<=r2.numerator;
64  }
65 
66  bool operator>=(const rationalt &n) const
67  {
68  return !(*this<n);
69  }
70 
71  bool operator>(const rationalt &n) const
72  {
73  return !(*this<=n);
74  }
75 
76  bool is_zero() const
77  { return numerator.is_zero(); }
78 
79  bool is_one() const
80  { return !is_zero() && numerator==denominator; }
81 
82  bool is_negative() const
83  { return !is_zero() && numerator.is_negative(); }
84 
85  void invert();
86 
87  const mp_integer &get_numerator() const
88  {
89  return numerator;
90  }
91 
92  const mp_integer &get_denominator() const
93  {
94  return denominator;
95  }
96 };
97 
98 inline rationalt operator+(const rationalt &a, const rationalt &b)
99 {
100  rationalt tmp(a);
101  tmp+=b;
102  return tmp;
103 }
104 
105 inline rationalt operator-(const rationalt &a, const rationalt &b)
106 {
107  rationalt tmp(a);
108  tmp-=b;
109  return tmp;
110 }
111 
112 inline rationalt operator-(const rationalt &a)
113 {
114  rationalt tmp(a);
115  return -tmp;
116 }
117 
118 inline rationalt operator*(const rationalt &a, const rationalt &b)
119 {
120  rationalt tmp(a);
121  tmp*=b;
122  return tmp;
123 }
124 
125 inline rationalt operator/(const rationalt &a, const rationalt &b)
126 {
127  rationalt tmp(a);
128  tmp/=b;
129  return tmp;
130 }
131 
132 std::ostream &operator<<(std::ostream &out, const rationalt &a);
133 
134 rationalt inverse(const rationalt &n);
135 
136 #endif // CPROVER_UTIL_RATIONAL_H
rationalt::is_zero
bool is_zero() const
Definition: rational.h:76
operator+
rationalt operator+(const rationalt &a, const rationalt &b)
Definition: rational.h:98
mp_arith.h
rationalt::denominator
mp_integer denominator
Definition: rational.h:21
rationalt::operator<
bool operator<(const rationalt &n) const
Definition: rational.h:52
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
rationalt::rationalt
rationalt(const mp_integer &i)
Definition: rational.h:29
rationalt::operator!=
bool operator!=(const rationalt &n) const
Definition: rational.h:45
rationalt::operator+=
rationalt & operator+=(const rationalt &n)
Definition: rational.cpp:19
rationalt::invert
void invert()
Definition: rational.cpp:93
operator<<
std::ostream & operator<<(std::ostream &out, const rationalt &a)
Definition: rational.cpp:106
rationalt::is_negative
bool is_negative() const
Definition: rational.h:82
rationalt::operator<=
bool operator<=(const rationalt &n) const
Definition: rational.h:59
rationalt::get_numerator
const mp_integer & get_numerator() const
Definition: rational.h:87
rationalt::operator-=
rationalt & operator-=(const rationalt &n)
Definition: rational.cpp:28
rationalt::operator-
rationalt & operator-()
Definition: rational.cpp:37
rationalt::same_denominator
void same_denominator(rationalt &n)
Definition: rational.cpp:80
rationalt::operator>
bool operator>(const rationalt &n) const
Definition: rational.h:71
inverse
rationalt inverse(const rationalt &n)
Definition: rational.cpp:99
rationalt::get_denominator
const mp_integer & get_denominator() const
Definition: rational.h:92
rationalt::numerator
mp_integer numerator
Definition: rational.h:20
rationalt::operator*=
rationalt & operator*=(const rationalt &n)
Definition: rational.cpp:43
operator-
rationalt operator-(const rationalt &a, const rationalt &b)
Definition: rational.h:105
rationalt::operator==
bool operator==(const rationalt &n) const
Definition: rational.h:38
operator*
rationalt operator*(const rationalt &a, const rationalt &b)
Definition: rational.h:118
rationalt::rationalt
rationalt()
Definition: rational.h:28
operator/
rationalt operator/(const rationalt &a, const rationalt &b)
Definition: rational.h:125
rationalt::operator/=
rationalt & operator/=(const rationalt &n)
Definition: rational.cpp:51
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
rationalt::rationalt
rationalt(int i)
Definition: rational.h:30
rationalt::operator>=
bool operator>=(const rationalt &n) const
Definition: rational.h:66
rationalt
Definition: rational.h:18
rationalt::normalize
void normalize()
Definition: rational.cpp:60
rationalt::is_one
bool is_one() const
Definition: rational.h:79