cprover
Loading...
Searching...
No Matches
rational.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Rational Numbers
4
5Author: 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);
24 normalize();
25 return *this;
26}
27
29{
30 rationalt tmp(n);
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
73 if(_gcd!=1 && !_gcd.is_zero())
74 {
75 denominator/=_gcd;
76 numerator/=_gcd;
77 }
78}
79
81{
83 return;
84
87
90 n.denominator=t;
91}
92
94{
96 std::swap(numerator, denominator);
97}
98
100{
101 rationalt tmp(n);
102 tmp.invert();
103 return tmp;
104}
105
106std::ostream &operator<<(std::ostream &out, const rationalt &a)
107{
108 std::string d=integer2string(a.get_numerator());
109 if(a.get_denominator()!=1)
111 return out << d;
112}
const mp_integer & get_numerator() const
Definition: rational.h:85
rationalt & operator/=(const rationalt &n)
Definition: rational.cpp:51
rationalt & operator+=(const rationalt &n)
Definition: rational.cpp:19
void same_denominator(rationalt &n)
Definition: rational.cpp:80
rationalt & operator-=(const rationalt &n)
Definition: rational.cpp:28
void normalize()
Definition: rational.cpp:60
rationalt & operator*=(const rationalt &n)
Definition: rational.cpp:43
rationalt & operator-()
Definition: rational.cpp:37
void invert()
Definition: rational.cpp:93
mp_integer denominator
Definition: rational.h:19
const mp_integer & get_denominator() const
Definition: rational.h:90
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:99
std::ostream & operator<<(std::ostream &out, const rationalt &a)
Definition: rational.cpp:106
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition: invariant.h:463