mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
LRA changes to rational
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d8c3b273d3
commit
42ea2d1ea5
|
@ -52,6 +52,9 @@ public:
|
|||
|
||||
rational(mpz const & z) { m().set(m_val, z); }
|
||||
|
||||
rational(double z) { UNREACHABLE(); }
|
||||
|
||||
|
||||
explicit rational(char const * v) { m().set(m_val, v); }
|
||||
|
||||
struct i64 {};
|
||||
|
@ -127,6 +130,12 @@ public:
|
|||
return *this;
|
||||
}
|
||||
|
||||
rational & operator=(int v) {
|
||||
*this = rational(v);
|
||||
return *this;
|
||||
}
|
||||
rational & operator=(double v) { UNREACHABLE(); return *this; }
|
||||
|
||||
friend inline rational numerator(rational const & r) { rational result; m().get_numerator(r.m_val, result.m_val); return result; }
|
||||
|
||||
friend inline rational denominator(rational const & r) { rational result; m().get_denominator(r.m_val, result.m_val); return result; }
|
||||
|
@ -136,6 +145,11 @@ public:
|
|||
return *this;
|
||||
}
|
||||
|
||||
rational & operator+=(int r) {
|
||||
(*this) += rational(r);
|
||||
return *this;
|
||||
}
|
||||
|
||||
rational & operator-=(rational const & r) {
|
||||
m().sub(m_val, r.m_val, m_val);
|
||||
return *this;
|
||||
|
@ -394,6 +408,7 @@ public:
|
|||
return num_bits;
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
inline bool operator!=(rational const & r1, rational const & r2) {
|
||||
|
@ -404,6 +419,10 @@ inline bool operator>(rational const & r1, rational const & r2) {
|
|||
return operator<(r2, r1);
|
||||
}
|
||||
|
||||
inline bool operator<(rational const & r1, int r2) {
|
||||
return r1 < rational(r2);
|
||||
}
|
||||
|
||||
inline bool operator<=(rational const & r1, rational const & r2) {
|
||||
return !operator>(r1, r2);
|
||||
}
|
||||
|
@ -412,14 +431,43 @@ inline bool operator>=(rational const & r1, rational const & r2) {
|
|||
return !operator<(r1, r2);
|
||||
}
|
||||
|
||||
inline bool operator>(rational const & a, int b) {
|
||||
return a > rational(b);
|
||||
}
|
||||
|
||||
inline bool operator!=(rational const & a, int b) {
|
||||
return !(a == rational(b));
|
||||
}
|
||||
|
||||
inline bool operator==(rational const & a, int b) {
|
||||
return a == rational(b);
|
||||
}
|
||||
|
||||
inline rational operator+(rational const & r1, rational const & r2) {
|
||||
return rational(r1) += r2;
|
||||
}
|
||||
|
||||
inline rational operator+(int r1, rational const & r2) {
|
||||
return rational(r1) + r2;
|
||||
}
|
||||
|
||||
inline rational operator+(rational const & r1, int r2) {
|
||||
return r1 + rational(r2);
|
||||
}
|
||||
|
||||
|
||||
inline rational operator-(rational const & r1, rational const & r2) {
|
||||
return rational(r1) -= r2;
|
||||
}
|
||||
|
||||
inline rational operator-(rational const & r1, int r2) {
|
||||
return r1 - rational(r2);
|
||||
}
|
||||
|
||||
inline rational operator-(int r1, rational const & r2) {
|
||||
return rational(r1) - r2;
|
||||
}
|
||||
|
||||
inline rational operator-(rational const & r) {
|
||||
rational result(r);
|
||||
result.neg();
|
||||
|
@ -430,10 +478,25 @@ inline rational operator*(rational const & r1, rational const & r2) {
|
|||
return rational(r1) *= r2;
|
||||
}
|
||||
|
||||
inline rational operator*(rational const & r1, int r2) {
|
||||
return r1 * rational(r2);
|
||||
}
|
||||
inline rational operator*(int r1, rational const & r2) {
|
||||
return rational(r1) * r2;
|
||||
}
|
||||
|
||||
inline rational operator/(rational const & r1, rational const & r2) {
|
||||
return rational(r1) /= r2;
|
||||
}
|
||||
|
||||
inline rational operator/(rational const & r1, int r2) {
|
||||
return r1 / rational(r2);
|
||||
}
|
||||
|
||||
inline rational operator/(int r1, rational const & r2) {
|
||||
return rational(r1) / r2;
|
||||
}
|
||||
|
||||
inline rational power(rational const & r, unsigned p) {
|
||||
return r.expt(p);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue