Add wrapper for GMP mpq numbers

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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; }
+
+}

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<unsigned long int>(v)); }
+    mpq & operator=(int v) { return operator=(static_cast<long int>(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<unsigned>(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<unsigned int>(k)); else return operator-=(static_cast<unsigned int>(-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<unsigned int>(k)); else return operator+=(static_cast<unsigned int>(-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);
+};
+
+}

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) {
+void display(std::ostream & out, __mpz_struct const * v) {
-    size_t sz = mpz_sizeinbase(v.m_val, 10) + 2;
+    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<char> 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;
 }
 

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<char*>(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); }

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; }       \