mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

mpq/mpz features from LRA

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-09 09:18:59 -07:00
parent 60725f5384
commit 085d31dca2
2 changed files with 14 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/util/mpq.h
View file

@ -34,6 +34,8 @@ public:
void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); } void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); }
mpz const & numerator() const { return m_num; } mpz const & numerator() const { return m_num; }
mpz const & denominator() const { return m_den; } mpz const & denominator() const { return m_den; }
double get_double() const;
}; };
inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); } inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
@ -833,9 +835,11 @@ public:
} }
bool is_even(mpz const & a) { return mpz_manager<SYNCH>::is_even(a); } bool is_even(mpz const & a) { return mpz_manager<SYNCH>::is_even(a); }
public:
bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); } bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); }
friend bool operator==(mpq const & a, mpq const & b) ;
friend bool operator>=(mpq const & a, mpq const & b);
}; };
typedef mpq_manager<true> synch_mpq_manager; typedef mpq_manager<true> synch_mpq_manager;

9
src/util/mpz.h
View file

@ -593,6 +593,15 @@ public:
} }
} }
bool lt(mpz const& a, int b) {
if (is_small(a)) {
return a.m_val < b;
}
else {
return lt(a, mpz(b));
}
}
bool lt(mpz const & a, mpz const & b) { bool lt(mpz const & a, mpz const & b) {
if (is_small(a) && is_small(b)) { if (is_small(a) && is_small(b)) {
return a.m_val < b.m_val; return a.m_val < b.m_val;