10#ifndef CPROVER_UTIL_RATIONAL_H
11#define CPROVER_UTIL_RATIONAL_H
39 r1.same_denominator(
r2);
40 return r1.numerator==
r2.numerator;
46 r1.same_denominator(
r2);
47 return r1.numerator!=
r2.numerator;
53 r1.same_denominator(
r2);
54 return r1.numerator<
r2.numerator;
60 r1.same_denominator(
r2);
61 return r1.numerator<=
r2.numerator;
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
const mp_integer & get_numerator() const
rationalt & operator/=(const rationalt &n)
bool operator>=(const rationalt &n) const
rationalt & operator+=(const rationalt &n)
bool operator<=(const rationalt &n) const
void same_denominator(rationalt &n)
rationalt & operator-=(const rationalt &n)
rationalt & operator*=(const rationalt &n)
bool operator<(const rationalt &n) const
bool operator==(const rationalt &n) const
bool operator!=(const rationalt &n) const
bool operator>(const rationalt &n) const
const mp_integer & get_denominator() const
rationalt(const mp_integer &i)
rationalt operator*(const rationalt &a, const rationalt &b)
rationalt operator-(const rationalt &a, const rationalt &b)
rationalt operator/(const rationalt &a, const rationalt &b)
rationalt inverse(const rationalt &n)
rationalt operator+(const rationalt &a, const rationalt &b)
std::ostream & operator<<(std::ostream &out, const rationalt &a)