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