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