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 <algorithm>
15 #include <ostream>
16 
17 #include "invariant.h"
18 
20 {
21  rationalt tmp(n);
22  same_denominator(tmp);
23  numerator+=tmp.numerator;
24  normalize();
25  return *this;
26 }
27 
29 {
30  rationalt tmp(n);
31  same_denominator(tmp);
32  numerator-=tmp.numerator;
33  normalize();
34  return *this;
35 }
36 
38 {
39  numerator.negate();
40  return *this;
41 }
42 
44 {
47  normalize();
48  return *this;
49 }
50 
52 {
53  PRECONDITION(!n.numerator.is_zero());
56  normalize();
57  return *this;
58 }
59 
61 {
62  // first do sign
63 
64  if(denominator.is_negative())
65  {
66  denominator.negate();
67  numerator.negate();
68  }
69 
70  // divide by gcd
71 
72  mp_integer _gcd=gcd(denominator, numerator);
73  if(_gcd!=1 && !_gcd.is_zero())
74  {
75  denominator/=_gcd;
76  numerator/=_gcd;
77  }
78 }
79 
81 {
83  return;
84 
87 
89  denominator=t;
90  n.denominator=t;
91 }
92 
94 {
95  PRECONDITION(numerator != 0);
96  std::swap(numerator, denominator);
97 }
98 
100 {
101  rationalt tmp(n);
102  tmp.invert();
103  return tmp;
104 }
105 
106 std::ostream &operator<<(std::ostream &out, const rationalt &a)
107 {
108  std::string d=integer2string(a.get_numerator());
109  if(a.get_denominator()!=1)
110  d+="/"+integer2string(a.get_denominator());
111  return out << d;
112 }
mp_integer
BigInt mp_integer
Definition: smt_terms.h:17
rational.h
rationalt::denominator
mp_integer denominator
Definition: rational.h:19
inverse
rationalt inverse(const rationalt &n)
Definition: rational.cpp:99
invariant.h
rationalt::operator+=
rationalt & operator+=(const rationalt &n)
Definition: rational.cpp:19
rationalt::invert
void invert()
Definition: rational.cpp:93
rationalt::get_numerator
const mp_integer & get_numerator() const
Definition: rational.h:85
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
rationalt::operator-=
rationalt & operator-=(const rationalt &n)
Definition: rational.cpp:28
rationalt::operator-
rationalt & operator-()
Definition: rational.cpp:37
operator<<
std::ostream & operator<<(std::ostream &out, const rationalt &a)
Definition: rational.cpp:106
rationalt::same_denominator
void same_denominator(rationalt &n)
Definition: rational.cpp:80
rationalt::get_denominator
const mp_integer & get_denominator() const
Definition: rational.h:90
rationalt::numerator
mp_integer numerator
Definition: rational.h:18
rationalt::operator*=
rationalt & operator*=(const rationalt &n)
Definition: rational.cpp:43
rationalt::operator/=
rationalt & operator/=(const rationalt &n)
Definition: rational.cpp:51
rationalt
Definition: rational.h:15
rationalt::normalize
void normalize()
Definition: rational.cpp:60
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103