From 5c76cac9b131fc5815821340b515d1c5d34550ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Jul 2013 15:54:36 -0700 Subject: [PATCH] Add wrapper for GMP mpq numbers Signed-off-by: Leonardo de Moura --- src/util/mpq.cpp | 67 ++++++++++++++++++++++++ src/util/mpq.h | 119 ++++++++++++++++++++++++++++++++++++++++++ src/util/mpz.cpp | 12 +++-- src/util/mpz.h | 12 +++-- src/util/num_macros.h | 22 ++++---- 5 files changed, 215 insertions(+), 17 deletions(-) create mode 100644 src/util/mpq.cpp create mode 100644 src/util/mpq.h diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp new file mode 100644 index 000000000..6bfd157c4 --- /dev/null +++ b/src/util/mpq.cpp @@ -0,0 +1,67 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "mpq.h" + +namespace lean { + +void mpq::floor() { + if (is_integer()) + return; + bool neg = is_neg(); + mpz_tdiv_q(mpq_numref(m_val), mpq_numref(m_val), mpq_denref(m_val)); + mpz_set_ui(mpq_denref(m_val), 1); + if (neg) + mpz_sub_ui(mpq_numref(m_val), mpq_numref(m_val), 1); +} + +void mpq::ceil() { + if (is_integer()) + return; + bool pos = is_pos(); + mpz_tdiv_q(mpq_numref(m_val), mpq_numref(m_val), mpq_denref(m_val)); + mpz_set_ui(mpq_denref(m_val), 1); + if (pos) + mpz_add_ui(mpq_numref(m_val), mpq_numref(m_val), 1); +} + +mpz floor(mpq const & a) { + if (a.is_integer()) + return a.get_numerator(); + mpz r; + mpz_tdiv_q(mpq::zval(r), mpq_numref(a.m_val), mpq_denref(a.m_val)); + if (a.is_neg()) + r -= 1; + return r; +} + +mpz ceil(mpq const & a) { + if (a.is_integer()) + return a.get_numerator(); + mpz r; + mpz_tdiv_q(mpq::zval(r), mpq_numref(a.m_val), mpq_denref(a.m_val)); + if (a.is_pos()) + r += 1; + return r; +} + +extern void display(std::ostream & out, __mpz_struct const * v); + +std::ostream & operator<<(std::ostream & out, mpq const & v) { + if (v.is_integer()) { + display(out, mpq_numref(v.m_val)); + } + else { + display(out, mpq_numref(v.m_val)); + out << "/"; + display(out, mpq_denref(v.m_val)); + } + return out; +} + +void pp(mpq const & v) { std::cout << v << std::endl; } + +} diff --git a/src/util/mpq.h b/src/util/mpq.h new file mode 100644 index 000000000..0ea79b6d0 --- /dev/null +++ b/src/util/mpq.h @@ -0,0 +1,119 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "mpz.h" + +namespace lean { + +// Wrapper for GMP rationals +class mpq { + mpq_t m_val; + static mpz_t const & zval(mpz const & v) { return v.m_val; } + static mpz_t & zval(mpz & v) { return v.m_val; } +public: + mpq & operator=(mpz const & v) { mpq_set_z(m_val, v.m_val); return *this; } + mpq & operator=(mpq const & v) { mpq_set(m_val, v.m_val); return *this; } + mpq & operator=(char const * v) { mpq_set_str(m_val, v, 10); return *this; } + mpq & operator=(unsigned long int v) { mpq_set_ui(m_val, v, 1u); return *this; } + mpq & operator=(long int v) { mpq_set_si(m_val, v, 1); return *this; } + mpq & operator=(unsigned int v) { return operator=(static_cast(v)); } + mpq & operator=(int v) { return operator=(static_cast(v)); } + + mpq() { mpq_init(m_val); } + mpq(mpq const & v):mpq() { operator=(v); } + mpq(mpz const & v):mpq() { operator=(v); } + mpq(mpq && s):mpq() { mpq_swap(m_val, s.m_val); } + mpq(char const * v):mpq() { operator=(v); } + mpq(unsigned long int v):mpq() { operator=(v); } + mpq(long int v):mpq() { operator=(v); } + mpq(unsigned int v):mpq() { operator=(v); } + mpq(int v):mpq() { operator=(v); } + mpq(unsigned long int n, unsigned long int d):mpq() { mpq_set_ui(m_val, n, d); mpq_canonicalize(m_val); } + mpq(long int n, long int d):mpq() { mpq_set_si(m_val, n, d); mpq_canonicalize(m_val); } + mpq(unsigned int n, unsigned int d):mpq() { mpq_set_ui(m_val, n, d); mpq_canonicalize(m_val); } + mpq(int n, int d):mpq() { mpq_set_si(m_val, n, d); mpq_canonicalize(m_val); } + mpq(double v):mpq() { mpq_set_d(m_val, v); } + ~mpq() { mpq_clear(m_val); } + + void neg() { mpq_neg(m_val, m_val); } + void abs() { mpq_abs(m_val, m_val); } + void inv() { mpq_inv(m_val, m_val); } + + friend mpq abs(mpq a) { a.abs(); return a; } + friend mpq neg(mpq a) { a.neg(); return a; } + friend mpq inv(mpq a) { a.inv(); return a; } + + int sgn() const { return mpq_sgn(m_val); } + friend int sgn(mpq const & a) { return a.sgn(); } + DEFINE_SIGN_METHODS() + + unsigned hash() const { return static_cast(mpz_get_si(mpq_numref(m_val))); } + + void swap(mpq & v) { mpq_swap(m_val, v.m_val); } + void swap_numerator(mpz & v) { mpz_swap(mpq_numref(m_val), v.m_val); mpq_canonicalize(m_val); } + void swap_denominator(mpz & v) { mpz_swap(mpq_denref(m_val), v.m_val); mpq_canonicalize(m_val); } + + double get_double() const { return mpq_get_d(m_val); } + + bool is_integer() const { return mpz_cmp_ui(mpq_denref(m_val), 1u) == 0; } + + friend int cmp(mpq const & a, mpq const & b) { return mpq_cmp(a.m_val, b.m_val); } + DEFINE_ORDER_OPS(mpq) + friend bool operator==(mpq const & a, mpq const & b) { return mpq_equal(a.m_val, b.m_val) != 0; } + friend bool operator==(mpq const & a, mpz const & b) { return a.is_integer() && mpz_cmp(mpq_numref(a.m_val), zval(b)) == 0; } + friend bool operator==(mpq const & a, unsigned long int b) { return a.is_integer() && mpz_cmp_ui(mpq_numref(a.m_val), b) == 0; } + friend bool operator==(mpq const & a, long int b) { return a.is_integer() && mpz_cmp_si(mpq_numref(a.m_val), b) == 0; } + friend bool operator==(mpq const & a, unsigned int b) { return a.is_integer() && mpz_cmp_ui(mpq_numref(a.m_val), b) == 0; } + friend bool operator==(mpq const & a, int b) { return a.is_integer() && mpz_cmp_si(mpq_numref(a.m_val), b) == 0; } + friend bool operator==(mpz const & a, mpq const & b) { return operator==(b, a); } + friend bool operator==(unsigned long int a, mpq const & b) { return operator==(b, a); } + friend bool operator==(long int a, mpq const & b) { return operator==(b, a); } + friend bool operator==(unsigned int a, mpq const & b) { return operator==(b, a); } + friend bool operator==(int a, mpq const & b) { return operator==(b, a); } + friend bool operator!=(mpq const & a, mpq const & b) { return !operator==(a,b); } + friend bool operator!=(mpq const & a, mpz const & b) { return !operator==(a,b); } + friend bool operator!=(mpz const & a, mpq const & b) { return !operator==(a,b); } + friend bool operator!=(mpq const & a, unsigned long int b) { return !operator==(a,b); } + friend bool operator!=(mpq const & a, long int b) { return !operator==(a,b); } + friend bool operator!=(mpq const & a, unsigned int b) { return !operator==(a,b); } + friend bool operator!=(mpq const & a, int b) { return !operator==(a,b); } + friend bool operator!=(unsigned long int a, mpq const & b) { return !operator==(a,b); } + friend bool operator!=(unsigned int a, mpq const & b) { return !operator==(a,b); } + friend bool operator!=(long int a, mpq const & b) { return !operator==(a,b); } + friend bool operator!=(int a, mpq const & b) { return !operator==(a,b); } + + mpq & operator+=(mpq const & o) { mpq_add(m_val, m_val, o.m_val); return *this; } + mpq & operator+=(unsigned int k) { mpz_addmul_ui(mpq_numref(m_val), mpq_denref(m_val), k); mpq_canonicalize(m_val); return *this; } + mpq & operator+=(int k) { if (k >= 0) return operator+=(static_cast(k)); else return operator-=(static_cast(-k)); } + mpq & operator-=(mpq const & o) { mpq_sub(m_val, m_val, o.m_val); return *this; } + mpq & operator-=(unsigned int k) { mpz_submul_ui(mpq_numref(m_val), mpq_denref(m_val), k); mpq_canonicalize(m_val); return *this; } + mpq & operator-=(int k) { if (k >= 0) return operator-=(static_cast(k)); else return operator+=(static_cast(-k)); } + mpq & operator*=(mpq const & o) { mpq_mul(m_val, m_val, o.m_val); return *this; } + mpq & operator*=(unsigned int k) { mpz_mul_ui(mpq_numref(m_val), mpq_numref(m_val), k); mpq_canonicalize(m_val); return *this; } + mpq & operator*=(int k) { mpz_mul_si(mpq_numref(m_val), mpq_numref(m_val), k); mpq_canonicalize(m_val); return *this; } + mpq & operator/=(mpq const & o) { mpq_div(m_val, m_val, o.m_val); return *this; } + mpq & operator/=(unsigned int k) { mpz_mul_ui(mpq_denref(m_val), mpq_denref(m_val), k); mpq_canonicalize(m_val); return *this; } + mpq & operator/=(int k) { mpz_mul_si(mpq_denref(m_val), mpq_denref(m_val), k); mpq_canonicalize(m_val); return *this; } + DEFINE_ARITH_OPS(mpq) + + mpq & operator++() { return operator+=(1); } + mpq & operator--() { return operator-=(1); } + mpq operator++(int) { mpq r(*this); ++(*this); return r; } + mpq operator--(int) { mpq r(*this); --(*this); return r; } + + mpz get_numerator() const { return mpz(mpq_numref(m_val)); } + mpz get_denominator() const { return mpz(mpq_denref(m_val)); } + + friend std::ostream & operator<<(std::ostream & out, mpq const & v); + + void floor(); + void ceil(); + friend mpz floor(mpq const & a); + friend mpz ceil(mpq const & a); +}; + +} diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 28fe1cee9..a31e90d15 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -52,18 +52,22 @@ mpz operator%(mpz const & a, mpz const & b) { return r; } -std::ostream & operator<<(std::ostream & out, mpz const & v) { - size_t sz = mpz_sizeinbase(v.m_val, 10) + 2; +void display(std::ostream & out, __mpz_struct const * v) { + size_t sz = mpz_sizeinbase(v, 10) + 2; if (sz < 1024) { char buffer[1024]; - mpz_get_str(buffer, 10, v.m_val); + mpz_get_str(buffer, 10, v); out << buffer; } else { std::unique_ptr buffer(new char[sz]); - mpz_get_str(buffer.get(), 10, v.m_val); + mpz_get_str(buffer.get(), 10, v); out << buffer.get(); } +} + +std::ostream & operator<<(std::ostream & out, mpz const & v) { + display(out, v.m_val); return out; } diff --git a/src/util/mpz.h b/src/util/mpz.h index 1b855be94..cfbe2587e 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -11,10 +11,13 @@ Author: Leonardo de Moura #include "debug.h" namespace lean { +class mpq; // Wrapper for GMP integers class mpz { + friend class mpq; mpz_t m_val; + mpz(__mpz_struct const * v) { mpz_init_set(m_val, v); } public: mpz() { mpz_init(m_val); } mpz(char const * v) { mpz_init_set_str(m_val, const_cast(v), 10); } @@ -27,10 +30,13 @@ public: ~mpz() { mpz_clear(m_val); } int sgn() const { return mpz_sgn(m_val); } + friend int sgn(mpz const & a) { return a.sgn(); } DEFINE_SIGN_METHODS() void neg() { mpz_neg(m_val, m_val); } void abs() { mpz_abs(m_val, m_val); } + friend mpz abs(mpz a) { a.abs(); return a; } + friend mpz neg(mpz a) { a.neg(); return a; } bool even() const { return mpz_even_p(m_val) != 0; } bool odd() const { return !even(); } @@ -55,6 +61,7 @@ public: friend int cmp(mpz const & a, unsigned b) { return mpz_cmp_ui(a.m_val, b); } friend int cmp(mpz const & a, int b) { return mpz_cmp_si(a.m_val, b); } DEFINE_ORDER_OPS(mpz) + DEFINE_EQ_OPS(mpz) mpz & operator+=(mpz const & o) { mpz_add(m_val, m_val, o.m_val); return *this; } mpz & operator+=(unsigned u) { mpz_add_ui(m_val, m_val, u); return *this; } @@ -69,6 +76,8 @@ public: mpz & operator/=(unsigned u) { mpz_tdiv_q_ui(m_val, m_val, u); return *this; } friend mpz rem(mpz const & a, mpz const & b) { mpz r; mpz_tdiv_r(r.m_val, a.m_val, b.m_val); return r; } mpz & operator%=(mpz const & o) { mpz r(*this % o); mpz_swap(m_val, r.m_val); return *this; } + DEFINE_ARITH_OPS(mpz) + friend mpz operator%(mpz const & a, mpz const & b); mpz & operator&=(mpz const & o) { mpz_and(m_val, m_val, o.m_val); return *this; } mpz & operator|=(mpz const & o) { mpz_ior(m_val, m_val, o.m_val); return *this; } @@ -113,9 +122,6 @@ public: friend mpz operator^(mpz a, mpz const & b) { return a ^= b; } friend mpz operator~(mpz a) { a.comp(); return a; } - DEFINE_ARITH_OPS(mpz) - friend mpz operator%(mpz const & a, mpz const & b); - friend void gcd(mpz & g, mpz const & a, mpz const & b) { mpz_gcd(g.m_val, a.m_val, b.m_val); } friend mpz gcd(mpz const & a, mpz const & b) { mpz r; gcd(r, a, b); return r; } friend void gcdext(mpz & g, mpz & s, mpz & t, mpz const & a, mpz const & b) { mpz_gcdext(g.m_val, s.m_val, t.m_val, a.m_val, b.m_val); } diff --git a/src/util/num_macros.h b/src/util/num_macros.h index 9c0965302..9b3f5a047 100644 --- a/src/util/num_macros.h +++ b/src/util/num_macros.h @@ -8,37 +8,39 @@ Author: Leonardo de Moura // Macros for defining numeral classes #define DEFINE_ORDER_OPS(T) \ -friend bool operator==(T const & a, T const & b) { return cmp(a, b) == 0; } \ -friend bool operator!=(T const & a, T const & b) { return cmp(a, b) != 0; } \ friend bool operator<(T const & a, T const & b) { return cmp(a, b) < 0; } \ friend bool operator>(T const & a, T const & b) { return cmp(a, b) > 0; } \ friend bool operator<=(T const & a, T const & b) { return cmp(a, b) <= 0; } \ friend bool operator>=(T const & a, T const & b) { return cmp(a, b) >= 0; } \ -friend bool operator==(T const & a, unsigned b) { return cmp(a, b) == 0; } \ -friend bool operator!=(T const & a, unsigned b) { return cmp(a, b) != 0; } \ friend bool operator<(T const & a, unsigned b) { return cmp(a, b) < 0; } \ friend bool operator>(T const & a, unsigned b) { return cmp(a, b) > 0; } \ friend bool operator<=(T const & a, unsigned b) { return cmp(a, b) <= 0; } \ friend bool operator>=(T const & a, unsigned b) { return cmp(a, b) >= 0; } \ -friend bool operator==(T const & a, int b) { return cmp(a, b) == 0; } \ -friend bool operator!=(T const & a, int b) { return cmp(a, b) != 0; } \ friend bool operator<(T const & a, int b) { return cmp(a, b) < 0; } \ friend bool operator>(T const & a, int b) { return cmp(a, b) > 0; } \ friend bool operator<=(T const & a, int b) { return cmp(a, b) <= 0; } \ friend bool operator>=(T const & a, int b) { return cmp(a, b) >= 0; } \ -friend bool operator==(unsigned a, T const & b) { return cmp(b, a) == 0; } \ -friend bool operator!=(unsigned a, T const & b) { return cmp(b, a) != 0; } \ friend bool operator<(unsigned a, T const & b) { return cmp(b, a) > 0; } \ friend bool operator>(unsigned a, T const & b) { return cmp(b, a) < 0; } \ friend bool operator<=(unsigned a, T const & b) { return cmp(b, a) >= 0; } \ friend bool operator>=(unsigned a, T const & b) { return cmp(b, a) <= 0; } \ -friend bool operator==(int a, T const & b) { return cmp(b, a) == 0; } \ -friend bool operator!=(int a, T const & b) { return cmp(b, a) != 0; } \ friend bool operator<(int a, T const & b) { return cmp(b, a) > 0; } \ friend bool operator>(int a, T const & b) { return cmp(b, a) < 0; } \ friend bool operator<=(int a, T const & b) { return cmp(b, a) >= 0; } \ friend bool operator>=(int a, T const & b) { return cmp(b, a) <= 0; } +#define DEFINE_EQ_OPS(T) \ +friend bool operator==(T const & a, T const & b) { return cmp(a, b) == 0; } \ +friend bool operator!=(T const & a, T const & b) { return cmp(a, b) != 0; } \ +friend bool operator==(T const & a, unsigned b) { return cmp(a, b) == 0; } \ +friend bool operator!=(T const & a, unsigned b) { return cmp(a, b) != 0; } \ +friend bool operator==(T const & a, int b) { return cmp(a, b) == 0; } \ +friend bool operator!=(T const & a, int b) { return cmp(a, b) != 0; } \ +friend bool operator==(unsigned a, T const & b) { return cmp(b, a) == 0; } \ +friend bool operator!=(unsigned a, T const & b) { return cmp(b, a) != 0; } \ +friend bool operator==(int a, T const & b) { return cmp(b, a) == 0; } \ +friend bool operator!=(int a, T const & b) { return cmp(b, a) != 0; } + #define DEFINE_SIGN_METHODS() \ bool is_pos() const { return sgn() > 0; } \