From e9c9974ee092be249b55cfb5ba1cf309b85da525 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Jul 2013 18:26:33 -0700 Subject: [PATCH] Reorganize methods. Remove num_macros.h. Add binary rationals mpbq. Signed-off-by: Leonardo de Moura --- src/util/mpbq.cpp | 55 ++++++++++++++++ src/util/mpbq.h | 146 ++++++++++++++++++++++++++++++++++++++++++ src/util/mpq.h | 116 +++++++++++++++++++++++++-------- src/util/mpz.cpp | 2 +- src/util/mpz.h | 117 ++++++++++++++++++++++++++------- src/util/num_macros.h | 72 --------------------- 6 files changed, 385 insertions(+), 123 deletions(-) create mode 100644 src/util/mpbq.cpp create mode 100644 src/util/mpbq.h delete mode 100644 src/util/num_macros.h diff --git a/src/util/mpbq.cpp b/src/util/mpbq.cpp new file mode 100644 index 000000000..c628eb945 --- /dev/null +++ b/src/util/mpbq.cpp @@ -0,0 +1,55 @@ +/* +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 "mpbq.h" + +namespace lean { + +void mpbq::normalize() { + if (m_k == 0) + return; + if (is_zero()) { + m_k = 0; + return; + } + + unsigned k = m_num.power_of_two_multiple(); + if (k > m_k) + k = m_k; + m_num.div2k(k); + m_k -= k; +} + + +int cmp(mpbq const & a, mpbq const & b) { + if (a.m_k == b.m_k) + return cmp(a.m_num, b.m_num); + else if (a.m_k < b.m_k) { + mpz tmp(a.m_num); + tmp.mul2k(b.m_k - a.m_k); + return cmp(tmp, b.m_num); + } + else { + lean_assert(a.m_k > b.m_k); + mpz tmp(b.m_num); + tmp.mul2k(a.m_k - b.m_k); + return cmp(a.m_num, tmp); + } +} + +int cmp(mpbq const & a, mpz const & b) { + if (a.m_k == 0) + return cmp(a.m_num, b); + else { + mpz tmp(b); + tmp.mul2k(a.m_k); + return cmp(a.m_num, tmp); + } +} + + +} + diff --git a/src/util/mpbq.h b/src/util/mpbq.h new file mode 100644 index 000000000..439e4f928 --- /dev/null +++ b/src/util/mpbq.h @@ -0,0 +1,146 @@ +/* +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 { + +// Multiple precision binary rationals +class mpbq { + mpz m_num; + unsigned m_k; + void normalize(); +public: + mpbq():m_k(0) {} + mpbq(mpbq const & v):m_num(v.m_num), m_k(v.m_k) {} + mpbq(mpbq && v); + mpbq(mpz const & v):m_num(v), m_k(0) {} + mpbq(int n):m_num(n), m_k(0) {} + mpbq(int n, unsigned k):m_num(n), m_k(k) { normalize(); } + ~mpbq() {} + + void swap(mpbq & o) { m_num.swap(o.m_num); std::swap(m_k, o.m_k); } + + unsigned hash() const { return m_num.hash(); } + + int sgn() const { return m_num.sgn(); } + friend int sgn(mpbq const & a) { return a.sgn(); } + bool is_pos() const { return sgn() > 0; } + bool is_neg() const { return sgn() < 0; } + bool is_zero() const { return sgn() == 0; } + bool is_nonpos() const { return !is_pos(); } + bool is_nonneg() const { return !is_neg(); } + + void neg() { m_num.neg(); } + friend mpbq neg(mpbq a) { a.neg(); return a; } + + void abs() { m_num.abs(); } + friend mpbq abs(mpbq a) { a.abs(); return a; } + + mpz const & get_numerator() const { return m_num; } + unsigned get_k() const { return m_k; } + bool is_integer() const { return m_k == 0; } + + friend int cmp(mpbq const & a, mpbq const & b); + friend int cmp(mpbq const & a, mpz const & b); + friend int cmp(mpbq const & a, unsigned b) { return cmp(a, mpbq(b)); } + friend int cmp(mpbq const & a, int b) { return cmp(a, mpbq(b)); } + + friend bool operator<(mpbq const & a, mpbq const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpbq const & a, mpz const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpbq const & a, unsigned b) { return cmp(a, b) < 0; } + friend bool operator<(mpbq const & a, int b) { return cmp(a, b) < 0; } + friend bool operator<(unsigned a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator<(int a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator<(mpz const & a, mpbq const & b) { return cmp(b, a) > 0; } + + friend bool operator>(mpbq const & a, mpbq const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpbq const & a, mpz const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpbq const & a, unsigned b) { return cmp(a, b) > 0; } + friend bool operator>(mpbq const & a, int b) { return cmp(a, b) > 0; } + friend bool operator>(unsigned a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator>(int a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator>(mpz const & a, mpbq const & b) { return cmp(b, a) > 0; } + + friend bool operator<=(mpbq const & a, mpbq const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpbq const & a, mpz const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpbq const & a, unsigned b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpbq const & a, int b) { return cmp(a, b) <= 0; } + friend bool operator<=(unsigned a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator<=(int a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator<=(mpz const & a, mpbq const & b) { return cmp(b, a) > 0; } + + friend bool operator>=(mpbq const & a, mpbq const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpbq const & a, mpz const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpbq const & a, unsigned b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpbq const & a, int b) { return cmp(a, b) >= 0; } + friend bool operator>=(unsigned a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator>=(int a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator>=(mpz const & a, mpbq const & b) { return cmp(b, a) > 0; } + + friend bool operator==(mpbq const & a, mpbq const & b) { return a.m_k == b.m_k && a.m_num == b.m_num; } + friend bool operator==(mpbq const & a, mpz const & b) { return a.is_integer() && a.m_num == b; } + friend bool operator==(mpbq const & a, unsigned int b) { return a.is_integer() && a.m_num == b; } + friend bool operator==(mpbq const & a, int b) { return a.is_integer() && a.m_num == b; } + friend bool operator==(mpz const & a, mpbq const & b) { return operator==(b, a); } + friend bool operator==(unsigned int a, mpbq const & b) { return operator==(b, a); } + friend bool operator==(int a, mpbq const & b) { return operator==(b, a); } + + friend bool operator!=(mpbq const & a, mpbq const & b) { return !operator==(a,b); } + friend bool operator!=(mpbq const & a, mpz const & b) { return !operator==(a,b); } + friend bool operator!=(mpz const & a, mpbq const & b) { return !operator==(a,b); } + friend bool operator!=(mpbq const & a, unsigned int b) { return !operator==(a,b); } + friend bool operator!=(mpbq const & a, int b) { return !operator==(a,b); } + friend bool operator!=(unsigned int a, mpbq const & b) { return !operator==(a,b); } + friend bool operator!=(int a, mpbq const & b) { return !operator==(a,b); } + + mpbq & operator+=(mpbq const & a); + mpbq & operator+=(unsigned a); + mpbq & operator+=(int a); + + mpbq & operator-=(mpbq const & a); + mpbq & operator-=(unsigned a); + mpbq & operator-=(int a); + + mpbq & operator*=(mpbq const & a); + mpbq & operator*=(unsigned a); + mpbq & operator*=(int a); + + friend mpbq operator+(mpbq a, mpbq const & b) { return a += b; } + friend mpbq operator+(mpbq a, mpz const & b) { return a += b; } + friend mpbq operator+(mpbq a, unsigned b) { return a += b; } + friend mpbq operator+(mpbq a, int b) { return a += b; } + friend mpbq operator+(mpz const & a, mpbq b) { return b += a; } + friend mpbq operator+(unsigned a, mpbq b) { return b += a; } + friend mpbq operator+(int a, mpbq b) { return b += a; } + + friend mpbq operator-(mpbq a, mpbq const & b) { return a -= b; } + friend mpbq operator-(mpbq a, mpz const & b) { return a -= b; } + friend mpbq operator-(mpbq a, unsigned b) { return a -= b; } + friend mpbq operator-(mpbq a, int b) { return a -= b; } + friend mpbq operator-(mpz const & a, mpbq b) { b.neg(); return b += a; } + friend mpbq operator-(unsigned a, mpbq b) { b.neg(); return b += a; } + friend mpbq operator-(int a, mpbq b) { b.neg(); return b += a; } + + friend mpbq operator*(mpbq a, mpbq const & b) { return a *= b; } + friend mpbq operator*(mpbq a, mpz const & b) { return a *= b; } + friend mpbq operator*(mpbq a, unsigned b) { return a *= b; } + friend mpbq operator*(mpbq a, int b) { return a *= b; } + friend mpbq operator*(mpz const & a, mpbq b) { return b *= a; } + friend mpbq operator*(unsigned a, mpbq b) { return b *= a; } + friend mpbq operator*(int a, mpbq b) { return b *= a; } + + mpbq & operator++() { return operator+=(1); } + mpbq operator++(int) { mpbq r(*this); ++(*this); return r; } + + mpbq & operator--() { return operator-=(1); } + mpbq operator--(int) { mpbq r(*this); --(*this); return r; } + + friend std::ostream & operator<<(std::ostream & out, mpbq const & v); +}; + +} diff --git a/src/util/mpq.h b/src/util/mpq.h index 0ea79b6d0..a4d317f4f 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -39,70 +39,133 @@ public: 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); } + unsigned hash() const { return static_cast(mpz_get_si(mpq_numref(m_val))); } + + int sgn() const { return mpq_sgn(m_val); } + friend int sgn(mpq const & a) { return a.sgn(); } + bool is_pos() const { return sgn() > 0; } + bool is_neg() const { return sgn() < 0; } + bool is_zero() const { return sgn() == 0; } + bool is_nonpos() const { return !is_pos(); } + bool is_nonneg() const { return !is_neg(); } + + void neg() { mpq_neg(m_val, m_val); } + friend mpq neg(mpq a) { a.neg(); return a; } + + void abs() { mpq_abs(m_val, m_val); } + friend mpq abs(mpq a) { a.abs(); return a; } + + void inv() { mpq_inv(m_val, m_val); } + friend mpq inv(mpq a) { a.inv(); return a; } + 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 int cmp(mpq const & a, unsigned b) { return mpq_cmp_ui(a.m_val, b, 1); } + friend int cmp(mpq const & a, int b) { return mpq_cmp_si(a.m_val, b, 1); } + + friend bool operator<(mpq const & a, mpq const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpq const & a, unsigned b) { return cmp(a, b) < 0; } + friend bool operator<(mpq const & a, int b) { return cmp(a, b) < 0; } + friend bool operator<(unsigned a, mpq const & b) { return cmp(b, a) > 0; } + friend bool operator<(int a, mpq const & b) { return cmp(b, a) > 0; } + + friend bool operator>(mpq const & a, mpq const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpq const & a, unsigned b) { return cmp(a, b) > 0; } + friend bool operator>(mpq const & a, int b) { return cmp(a, b) > 0; } + friend bool operator>(unsigned a, mpq const & b) { return cmp(b, a) < 0; } + friend bool operator>(int a, mpq const & b) { return cmp(b, a) < 0; } + + friend bool operator<=(mpq const & a, mpq const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpq const & a, unsigned b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpq const & a, int b) { return cmp(a, b) <= 0; } + friend bool operator<=(unsigned a, mpq const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(int a, mpq const & b) { return cmp(b, a) >= 0; } + + friend bool operator>=(mpq const & a, mpq const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpq const & a, unsigned b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpq const & a, int b) { return cmp(a, b) >= 0; } + friend bool operator>=(unsigned a, mpq const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(int a, mpq const & b) { return cmp(b, a) <= 0; } + 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+=(mpz const & o) { mpz_addmul(mpq_numref(m_val), mpq_denref(m_val), o.m_val); mpq_canonicalize(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-=(mpz const & o) { mpz_submul(mpq_numref(m_val), mpq_denref(m_val), o.m_val); mpq_canonicalize(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*=(mpz const & o) { mpz_mul(mpq_numref(m_val), mpq_numref(m_val), o.m_val); mpq_canonicalize(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/=(mpz const & o) { mpz_mul(mpq_denref(m_val), mpq_denref(m_val), o.m_val); mpq_canonicalize(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) + + friend mpq operator+(mpq a, mpq const & b) { return a += b; } + friend mpq operator+(mpq a, mpz const & b) { return a += b; } + friend mpq operator+(mpq a, unsigned b) { return a += b; } + friend mpq operator+(mpq a, int b) { return a += b; } + friend mpq operator+(mpz const & a, mpq b) { return b += a; } + friend mpq operator+(unsigned a, mpq b) { return b += a; } + friend mpq operator+(int a, mpq b) { return b += a; } + + friend mpq operator-(mpq a, mpq const & b) { return a -= b; } + friend mpq operator-(mpq a, mpz const & b) { return a -= b; } + friend mpq operator-(mpq a, unsigned b) { return a -= b; } + friend mpq operator-(mpq a, int b) { return a -= b; } + friend mpq operator-(mpz const & a, mpq b) { b.neg(); return b += a; } + friend mpq operator-(unsigned a, mpq b) { b.neg(); return b += a; } + friend mpq operator-(int a, mpq b) { b.neg(); return b += a; } + + friend mpq operator*(mpq a, mpq const & b) { return a *= b; } + friend mpq operator*(mpq a, mpz const & b) { return a *= b; } + friend mpq operator*(mpq a, unsigned b) { return a *= b; } + friend mpq operator*(mpq a, int b) { return a *= b; } + friend mpq operator*(mpz const & a, mpq b) { return b *= a; } + friend mpq operator*(unsigned a, mpq b) { return b *= a; } + friend mpq operator*(int a, mpq b) { return b *= a; } + + friend mpq operator/(mpq a, mpq const & b) { return a /= b; } + friend mpq operator/(mpq a, mpz const & b) { return a /= b; } + friend mpq operator/(mpq a, unsigned b) { return a /= b; } + friend mpq operator/(mpq a, int b) { return a /= b; } + friend mpq operator/(mpz const & a, mpq b) { b.inv(); return b *= a; } + friend mpq operator/(unsigned a, mpq b) { b.inv(); return b *= a; } + friend mpq operator/(int a, mpq b) { b.inv(); return b *= a; } mpq & operator++() { return operator+=(1); } - mpq & operator--() { return operator-=(1); } mpq operator++(int) { mpq r(*this); ++(*this); return r; } + + mpq & operator--() { return operator-=(1); } mpq operator--(int) { mpq r(*this); --(*this); return r; } mpz get_numerator() const { return mpz(mpq_numref(m_val)); } @@ -111,8 +174,9 @@ public: friend std::ostream & operator<<(std::ostream & out, mpq const & v); void floor(); - void ceil(); friend mpz floor(mpq const & a); + + void ceil(); friend mpz ceil(mpq const & a); }; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index a31e90d15..961222e07 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -40,7 +40,7 @@ bool mpz::is_power_of_two(unsigned & shift) const { return false; } } - + mpz operator%(mpz const & a, mpz const & b) { mpz r(rem(a, b)); if (r.is_neg()) { diff --git a/src/util/mpz.h b/src/util/mpz.h index 7be07ebc7..e0ad7212a 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -7,7 +7,6 @@ Author: Leonardo de Moura #pragma once #include #include -#include "num_macros.h" #include "debug.h" namespace lean { @@ -28,23 +27,28 @@ public: mpz(mpz const & s) { mpz_init_set(m_val, s.m_val); } mpz(mpz && s):mpz() { mpz_swap(m_val, s.m_val); } ~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(); } void swap(mpz & o) { mpz_swap(m_val, o.m_val); } unsigned hash() const { return static_cast(mpz_get_si(m_val)); } + int sgn() const { return mpz_sgn(m_val); } + friend int sgn(mpz const & a) { return a.sgn(); } + bool is_pos() const { return sgn() > 0; } + bool is_neg() const { return sgn() < 0; } + bool is_zero() const { return sgn() == 0; } + bool is_nonpos() const { return !is_pos(); } + bool is_nonneg() const { return !is_neg(); } + + void neg() { mpz_neg(m_val, m_val); } + friend mpz neg(mpz a) { a.neg(); return a; } + + void abs() { mpz_abs(m_val, m_val); } + friend mpz abs(mpz a) { a.abs(); return a; } + + bool even() const { return mpz_even_p(m_val) != 0; } + bool odd() const { return !even(); } + bool is_int() const { return mpz_fits_sint_p(m_val) != 0; } bool is_unsigned_int() const { return mpz_fits_uint_p(m_val) != 0; } bool is_long_int() const { return mpz_fits_slong_p(m_val) != 0; } @@ -55,33 +59,94 @@ public: unsigned long int get_unsigned_long_int() const { lean_assert(is_unsigned_long_int()); return mpz_get_ui(m_val); } unsigned int get_unsigned_int() const { lean_assert(is_unsigned_int()); return static_cast(get_unsigned_long_int()); } - friend mpz abs(mpz const & a) { mpz r; mpz_abs(r.m_val, a.m_val); return r; } - friend int cmp(mpz const & a, mpz const & b) { return mpz_cmp(a.m_val, b.m_val); } 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) + friend bool operator<(mpz const & a, mpz const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpz const & a, unsigned b) { return cmp(a, b) < 0; } + friend bool operator<(mpz const & a, int b) { return cmp(a, b) < 0; } + friend bool operator<(unsigned a, mpz const & b) { return cmp(b, a) > 0; } + friend bool operator<(int a, mpz const & b) { return cmp(b, a) > 0; } + + friend bool operator>(mpz const & a, mpz const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpz const & a, unsigned b) { return cmp(a, b) > 0; } + friend bool operator>(mpz const & a, int b) { return cmp(a, b) > 0; } + friend bool operator>(unsigned a, mpz const & b) { return cmp(b, a) < 0; } + friend bool operator>(int a, mpz const & b) { return cmp(b, a) < 0; } + + friend bool operator<=(mpz const & a, mpz const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpz const & a, unsigned b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpz const & a, int b) { return cmp(a, b) <= 0; } + friend bool operator<=(unsigned a, mpz const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(int a, mpz const & b) { return cmp(b, a) >= 0; } + + friend bool operator>=(mpz const & a, mpz const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpz const & a, unsigned b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpz const & a, int b) { return cmp(a, b) >= 0; } + friend bool operator>=(unsigned a, mpz const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(int a, mpz const & b) { return cmp(b, a) <= 0; } + + friend bool operator==(mpz const & a, mpz const & b) { return cmp(a, b) == 0; } + friend bool operator==(mpz const & a, unsigned b) { return cmp(a, b) == 0; } + friend bool operator==(mpz const & a, int b) { return cmp(a, b) == 0; } + friend bool operator==(unsigned a, mpz const & b) { return cmp(b, a) == 0; } + friend bool operator==(int a, mpz const & b) { return cmp(b, a) == 0; } + + friend bool operator!=(mpz const & a, mpz const & b) { return cmp(a, b) != 0; } + friend bool operator!=(mpz const & a, unsigned b) { return cmp(a, b) != 0; } + friend bool operator!=(mpz const & a, int b) { return cmp(a, b) != 0; } + friend bool operator!=(unsigned a, mpz const & b) { return cmp(b, a) != 0; } + friend bool operator!=(int a, mpz const & b) { return cmp(b, a) != 0; } + 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; } mpz & operator+=(int u) { if (u >= 0) mpz_add_ui(m_val, m_val, u); else mpz_sub_ui(m_val, m_val, u); return *this; } + mpz & operator-=(mpz const & o) { mpz_sub(m_val, m_val, o.m_val); return *this; } mpz & operator-=(unsigned u) { mpz_sub_ui(m_val, m_val, u); return *this; } mpz & operator-=(int u) { if (u >= 0) mpz_sub_ui(m_val, m_val, u); else mpz_add_ui(m_val, m_val, u); return *this; } + mpz & operator*=(mpz const & o) { mpz_mul(m_val, m_val, o.m_val); return *this; } mpz & operator*=(unsigned u) { mpz_mul_ui(m_val, m_val, u); return *this; } mpz & operator*=(int u) { mpz_mul_si(m_val, m_val, u); return *this; } + mpz & operator/=(mpz const & o) { mpz_tdiv_q(m_val, m_val, o.m_val); return *this; } 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 a, mpz const & b) { return a += b; } + friend mpz operator+(mpz a, unsigned b) { return a += b; } + friend mpz operator+(mpz a, int b) { return a += b; } + friend mpz operator+(unsigned a, mpz b) { return b += a; } + friend mpz operator+(int a, mpz b) { return b += a; } + + friend mpz operator-(mpz a, mpz const & b) { return a -= b; } + friend mpz operator-(mpz a, unsigned b) { return a -= b; } + friend mpz operator-(mpz a, int b) { return a -= b; } + friend mpz operator-(unsigned a, mpz b) { b.neg(); return b += a; } + friend mpz operator-(int a, mpz b) { b.neg(); return b += a; } + + friend mpz operator*(mpz a, mpz const & b) { return a *= b; } + friend mpz operator*(mpz a, unsigned b) { return a *= b; } + friend mpz operator*(mpz a, int b) { return a *= b; } + friend mpz operator*(unsigned a, mpz b) { return b *= a; } + friend mpz operator*(int a, mpz b) { return b *= a; } + + friend mpz operator/(mpz a, mpz const & b) { return a /= b; } + friend mpz operator/(mpz a, unsigned b) { return a /= b; } + friend mpz operator/(mpz a, int b) { return a /= b; } + friend mpz operator/(unsigned a, mpz const & b) { mpz r(a); return r /= b; } + friend mpz operator/(int a, mpz const & b) { mpz r(a); return r /= b; } + friend mpz operator%(mpz const & a, mpz const & b); mpz & operator++() { return operator+=(1); } - mpz & operator--() { return operator-=(1); } mpz operator++(int) { mpz r(*this); ++(*this); return r; } + + mpz & operator--() { return operator-=(1); } mpz operator--(int) { mpz r(*this); --(*this); return r; } mpz & operator&=(mpz const & o) { mpz_and(m_val, m_val, o.m_val); return *this; } @@ -89,6 +154,11 @@ public: mpz & operator^=(mpz const & o) { mpz_xor(m_val, m_val, o.m_val); return *this; } void comp() { mpz_com(m_val, m_val); } + friend mpz operator&(mpz a, mpz const & b) { return a &= b; } + friend mpz operator|(mpz a, mpz const & b) { return a |= b; } + friend mpz operator^(mpz a, mpz const & b) { return a ^= b; } + friend mpz operator~(mpz a) { a.comp(); return a; } + // this <- this + a*b void addmul(mpz const & a, mpz const & b) { mpz_addmul(m_val, a.m_val, b.m_val); } // this <- this - a*b @@ -115,6 +185,10 @@ public: bool is_power_of_two() const { return is_pos() && mpz_popcount(m_val) == 1; } bool is_power_of_two(unsigned & shift) const; + /** + \brief Return largest k s.t. n is a multiple of 2^k + */ + unsigned power_of_two_multiple() const { return mpz_scan1(m_val, 0); } friend mpz power(mpz const & a, unsigned k) { mpz r; mpz_pow_ui(r.m_val, a.m_val, k); return r; } @@ -122,11 +196,6 @@ public: friend void root(mpz & root, mpz const & a, unsigned k) { mpz_root(root.m_val, a.m_val, k); } friend mpz root(mpz const & a, unsigned k) { mpz r; root(r, a, k); return r; } - friend mpz operator&(mpz a, mpz const & b) { return a &= b; } - friend mpz operator|(mpz a, mpz const & b) { return a |= b; } - friend mpz operator^(mpz a, mpz const & b) { return a ^= b; } - friend mpz operator~(mpz a) { a.comp(); return a; } - 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 deleted file mode 100644 index 9b3f5a047..000000000 --- a/src/util/num_macros.h +++ /dev/null @@ -1,72 +0,0 @@ -/* -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 - -// 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, 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<(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; } - -#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; } \ -bool is_neg() const { return sgn() < 0; } \ -bool is_zero() const { return sgn() == 0; } \ -bool is_nonpos() const { return !is_pos(); } \ -bool is_nonneg() const { return !is_neg(); } - -#define DEFINE_ARITH_OPS(T) \ -friend T operator+(T a, T const & b) { return a += b; } \ -friend T operator-(T a, T const & b) { return a -= b; } \ -friend T operator*(T a, T const & b) { return a *= b; } \ -friend T operator/(T a, T const & b) { return a /= b; } \ -friend T operator+(T a, unsigned b) { return a += b; } \ -friend T operator-(T a, unsigned b) { return a -= b; } \ -friend T operator*(T a, unsigned b) { return a *= b; } \ -friend T operator/(T a, unsigned b) { return a /= b; } \ -friend T operator+(T a, int b) { return a += b; } \ -friend T operator-(T a, int b) { return a -= b; } \ -friend T operator*(T a, int b) { return a *= b; } \ -friend T operator/(T a, int b) { return a /= b; } \ -friend T operator+(unsigned a, T b) { return b += a; } \ -friend T operator-(unsigned a, T b) { b.neg(); return b += a; } \ -friend T operator*(unsigned a, T b) { return b *= a; } \ -friend T operator/(unsigned a, T const & b) { T r(a); return r /= b; } \ -friend T operator+(int a, T b) { return b += a; } \ -friend T operator-(int a, T b) { b.neg(); return b += a; } \ -friend T operator*(int a, T b) { return b *= a; } \ -friend T operator/(int a, T const & b) { T r(a); return r /= b; }