CBMC
rational.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Rational Numbers
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "rational.h"
13 
14 #include <ostream>
15 
16 #include "invariant.h"
17 
19 {
20  rationalt tmp(n);
21  same_denominator(tmp);
22  numerator+=tmp.numerator;
23  normalize();
24  return *this;
25 }
26 
28 {
29  rationalt tmp(n);
30  same_denominator(tmp);
31  numerator-=tmp.numerator;
32  normalize();
33  return *this;
34 }
35 
37 {
38  numerator.negate();
39  return *this;
40 }
41 
43 {
46  normalize();
47  return *this;
48 }
49 
51 {
52  PRECONDITION(!n.numerator.is_zero());
55  normalize();
56  return *this;
57 }
58 
60 {
61  // first do sign
62 
63  if(denominator.is_negative())
64  {
65  denominator.negate();
66  numerator.negate();
67  }
68 
69  // divide by gcd
70 
71  mp_integer _gcd=gcd(denominator, numerator);
72  if(_gcd!=1 && !_gcd.is_zero())
73  {
74  denominator/=_gcd;
75  numerator/=_gcd;
76  }
77 }
78 
80 {
82  return;
83 
86 
88  denominator=t;
89  n.denominator=t;
90 }
91 
93 {
94  PRECONDITION(numerator != 0);
95  std::swap(numerator, denominator);
96 }
97 
99 {
100  rationalt tmp(n);
101  tmp.invert();
102  return tmp;
103 }
104 
105 std::ostream &operator<<(std::ostream &out, const rationalt &a)
106 {
107  std::string d=integer2string(a.get_numerator());
108  if(a.get_denominator()!=1)
109  d+="/"+integer2string(a.get_denominator());
110  return out << d;
111 }
rationalt & operator/=(const rationalt &n)
Definition: rational.cpp:50
rationalt & operator+=(const rationalt &n)
Definition: rational.cpp:18
const mp_integer & get_denominator() const
Definition: rational.h:90
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
void invert()
Definition: rational.cpp:92
mp_integer denominator
Definition: rational.h:19
mp_integer numerator
Definition: rational.h:18
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
rationalt inverse(const rationalt &n)
Definition: rational.cpp:98
std::ostream & operator<<(std::ostream &out, const rationalt &a)
Definition: rational.cpp:105
BigInt mp_integer
Definition: smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition: invariant.h:463