CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
rational.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
16{
17protected:
20
21 void normalize();
23
24public:
25 // constructors
27 explicit rationalt(const mp_integer &i):numerator(i), denominator(1) { }
28 explicit rationalt(int i):numerator(i), denominator(1) { }
29
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
86 {
87 return numerator;
88 }
89
91 {
92 return denominator;
93 }
94};
95
96inline rationalt operator+(const rationalt &a, const rationalt &b)
97{
99 tmp+=b;
100 return tmp;
101}
102
103inline rationalt operator-(const rationalt &a, const rationalt &b)
104{
105 rationalt tmp(a);
106 tmp-=b;
107 return tmp;
108}
109
111{
112 rationalt tmp(a);
113 return -tmp;
114}
115
116inline rationalt operator*(const rationalt &a, const rationalt &b)
117{
118 rationalt tmp(a);
119 tmp*=b;
120 return tmp;
121}
122
123inline rationalt operator/(const rationalt &a, const rationalt &b)
124{
125 rationalt tmp(a);
126 tmp/=b;
127 return tmp;
128}
129
130std::ostream &operator<<(std::ostream &out, const rationalt &a);
131
133
134#endif // CPROVER_UTIL_RATIONAL_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
const mp_integer & get_numerator() const
Definition rational.h:85
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
bool operator<=(const rationalt &n) const
Definition rational.h:57
void same_denominator(rationalt &n)
Definition rational.cpp:79
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
const mp_integer & get_denominator() const
Definition rational.h:90
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