cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
18
rationalt
&
rationalt::operator+=
(
const
rationalt
&n)
19
{
20
rationalt
tmp(n);
21
same_denominator
(tmp);
22
numerator
+=tmp.
numerator
;
23
normalize
();
24
return
*
this
;
25
}
26
27
rationalt
&
rationalt::operator-=
(
const
rationalt
&n)
28
{
29
rationalt
tmp(n);
30
same_denominator
(tmp);
31
numerator
-=tmp.
numerator
;
32
normalize
();
33
return
*
this
;
34
}
35
36
rationalt
&
rationalt::operator-
()
37
{
38
numerator
.negate();
39
return
*
this
;
40
}
41
42
rationalt
&
rationalt::operator*=
(
const
rationalt
&n)
43
{
44
numerator
*=n.
numerator
;
45
denominator
*=n.
denominator
;
46
normalize
();
47
return
*
this
;
48
}
49
50
rationalt
&
rationalt::operator/=
(
const
rationalt
&n)
51
{
52
PRECONDITION
(!n.
numerator
.is_zero());
53
numerator
*=n.
denominator
;
54
denominator
*=n.
numerator
;
55
normalize
();
56
return
*
this
;
57
}
58
59
void
rationalt::normalize
()
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
79
void
rationalt::same_denominator
(
rationalt
&n)
80
{
81
if
(
denominator
==n.
denominator
)
82
return
;
83
84
numerator
*=n.
denominator
;
85
n.
numerator
*=
denominator
;
86
87
mp_integer
t=
denominator
*n.
denominator
;
88
denominator
=t;
89
n.
denominator
=t;
90
}
91
92
void
rationalt::invert
()
93
{
94
PRECONDITION
(
numerator
!= 0);
95
std::swap(
numerator
,
denominator
);
96
}
97
98
rationalt
inverse
(
const
rationalt
&n)
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
Definition
rational.h:16
rationalt::get_numerator
const mp_integer & get_numerator() const
Definition
rational.h:85
rationalt::operator/=
rationalt & operator/=(const rationalt &n)
Definition
rational.cpp:50
rationalt::operator+=
rationalt & operator+=(const rationalt &n)
Definition
rational.cpp:18
rationalt::same_denominator
void same_denominator(rationalt &n)
Definition
rational.cpp:79
rationalt::operator-=
rationalt & operator-=(const rationalt &n)
Definition
rational.cpp:27
rationalt::normalize
void normalize()
Definition
rational.cpp:59
rationalt::operator*=
rationalt & operator*=(const rationalt &n)
Definition
rational.cpp:42
rationalt::operator-
rationalt & operator-()
Definition
rational.cpp:36
rationalt::invert
void invert()
Definition
rational.cpp:92
rationalt::denominator
mp_integer denominator
Definition
rational.h:19
rationalt::get_denominator
const mp_integer & get_denominator() const
Definition
rational.h:90
rationalt::numerator
mp_integer numerator
Definition
rational.h:18
rationalt::rationalt
rationalt()
Definition
rational.h:26
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition
mp_arith.cpp:103
inverse
rationalt inverse(const rationalt &n)
Definition
rational.cpp:98
operator<<
std::ostream & operator<<(std::ostream &out, const rationalt &a)
Definition
rational.cpp:105
rational.h
mp_integer
BigInt mp_integer
Definition
smt_terms.h:17
invariant.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
util
rational.cpp
Generated by
1.17.0