max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(*): remove mpfr dependency

Browse source 
closes #1380
This commit is contained in:
Leonardo de Moura 2017-02-17 20:35:42 -08:00
parent bb4920fcbc
commit 7eef501ae1
22 changed files with 18 additions and 3739 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
doc/make/fedora-19.md
View file

@ -1,9 +1,9 @@
Install Packages on Fedora 19
-----------------------------
Instructions for installing git, cmake, mpfr, gmp, gperftools on Fedora
Instructions for installing git, cmake, gmp, gperftools on Fedora
sudo yum install -y git cmake mpfr-devel gmp-devel gperftools-devel
sudo yum install -y git cmake gmp-devel gperftools-devel
Instructions for installing gcc-4.8 (C++11 compatible) on Fedora
@ -12,4 +12,3 @@ Instructions for installing gcc-4.8 (C++11 compatible) on Fedora
Instructions for installing clang-3.3 (C++11 compatible) on Fedora
sudo yum install -y clang-devel

2
doc/make/msys2.md
View file

@ -19,7 +19,7 @@ It has a package management system, [pacman][pacman], which is used in Arch Linu
Here are the commands to install all dependencies needed to compile Lean on your machine.
```bash
pacman -S mingw-w64-x86_64-gcc mingw-w64-x86_64-mpfr mingw-w64-x86_64-ninja mingw-w64-x86_64-cmake git
pacman -S mingw-w64-x86_64-gcc mingw-w64-x86_64-ninja mingw-w64-x86_64-cmake git
```
## Build Lean

3
doc/make/osx-10.9.md
View file

@ -33,12 +33,11 @@ following to use `g++`.
cmake -DCMAKE_CXX_COMPILER=g++ ...
Required Packages: CMake, GMP, MPFR
Required Packages: CMake, GMP
---------------------
brew install cmake
brew install gmp
brew install mpfr
Optional Packages: tcmalloc and ninja

16
doc/make/split-stack.md
View file

@ -48,20 +48,6 @@ Then, build and install using
We should have the file `libgmp.a` at `$HOME/tools/split-stack/lib`.
Compiling MPFR using split-stacks
----------------------------------
Download MPFR from [http://www.mpfr.org/](http://www.mpfr.org/); uncompress the mpfr tar-ball at `$HOME/tools`; and configure it using
./configure CFLAGS=-fsplit-stack --prefix=$HOME/tools/split-stack --with-gmp-include=$HOME/tools/split-stack/include --with-gmp-lib=$HOME/tools/split-stack/lib --enable-static
Make sure MPFR does not produce any warning/error message. Then, build and install using:
make
make install
We should have the file `libmpfr.a` at `$HOME/tools/split-stack/lib`.
Compiling Lean using split-stacks
--------------------------------
@ -71,7 +57,7 @@ Go to the Lean directory, and create the folder `build/release`
Configure Lean using
cmake -D CMAKE_BUILD_TYPE=Release -D CMAKE_CXX_COMPILER=g++ -D TCMALLOC=OFF -D GMP_INCLUDE_DIR=$HOME/tools/split-stack/include -D GMP_LIBRARIES=$HOME/tools/split-stack/lib/libgmp.a -D MPFR_LIBRARIES=$HOME/tools/split-stack/lib/libmpfr.a ../../src
cmake -D CMAKE_BUILD_TYPE=Release -D CMAKE_CXX_COMPILER=g++ -D TCMALLOC=OFF -D GMP_INCLUDE_DIR=$HOME/tools/split-stack/include -D GMP_LIBRARIES=$HOME/tools/split-stack/lib/libgmp.a ../../src
Remark: if you have ninja build tool installed in your system, you can also provide `-G Ninja`

1
doc/make/ubuntu-12.04-detailed.md
View file

@ -5,7 +5,6 @@ Preparing working environment on Ubuntu 12.04
sudo apt-get install git
sudo apt-get install libgmp-dev
sudo apt-get install libmpfr-dev
sudo add-apt-repository ppa:kalakris/cmake -y
sudo apt-get install cmake

2
doc/make/ubuntu-16.04.md
View file

@ -3,7 +3,7 @@ Installing Lean on Ubuntu 16.04
### Basic packages
sudo apt-get install git libgmp-dev libmpfr-dev cmake
sudo apt-get install git libgmp-dev cmake
### Optional packages

28
src/CMakeLists.txt
View file

@ -197,29 +197,12 @@ if (EMSCRIPTEN)
BUILD_COMMAND emmake make -j4
INSTALL_COMMAND make install
)
set(mpfr_install_prefix ${CMAKE_CURRENT_BINARY_DIR}/mpfr-root)
ExternalProject_Add(
mpfr
DEPENDS gmp
URL http://www.mpfr.org/mpfr-current/mpfr-3.1.5.tar.bz2
URL_HASH SHA256=ca498c1c7a74dd37a576f353312d1e68d490978de4395fa28f1cbd46a364e658
BUILD_IN_SOURCE 1
CONFIGURE_COMMAND emconfigure ./configure "CFLAGS=${CFLAGS_EMSCRIPTEN}" --prefix=${mpfr_install_prefix} --with-gmp-include=${gmp_install_prefix}/include --with-gmp-lib=${gmp_install_prefix}/lib
BUILD_COMMAND emmake make -j4
INSTALL_COMMAND make install
)
add_library(lean_external_deps INTERFACE)
target_link_libraries(lean_external_deps INTERFACE ${gmp_install_prefix}/lib/libgmp.so ${mpfr_install_prefix}/lib/libmpfr.so)
include_directories(lean_external_deps INTERFACE ${gmp_install_prefix}/include ${mpfr_install_prefix}/include)
add_dependencies(lean_external_deps gmp mpfr)
target_link_libraries(lean_external_deps INTERFACE ${gmp_install_prefix}/lib/libgmp.so)
include_directories(lean_external_deps INTERFACE ${gmp_install_prefix}/include)
add_dependencies(lean_external_deps gmp)
set(EXTRA_LIBS lean_external_deps)
else()
# MPFR
find_package(MPFR 3.1.0 REQUIRED)
include_directories(${MPFR_INCLUDES})
set(EXTRA_LIBS ${EXTRA_LIBS} ${MPFR_LIBRARIES})
# GMP
find_package(GMP 5.0.5 REQUIRED)
include_directories(${GMP_INCLUDE_DIR})
@ -323,8 +306,6 @@ add_subdirectory(util/numerics)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:numerics>)
add_subdirectory(util/sexpr)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:sexpr>)
add_subdirectory(util/interval)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:interval>)
add_subdirectory(util/lp)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:lp>)
add_subdirectory(kernel)
@ -394,7 +375,6 @@ endfunction()
add_subdirectory(tests/util)
add_subdirectory(tests/util/numerics)
add_subdirectory(tests/util/interval)
add_subdirectory(tests/kernel)
add_subdirectory(tests/library)
add_subdirectory(tests/frontends/lean)
@ -488,7 +468,7 @@ endif()
if(STATIC)
SET(CPACK_DEBIAN_PACKAGE_DEPENDS "")
else()
SET(CPACK_DEBIAN_PACKAGE_DEPENDS "libstdc++-4.8-dev,libgmp-dev,libmpfr-dev")
SET(CPACK_DEBIAN_PACKAGE_DEPENDS "libstdc++-4.8-dev,libgmp-dev")
endif()
SET(CPACK_DEBIAN_PACKAGE_DESCRIPTION "Lean Theorem Prover")
SET(CPACK_DEBIAN_PACKAGE_SECTION "devel")

3
src/tests/util/numerics/CMakeLists.txt
View file

