Reorganize methods. Remove num_macros.h. Add binary rationals mpbq.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
c6e68289da
commit
e9c9974ee0
6 changed files with 385 additions and 123 deletions
55
src/util/mpbq.cpp
Normal file
55
src/util/mpbq.cpp
Normal file
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
146
src/util/mpbq.h
Normal file
146
src/util/mpbq.h
Normal file
|
|
@ -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);
|
||||
};
|
||||
|
||||
}
|
||||
116
src/util/mpq.h
116
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<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); }
|
||||
|
||||
unsigned hash() const { return static_cast<unsigned>(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<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-=(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<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*=(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);
|
||||
};
|
||||
|
||||
|
|
|
|||
117
src/util/mpz.h
117
src/util/mpz.h
|
|
@ -7,7 +7,6 @@ Author: Leonardo de Moura
|
|||
#pragma once
|
||||
#include <iostream>
|
||||
#include <gmp.h>
|
||||
#include "num_macros.h"
|
||||
#include "debug.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -29,22 +28,27 @@ public:
|
|||
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<unsigned>(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<unsigned>(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); }
|
||||
|
|
|
|||
|
|
@ -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; }
|
||||
Loading…
Reference in a new issue