@ -4,9 +4,6 @@ add_exec_test(mpq "mpq")
add_executable(mpbq mpbq.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
target_link_libraries(mpbq ${EXTRA_LIBS})
add_exec_test(mpbq "mpbq")
add_executable(mpfp mpfp.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
target_link_libraries(mpfp ${EXTRA_LIBS})
add_exec_test(mpfp "mpfp")
add_executable(mpz mpz.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
target_link_libraries(mpz ${EXTRA_LIBS})
add_exec_test(mpz "mpz")

63
src/tests/util/numerics/mpfp.cpp
View file

@ -1,63 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Soonho Kong
*/
#include <iostream>
#include "util/test.h"
#include "util/numerics/mpfp.h"
using namespace lean;
static void tst1() {
mpfp a(3.141592, 64);
std::cout << "a = |" << a << "|" << std::endl;
std::cout << "exp(a, UP ) = |" << exp(a, MPFR_RNDU) << "|" << std::endl;
std::cout << "exp(a, NEAR) = |" << exp(a, MPFR_RNDN) << "|" << std::endl;
std::cout << "exp(a, DOWN) = |" << exp(a, MPFR_RNDD) << "|" << std::endl;
mpfp b = mpfp(5.141592, 128);
std::cout << "b = |" << b << "|" << std::endl;
std::cout << "exp(b, UP ) = |" << exp(b, MPFR_RNDU) << "|" << std::endl;
std::cout << "exp(b, NEBR) = |" << exp(b, MPFR_RNDN) << "|" << std::endl;
std::cout << "exp(b, DOWN) = |" << exp(b, MPFR_RNDD) << "|" << std::endl;
mpfp c = mpfp(6.141592, 256);
std::cout << "c = |" << c << "|" << std::endl;
std::cout << "exp(c, UP ) = |" << exp(c, MPFR_RNDU) << "|" << std::endl;
std::cout << "exp(c, NEAR) = |" << exp(c, MPFR_RNDN) << "|" << std::endl;
std::cout << "exp(c, DOWN) = |" << exp(c, MPFR_RNDD) << "|" << std::endl;
std::cout << "a = |" << a << "|" << std::endl;
std::cout << "exp(a, UP ) = |" << exp(a, MPFR_RNDU) << "|" << std::endl;
std::cout << "exp(a, NEAR) = |" << exp(a, MPFR_RNDN) << "|" << std::endl;
std::cout << "exp(a, DOWN) = |" << exp(a, MPFR_RNDD) << "|" << std::endl;
std::cout << "b = |" << b << "|" << std::endl;
std::cout << "exp(b, UP ) = |" << exp(b, MPFR_RNDU) << "|" << std::endl;
std::cout << "exp(b, NEAR) = |" << exp(b, MPFR_RNDN) << "|" << std::endl;
std::cout << "exp(b, DOWN) = |" << exp(b, MPFR_RNDD) << "|" << std::endl;
mpfp d = mpfp(6.141592, 512);
std::cout << "d = |" << d << "|" << std::endl;
std::cout << "exp(d, UP ) = |" << exp(d, MPFR_RNDU) << "|" << std::endl;
std::cout << "exp(d, NEAR) = |" << exp(d, MPFR_RNDN) << "|" << std::endl;
std::cout << "exp(d, DOWN) = |" << exp(d, MPFR_RNDD) << "|" << std::endl;
}
static void tst2() {
mpfp a(10.0, 64);
mpfp b(10.0, 128);
lean_assert(a == b);
for (unsigned i = 16; i < 256; i++) {
for (unsigned j = 16; j < 256; j++) {
lean_assert_eq(mpfp(0.0, i), mpfp(0.0, j));
}
}
}
int main() {
tst1();
tst2();
return has_violations() ? 1 : 0;
}

4
src/tests/util/numerics/numeric_traits.cpp
View file

@ -12,7 +12,6 @@ Author: Leonardo de Moura
#include "util/numerics/mpbq.h"
#include "util/numerics/double.h"
#include "util/numerics/float.h"
#include "util/numerics/mpfp.h"
using namespace lean;
template<typename T>
@ -31,9 +30,6 @@ static void tst1() {
tst_num(mpq(0));
tst_num(mpz(3));
tst_num(mpz(0));
tst_num(mpfp(2.0));
tst_num(mpfp(0.0));
tst_num(mpfp(0.0, 512));
tst_num(mpbq(3));
tst_num(1.0);
tst_num(static_cast<float>(1.0));

1
src/util/interval/CMakeLists.txt
View file

@ -1 +0,0 @@
add_library(interval OBJECT interval_instances.cpp)

2487
src/util/interval/interval.cpp
View file

File diff suppressed because it is too large Load diff

369
src/util/interval/interval.h
View file

@ -1,369 +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
Soonho Kong
*/
#pragma once
#include "util/numerics/numeric_traits.h"
#include "util/numerics/xnumeral.h"
namespace lean {
#define DEP_IN_LOWER1 1
#define DEP_IN_UPPER1 2
#define DEP_IN_LOWER2 4
#define DEP_IN_UPPER2 8
typedef unsigned short bound_deps;
inline bool dep_in_lower1(bound_deps d) { return (d & DEP_IN_LOWER1) != 0; }
inline bool dep_in_lower2(bound_deps d) { return (d & DEP_IN_LOWER2) != 0; }
inline bool dep_in_upper1(bound_deps d) { return (d & DEP_IN_UPPER1) != 0; }
inline bool dep_in_upper2(bound_deps d) { return (d & DEP_IN_UPPER2) != 0; }
inline bound_deps dep1_to_dep2(bound_deps d) {
lean_assert(!dep_in_lower2(d) && !dep_in_upper2(d));
bound_deps r = d << 2;
lean_assert(dep_in_lower1(d) == dep_in_lower2(r));
lean_assert(dep_in_upper1(d) == dep_in_upper2(r));
lean_assert(!dep_in_lower1(r) && !dep_in_upper1(r));
return r;
}
/**
\brief Interval dependencies for unary and binary operations on intervals.
It contains the dependencies for the output lower and upper bounds
for the resultant interval.
*/
struct interval_deps {
bound_deps m_lower_deps;
bound_deps m_upper_deps;
};
template<typename T>
class interval {
T m_lower;
T m_upper;
unsigned m_lower_open:1;
unsigned m_upper_open:1;
unsigned m_lower_inf:1;
unsigned m_upper_inf:1;
static interval_deps dummy;
xnumeral_kind lower_kind() const { return m_lower_inf ? XN_MINUS_INFINITY : XN_NUMERAL; }
xnumeral_kind upper_kind() const { return m_upper_inf ? XN_PLUS_INFINITY : XN_NUMERAL; }
void set_closed_endpoints();
static void round_to_plus_inf() { numeric_traits<T>::set_rounding(true); }
static void round_to_minus_inf() { numeric_traits<T>::set_rounding(false); }
static void reset(T & v) { numeric_traits<T>::reset(v); }
static void inv(T & v) { numeric_traits<T>::inv(v); }
static void neg(T & v) { numeric_traits<T>::neg(v); }
static bool is_zero(T const & v) { return numeric_traits<T>::is_zero(v); }
static void power(T & v, unsigned k) { return numeric_traits<T>::power(v, k); }
void _swap(interval & b);
bool _eq(interval const & b) const;
public:
template<typename T2> interval & operator=(T2 const & n) { m_lower = n; m_upper = n; set_closed_endpoints(); return *this; }
interval & operator=(T const & n);
interval & operator=(interval const & n);
interval & operator=(interval && n);
// (-oo, oo)
interval();
// [n, n]
template<typename T2> interval(T2 const & n):m_lower(n), m_upper(n) { set_closed_endpoints();}
// copy constructor
interval(interval const & n);
// move constructor
interval(interval && src);
// [l, u], (l, u], [l, u), (l, u)
template<typename T2> interval(T2 const & l, T2 const & u, bool l_open = false, bool u_open = false):m_lower(l), m_upper(u) {
m_lower_open = l_open; m_upper_open = u_open; m_lower_inf = false; m_upper_inf = false;
}
// [l, u], (l, u], [l, u), (l, u)
template<typename T2> interval(bool l_open, T2 const & l, T2 const & u, bool u_open):interval(l, u, l_open, u_open) {}
// (-oo, u], (-oo, u]
template<typename T2> interval(T2 const & u, bool u_open):m_upper(u) {
m_lower_open = true; m_upper_open = u_open; m_lower_inf = true; m_upper_inf = false;
}
// [u, +oo), (u, +oo)
template<typename T2> interval(bool l_open, T2 const & l):m_lower(l) {
m_lower_open = l_open; m_upper_open = true; m_lower_inf = false; m_upper_inf = true;
}
~interval();
friend void swap(interval & a, interval & b) { a._swap(b); }
T const & lower() const { return m_lower; }
T const & upper() const { return m_upper; }
bool is_lower_neg() const { return ::lean::is_neg(m_lower, lower_kind()); }
bool is_lower_pos() const { return ::lean::is_pos(m_lower, lower_kind()); }
bool is_lower_zero() const { return ::lean::is_zero(m_lower, lower_kind()); }
bool is_upper_neg() const { return ::lean::is_neg(m_upper, upper_kind()); }
bool is_upper_pos() const { return ::lean::is_pos(m_upper, upper_kind()); }
bool is_upper_zero() const { return ::lean::is_zero(m_upper, upper_kind()); }
bool is_lower_open() const { return m_lower_open; }
bool is_upper_open() const { return m_upper_open; }
bool is_lower_inf() const { return m_lower_inf; }
bool is_upper_inf() const { return m_upper_inf; }
// all values in the interval are non-negative
bool is_P() const { return is_lower_pos() || is_lower_zero(); }
// interval of the form [0, ...
bool is_P0() const { return is_lower_zero() && !is_lower_open(); }
// all values in the interval are positive
bool is_P1() const { return is_lower_pos() || (is_lower_zero() && is_lower_open()); }
// all values in the interval are non-positive
bool is_N() const { return is_upper_neg() || is_upper_zero(); }
// interval of the form ..., 0]
bool is_N0() const { return is_upper_zero() && !is_upper_open(); }
// all values in the interval are negative
bool is_N1() const { return is_upper_neg() || (is_upper_zero() && is_upper_open()); }
// lower is negative and upper is positive
bool is_M() const { return is_lower_neg() && is_upper_pos(); }
// [0, 0]
bool is_zero() const { return is_lower_zero() && is_upper_zero(); }
// Interval contains the value zero
bool contains_zero() const;
/**
\brief Return true iff this contains b.
That is, every value in b is a value of this.
*/
bool contains(interval const & b) const;
bool is_empty() const;
void set_empty();
/**
\brief Return true is the interval contains only one value.
*/
bool is_singleton() const;
/**
\brief Return true is the interval contains only v.
*/
template<typename T2> bool is_singleton(T2 const & v) const { return is_singleton() && m_lower == v; }
friend bool operator==(interval const & a, interval const & b) { return a._eq(b); }
friend bool operator!=(interval const & a, interval const & b) { return !operator==(a, b); }
/**
\brief Return true if all values in this are less than all values in 'b'.
*/
bool before(interval const & b) const;
template<typename T2> void set_lower(T2 const & n) { m_lower = n; }
template<typename T2> void set_upper(T2 const & n) { m_upper = n; }
void set_is_lower_open(bool v) { m_lower_open = v; }
void set_is_upper_open(bool v) { m_upper_open = v; }
void set_is_lower_inf(bool v) { m_lower_inf = v; }
void set_is_upper_inf(bool v) { m_upper_inf = v; }
template<bool compute_intv = true, bool compute_deps = false> void neg(interval_deps & deps = dummy);
void neg_jst(interval_deps & deps) { neg<false, true>(deps); }
friend interval neg(interval o) { o.neg(); return o; }
friend interval neg_jst(interval o, interval_deps & deps) { o.neg(deps); return o; }
interval & operator+=(interval const & o);
interval & operator-=(interval const & o);
interval & operator*=(interval const & o);
interval & operator/=(interval const & o);
template<bool compute_intv = true, bool compute_deps = false>
interval & add(interval const & o, interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false>
interval & sub(interval const & o, interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false>
interval & mul(interval const & o, interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false>
interval & div(interval const & o, interval_deps & deps = dummy);
void add_jst (interval const & o, interval_deps & deps);
void sub_jst (interval const & o, interval_deps & deps);
void mul_jst (interval const & o, interval_deps & deps);
void div_jst (interval const & o, interval_deps & deps);
interval & operator+=(T const & o);
interval & operator-=(T const & o);
interval & operator*=(T const & o);
interval & operator/=(T const & o);
template<bool compute_intv = true, bool compute_deps = false> void inv(interval_deps & deps = dummy);
void inv_jst (interval_deps & deps) { inv<false, true>(deps); }
friend interval inv(interval o) { o.inv(); return o; }
friend interval inv_jst(interval o, interval_deps & deps) { o.inv(deps); return o; }
void fmod(interval y);
void fmod(T y);
friend interval fmod(interval o, interval y) { o.fmod(y); return o; }
friend interval fmod(interval o, T y) { o.fmod(y); return o; }
template<bool compute_intv = true, bool compute_deps = false>
void power(unsigned n, interval_deps & deps = dummy);
void power_jst(unsigned n, interval_deps & deps);
friend interval power(interval o, unsigned k) { o.power(k); return o; }
template<bool compute_intv = true, bool compute_deps = false> void exp(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void exp2(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void exp10(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void log(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void log2(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void log10(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void sin(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void cos(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void tan(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void csc(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void sec(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void cot(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void asin(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void acos(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void atan(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void sinh(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void cosh(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void tanh(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void asinh(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void acosh(interval_deps & deps = dummy);
template<bool compute_intv = true, bool compute_deps = false> void atanh(interval_deps & deps = dummy);
void exp_jst (interval_deps & deps);
void exp2_jst (interval_deps & deps);
void exp10_jst(interval_deps & deps);
void log_jst (interval_deps & deps);
void log2_jst (interval_deps & deps);
void log10_jst(interval_deps & deps);
void sin_jst(interval_deps & deps);
void cos_jst(interval_deps & deps);
void tan_jst(interval_deps & deps);
void csc_jst(interval_deps & deps);
void sec_jst(interval_deps & deps);
void cot_jst(interval_deps & deps);
void asin_jst(interval_deps & deps);
void acos_jst(interval_deps & deps);
void atan_jst(interval_deps & deps);
void sinh_jst(interval_deps & deps);
void cosh_jst(interval_deps & deps);
void tanh_jst(interval_deps & deps);
void asinh_jst(interval_deps & deps);
void acosh_jst(interval_deps & deps);
void atanh_jst(interval_deps & deps);
friend interval exp (interval o) { o.exp(); return o; }
friend interval exp (interval o, interval_deps & deps) { o.exp(deps); return o; }
friend interval exp_jst(interval o, interval_deps & deps) { o.exp_jst(deps); return o; }
friend interval exp2 (interval o) { o.exp2(); return o; }
friend interval exp2 (interval o, interval_deps & deps) { o.exp2(deps); return o; }
friend interval exp2_jst(interval o, interval_deps & deps) { o.exp2_jst(deps); return o; }
friend interval exp10(interval o) { o.exp10(); return o; }
friend interval exp10(interval o, interval_deps & deps) { o.exp10(deps); return o; }
friend interval exp10_jst(interval o, interval_deps & deps) { o.exp10(deps); return o; }
friend interval log (interval o) { o.log(); return o; }
friend interval log (interval o, interval_deps & deps) { o.log(deps); return o; }
friend interval log_jst(interval o, interval_deps & deps) { o.log_jst(deps); return o; }
friend interval log2 (interval o) { o.log2(); return o; }
friend interval log2 (interval o, interval_deps & deps) { o.log2(deps); return o; }
friend interval log2_jst(interval o, interval_deps & deps) { o.log2_jst(deps); return o; }
friend interval log10(interval o) { o.log10(); return o; }
friend interval log10(interval o, interval_deps & deps) { o.log10(deps); return o; }
friend interval log10_jst(interval o, interval_deps & deps) { o.log10_jst(deps); return o; }
friend interval sin (interval o) { o.sin(); return o; }
friend interval sin (interval o, interval_deps & deps) { o.sin(deps); return o; }
friend interval sin_jst(interval o, interval_deps & deps) { o.sin_jst(deps); return o; }
friend interval cos (interval o) { o.cos(); return o; }
friend interval cos (interval o, interval_deps & deps) { o.cos(deps); return o; }
friend interval cos_jst(interval o, interval_deps & deps) { o.cos_jst(deps); return o; }
friend interval tan (interval o) { o.tan(); return o; }
friend interval tan (interval o, interval_deps & deps) { o.tan(deps); return o; }
friend interval tan_jst(interval o, interval_deps & deps) { o.tan_jst(deps); return o; }
friend interval csc (interval o) { o.csc(); return o; }
friend interval csc (interval o, interval_deps & deps) { o.csc(deps); return o; }
friend interval csc_jst(interval o, interval_deps & deps) { o.csc_jst(deps); return o; }
friend interval sec (interval o) { o.sec(); return o; }
friend interval sec (interval o, interval_deps & deps) { o.sec(deps); return o; }
friend interval sec_jst(interval o, interval_deps & deps) { o.sec_jst(deps); return o; }
friend interval cot (interval o) { o.cot(); return o; }
friend interval cot (interval o, interval_deps & deps) { o.cot(deps); return o; }
friend interval cot_jst(interval o, interval_deps & deps) { o.cot_jst(deps); return o; }
friend interval asin (interval o) { o.asin(); return o; }
friend interval asin (interval o, interval_deps & deps) { o.asin(deps); return o; }
friend interval asin_jst(interval o, interval_deps & deps) { o.asin_jst(deps); return o; }
friend interval acos (interval o) { o.acos(); return o; }
friend interval acos (interval o, interval_deps & deps) { o.acos(deps); return o; }
friend interval acos_jst(interval o, interval_deps & deps) { o.acos_jst(deps); return o; }
friend interval atan (interval o) { o.atan(); return o; }
friend interval atan (interval o, interval_deps & deps) { o.atan(deps); return o; }
friend interval atan_jst(interval o, interval_deps & deps) { o.atan_jst(deps); return o; }
friend interval sinh (interval o) { o.sinh(); return o; }
friend interval sinh (interval o, interval_deps & deps) { o.sinh(deps); return o; }
friend interval sinh_jst(interval o, interval_deps & deps) { o.sinh_jst(deps); return o; }
friend interval cosh (interval o) { o.cosh(); return o; }
friend interval cosh (interval o, interval_deps & deps) { o.cosh(deps); return o; }
friend interval cosh_jst(interval o, interval_deps & deps) { o.cosh_jst(deps); return o; }
friend interval tanh (interval o) { o.tanh(); return o; }
friend interval tanh (interval o, interval_deps & deps) { o.tanh(deps); return o; }
friend interval tanh_jst(interval o, interval_deps & deps) { o.tanh_jst(deps); return o; }
friend interval asinh(interval o) { o.asinh(); return o; }
friend interval asinh(interval o, interval_deps & deps) { o.asinh(deps); return o; }
friend interval asinh_jst(interval o, interval_deps & deps) { o.asinh_jst(deps); return o; }
friend interval acosh(interval o) { o.acosh(); return o; }
friend interval acosh(interval o, interval_deps & deps) { o.acosh(deps); return o; }
friend interval acosh_jst(interval o, interval_deps & deps) { o.acosh_jst(deps); return o; }
friend interval atanh(interval o) { o.atanh(); return o; }
friend interval atanh(interval o, interval_deps & deps) { o.atanh(deps); return o; }
friend interval atanh_jst(interval o, interval_deps & deps) { o.atanh_jst(deps); return o; }
friend interval operator+(interval a, interval const & b) { return a += b; }
friend interval operator-(interval a, interval const & b) { return a -= b; }
friend interval operator*(interval a, interval const & b) { return a *= b; }
friend interval operator/(interval a, interval const & b) { return a /= b; }
friend interval operator+(interval a, T const & b) { return a += b; }
friend interval operator-(interval a, T const & b) { return a -= b; }
friend interval operator*(interval a, T const & b) { return a *= b; }
friend interval operator/(interval a, T const & b) { return a /= b; }
friend interval operator+(T const & a, interval b) { return b += a; }
friend interval operator-(T const & a, interval b) { b.neg(); return b += a; }
friend interval operator*(T const & a, interval b) { return b *= a; }
friend interval operator/(T const & a, interval b) { b.inv(); return b *= a; }
bool check_invariant() const;
void display(std::ostream & out) const;
friend std::ostream & operator<<(std::ostream & out, interval const & n) {
n.display(out);
return out;
}
};
}

101
src/util/interval/interval_instances.cpp
View file

@ -1,101 +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
*/
#include "util/thread.h"
#include "util/numerics/mpq.h"
#include "util/numerics/double.h"
#include "util/numerics/float.h"
#include "util/numerics/mpfp.h"
#include "util/interval/interval.cpp"
namespace lean {
template class interval<mpq>;
template void interval<mpq>::neg<true, false>(interval_deps &);
template void interval<mpq>::neg<false, true>(interval_deps &);
template void interval<mpq>::inv<true, false>(interval_deps &);
template void interval<mpq>::power<true, false>(unsigned, interval_deps &);
template class interval<double>;
template void interval<double>::neg<true, false>(interval_deps &);
template void interval<double>::inv<true, false>(interval_deps &);
template void interval<double>::power<true, false>(unsigned, interval_deps &);
template void interval<double>::exp<true, false>(interval_deps &);
template void interval<double>::exp2<true, false>(interval_deps &);
template void interval<double>::exp10<true, false>(interval_deps &);
template void interval<double>::log<true, false>(interval_deps &);
template void interval<double>::log2<true, false>(interval_deps &);
template void interval<double>::log10<true, false>(interval_deps &);
template void interval<double>::sin<true, false>(interval_deps &);
template void interval<double>::cos<true, false>(interval_deps &);
template void interval<double>::tan<true, false>(interval_deps &);
template void interval<double>::asin<true, false>(interval_deps &);
template void interval<double>::acos<true, false>(interval_deps &);
template void interval<double>::atan<true, false>(interval_deps &);
template void interval<double>::sinh<true, false>(interval_deps &);
template void interval<double>::cosh<true, false>(interval_deps &);
template void interval<double>::tanh<true, false>(interval_deps &);
template void interval<double>::csc<true, false>(interval_deps &);
template void interval<double>::sec<true, false>(interval_deps &);
template void interval<double>::cot<true, false>(interval_deps &);
template void interval<double>::asinh<true, false>(interval_deps &);
template void interval<double>::acosh<true, false>(interval_deps &);
template void interval<double>::atanh<true, false>(interval_deps &);
template class interval<float>;
template void interval<float>::neg<true, false>(interval_deps &);
template void interval<float>::inv<true, false>(interval_deps &);
template void interval<float>::power<true, false>(unsigned, interval_deps &);
template void interval<float>::exp<true, false>(interval_deps &);
template void interval<float>::exp2<true, false>(interval_deps &);
template void interval<float>::exp10<true, false>(interval_deps &);
template void interval<float>::log<true, false>(interval_deps &);
template void interval<float>::log2<true, false>(interval_deps &);
template void interval<float>::log10<true, false>(interval_deps &);
template void interval<float>::sin<true, false>(interval_deps &);
template void interval<float>::cos<true, false>(interval_deps &);
template void interval<float>::tan<true, false>(interval_deps &);
template void interval<float>::asin<true, false>(interval_deps &);
template void interval<float>::acos<true, false>(interval_deps &);
template void interval<float>::atan<true, false>(interval_deps &);
template void interval<float>::sinh<true, false>(interval_deps &);
template void interval<float>::cosh<true, false>(interval_deps &);
template void interval<float>::tanh<true, false>(interval_deps &);
template void interval<float>::csc<true, false>(interval_deps &);
template void interval<float>::sec<true, false>(interval_deps &);
template void interval<float>::cot<true, false>(interval_deps &);
template void interval<float>::asinh<true, false>(interval_deps &);
template void interval<float>::acosh<true, false>(interval_deps &);
template void interval<float>::atanh<true, false>(interval_deps &);
template class interval<mpfp>;
template void interval<mpfp>::neg<true, false>(interval_deps &);
template void interval<mpfp>::inv<true, false>(interval_deps &);
template void interval<mpfp>::power<true, false>(unsigned, interval_deps &);
template void interval<mpfp>::exp<true, false>(interval_deps &);
template void interval<mpfp>::exp2<true, false>(interval_deps &);
template void interval<mpfp>::exp10<true, false>(interval_deps &);
template void interval<mpfp>::log<true, false>(interval_deps &);
template void interval<mpfp>::log2<true, false>(interval_deps &);
template void interval<mpfp>::log10<true, false>(interval_deps &);
template void interval<mpfp>::sin<true, false>(interval_deps &);
template void interval<mpfp>::cos<true, false>(interval_deps &);
template void interval<mpfp>::tan<true, false>(interval_deps &);
template void interval<mpfp>::asin<true, false>(interval_deps &);
template void interval<mpfp>::acos<true, false>(interval_deps &);
template void interval<mpfp>::atan<true, false>(interval_deps &);
template void interval<mpfp>::sinh<true, false>(interval_deps &);
template void interval<mpfp>::cosh<true, false>(interval_deps &);
template void interval<mpfp>::tanh<true, false>(interval_deps &);
template void interval<mpfp>::csc<true, false>(interval_deps &);
template void interval<mpfp>::sec<true, false>(interval_deps &);
template void interval<mpfp>::cot<true, false>(interval_deps &);
template void interval<mpfp>::asinh<true, false>(interval_deps &);
template void interval<mpfp>::acosh<true, false>(interval_deps &);
template void interval<mpfp>::atanh<true, false>(interval_deps &);
}
void print(lean::interval<lean::mpq> const & i) { std::cout << i << std::endl; }
void print(lean::interval<double> const & i) { std::cout << i << std::endl; }

3
src/util/numerics/CMakeLists.txt
View file

@ -1,2 +1 @@
add_library(numerics OBJECT init_module.cpp mpz.cpp mpq.cpp mpbq.cpp mpfp.cpp
float.cpp double.cpp numeric_traits.cpp primes.cpp zpz.cpp)
add_library(numerics OBJECT init_module.cpp mpz.cpp mpq.cpp mpbq.cpp float.cpp double.cpp numeric_traits.cpp primes.cpp zpz.cpp)

13
src/util/numerics/double.cpp
View file

@ -10,15 +10,6 @@ Author: Soonho Kong
#include "util/numerics/double.h"
namespace lean {
MK_THREAD_LOCAL_GET_DEF(mpfr_rnd_t, get_g_rnd);
void set_double_rnd(bool plus_inf) {
get_g_rnd() = plus_inf ? MPFR_RNDU : MPFR_RNDD;
}
mpfr_rnd_t get_double_rnd() {
return get_g_rnd();
}
void double_power(double & v, unsigned k) { v = std::pow(v, k); }
void double_abs(double & v) { v = std::abs(v); }
void double_ceil(double & v) { v = std::ceil(v); }
@ -26,4 +17,8 @@ void double_floor(double & v) { v = std::floor(v); }
double numeric_traits<double>::g_zero = 0.0;
double numeric_traits<double>::g_one = 1.0;
double numeric_traits<double>::log(double d) {
return std::log(d);
}
};

39
src/util/numerics/double.h
View file

@ -6,11 +6,9 @@ Author: Soonho Kong
*/
#pragma once
#include <cstddef>
#include <mpfr.h>
#include "util/numerics/mpfp.h"
#include "util/numerics/numeric_traits.h"
namespace lean {
/**
\brief Template specializations define traits for native and lean
numeric types.
@ -20,16 +18,6 @@ void double_abs(double & v);
void double_ceil(double & v);
void double_floor(double & v);
// Macro to implement transcendental functions using MPFR
#define LEAN_TRANS_DOUBLE_FUNC(f, v, rnd) \
mpfp t(53); \
t = v; \
t.f(rnd); \
v = t.get_double(rnd);
void set_double_rnd(bool plus_inf);
mpfr_rnd_t get_double_rnd();
template<>
class numeric_traits<double> {
public:
@ -37,8 +25,6 @@ public:
static bool is_zero(double v) { return v == 0.0; }
static bool is_pos(double v) { return v > 0.0; }
static bool is_neg(double v) { return v < 0.0; }
static mpfr_rnd_t rnd() { return get_double_rnd(); }
static void set_rounding(bool plus_inf) { set_double_rnd(plus_inf); }
static void neg(double & v) { v = -v; }
static void inv(double & v) { v = 1.0/v; }
static void reset(double & v) { v = 0.0; }
@ -73,27 +59,6 @@ public:
static inline double pi_twice() { return pi_n * 2; }
static inline double pi_twice_upper() { return pi_u * 2; }
// Transcendental functions using MPFR
static void exp(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp, v, rnd()); }
static void exp2(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp2, v, rnd()); }
static void exp10(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp10, v, rnd()); }
static void log(double & v) { LEAN_TRANS_DOUBLE_FUNC(log, v, rnd()); }
static void log2(double & v) { LEAN_TRANS_DOUBLE_FUNC(log2, v, rnd()); }
static void log10(double & v) { LEAN_TRANS_DOUBLE_FUNC(log10, v, rnd()); }
static void sin(double & v) { LEAN_TRANS_DOUBLE_FUNC(sin, v, rnd()); }
static void cos(double & v) { LEAN_TRANS_DOUBLE_FUNC(cos, v, rnd()); }
static void tan(double & v) { LEAN_TRANS_DOUBLE_FUNC(tan, v, rnd()); }
static void sec(double & v) { LEAN_TRANS_DOUBLE_FUNC(sec, v, rnd()); }
static void csc(double & v) { LEAN_TRANS_DOUBLE_FUNC(csc, v, rnd()); }
static void cot(double & v) { LEAN_TRANS_DOUBLE_FUNC(cot, v, rnd()); }
static void asin(double & v) { LEAN_TRANS_DOUBLE_FUNC(asin, v, rnd()); }
static void acos(double & v) { LEAN_TRANS_DOUBLE_FUNC(acos, v, rnd()); }
static void atan(double & v) { LEAN_TRANS_DOUBLE_FUNC(atan, v, rnd()); }
static void sinh(double & v) { LEAN_TRANS_DOUBLE_FUNC(sinh, v, rnd()); }
static void cosh(double & v) { LEAN_TRANS_DOUBLE_FUNC(cosh, v, rnd()); }
static void tanh(double & v) { LEAN_TRANS_DOUBLE_FUNC(tanh, v, rnd()); }
static void asinh(double & v) { LEAN_TRANS_DOUBLE_FUNC(asinh, v, rnd()); }
static void acosh(double & v) { LEAN_TRANS_DOUBLE_FUNC(acosh, v, rnd()); }
static void atanh(double & v) { LEAN_TRANS_DOUBLE_FUNC(atanh, v, rnd()); }
static double log(double d);
};
}

9
src/util/numerics/float.cpp
View file

@ -10,15 +10,6 @@ Author: Soonho Kong
#include "util/numerics/float.h"
namespace lean {
MK_THREAD_LOCAL_GET_DEF(mpfr_rnd_t, get_g_rnd);
void set_float_rnd(bool plus_inf) {
get_g_rnd() = plus_inf ? MPFR_RNDU : MPFR_RNDD;
}
mpfr_rnd_t get_float_rnd() {
return get_g_rnd();
}
void float_power(float & v, unsigned k) { v = std::pow(v, k); }
void float_abs(float & v) { v = std::abs(v); }
void float_ceil(float & v) { v = std::ceil(v); }

39
src/util/numerics/float.h
View file

@ -6,11 +6,9 @@ Author: Soonho Kong
*/
#pragma once
#include <cstddef>
#include <mpfr.h>
#include "util/numerics/mpfp.h"
#include "util/numerics/numeric_traits.h"
namespace lean {
/**
\brief Template specializations define traits for native and lean
numeric types.
@ -20,16 +18,6 @@ void float_abs(float & v);
void float_ceil(float & v);
void float_floor(float & v);
// Macro to implement transcendental functions using MPFR
#define LEAN_TRANS_FLOAT_FUNC(f, v, rnd) \
mpfp t(24); \
t = v; \
t.f(rnd); \
v = t.get_float(rnd);
void set_float_rnd(bool plus_inf);
mpfr_rnd_t get_float_rnd();
template<>
class numeric_traits<float> {
public:
@ -37,8 +25,6 @@ public:
static bool is_zero(float v) { return v == 0.0; }
static bool is_pos(float v) { return v > 0.0; }
static bool is_neg(float v) { return v < 0.0; }
static mpfr_rnd_t rnd() { return get_float_rnd(); }
static void set_rounding(bool plus_inf) { set_float_rnd(plus_inf); }
static void neg(float & v) { v = -v; }
static void inv(float & v) { v = 1.0/v; }
static void reset(float & v) { v = 0.0; }
@ -71,28 +57,5 @@ public:
static inline float pi_twice_lower() { return pi_l * 2; }
static inline float pi_twice() { return pi_n * 2; }
static inline float pi_twice_upper() { return pi_u * 2; }
// Transcendental functions using MPFR
static void exp(float & v) { LEAN_TRANS_FLOAT_FUNC(exp, v, rnd()); }
static void exp2(float & v) { LEAN_TRANS_FLOAT_FUNC(exp2, v, rnd()); }
static void exp10(float & v) { LEAN_TRANS_FLOAT_FUNC(exp10, v, rnd()); }
static void log(float & v) { LEAN_TRANS_FLOAT_FUNC(log, v, rnd()); }
static void log2(float & v) { LEAN_TRANS_FLOAT_FUNC(log2, v, rnd()); }
static void log10(float & v) { LEAN_TRANS_FLOAT_FUNC(log10, v, rnd()); }
static void sin(float & v) { LEAN_TRANS_FLOAT_FUNC(sin, v, rnd()); }
static void cos(float & v) { LEAN_TRANS_FLOAT_FUNC(cos, v, rnd()); }
static void tan(float & v) { LEAN_TRANS_FLOAT_FUNC(tan, v, rnd()); }
static void sec(float & v) { LEAN_TRANS_FLOAT_FUNC(sec, v, rnd()); }
static void csc(float & v) { LEAN_TRANS_FLOAT_FUNC(csc, v, rnd()); }
static void cot(float & v) { LEAN_TRANS_FLOAT_FUNC(cot, v, rnd()); }
static void asin(float & v) { LEAN_TRANS_FLOAT_FUNC(asin, v, rnd()); }
static void acos(float & v) { LEAN_TRANS_FLOAT_FUNC(acos, v, rnd()); }
static void atan(float & v) { LEAN_TRANS_FLOAT_FUNC(atan, v, rnd()); }
static void sinh(float & v) { LEAN_TRANS_FLOAT_FUNC(sinh, v, rnd()); }
static void cosh(float & v) { LEAN_TRANS_FLOAT_FUNC(cosh, v, rnd()); }
static void tanh(float & v) { LEAN_TRANS_FLOAT_FUNC(tanh, v, rnd()); }
static void asinh(float & v) { LEAN_TRANS_FLOAT_FUNC(asinh, v, rnd()); }
static void acosh(float & v) { LEAN_TRANS_FLOAT_FUNC(acosh, v, rnd()); }
static void atanh(float & v) { LEAN_TRANS_FLOAT_FUNC(atanh, v, rnd()); }
};
}

3
src/util/numerics/init_module.cpp
View file

@ -10,7 +10,6 @@ Author: Leonardo de Moura
#include "util/numerics/mpz.h"
#include "util/numerics/mpq.h"
#include "util/numerics/mpbq.h"
#include "util/numerics/mpfp.h"
#include "util/numerics/zpz.h"
#include "util/numerics/primes.h"
@ -19,7 +18,6 @@ void initialize_numerics_module() {
initialize_mpz();
initialize_mpq();
initialize_mpbq();
initialize_mpfp();
initialize_zpz();
initialize_primes();
}
@ -27,7 +25,6 @@ void initialize_numerics_module() {
void finalize_numerics_module() {
finalize_primes();
finalize_zpz();
finalize_mpfp();
finalize_mpbq();
finalize_mpq();
finalize_mpz();

564
src/util/numerics/mpfp.h
View file

@ -1,564 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Soonho Kong
*/
#pragma once
#include <stdint.h>
#include <cstddef>
#include <mpfr.h>
#include "util/numerics/mpz.h"
#include "util/numerics/mpq.h"
#include "util/numerics/mpbq.h"
namespace lean {
void set_mpfp_rnd(bool plus_inf);
mpfr_rnd_t get_mpfp_rnd();
/**
\brief Wrapper for MPFR
*/
class mpfp {
friend numeric_traits<mpfp>;
mpfr_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; }
static mpq_t const & qval(mpq const & v) { return v.m_val; }
static mpq_t & qval(mpq & v) { return v.m_val; }
public:
friend void swap(mpfp & a, mpfp & b) { mpfr_swap(a.m_val, b.m_val); }
// Setter functions
mpfp & set(mpfp const & v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set(m_val, v.m_val, rnd); return *this;
}
mpfp & set(unsigned long int const v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_ui(m_val, v, rnd); return *this;
}
mpfp & set(long int const v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_si(m_val, v, rnd); return *this;
}
mpfp & set(float const v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_flt(m_val, v, rnd); return *this;
}
mpfp & set(double const v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_d(m_val, v, rnd); return *this;
}
mpfp & set(long double const v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_ld(m_val, v, rnd); return *this;
}
mpfp & set(mpz_t const & v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_z(m_val, v, rnd); return *this;
}
mpfp & set(mpq_t const & v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_q(m_val, v, rnd); return *this;
}
mpfp & set(mpf_t const & v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_f(m_val, v, rnd); return *this;
}
mpfp & set(mpz const & v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_z(m_val, v.m_val, rnd); return *this;
}
mpfp & set(mpq const & v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_q(m_val, v.m_val, rnd); return *this;
}
mpfp & set(mpbq const & v, mpfr_rnd_t rnd = MPFR_RNDN) {
mpfr_set_z(m_val, v.m_num.m_val, rnd); // this = m_num
mpfr_div_2ui(m_val, m_val, v.m_k, rnd); // this = m_num / (2^k)
return *this;
}
// Assignment operators
mpfp & operator=(mpfp const & v) { return set(v); }
mpfp & operator=(unsigned long int const v) { return set(v); }
mpfp & operator=(long int const v) { return set(v); }
mpfp & operator=(float const v) { return set(v); }
mpfp & operator=(double const v) { return set(v); }
mpfp & operator=(long double const v) { return set(v); }
mpfp & operator=(mpz_t const & v) { return set(v); }
mpfp & operator=(mpq_t const & v) { return set(v); }
mpfp & operator=(mpf_t const & v) { return set(v); }
mpfp & operator=(mpz const & v) { return set(v); }
mpfp & operator=(mpq const & v) { return set(v); }
mpfp & operator=(mpbq const & v) { return set(v); }
// Basic Constructors
mpfp() { mpfr_init(m_val); } // with default precision
explicit mpfp(int prec) { mpfr_init2(m_val, prec); }
explicit mpfp(unsigned prec) { mpfr_init2(m_val, prec); }
explicit mpfp(mpfr_prec_t prec) { mpfr_init2(m_val, prec); }
// Constructors using the default precision
explicit mpfp(float const v ):mpfp() { set(v); }
explicit mpfp(double const v ):mpfp() { set(v); }
explicit mpfp(long double const v):mpfp() { set(v); }
explicit mpfp(mpz_t const & v ):mpfp() { set(v); }
explicit mpfp(mpq_t const & v ):mpfp() { set(v); }
explicit mpfp(mpf_t const & v ):mpfp() { set(v); }
explicit mpfp(mpz const & v ):mpfp() { set(v); }
explicit mpfp(mpq const & v ):mpfp() { set(v); }
explicit mpfp(mpbq const & v ):mpfp() { set(v); }
mpfp(mpfp const & v ):mpfp(mpfr_get_prec(v.m_val)) { set(v); }
// Constructors using the provided precision
mpfp(float const v , mpfr_prec_t p):mpfp(p) { set(v); }
mpfp(double const v , mpfr_prec_t p):mpfp(p) { set(v); }
mpfp(long double const v, mpfr_prec_t p):mpfp(p) { set(v); }
mpfp(mpz_t const & v , mpfr_prec_t p):mpfp(p) { set(v); }
mpfp(mpq_t const & v , mpfr_prec_t p):mpfp(p) { set(v); }
mpfp(mpf_t const & v , mpfr_prec_t p):mpfp(p) { set(v); }
mpfp(mpz const & v , mpfr_prec_t p):mpfp(p) { set(v); }
mpfp(mpq const & v , mpfr_prec_t p):mpfp(p) { set(v); }
mpfp(mpbq const & v , mpfr_prec_t p):mpfp(p) { set(v); }
mpfp(mpfp const & v , mpfr_prec_t p):mpfp(p) { set(v); }
// Constructors using the provided precision and rounding mode
mpfp(float const v , mpfr_prec_t p, mpfr_rnd_t rnd):mpfp(p) { set(v, rnd); }
mpfp(double const v , mpfr_prec_t p, mpfr_rnd_t rnd):mpfp(p) { set(v, rnd); }
mpfp(long double const v, mpfr_prec_t p, mpfr_rnd_t rnd):mpfp(p) { set(v, rnd); }
mpfp(mpz_t const & v , mpfr_prec_t p, mpfr_rnd_t rnd):mpfp(p) { set(v, rnd); }
mpfp(mpq_t const & v , mpfr_prec_t p, mpfr_rnd_t rnd):mpfp(p) { set(v, rnd); }
mpfp(mpf_t const & v , mpfr_prec_t p, mpfr_rnd_t rnd):mpfp(p) { set(v, rnd); }
mpfp(mpz const & v , mpfr_prec_t p, mpfr_rnd_t rnd):mpfp(p) { set(v, rnd); }
mpfp(mpq const & v , mpfr_prec_t p, mpfr_rnd_t rnd):mpfp(p) { set(v, rnd); }
mpfp(mpbq const & v , mpfr_prec_t p, mpfr_rnd_t rnd):mpfp(p) { set(v, rnd); }
mpfp(mpfp const & v , mpfr_prec_t p, mpfr_rnd_t rnd):mpfp(p) { set(v, rnd); }
mpfp(mpfp && s):mpfp(mpfr_get_prec(s.m_val)) { mpfr_swap(m_val, s.m_val); }
~mpfp() { mpfr_clear(m_val); mpfr_free_cache(); }
unsigned hash() const { return static_cast<unsigned>(mpfr_get_si(m_val, MPFR_RNDN)); }
int sgn() const { return mpfr_sgn(m_val); }
friend int sgn(mpfp 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() { mpfr_neg(m_val, m_val, MPFR_RNDN); }
friend mpfp neg(mpfp a) { a.neg(); return a; }
// Math functions and theirs friend functions
void abs (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_abs(m_val, m_val, rnd); }
void exp (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_exp(m_val, m_val, rnd); }
void exp2 (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_exp2(m_val, m_val, rnd); }
void exp10(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_exp10(m_val, m_val, rnd); }
void log (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_log(m_val, m_val, rnd); }
void log2 (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_log2(m_val, m_val, rnd); }
void log10(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_log10(m_val, m_val, rnd); }
void sin (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sin(m_val, m_val, rnd); }
void cos (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_cos(m_val, m_val, rnd); }
void tan (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_tan(m_val, m_val, rnd); }
void sec (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sec(m_val, m_val, rnd); }
void csc (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_csc(m_val, m_val, rnd); }
void cot (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_cot(m_val, m_val, rnd); }
void asin (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_asin(m_val, m_val, rnd); }
void acos (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_acos(m_val, m_val, rnd); }
void atan (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_atan(m_val, m_val, rnd); }
void sinh (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sinh(m_val, m_val, rnd); }
void cosh (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_cosh(m_val, m_val, rnd); }
void tanh (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_tanh(m_val, m_val, rnd); }
void asinh(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_asinh(m_val, m_val, rnd); }
void acosh(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_acosh(m_val, m_val, rnd); }
void atanh(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_atanh(m_val, m_val, rnd); }
friend mpfp abs (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.abs(rnd); return a; }
friend mpfp exp (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.exp(rnd); return a; }
friend mpfp exp2 (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.exp2(rnd); return a; }
friend mpfp exp10(mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.exp10(rnd); return a; }
friend mpfp log (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.log(rnd); return a; }
friend mpfp log2 (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.log2(rnd); return a; }
friend mpfp log10(mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.log10(rnd); return a; }
friend mpfp sin (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.sin(rnd); return a; }
friend mpfp cos (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.cos(rnd); return a; }
friend mpfp tan (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.tan(rnd); return a; }
friend mpfp sec (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.sec(rnd); return a; }
friend mpfp csc (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.csc(rnd); return a; }
friend mpfp cot (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.cot(rnd); return a; }
friend mpfp asin (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.asin(rnd); return a; }
friend mpfp acos (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.acos(rnd); return a; }
friend mpfp atan (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.atan(rnd); return a; }
friend mpfp sinh (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.sinh(rnd); return a; }
friend mpfp cosh (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.cosh(rnd); return a; }
friend mpfp tanh (mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.tanh(rnd); return a; }
friend mpfp asinh(mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.asinh(rnd); return a; }
friend mpfp acosh(mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.acosh(rnd); return a; }
friend mpfp atanh(mpfp a, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.atanh(rnd); return a; }
void inv() { mpfr_d_div(m_val, 1.0, m_val, MPFR_RNDN); }
friend mpfp inv(mpfp a) { a.inv(); return a; }
double get_double(mpfr_rnd_t rnd = get_mpfp_rnd()) const { return mpfr_get_d(m_val, rnd); }
float get_float (mpfr_rnd_t rnd = get_mpfp_rnd()) const { return mpfr_get_flt(m_val, rnd); }
friend int cmp(mpfp const & a, mpfp const & b ) { return mpfr_cmp(a.m_val, b.m_val); }
friend int cmp(mpfp const & a, unsigned long int const b) { return mpfr_cmp_ui(a.m_val, b); }
friend int cmp(mpfp const & a, long int const b ) { return mpfr_cmp_si(a.m_val, b); }
friend int cmp(mpfp const & a, double const b ) { return mpfr_cmp_d (a.m_val, b); }
friend int cmp(mpfp const & a, long double const b ) { return mpfr_cmp_ld(a.m_val, b); }
friend int cmp(mpfp const & a, mpz_t const & b ) { return mpfr_cmp_z (a.m_val, b); }
friend int cmp(mpfp const & a, mpq_t const & b ) { return mpfr_cmp_q (a.m_val, b); }
friend int cmp(mpfp const & a, mpf_t const & b ) { return mpfr_cmp_f (a.m_val, b); }
friend int cmp(mpfp const & a, mpz const & b ) { return mpfr_cmp_z (a.m_val, zval(b)); }
friend int cmp(mpfp const & a, mpq const & b ) { return mpfr_cmp_q (a.m_val, qval(b)); }
// friend int cmp(mpfp const & a, mpbq const & b) { return mpfr_cmp_(a.m_val, b); }
friend bool operator<(mpfp const & a, mpfp const & b ) { return cmp(a, b) < 0; }
friend bool operator<(mpfp const & a, mpz const & b ) { return cmp(a, b) < 0; }
friend bool operator<(mpfp const & a, unsigned long int const b) { return cmp(a, b) < 0; }
friend bool operator<(mpfp const & a, long int const b ) { return cmp(a, b) < 0; }
friend bool operator<(mpfp const & a, double const b ) { return cmp(a, b) < 0; }
friend bool operator<(mpfp const & a, long double const b ) { return cmp(a, b) < 0; }
friend bool operator<(mpfp const & a, mpz_t const & b ) { return cmp(a, b) < 0; }
friend bool operator<(mpfp const & a, mpq_t const & b ) { return cmp(a, b) < 0; }
friend bool operator<(mpfp const & a, mpf_t const & b ) { return cmp(a, b) < 0; }
friend bool operator<(mpz const & a , mpfp const & b) { return cmp(b, a) > 0; }
friend bool operator<(unsigned long int const a, mpfp const & b) { return cmp(b, a) > 0; }
friend bool operator<(long int const a , mpfp const & b) { return cmp(b, a) > 0; }
friend bool operator<(double const a , mpfp const & b) { return cmp(b, a) > 0; }
friend bool operator<(long double const a , mpfp const & b) { return cmp(b, a) > 0; }
friend bool operator<(mpz_t const & a , mpfp const & b) { return cmp(b, a) > 0; }
friend bool operator<(mpq_t const & a , mpfp const & b) { return cmp(b, a) > 0; }
friend bool operator<(mpf_t const & a , mpfp const & b) { return cmp(b, a) > 0; }
friend bool operator>(mpfp const & a, mpfp const & b ) { return cmp(a, b) > 0; }
friend bool operator>(mpfp const & a, mpz const & b ) { return cmp(a, b) > 0; }
friend bool operator>(mpfp const & a, unsigned long int const b) { return cmp(a, b) > 0; }
friend bool operator>(mpfp const & a, long int const b ) { return cmp(a, b) > 0; }
friend bool operator>(mpfp const & a, double const b ) { return cmp(a, b) > 0; }
friend bool operator>(mpfp const & a, long double const b ) { return cmp(a, b) > 0; }
friend bool operator>(mpfp const & a, mpz_t const & b ) { return cmp(a, b) > 0; }
friend bool operator>(mpfp const & a, mpq_t const & b ) { return cmp(a, b) > 0; }
friend bool operator>(mpfp const & a, mpf_t const & b ) { return cmp(a, b) > 0; }
friend bool operator>(mpz const & a , mpfp const & b) { return cmp(b, a) < 0; }
friend bool operator>(unsigned long int const a, mpfp const & b) { return cmp(b, a) < 0; }
friend bool operator>(long int const a , mpfp const & b) { return cmp(b, a) < 0; }
friend bool operator>(double const a , mpfp const & b) { return cmp(b, a) < 0; }
friend bool operator>(long double const a , mpfp const & b) { return cmp(b, a) < 0; }
friend bool operator>(mpz_t const & a , mpfp const & b) { return cmp(b, a) < 0; }
friend bool operator>(mpq_t const & a , mpfp const & b) { return cmp(b, a) < 0; }
friend bool operator>(mpf_t const & a , mpfp const & b) { return cmp(b, a) < 0; }
friend bool operator<=(mpfp const & a, mpfp const & b ) { return cmp(a, b) <= 0; }
friend bool operator<=(mpfp const & a, mpz const & b ) { return cmp(a, b) <= 0; }
friend bool operator<=(mpfp const & a, unsigned long int const b) { return cmp(a, b) <= 0; }
friend bool operator<=(mpfp const & a, long int const b ) { return cmp(a, b) <= 0; }
friend bool operator<=(mpfp const & a, double const b ) { return cmp(a, b) <= 0; }
friend bool operator<=(mpfp const & a, long double const b ) { return cmp(a, b) <= 0; }
friend bool operator<=(mpfp const & a, mpz_t const & b ) { return cmp(a, b) <= 0; }
friend bool operator<=(mpfp const & a, mpq_t const & b ) { return cmp(a, b) <= 0; }
friend bool operator<=(mpfp const & a, mpf_t const & b ) { return cmp(a, b) <= 0; }
friend bool operator<=(mpz const & a , mpfp const & b) { return cmp(b, a) >= 0; }
friend bool operator<=(unsigned long int const a, mpfp const & b) { return cmp(b, a) >= 0; }
friend bool operator<=(long int const a , mpfp const & b) { return cmp(b, a) >= 0; }
friend bool operator<=(double const a , mpfp const & b) { return cmp(b, a) >= 0; }
friend bool operator<=(long double const a , mpfp const & b) { return cmp(b, a) >= 0; }
friend bool operator<=(mpz_t const & a , mpfp const & b) { return cmp(b, a) >= 0; }
friend bool operator<=(mpq_t const & a , mpfp const & b) { return cmp(b, a) >= 0; }
friend bool operator<=(mpf_t const & a , mpfp const & b) { return cmp(b, a) >= 0; }
friend bool operator>=(mpfp const & a, mpfp const & b ) { return cmp(a, b) >= 0; }
friend bool operator>=(mpfp const & a, mpz const & b ) { return cmp(a, b) >= 0; }
friend bool operator>=(mpfp const & a, unsigned long int const b) { return cmp(a, b) >= 0; }
friend bool operator>=(mpfp const & a, long int const b ) { return cmp(a, b) >= 0; }
friend bool operator>=(mpfp const & a, double const b ) { return cmp(a, b) >= 0; }
friend bool operator>=(mpfp const & a, long double const b ) { return cmp(a, b) >= 0; }
friend bool operator>=(mpfp const & a, mpz_t const & b ) { return cmp(a, b) >= 0; }
friend bool operator>=(mpfp const & a, mpq_t const & b ) { return cmp(a, b) >= 0; }
friend bool operator>=(mpfp const & a, mpf_t const & b ) { return cmp(a, b) >= 0; }
friend bool operator>=(mpz const & a , mpfp const & b) { return cmp(b, a) <= 0; }
friend bool operator>=(unsigned long int const a, mpfp const & b) { return cmp(b, a) <= 0; }
friend bool operator>=(long int const a , mpfp const & b) { return cmp(b, a) <= 0; }
friend bool operator>=(double const a , mpfp const & b) { return cmp(b, a) <= 0; }
friend bool operator>=(long double const a , mpfp const & b) { return cmp(b, a) <= 0; }
friend bool operator>=(mpz_t const & a , mpfp const & b) { return cmp(b, a) <= 0; }
friend bool operator>=(mpq_t const & a , mpfp const & b) { return cmp(b, a) <= 0; }
friend bool operator>=(mpf_t const & a , mpfp const & b) { return cmp(b, a) <= 0; }
friend bool operator==(mpfp const & a, mpfp const & b) { return mpfr_equal_p(a.m_val, b.m_val) != 0; }
friend bool operator==(unsigned long int const a, mpfp const & b) { return cmp(b, a) == 0; }
friend bool operator==(long int const a , mpfp const & b) { return cmp(b, a) == 0; }
friend bool operator==(double const a , mpfp const & b) { return cmp(b, a) == 0; }
friend bool operator==(long double const a , mpfp const & b) { return cmp(b, a) == 0; }
friend bool operator==(mpz_t const & a , mpfp const & b) { return cmp(b, a) == 0; }
friend bool operator==(mpq_t const & a , mpfp const & b) { return cmp(b, a) == 0; }
friend bool operator==(mpf_t const & a , mpfp const & b) { return cmp(b, a) == 0; }
friend bool operator==(mpfp const & a, mpz const & b ) { return cmp(a, b) == 0; }
friend bool operator==(mpfp const & a, unsigned long int const b) { return cmp(a, b) == 0; }
friend bool operator==(mpfp const & a, long int const b ) { return cmp(a, b) == 0; }
friend bool operator==(mpfp const & a, double const b ) { return cmp(a, b) == 0; }
friend bool operator==(mpfp const & a, long double const b ) { return cmp(a, b) == 0; }
friend bool operator==(mpfp const & a, mpz_t const & b ) { return cmp(a, b) == 0; }
friend bool operator==(mpfp const & a, mpq_t const & b ) { return cmp(a, b) == 0; }
friend bool operator==(mpfp const & a, mpf_t const & b ) { return cmp(a, b) == 0; }
friend bool operator!=(mpfp const & a, mpfp const & b) { return !operator==(a, b); }
friend bool operator!=(unsigned long int const a, mpfp const & b) { return cmp(b, a) != 0; }
friend bool operator!=(long int const a , mpfp const & b) { return cmp(b, a) != 0; }
friend bool operator!=(double const a , mpfp const & b) { return cmp(b, a) != 0; }
friend bool operator!=(long double const a , mpfp const & b) { return cmp(b, a) != 0; }
friend bool operator!=(mpz_t const & a , mpfp const & b) { return cmp(b, a) != 0; }
friend bool operator!=(mpq_t const & a , mpfp const & b) { return cmp(b, a) != 0; }
friend bool operator!=(mpf_t const & a , mpfp const & b) { return cmp(b, a) != 0; }
friend bool operator!=(mpfp const & a, mpz const & b ) { return cmp(a, b) != 0; }
friend bool operator!=(mpfp const & a, unsigned long int const b) { return cmp(a, b) != 0; }
friend bool operator!=(mpfp const & a, long int const b ) { return cmp(a, b) != 0; }
friend bool operator!=(mpfp const & a, double const b ) { return cmp(a, b) != 0; }
friend bool operator!=(mpfp const & a, long double const b ) { return cmp(a, b) != 0; }
friend bool operator!=(mpfp const & a, mpz_t const & b ) { return cmp(a, b) != 0; }
friend bool operator!=(mpfp const & a, mpq_t const & b ) { return cmp(a, b) != 0; }
friend bool operator!=(mpfp const & a, mpf_t const & b ) { return cmp(a, b) != 0; }
mpfp & add(mpfp const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_add(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & add(unsigned long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_add_ui(m_val, m_val, o, rnd); return *this; }
mpfp & add(long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_add_si(m_val, m_val, o, rnd); return *this; }
mpfp & add(double const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_add_d(m_val, m_val, o, rnd); return *this; }
mpfp & add(mpz_t const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_add_z(m_val, m_val, o, rnd); return *this; }
mpfp & add(mpq_t const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_add_q(m_val, m_val, o, rnd); return *this; }
mpfp & add(mpz const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_add_z(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & add(mpq const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_add_q(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & operator+=(mpfp const & o) { return add(o); }
mpfp & operator+=(unsigned long int o) { return add(o); }
mpfp & operator+=(long int const o) { return add(o); }
mpfp & operator+=(double const o) { return add(o); }
mpfp & operator+=(mpz_t const & o) { return add(o); }
mpfp & operator+=(mpq_t const & o) { return add(o); }
mpfp & operator+=(mpz const & o) { return add(o); }
mpfp & operator+=(mpq const & o) { return add(o); }
friend mpfp operator+(mpfp a, mpfp const & b) { return a += b; }
friend mpfp operator+(mpfp a, unsigned long const b) { return a += b; }
friend mpfp operator+(mpfp a, long int const b) { return a += b; }
friend mpfp operator+(mpfp a, double const b) { return a += b; }
friend mpfp operator+(mpfp a, mpz_t const & b) { return a += b; }
friend mpfp operator+(mpfp a, mpq_t const & b) { return a += b; }
friend mpfp operator+(mpfp a, mpz const & b) { return a += b; }
friend mpfp operator+(mpfp a, mpq const & b) { return a += b; }
mpfp & sub(mpfp const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sub(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & sub(unsigned long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sub_ui(m_val, m_val, o, rnd); return *this; }
mpfp & sub(long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sub_si(m_val, m_val, o, rnd); return *this; }
mpfp & sub(double const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sub_d(m_val, m_val, o, rnd); return *this; }
mpfp & sub(mpz_t const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sub_z(m_val, m_val, o, rnd); return *this; }
mpfp & sub(mpq_t const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sub_q(m_val, m_val, o, rnd); return *this; }
mpfp & sub(mpz const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sub_z(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & sub(mpq const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_sub_q(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & rsub(unsigned long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_ui_sub(m_val, o, m_val, rnd); return *this; }
mpfp & rsub(long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_si_sub(m_val, o, m_val, rnd); return *this; }
mpfp & rsub(double const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_d_sub(m_val, o, m_val, rnd); return *this; }
mpfp & rsub(mpz_t const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_z_sub(m_val, o, m_val, rnd); return *this; }
mpfp & rsub(mpz const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_z_sub(m_val, o.m_val, m_val, rnd); return *this; }
mpfp & operator-=(mpfp const & o) { return sub(o); }
mpfp & operator-=(unsigned long int o) { return sub(o); }
mpfp & operator-=(long int const o) { return sub(o); }
mpfp & operator-=(double const o) { return sub(o); }
mpfp & operator-=(mpz_t const & o) { return sub(o); }
mpfp & operator-=(mpq_t const & o) { return sub(o); }
mpfp & operator-=(mpz const & o) { return sub(o); }
mpfp & operator-=(mpq const & o) { return sub(o); }
friend mpfp operator-(mpfp a, mpfp const & b) { return a -= b; }
friend mpfp operator-(mpfp a, unsigned long const b) { return a -= b; }
friend mpfp operator-(mpfp a, long int const b) { return a -= b; }
friend mpfp operator-(mpfp a, double const b) { return a -= b; }
friend mpfp operator-(mpfp a, mpz_t const & b) { return a -= b; }
friend mpfp operator-(mpfp a, mpq_t const & b) { return a -= b; }
friend mpfp operator-(mpfp a, mpz const & b) { return a -= b; }
friend mpfp operator-(mpfp a, mpq const & b) { return a -= b; }
friend mpfp operator-(unsigned long const a, mpfp b) { return b.rsub(a); }
friend mpfp operator-(long int const a, mpfp b) { return b.rsub(a); }
friend mpfp operator-(double const a, mpfp b) { return b.rsub(a); }
friend mpfp operator-(mpz_t const & a, mpfp b) { return b.rsub(a); }
// friend mpfp operator-(mpq_t const & a, mpfp b) { return b.rsub(a); }
friend mpfp operator-(mpz const & a, mpfp b) { return b.rsub(a); }
// friend mpfp operator-(mpq const & a, mpfp b) { return b.rsub(a); }
mpfp & mul(mpfp const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_mul(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & mul(unsigned long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_mul_ui(m_val, m_val, o, rnd); return *this; }
mpfp & mul(long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_mul_si(m_val, m_val, o, rnd); return *this; }
mpfp & mul(double const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_mul_d(m_val, m_val, o, rnd); return *this; }
mpfp & mul(mpz_t const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_mul_z(m_val, m_val, o, rnd); return *this; }
mpfp & mul(mpq_t const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_mul_q(m_val, m_val, o, rnd); return *this; }
mpfp & mul(mpz const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_mul_z(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & mul(mpq const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_mul_q(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & operator*=(mpfp const & o) { return mul(o); }
mpfp & operator*=(unsigned long int o) { return mul(o); }
mpfp & operator*=(long int const o) { return mul(o); }
mpfp & operator*=(double const o) { return mul(o); }
mpfp & operator*=(mpz_t const & o) { return mul(o); }
mpfp & operator*=(mpq_t const & o) { return mul(o); }
mpfp & operator*=(mpz const & o) { return mul(o); }
mpfp & operator*=(mpq const & o) { return mul(o); }
friend mpfp operator*(mpfp a, mpfp const & b) { return a *= b; }
friend mpfp operator*(mpfp a, unsigned long const b) { return a *= b; }
friend mpfp operator*(mpfp a, long int const b) { return a *= b; }
friend mpfp operator*(mpfp a, double const b) { return a *= b; }
friend mpfp operator*(mpfp a, mpz_t const & b) { return a *= b; }
friend mpfp operator*(mpfp a, mpq_t const & b) { return a *= b; }
friend mpfp operator*(mpfp a, mpz const & b) { return a *= b; }
friend mpfp operator*(mpfp a, mpq const & b) { return a *= b; }
mpfp & div(mpfp const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_div(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & div(unsigned long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_div_ui(m_val, m_val, o, rnd); return *this; }
mpfp & div(long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_div_si(m_val, m_val, o, rnd); return *this; }
mpfp & div(double const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_div_d(m_val, m_val, o, rnd); return *this; }
mpfp & div(mpz_t const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_div_z(m_val, m_val, o, rnd); return *this; }
mpfp & div(mpq_t const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_div_q(m_val, m_val, o, rnd); return *this; }
mpfp & div(mpz const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_div_z(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & div(mpq const & o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_div_q(m_val, m_val, o.m_val, rnd); return *this; }
mpfp & rdiv(unsigned long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_ui_div(m_val, o, m_val, rnd); return *this; }
mpfp & rdiv(long int const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_si_div(m_val, o, m_val, rnd); return *this; }
mpfp & rdiv(double const o, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_d_div(m_val, o, m_val, rnd); return *this; }
mpfp & operator/=(mpfp const & o) { return div(o); }
mpfp & operator/=(unsigned long int o) { return div(o); }
mpfp & operator/=(long int const o) { return div(o); }
mpfp & operator/=(double const o) { return div(o); }
mpfp & operator/=(mpz_t const & o) { return div(o); }
mpfp & operator/=(mpq_t const & o) { return div(o); }
mpfp & operator/=(mpz const & o) { return div(o); }
mpfp & operator/=(mpq const & o) { return div(o); }
friend mpfp operator/(mpfp a, mpfp const & b) { return a /= b; }
friend mpfp operator/(mpfp a, unsigned long const b) { return a /= b; }
friend mpfp operator/(mpfp a, long int const b) { return a /= b; }
friend mpfp operator/(mpfp a, double const b) { return a /= b; }
friend mpfp operator/(mpfp a, mpz_t const & b) { return a /= b; }
friend mpfp operator/(mpfp a, mpq_t const & b) { return a /= b; }
friend mpfp operator/(mpfp a, mpz const & b) { return a /= b; }
friend mpfp operator/(mpfp a, mpq const & b) { return a /= b; }
friend mpfp operator/(unsigned long const a, mpfp b) { return b.rdiv(a); }
friend mpfp operator/(long int const a, mpfp b) { return b.rdiv(a); }
friend mpfp operator/(double const a, mpfp b) { return b.rdiv(a); }
// friend mpfp operator/(mpz_t const & a, mpfp b) { return a.rdiv(b); }
// friend mpfp operator/(mpq_t const & a, mpfp b) { return a.rdiv(b); }
// friend mpfp operator/(mpz const & a, mpfp b) { return a.rdiv(b); }
// friend mpfp operator/(mpq const & a, mpfp b) { return a.rdiv(b); }
mpfp & operator^=(unsigned long int k) { power(k); return *this; }
friend mpfp operator^(mpfp a, unsigned long int k) { return a ^= k; }
mpfp & operator++() { return operator+=(1lu); }
mpfp operator++(int) { mpfp r(*this); ++(*this); return r; }
mpfp & operator--() { return operator-=(1lu); }
mpfp operator--(int) { mpfp r(*this); --(*this); return r; }
mpfp operator-() const { mpfp t = *this; t.neg(); return t; }
void floor() { mpfr_floor(m_val, m_val); }
void ceil () { mpfr_ceil (m_val, m_val); }
void round() { mpfr_round(m_val, m_val); }
void trunc() { mpfr_trunc(m_val, m_val); }
void rfloor(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_rint_floor(m_val, m_val, rnd); }
void rceil (mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_rint_ceil (m_val, m_val, rnd); }
void rround(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_rint_round(m_val, m_val, rnd); }
void rtrunc(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_rint_trunc(m_val, m_val, rnd); }
friend mpfp floor(mpfp const & a) { mpfp tmp; tmp = a; tmp.floor(); return tmp; }
friend mpfp ceil (mpfp const & a) { mpfp tmp; tmp = a; tmp.ceil(); return tmp; }
friend mpfp round(mpfp const & a) { mpfp tmp; tmp = a; tmp.round(); return tmp; }
friend mpfp trunc(mpfp const & a) { mpfp tmp; tmp = a; tmp.trunc(); return tmp; }
friend mpfp rfloor(mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) {
mpfp tmp; tmp = a; tmp.rfloor(rnd); return tmp;
}
friend mpfp rceil (mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) {
mpfp tmp; tmp = a; tmp.rceil(rnd); return tmp;
}
friend mpfp rround(mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) {
mpfp tmp; tmp = a; tmp.rround(rnd); return tmp;
}
friend mpfp rtrunc(mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) {
mpfp tmp; tmp = a; tmp.rtrunc(rnd); return tmp;
}
void power(mpfp const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_pow(m_val, m_val, b.m_val, rnd); }
void power(unsigned long int b, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_pow_ui(m_val, m_val, b, rnd); }
void power(long int b, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_pow_si(m_val, m_val, b, rnd); }
void power(mpz_t const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_pow_z(m_val, m_val, b, rnd); }
void power(mpz const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_pow_z(m_val, m_val, b.m_val, rnd); }
friend mpfp pow(mpfp a, mpfp const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a; }
friend mpfp pow(mpfp a, unsigned long int b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a; }
friend mpfp pow(mpfp a, long int b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a; }
friend mpfp pow(mpfp a, mpz_t const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a; }
friend mpfp pow(mpfp a, mpz const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { a.power(b, rnd); return a; }
friend std::ostream & operator<<(std::ostream & out, mpfp const & v);
};
// Macro to implement transcendental functions
#define LEAN_TRANS_MPFP_FUNC(f, v, rnd) v.f(rnd);
template<>
class numeric_traits<mpfp> {
public:
static mpfr_rnd_t rnd() { return get_mpfp_rnd(); }
static bool precise() { return false; }
static bool is_zero(mpfp const & v) { return v.is_zero(); }
static bool is_pos(mpfp const & v) { return v.is_pos(); }
static bool is_neg(mpfp const & v) { return v.is_neg(); }
static void set_rounding(bool plus_inf) { set_mpfp_rnd(plus_inf); }
static void neg(mpfp & v) { v.neg(); }
static void inv(mpfp & v) { v.inv(); }
static void reset(mpfp & v) { v = 0.0; }
static mpfp const & zero();
// v <- v^k
static void power(mpfp & v, unsigned k) { v.power(static_cast<unsigned long>(k)); }
static void abs(mpfp & v) { v.abs(); }
static void ceil(mpfp & v) { v.ceil(); }
static void floor(mpfp & v) { v.floor(); }
static inline mpfp pi_lower() {
mpfp pi_l;
mpfr_const_pi(pi_l.m_val, MPFR_RNDD);
return pi_l;
}
static inline mpfp pi() {
mpfp pi_n;
mpfr_const_pi(pi_n.m_val, MPFR_RNDN);
return pi_n;
}
static inline mpfp pi_upper() {
mpfp pi_u;
mpfr_const_pi(pi_u.m_val, MPFR_RNDU);
return pi_u;
}
static inline mpfp pi_half_lower() { return pi_lower() / 2lu; }
static inline mpfp pi_half() { return pi() / 2lu; }
static inline mpfp pi_half_upper() { return pi_upper() / 2lu; }
static inline mpfp pi_twice_lower() { return pi_lower() * 2lu; }
static inline mpfp pi_twice() { return pi() * 2lu; }
static inline mpfp pi_twice_upper() { return pi_upper() * 2lu; }
// Transcendental functions
static void exp(mpfp & v) { LEAN_TRANS_MPFP_FUNC(exp, v, rnd()); }
static void exp2(mpfp & v) { LEAN_TRANS_MPFP_FUNC(exp2, v, rnd()); }
static void exp10(mpfp & v) { LEAN_TRANS_MPFP_FUNC(exp10, v, rnd()); }
static void log(mpfp & v) { LEAN_TRANS_MPFP_FUNC(log, v, rnd()); }
static void log2(mpfp & v) { LEAN_TRANS_MPFP_FUNC(log2, v, rnd()); }
static void log10(mpfp & v) { LEAN_TRANS_MPFP_FUNC(log10, v, rnd()); }
static void sin(mpfp & v) { LEAN_TRANS_MPFP_FUNC(sin, v, rnd()); }
static void cos(mpfp & v) { LEAN_TRANS_MPFP_FUNC(cos, v, rnd()); }
static void tan(mpfp & v) { LEAN_TRANS_MPFP_FUNC(tan, v, rnd()); }
static void sec(mpfp & v) { LEAN_TRANS_MPFP_FUNC(sec, v, rnd()); }
static void csc(mpfp & v) { LEAN_TRANS_MPFP_FUNC(csc, v, rnd()); }
static void cot(mpfp & v) { LEAN_TRANS_MPFP_FUNC(cot, v, rnd()); }
static void asin(mpfp & v) { LEAN_TRANS_MPFP_FUNC(asin, v, rnd()); }
static void acos(mpfp & v) { LEAN_TRANS_MPFP_FUNC(acos, v, rnd()); }
static void atan(mpfp & v) { LEAN_TRANS_MPFP_FUNC(atan, v, rnd()); }
static void sinh(mpfp & v) { LEAN_TRANS_MPFP_FUNC(sinh, v, rnd()); }
static void cosh(mpfp & v) { LEAN_TRANS_MPFP_FUNC(cosh, v, rnd()); }
static void tanh(mpfp & v) { LEAN_TRANS_MPFP_FUNC(tanh, v, rnd()); }
static void asinh(mpfp & v) { LEAN_TRANS_MPFP_FUNC(asinh, v, rnd()); }
static void acosh(mpfp & v) { LEAN_TRANS_MPFP_FUNC(acosh, v, rnd()); }
static void atanh(mpfp & v) { LEAN_TRANS_MPFP_FUNC(atanh, v, rnd()); }
};
void initialize_mpfp();
void finalize_mpfp();
}

2
src/util/numerics/numeric_traits.h
View file

@ -8,7 +8,6 @@ Author: Leonardo de Moura
#pragma once
namespace lean {
/**
\brief Template specializations define traits for native and lean
numeric types.
@ -18,5 +17,4 @@ class numeric_traits {
};
void set_processor_rounding(bool plus_inf);
}