From 7eef501ae15c4ab3f01e8f2ef04e5eee9e80cb47 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Feb 2017 20:35:42 -0800 Subject: [PATCH] chore(*): remove mpfr dependency closes #1380 --- doc/make/fedora-19.md | 5 +- doc/make/msys2.md | 2 +- doc/make/osx-10.9.md | 3 +- doc/make/split-stack.md | 16 +- doc/make/ubuntu-12.04-detailed.md | 1 - doc/make/ubuntu-16.04.md | 2 +- src/CMakeLists.txt | 28 +- src/tests/util/numerics/CMakeLists.txt | 3 - src/tests/util/numerics/mpfp.cpp | 63 - src/tests/util/numerics/numeric_traits.cpp | 4 - src/util/interval/CMakeLists.txt | 1 - src/util/interval/interval.cpp | 2487 -------------------- src/util/interval/interval.h | 369 --- src/util/interval/interval_instances.cpp | 101 - src/util/numerics/CMakeLists.txt | 3 +- src/util/numerics/double.cpp | 13 +- src/util/numerics/double.h | 39 +- src/util/numerics/float.cpp | 9 - src/util/numerics/float.h | 39 +- src/util/numerics/init_module.cpp | 3 - src/util/numerics/mpfp.h | 564 ----- src/util/numerics/numeric_traits.h | 2 - 22 files changed, 18 insertions(+), 3739 deletions(-) delete mode 100644 src/tests/util/numerics/mpfp.cpp delete mode 100644 src/util/interval/CMakeLists.txt delete mode 100644 src/util/interval/interval.cpp delete mode 100644 src/util/interval/interval.h delete mode 100644 src/util/interval/interval_instances.cpp delete mode 100644 src/util/numerics/mpfp.h diff --git a/doc/make/fedora-19.md b/doc/make/fedora-19.md index a91ac7ee47..6ea028052a 100644 --- a/doc/make/fedora-19.md +++ b/doc/make/fedora-19.md @@ -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 - diff --git a/doc/make/msys2.md b/doc/make/msys2.md index 16ff213806..70d2684f31 100644 --- a/doc/make/msys2.md +++ b/doc/make/msys2.md @@ -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 diff --git a/doc/make/osx-10.9.md b/doc/make/osx-10.9.md index c01f1ccd91..c4459eb1b7 100644 --- a/doc/make/osx-10.9.md +++ b/doc/make/osx-10.9.md @@ -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 diff --git a/doc/make/split-stack.md b/doc/make/split-stack.md index 4ce4d25220..e4712beb49 100644 --- a/doc/make/split-stack.md +++ b/doc/make/split-stack.md @@ -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` diff --git a/doc/make/ubuntu-12.04-detailed.md b/doc/make/ubuntu-12.04-detailed.md index 22dab16541..f4d1d164d4 100644 --- a/doc/make/ubuntu-12.04-detailed.md +++ b/doc/make/ubuntu-12.04-detailed.md @@ -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 diff --git a/doc/make/ubuntu-16.04.md b/doc/make/ubuntu-16.04.md index f6e04fa6e2..8fa21fc983 100644 --- a/doc/make/ubuntu-16.04.md +++ b/doc/make/ubuntu-16.04.md @@ -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 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ee72655220..7618dd7bee 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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} $) add_subdirectory(util/sexpr) set(LEAN_OBJS ${LEAN_OBJS} $) -add_subdirectory(util/interval) -set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(util/lp) set(LEAN_OBJS ${LEAN_OBJS} $) 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") diff --git a/src/tests/util/numerics/CMakeLists.txt b/src/tests/util/numerics/CMakeLists.txt index bf754510bc..dc97cef461 100644 --- a/src/tests/util/numerics/CMakeLists.txt +++ b/src/tests/util/numerics/CMakeLists.txt @@ -4,9 +4,6 @@ add_exec_test(mpq "mpq") add_executable(mpbq mpbq.cpp $ $ $) target_link_libraries(mpbq ${EXTRA_LIBS}) add_exec_test(mpbq "mpbq") -add_executable(mpfp mpfp.cpp $ $ $) -target_link_libraries(mpfp ${EXTRA_LIBS}) -add_exec_test(mpfp "mpfp") add_executable(mpz mpz.cpp $ $ $) target_link_libraries(mpz ${EXTRA_LIBS}) add_exec_test(mpz "mpz") diff --git a/src/tests/util/numerics/mpfp.cpp b/src/tests/util/numerics/mpfp.cpp deleted file mode 100644 index 3fe9a7d61f..0000000000 --- a/src/tests/util/numerics/mpfp.cpp +++ /dev/null @@ -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 -#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; -} diff --git a/src/tests/util/numerics/numeric_traits.cpp b/src/tests/util/numerics/numeric_traits.cpp index ed7c5276cb..8b11827fc6 100644 --- a/src/tests/util/numerics/numeric_traits.cpp +++ b/src/tests/util/numerics/numeric_traits.cpp @@ -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 @@ -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(1.0)); diff --git a/src/util/interval/CMakeLists.txt b/src/util/interval/CMakeLists.txt deleted file mode 100644 index bba3ca26c3..0000000000 --- a/src/util/interval/CMakeLists.txt +++ /dev/null @@ -1 +0,0 @@ -add_library(interval OBJECT interval_instances.cpp) diff --git a/src/util/interval/interval.cpp b/src/util/interval/interval.cpp deleted file mode 100644 index b812d0f6b0..0000000000 --- a/src/util/interval/interval.cpp +++ /dev/null @@ -1,2487 +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 -#include -#include -#include -#include -#include "util/numerics/mpz.h" -#include "util/interval/interval.h" - -namespace lean { - -template -interval_deps interval::dummy; - -template -void interval::set_closed_endpoints() { - m_lower_open = false; - m_upper_open = false; - m_lower_inf = false; - m_upper_inf = false; -} - -template -interval & interval::operator=(interval const & n) { - m_lower = n.m_lower; - m_upper = n.m_upper; - m_lower_open = n.m_lower_open; - m_upper_open = n.m_upper_open; - m_lower_inf = n.m_lower_inf; - m_upper_inf = n.m_upper_inf; - return *this; -} - -template -interval & interval::operator=(interval && n) { - m_lower = std::move(n.m_lower); - m_upper = std::move(n.m_upper); - m_lower_open = n.m_lower_open; - m_upper_open = n.m_upper_open; - m_lower_inf = n.m_lower_inf; - m_upper_inf = n.m_upper_inf; - return *this; -} - -template -interval::interval(): - m_lower(), - m_upper() { - numeric_traits::reset(m_lower); - numeric_traits::reset(m_upper); - m_lower_inf = true; - m_lower_open = true; - m_upper_inf = true; - m_upper_open = true; - lean_assert(check_invariant()); -} - -template -interval::interval(interval const & n): - m_lower(n.m_lower), - m_upper(n.m_upper), - m_lower_open(n.m_lower_open), - m_upper_open(n.m_upper_open), - m_lower_inf(n.m_lower_inf), - m_upper_inf(n.m_upper_inf) { - lean_assert(check_invariant()); -} - -template -interval::interval(interval && n): - m_lower(std::move(n.m_lower)), - m_upper(std::move(n.m_upper)), - m_lower_open(n.m_lower_open), - m_upper_open(n.m_upper_open), - m_lower_inf(n.m_lower_inf), - m_upper_inf(n.m_upper_inf) { - lean_assert(check_invariant()); -} - -template -interval::~interval() { -} - -template -void interval::_swap(interval & b) { - using std::swap; - swap(m_lower, b.m_lower); - swap(m_upper, b.m_upper); - unsigned tmp; - tmp = m_lower_inf; m_lower_inf = b.m_lower_inf; b.m_lower_inf = tmp; - tmp = m_upper_inf; m_upper_inf = b.m_upper_inf; b.m_upper_inf = tmp; - tmp = m_lower_open; m_lower_open = b.m_lower_open; b.m_lower_open = tmp; - tmp = m_upper_open; m_upper_open = b.m_upper_open; b.m_upper_open = tmp; -} - -template -bool interval::contains_zero() const { - return - (is_lower_neg() || (is_lower_zero() && !is_lower_open())) && - (is_upper_pos() || (is_upper_zero() && !is_upper_open())); -} - -template -bool interval::contains(interval const & b) const { - if (!m_lower_inf) { - if (b.m_lower_inf) - return false; - if (m_lower > b.m_lower) - return false; - if (m_lower == b.m_lower && m_lower_open && !b.m_lower_open) - return false; - } - if (!m_upper_inf) { - if (b.m_upper_inf) - return false; - if (m_upper < b.m_upper) - return false; - if (m_upper == b.m_upper && m_upper_open && !b.m_upper_open) - return false; - } - return true; -} - -template -bool interval::is_empty() const { - return - (m_lower == m_upper && (m_lower_open || m_upper_open) && !m_lower_inf && !m_upper_inf) || - (m_lower > m_upper && !m_lower_inf && !m_upper_inf); -} - -template -void interval::set_empty() { - numeric_traits::reset(m_lower); - numeric_traits::reset(m_upper); - m_lower_open = m_upper_open = true; - m_lower_inf = m_upper_inf = false; -} - -template -bool interval::is_singleton() const { - return !m_lower_inf && !m_upper_inf && !m_lower_open && !m_upper_open && m_lower == m_upper; -} - -template -bool interval::_eq(interval const & b) const { - return - m_lower_open == b.m_lower_open && - m_upper_open == b.m_upper_open && - eq(m_lower, lower_kind(), b.m_lower, b.lower_kind()) && - eq(m_upper, upper_kind(), b.m_upper, b.upper_kind()); -} - -template -bool interval::before(interval const & b) const { - if (is_upper_inf() || b.is_lower_inf()) - return false; - return m_upper < b.m_lower || (is_upper_open() && m_upper == b.m_lower); -} - -template -template -void interval::neg(interval_deps & deps) { - using std::swap; - if (is_lower_inf()) { - if (is_upper_inf()) { - // (-oo, oo) case - // do nothing - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = 0; - } - } else { - // (-oo, a| --> |-a, oo) - if (compute_intv) { - swap(m_lower, m_upper); - neg(m_lower); - m_lower_inf = false; - m_lower_open = m_upper_open; - reset(m_upper); - m_upper_inf = true; - m_upper_open = true; - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1; - deps.m_upper_deps = 0; - } - } - } else { - if (is_upper_inf()) { - // |a, oo) --> (-oo, -a| - if (compute_intv) { - swap(m_upper, m_lower); - neg(m_upper); - m_upper_inf = false; - m_upper_open = m_lower_open; - - reset(m_lower); - m_lower_inf = true; - m_lower_open = true; - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = DEP_IN_LOWER1; - } - } else { - // |a, b| --> |-b, -a| - if (compute_intv) { - swap(m_lower, m_upper); - neg(m_lower); - neg(m_upper); - - unsigned lo = m_lower_open; - unsigned li = m_lower_inf; - m_lower_open = m_upper_open; - m_lower_inf = m_upper_inf; - m_upper_open = lo; - m_upper_inf = li; - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_LOWER1; - deps.m_lower_deps = DEP_IN_UPPER1; - } - } - } - if (compute_intv) { - lean_assert(check_invariant()); - } -} - -template -interval & interval::operator+=(interval const & o) { - return add(o); -} - -template -interval & interval::operator-=(interval const & o) { - return sub(o); -} - -template -interval & interval::operator*=(interval const & o) { - return mul(o); -} - -template -interval & interval::operator/=(interval const & o) { - return div(o); -} - -template -template -interval & interval::add(interval const & o, interval_deps & deps) { - if (compute_intv) { - xnumeral_kind new_l_kind, new_u_kind; - round_to_minus_inf(); - lean::add(m_lower, new_l_kind, m_lower, lower_kind(), o.m_lower, o.lower_kind()); - round_to_plus_inf(); - lean::add(m_upper, new_u_kind, m_upper, upper_kind(), o.m_upper, o.upper_kind()); - m_lower_inf = new_l_kind == XN_MINUS_INFINITY; - m_upper_inf = new_u_kind == XN_PLUS_INFINITY; - m_lower_open = m_lower_open || o.m_lower_open; - m_upper_open = m_upper_open || o.m_upper_open; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2; - deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2; - } - return *this; -} -template -template -interval & interval::sub(interval const & o, interval_deps & deps) { - if (compute_intv) { - using std::swap; - T new_l_val; - T new_u_val; - xnumeral_kind new_l_kind, new_u_kind; - round_to_minus_inf(); - lean::sub(new_l_val, new_l_kind, m_lower, lower_kind(), o.m_upper, o.upper_kind()); - round_to_plus_inf(); - lean::sub(new_u_val, new_u_kind, m_upper, upper_kind(), o.m_lower, o.lower_kind()); - swap(new_l_val, m_lower); - swap(new_u_val, m_upper); - m_lower_inf = new_l_kind == XN_MINUS_INFINITY; - m_upper_inf = new_u_kind == XN_PLUS_INFINITY; - bool o_l = o.m_lower_open; - m_lower_open = m_lower_open || o.m_upper_open; - m_upper_open = m_upper_open || o_l; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2; - deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2; - } - return *this; -} -template -template -interval & interval::mul(interval const & o, interval_deps & deps) { - using std::swap; - interval const & i1 = *this; - interval const & i2 = o; -#if defined(LEAN_DEBUG) || defined(LEAN_TRACE) - bool i1_contains_zero = i1.contains_zero(); - bool i2_contains_zero = i2.contains_zero(); -#endif - if (i1.is_zero()) { - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return *this; - } - if (i2.is_zero()) { - if (compute_intv) { - *this = i2; - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return *this; - } - - T const & a = i1.m_lower; xnumeral_kind a_k = i1.lower_kind(); - T const & b = i1.m_upper; xnumeral_kind b_k = i1.upper_kind(); - T const & c = i2.m_lower; xnumeral_kind c_k = i2.lower_kind(); - T const & d = i2.m_upper; xnumeral_kind d_k = i2.upper_kind(); - - bool a_o = i1.is_lower_open(); - bool b_o = i1.is_upper_open(); - bool c_o = i2.is_lower_open(); - bool d_o = i2.is_upper_open(); - - T new_l_val; - T new_u_val; - xnumeral_kind new_l_kind, new_u_kind; - - if (i1.is_N()) { - if (i2.is_N()) { - // x <= b <= 0, y <= d <= 0 --> b*d <= x*y - // a <= x <= b <= 0, c <= y <= d <= 0 --> x*y <= a*c (we - // can use the fact that x or y is always negative (i.e., - // b is neg or d is neg)) - if (compute_intv) { - set_is_lower_open((i1.is_N0() || i2.is_N0()) ? false : (b_o || d_o)); - set_is_upper_open(a_o || c_o); - // if b = 0 (and the interval is closed), then the lower bound is closed - - round_to_minus_inf(); - lean::mul(new_l_val, new_l_kind, b, b_k, d, d_k); - round_to_plus_inf(); - lean::mul(new_u_val, new_u_kind, a, a_k, c, c_k); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER1; // we can replace DEP_IN_UPPER1 with DEP_IN_UPPER2 - } - } else if (i2.is_M()) { - // a <= x <= b <= 0, y <= d, d > 0 --> a*d <= x*y (uses the fact that b is not positive) - // a <= x <= b <= 0, c <= y, c < 0 --> x*y <= a*c (uses - // the fact that b is not positive) - if (compute_intv) { - set_is_lower_open(a_o || d_o); - set_is_upper_open(a_o || c_o); - - round_to_minus_inf(); - lean::mul(new_l_val, new_l_kind, a, a_k, d, d_k); - round_to_plus_inf(); - lean::mul(new_u_val, new_u_kind, a, a_k, c, c_k); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER1; - } - } else { - // a <= x <= b <= 0, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that x is neg (b is not positive) or y is pos (c is not negative)) - // x <= b <= 0, 0 <= c <= y --> x*y <= b*c - lean_assert(i2.is_P()); - - // must update upper_is_open first, since value of is_N0(i1) and is_P0(i2) may be affected by update - if (compute_intv) { - set_is_upper_open((i1.is_N0() || i2.is_P0()) ? false : (b_o || c_o)); - set_is_lower_open(a_o || d_o); - - round_to_minus_inf(); - lean::mul(new_l_val, new_l_kind, a, a_k, d, d_k); - round_to_plus_inf(); - lean::mul(new_u_val, new_u_kind, b, b_k, c, c_k); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2 | DEP_IN_UPPER1; // we can replace DEP_IN_UPPER1 with DEP_IN_UPPER2 - deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2; - } - } - } else if (i1.is_M()) { - if (i2.is_N()) { - // b > 0, x <= b, c <= y <= d <= 0 --> b*c <= x*y (uses the fact that d is not positive) - // a < 0, a <= x, c <= y <= d <= 0 --> x*y <= a*c (uses - // the fact that d is not positive) - if (compute_intv) { - set_is_lower_open(b_o || c_o); - set_is_upper_open(a_o || c_o); - - round_to_minus_inf(); - lean::mul(new_l_val, new_l_kind, b, b_k, c, c_k); - round_to_plus_inf(); - lean::mul(new_u_val, new_u_kind, a, a_k, c, c_k); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2; - } - } else if (i2.is_M()) { - T ad; xnumeral_kind ad_k = XN_NUMERAL; - T bc; xnumeral_kind bc_k = XN_NUMERAL; - T ac; xnumeral_kind ac_k = XN_NUMERAL; - T bd; xnumeral_kind bd_k = XN_NUMERAL; - - bool ad_o = a_o || d_o; - bool bc_o = b_o || c_o; - bool ac_o = a_o || c_o; - bool bd_o = b_o || d_o; - - if (compute_intv) { - round_to_minus_inf(); - lean::mul(ad, ad_k, a, a_k, d, d_k); - lean::mul(bc, bc_k, b, b_k, c, c_k); - round_to_plus_inf(); - lean::mul(ac, ac_k, a, a_k, c, c_k); - lean::mul(bd, bd_k, b, b_k, d, d_k); - } - if (lt(ad, ad_k, bc, bc_k) || (eq(ad, ad_k, bc, bc_k) && !ad_o && bc_o)) { - if (compute_intv) { - swap(new_l_val, ad); - new_l_kind = ad_k; - set_is_lower_open(ad_o); - } - } else { - if (compute_intv) { - swap(new_l_val, bc); - new_l_kind = bc_k; - set_is_lower_open(bc_o); - } - } - if (gt(ac, ac_k, bd, bd_k) || (eq(ac, ac_k, bd, bd_k) && !ac_o && bd_o)) { - if (compute_intv) { - swap(new_u_val, ac); - new_u_kind = ac_k; - set_is_upper_open(ac_o); - } - } else { - if (compute_intv) { - swap(new_u_val, bd); - new_u_kind = bd_k; - set_is_upper_open(bd_o); - } - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2; - } - } else { - // a < 0, a <= x, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that c is not negative) - // b > 0, x <= b, 0 <= c <= y <= d --> x*y <= b*d (uses the fact that c is not negative) - lean_assert(i2.is_P()); - - if (compute_intv) { - set_is_lower_open(a_o || d_o); - set_is_upper_open(b_o || d_o); - - round_to_minus_inf(); - lean::mul(new_l_val, new_l_kind, a, a_k, d, d_k); - round_to_plus_inf(); - lean::mul(new_u_val, new_u_kind, b, b_k, d, d_k); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2 | DEP_IN_LOWER2; - deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2 | DEP_IN_LOWER2; - } - } - } else { - lean_assert(i1.is_P()); - if (i2.is_N()) { - // 0 <= a <= x <= b, c <= y <= d <= 0 --> x*y <= b*c (uses the fact that x is pos (a is not neg) or y is neg (d is not pos)) - // 0 <= a <= x, y <= d <= 0 --> a*d <= x*y - - // must update upper_is_open first, since value of is_P0(i1) and is_N0(i2) may be affected by update - if (compute_intv) { - set_is_upper_open((i1.is_P0() || i2.is_N0()) ? false : a_o || d_o); - set_is_lower_open(b_o || c_o); - - round_to_minus_inf(); - lean::mul(new_l_val, new_l_kind, b, b_k, c, c_k); - round_to_plus_inf(); - lean::mul(new_u_val, new_u_kind, a, a_k, d, d_k); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_LOWER1; // we can replace DEP_IN_LOWER1 with DEP_IN_UPPER2 - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2; - } - } else if (i2.is_M()) { - // 0 <= a <= x <= b, c <= y --> b*c <= x*y (uses the fact that a is not negative) - // 0 <= a <= x <= b, y <= d --> x*y <= b*d (uses the fact - // that a is not negative) - if (compute_intv) { - set_is_lower_open(b_o || c_o); - set_is_upper_open(b_o || d_o); - - round_to_minus_inf(); - lean::mul(new_l_val, new_l_kind, b, b_k, c, c_k); - round_to_plus_inf(); - lean::mul(new_u_val, new_u_kind, b, b_k, d, d_k); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_LOWER1; - deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2 | DEP_IN_LOWER1; - } - } else { - lean_assert(i2.is_P()); - // 0 n<= a <= x, 0 <= c <= y --> a*c <= x*y - // x <= b, y <= d --> x*y <= b*d (uses the fact that x is pos (a is not negative) or y is pos (c is not negative)) - if (compute_intv) { - set_is_lower_open((i1.is_P0() || i2.is_P0()) ? false : a_o || c_o); - set_is_upper_open(b_o || d_o); - - round_to_minus_inf(); - lean::mul(new_l_val, new_l_kind, a, a_k, c, c_k); - round_to_plus_inf(); - lean::mul(new_u_val, new_u_kind, b, b_k, d, d_k); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2; - deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2 | DEP_IN_LOWER1; - } - } - } - if (compute_intv) { - swap(m_lower, new_l_val); - swap(m_upper, new_u_val); - set_is_lower_inf(new_l_kind == XN_MINUS_INFINITY); - set_is_upper_inf(new_u_kind == XN_PLUS_INFINITY); - lean_assert(!(i1_contains_zero || i2_contains_zero) || contains_zero()); - lean_assert(check_invariant()); - } - return *this; -} -template -template -interval & interval::div(interval const & o, interval_deps & deps) { - using std::swap; - interval const & i1 = *this; - interval const & i2 = o; - lean_assert(!i2.contains_zero()); - - if (i1.is_zero()) { - // 0/other = 0 if other != 0 - // do nothing - if (compute_deps) { - if (i2.is_P1()) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2; - deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2; - } else { - deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2; - } - } - } else { - T const & a = i1.m_lower; xnumeral_kind a_k = i1.lower_kind(); - T const & b = i1.m_upper; xnumeral_kind b_k = i1.upper_kind(); - T const & c = i2.m_lower; xnumeral_kind c_k = i2.lower_kind(); - T const & d = i2.m_upper; xnumeral_kind d_k = i2.upper_kind(); - - bool a_o = i1.m_lower_open; - bool b_o = i1.m_upper_open; - bool c_o = i2.m_lower_open; - bool d_o = i2.m_upper_open; - - T new_l_val; - T new_u_val; - xnumeral_kind new_l_kind, new_u_kind; - - if (i1.is_N()) { - if (i2.is_N1()) { - // x <= b <= 0, c <= y <= d < 0 --> b/c <= x/y - // a <= x <= b <= 0, y <= d < 0 --> x/y <= a/d - - if (compute_intv) { - set_is_lower_open(i1.is_N0() ? false : b_o || c_o); - set_is_upper_open(a_o || d_o); - - round_to_minus_inf(); - lean::div(new_l_val, new_l_kind, b, b_k, c, c_k); - if (is_zero(d)) { - lean_assert(d_o); - reset(new_u_val); - new_u_kind = XN_PLUS_INFINITY; - } else { - round_to_plus_inf(); - lean::div(new_u_val, new_u_kind, a, a_k, d, d_k); - } - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2; - } - } else { - // a <= x, a < 0, 0 < c <= y --> a/c <= x/y - // x <= b <= 0, 0 < c <= y <= d --> x/y <= b/d - lean_assert(i2.is_P1()); - - if (compute_intv) { - set_is_upper_open(i1.is_N0() ? false : (b_o || d_o)); - set_is_lower_open(a_o || c_o); - - if (is_zero(c)) { - lean_assert(c_o); - reset(new_l_val); - new_l_kind = XN_MINUS_INFINITY; - } else { - round_to_minus_inf(); - lean::div(new_l_val, new_l_kind, a, a_k, c, c_k); - } - round_to_plus_inf(); - lean::div(new_u_val, new_u_kind, b, b_k, d, d_k); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2; - deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2; - } - } - } else if (i1.is_M()) { - if (i2.is_N1()) { - // 0 < a <= x <= b < 0, y <= d < 0 --> b/d <= x/y - // 0 < a <= x <= b < 0, y <= d < 0 --> x/y <= a/d - - if (compute_intv) { - set_is_lower_open(b_o || d_o); - set_is_upper_open(a_o || d_o); - - if (is_zero(d)) { - lean_assert(d_o); - reset(new_l_val); - reset(new_u_val); - new_l_kind = XN_MINUS_INFINITY; - new_u_kind = XN_PLUS_INFINITY; - } else { - round_to_minus_inf(); - lean::div(new_l_val, new_l_kind, b, b_k, d, d_k); - round_to_plus_inf(); - lean::div(new_u_val, new_u_kind, a, a_k, d, d_k); - } - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2; - } - } else { - // 0 < a <= x <= b < 0, 0 < c <= y --> a/c <= x/y - // 0 < a <= x <= b < 0, 0 < c <= y --> x/y <= b/c - lean_assert(i1.is_P1()); - if (compute_intv) { - set_is_lower_open(a_o || c_o); - set_is_upper_open(b_o || c_o); - - if (is_zero(c)) { - lean_assert(c_o); - reset(new_l_val); - reset(new_u_val); - new_l_kind = XN_MINUS_INFINITY; - new_u_kind = XN_PLUS_INFINITY; - } else { - round_to_minus_inf(); - lean::div(new_l_val, new_l_kind, a, a_k, c, c_k); - round_to_plus_inf(); - lean::div(new_u_val, new_u_kind, b, b_k, c, c_k); - } - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2; - deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2; - } - } - } else { - lean_assert(i1.is_P()); - if (i2.is_N1()) { - // b > 0, x <= b, c <= y <= d < 0 --> b/d <= x/y - // 0 <= a <= x, c <= y <= d < 0 --> x/y <= a/c - if (compute_intv) { - set_is_upper_open(i1.is_P0() ? false : a_o || c_o); - set_is_lower_open(b_o || d_o); - - if (is_zero(d)) { - lean_assert(d_o); - reset(new_l_val); - new_l_kind = XN_MINUS_INFINITY; - } else { - round_to_minus_inf(); - lean::div(new_l_val, new_l_kind, b, b_k, d, d_k); - } - round_to_plus_inf(); - lean::div(new_u_val, new_u_kind, a, a_k, c, c_k); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2; - } - } else { - lean_assert(i2.is_P1()); - // 0 <= a <= x, 0 < c <= y <= d --> a/d <= x/y - // b > 0 x <= b, 0 < c <= y --> x/y <= b/c - if (compute_intv) { - set_is_lower_open(i1.is_P0() ? false : a_o || d_o); - set_is_upper_open(b_o || c_o); - - round_to_minus_inf(); - lean::div(new_l_val, new_l_kind, a, a_k, d, d_k); - if (is_zero(c)) { - lean_assert(c_o); - reset(new_u_val); - new_u_kind = XN_PLUS_INFINITY; - } else { - round_to_plus_inf(); - lean::div(new_u_val, new_u_kind, b, b_k, c, c_k); - } - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2; - deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2; - } - } - } - if (compute_intv) { - swap(m_lower, new_l_val); - swap(m_upper, new_u_val); - m_lower_inf = (new_l_kind == XN_MINUS_INFINITY); - m_upper_inf = (new_u_kind == XN_PLUS_INFINITY); - } - } - return *this; -} -template void interval::add_jst(interval const & o, interval_deps & deps) { - add(o, deps); - return; -} -template void interval::sub_jst(interval const & o, interval_deps & deps) { - sub(o, deps); - return; -} -template void interval::mul_jst(interval const & o, interval_deps & deps) { - mul(o, deps); - return; -} -template void interval::div_jst(interval const & o, interval_deps & deps) { - div(o, deps); - return; -} - -template -interval & interval::operator+=(T const & o) { - xnumeral_kind new_l_kind, new_u_kind; - round_to_minus_inf(); - lean::add(m_lower, new_l_kind, m_lower, lower_kind(), o, XN_NUMERAL); - round_to_plus_inf(); - lean::add(m_upper, new_u_kind, m_upper, upper_kind(), o, XN_NUMERAL); - m_lower_inf = new_l_kind == XN_MINUS_INFINITY; - m_upper_inf = new_u_kind == XN_PLUS_INFINITY; - lean_assert(check_invariant()); - return *this; -} - -template -interval & interval::operator-=(T const & o) { - xnumeral_kind new_l_kind, new_u_kind; - round_to_minus_inf(); - lean::sub(m_lower, new_l_kind, m_lower, lower_kind(), o, XN_NUMERAL); - round_to_plus_inf(); - lean::sub(m_upper, new_u_kind, m_upper, upper_kind(), o, XN_NUMERAL); - m_lower_inf = new_l_kind == XN_MINUS_INFINITY; - m_upper_inf = new_u_kind == XN_PLUS_INFINITY; - lean_assert(check_invariant()); - return *this; -} - -template -interval & interval::operator*=(T const & o) { - xnumeral_kind new_l_kind, new_u_kind; - T tmp1; - if (this->is_zero()) { - return *this; - } - if (numeric_traits::is_zero(o)) { - numeric_traits::reset(m_lower); - numeric_traits::reset(m_upper); - m_lower_open = m_upper_open = false; - m_lower_inf = m_upper_inf = false; - return *this; - } - - if (numeric_traits::is_pos(o)) { - // [a, b] * c = [a*c, b*c] when c > 0 - round_to_minus_inf(); - lean::mul(m_lower, new_l_kind, m_lower, lower_kind(), o, XN_NUMERAL); - round_to_plus_inf(); - lean::mul(m_upper, new_u_kind, m_upper, upper_kind(), o, XN_NUMERAL); - m_lower_inf = new_l_kind == XN_MINUS_INFINITY; - m_upper_inf = new_u_kind == XN_PLUS_INFINITY; - } else { - // [a, b] * c = [b*c, a*c] when c < 0 - round_to_minus_inf(); - lean::mul(tmp1, new_l_kind, m_upper, upper_kind(), o, XN_NUMERAL); - round_to_plus_inf(); - lean::mul(m_upper, new_u_kind, m_lower, lower_kind(), o, XN_NUMERAL); - m_lower = tmp1; - m_lower_inf = new_l_kind == XN_MINUS_INFINITY; - m_upper_inf = new_u_kind == XN_PLUS_INFINITY; - } - return *this; -} - -template -interval & interval::operator/=(T const & o) { - xnumeral_kind new_l_kind, new_u_kind; - T tmp1; - if (this->is_zero()) { - return *this; - } - if (numeric_traits::is_zero(o)) { - numeric_traits::reset(m_lower); - numeric_traits::reset(m_upper); - m_lower_open = m_upper_open = true; - m_lower_inf = m_upper_inf = true; - return *this; - } - - if (numeric_traits::is_pos(o)) { - // [a, b] / c = [a/c, b/c] when c > 0 - round_to_minus_inf(); - lean::div(m_lower, new_l_kind, m_lower, lower_kind(), o, XN_NUMERAL); - round_to_plus_inf(); - lean::div(m_upper, new_u_kind, m_upper, upper_kind(), o, XN_NUMERAL); - m_lower_inf = new_l_kind == XN_MINUS_INFINITY; - m_upper_inf = new_u_kind == XN_PLUS_INFINITY; - } else { - // [a, b] / c = [b/c, a/c] when c < 0 - round_to_minus_inf(); - lean::div(tmp1, new_l_kind, m_upper, upper_kind(), o, XN_NUMERAL); - round_to_plus_inf(); - lean::div(m_upper, new_u_kind, m_lower, lower_kind(), o, XN_NUMERAL); - m_lower = tmp1; - m_lower_inf = new_l_kind == XN_MINUS_INFINITY; - m_upper_inf = new_u_kind == XN_PLUS_INFINITY; - } - return *this; -} - -template -template -void interval::inv(interval_deps & deps) { - // If the interval [l, u] does not contain 0, then 1/[l, u] = [1/u, 1/l] - lean_assert(!contains_zero()); - - using std::swap; - - T new_l_val; - T new_u_val; - xnumeral_kind new_l_kind, new_u_kind; - - if (is_P1()) { - // 0 < l <= x --> 1/x <= 1/l - // 0 < l <= x <= u --> 1/u <= 1/x (use lower and upper bounds) - if (compute_intv) { - round_to_minus_inf(); - new_l_val = m_upper; - new_l_kind = upper_kind(); - ::lean::inv(new_l_val, new_l_kind); - lean_assert(new_l_kind == XN_NUMERAL); - bool new_l_open = is_upper_open(); - - if (is_lower_zero()) { - lean_assert(is_lower_open()); - reset(m_upper); - set_is_upper_inf(true); - set_is_upper_open(true); - } else { - round_to_plus_inf(); - new_u_val = m_lower; - inv(new_u_val); - swap(m_upper, new_u_val); - set_is_upper_inf(false); - set_is_upper_open(is_lower_open()); - } - - swap(m_lower, new_l_val); - set_is_lower_inf(false); - set_is_lower_open(new_l_open); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1; - } - } else if (is_N1()) { - // x <= u < 0 --> 1/u <= 1/x - // l <= x <= u < 0 --> 1/l <= 1/x (use lower and upper bounds) - if (compute_intv) { - round_to_plus_inf(); - new_u_val = m_lower; - new_u_kind = lower_kind(); - ::lean::inv(new_u_val, new_u_kind); - lean_assert(new_u_kind == XN_NUMERAL); - - bool new_u_open = is_lower_open(); - - if (is_upper_zero()) { - lean_assert(is_upper_open()); - reset(m_lower); - set_is_lower_open(true); - set_is_lower_inf(true); - } else { - round_to_minus_inf(); - new_l_val = m_upper; - inv(new_l_val); - swap(m_lower, new_l_val); - set_is_lower_inf(false); - set_is_lower_open(is_upper_open()); - } - - swap(m_upper, new_u_val); - set_is_upper_inf(false); - set_is_upper_open(new_u_open); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - } else { - lean_unreachable(); // LCOV_EXCL_LINE - } - lean_assert(check_invariant()); -} - -template -template -void interval::power(unsigned n, interval_deps & deps) { - using std::swap; - lean_assert(n > 0); - if (n == 1) { - // a^1 = a - // nothing to be done - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - deps.m_upper_deps = DEP_IN_UPPER1; - } - return; - } else if (n % 2 == 0) { - if (is_lower_pos()) { - // [l, u]^n = [l^n, u^n] if l > 0 - // 0 < l <= x --> l^n <= x^n (lower bound guarantees that is positive) - // 0 < l <= x <= u --> x^n <= u^n (use lower and upper bound -- need the fact that x is positive) - lean_assert(!is_lower_inf()); - if (compute_intv) { - round_to_minus_inf(); - power(m_lower, n); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - - if (!m_upper_inf) { - if (compute_intv) { - round_to_plus_inf(); - power(m_upper, n); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - } else { - deps.m_upper_deps = 0; - } - } else if (is_upper_neg()) { - // [l, u]^n = [u^n, l^n] if u < 0 - // l <= x <= u < 0 --> x^n <= l^n (use lower and upper bound -- need the fact that x is negative) - // x <= u < 0 --> u^n <= x^n - lean_assert(!is_upper_inf()); - const bool lo = m_lower_open; - const bool li = m_lower_inf; - - if (compute_intv) { - swap(m_lower, m_upper); - round_to_minus_inf(); - power(m_lower, n); - m_lower_open = m_upper_open; - m_lower_inf = false; - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1; - } - - if (li) { - if (compute_intv) { - reset(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = 0; - } - } else { - if (compute_intv) { - round_to_plus_inf(); - power(m_upper, n); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_lower_deps = 0; - } - } - if (compute_intv) { - m_upper_inf = li; - m_upper_open = lo; - } - } else { - // [l, u]^n = [0, max{l^n, u^n}] otherwise - // we need both bounds to justify upper bound - xnumeral_kind un1_kind = lower_kind(); - xnumeral_kind un2_kind = upper_kind(); - T un1; - T un2; - if (compute_intv) { - swap(un1, m_lower); - swap(un2, m_upper); - round_to_plus_inf(); - ::lean::power(un1, un1_kind, n); - ::lean::power(un2, un2_kind, n); - if (gt(un1, un1_kind, un2, un2_kind) || (eq(un1, un1_kind, un2, un2_kind) && !m_lower_open && m_upper_open)) { - swap(m_upper, un1); - m_upper_inf = (un1_kind == XN_PLUS_INFINITY); - m_upper_open = m_lower_open; - } else { - swap(m_upper, un2); - m_upper_inf = (un2_kind == XN_PLUS_INFINITY); - } - - reset(m_lower); - m_lower_inf = false; - m_lower_open = false; - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_lower_deps = 0; - } - } - } else { - // Remark: when n is odd x^n is monotonic. - if (!m_lower_inf) { - if (compute_intv) { - round_to_minus_inf(); - power(m_lower, n); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } else { - if (compute_deps) { - deps.m_lower_deps = 0; - } - } - if (!m_upper_inf) { - if (compute_intv) { - round_to_plus_inf(); - power(m_upper, n); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } else { - if (compute_deps) { - deps.m_upper_deps = 0; - } - } - } -} -template void interval::power_jst(unsigned n, interval_deps & deps) { - power(n, deps); - return; -} - -/** - return a/(x^n) - - If to_plus_inf, then result >= a/(x^n) - If not to_plus_inf, then result <= a/(x^n) - -*/ -template -T a_div_x_n(T a, T const & x, unsigned n, bool to_plus_inf) { - if (n == 1) { - numeric_traits::set_rounding(to_plus_inf); - a /= x; - } else { - T tmp; - numeric_traits::set_rounding(!to_plus_inf); - tmp = x; - numeric_traits::power(tmp, n); - numeric_traits::set_rounding(to_plus_inf); - a /= x; - } - return a; -} - -template -bool interval::check_invariant() const { - lean_assert(!m_lower_inf || m_lower_open); - lean_assert(!m_upper_inf || m_upper_open); - if (eq(m_lower, lower_kind(), m_upper, upper_kind())) { - lean_assert(!is_lower_open()); - lean_assert(!is_upper_open()); - } else { - lean_assert(lt(m_lower, lower_kind(), m_upper, upper_kind())); - } - return true; -} - -template -void interval::display(std::ostream & out) const { - out << (m_lower_open ? "(" : "["); - ::lean::display(out, m_lower, lower_kind()); - out << ", "; - ::lean::display(out, m_upper, upper_kind()); - out << (m_upper_open ? ")" : "]"); -} - - -template void interval::fmod(interval y) { - T const & yb = numeric_traits::is_neg(m_lower) ? y.m_lower : y.m_upper; - T n; - numeric_traits::set_rounding(false); - n = m_lower / yb; - numeric_traits::floor(n); - *this -= n * y; -} - -template void interval::fmod(T y) { - T n; - numeric_traits::set_rounding(false); - n = m_lower / y; - numeric_traits::floor(n); - *this -= n * y; -} - -template -template -void interval::exp(interval_deps & deps) { - if (m_lower_inf) { - if (compute_intv) { - numeric_traits::reset(m_lower); - } - if (compute_deps) { - deps.m_lower_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(false); - numeric_traits::exp(m_lower); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } - if (m_upper_inf) { - if (compute_deps) { - deps.m_lower_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::exp(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } - lean_assert(check_invariant()); - return; -} - -template -template -void interval::exp2(interval_deps & deps) { - if (m_lower_inf) { - if (compute_intv) { - numeric_traits::reset(m_lower); - } - if (compute_deps) { - deps.m_lower_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(false); - numeric_traits::exp2(m_lower); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } - if (m_upper_inf) { - if (compute_deps) { - deps.m_lower_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::exp2(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } - lean_assert(check_invariant()); - return; -} - -template -template -void interval::exp10(interval_deps & deps) { - if (m_lower_inf) { - if (compute_intv) { - numeric_traits::reset(m_lower); - } - if (compute_deps) { - deps.m_lower_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(false); - numeric_traits::exp10(m_lower); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } - if (m_upper_inf) { - if (compute_deps) { - deps.m_lower_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::exp10(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } - lean_assert(check_invariant()); - return; -} - -template -template -void interval::log(interval_deps & deps) { - lean_assert(lower_kind() == XN_NUMERAL); - // lower_open => lower >= 0 - lean_assert(!m_lower_open || numeric_traits::is_pos(m_lower) || numeric_traits::is_zero(m_lower)); - // !lower_open => lower > 0 - lean_assert(m_lower_open || numeric_traits::is_pos(m_lower)); - if (is_lower_pos()) { - if (compute_intv) { - numeric_traits::set_rounding(false); - numeric_traits::log(m_lower); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } else { - if (compute_intv) { - numeric_traits::reset(m_lower); - m_lower_inf = true; - } - if (compute_deps) { - deps.m_lower_deps = 0; - } - } - if (m_upper_inf) { - // Nothing to do - if (compute_deps) { - deps.m_upper_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::log(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } - lean_assert(check_invariant()); - return; -} - -template -template -void interval::log2(interval_deps & deps) { - lean_assert(lower_kind() == XN_NUMERAL); - // lower_open => lower >= 0 - lean_assert(!m_lower_open || numeric_traits::is_pos(m_lower) || numeric_traits::is_zero(m_lower)); - // !lower_open => lower > 0 - lean_assert(m_lower_open || numeric_traits::is_pos(m_lower)); - if (is_lower_pos()) { - if (compute_intv) { - numeric_traits::set_rounding(false); - numeric_traits::log2(m_lower); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } else { - if (compute_intv) { - numeric_traits::reset(m_lower); - m_lower_inf = true; - } - if (compute_deps) { - deps.m_lower_deps = 0; - } - } - if (m_upper_inf) { - // Nothing to do - if (compute_deps) { - deps.m_upper_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::log2(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } - lean_assert(check_invariant()); - return; -} - -template -template -void interval::log10(interval_deps & deps) { - lean_assert(lower_kind() == XN_NUMERAL); - // lower_open => lower >= 0 - lean_assert(!m_lower_open || numeric_traits::is_pos(m_lower) || numeric_traits::is_zero(m_lower)); - // !lower_open => lower > 0 - lean_assert(m_lower_open || numeric_traits::is_pos(m_lower)); - if (is_lower_pos()) { - if (compute_intv) { - numeric_traits::set_rounding(false); - numeric_traits::log10(m_lower); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } else { - if (compute_intv) { - numeric_traits::reset(m_lower); - m_lower_inf = true; - } - if (compute_deps) { - deps.m_lower_deps = 0; - } - } - if (m_upper_inf) { - // Nothing to do - if (compute_deps) { - deps.m_upper_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::log10(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } - lean_assert(check_invariant()); - return; -} - -template -template -void interval::sin(interval_deps & deps) { - if (m_lower_inf || m_upper_inf) { - // sin([-oo, c]) = [-1.0, +1.0] - // sin([c, +oo]) = [-1.0, +1.0] - if (compute_intv) { - m_lower_open = m_upper_open = false; - m_lower_inf = m_upper_inf = false; - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = 0; - } - return; - } - - m_lower_open = m_upper_open = false; - m_lower_inf = m_upper_inf = false; - - T const pi_twice = numeric_traits::pi_twice(); - fmod(interval(numeric_traits::pi_twice_lower(), numeric_traits::pi_twice_upper())); - if (m_upper - m_lower >= pi_twice) { - // If the input width is bigger than 2pi, - // it covers whole domain and gets [-1.0, 1.0] - if (compute_intv) { - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = 0; - } - return; - } - - // Use sin(x - pi) = - sin(x) - // l \in [-pi, pi] - *this -= interval(numeric_traits::pi_lower(), numeric_traits::pi_upper()); - - T const pi_half = numeric_traits::pi_half(); - T const pi = numeric_traits::pi(); - - if (m_lower <= - pi_half) { - if (m_upper <= - pi_half) { - // 1. -pi <= l' <= u' <= -1/2 pi - // sin(x - pi) = [sin(u'), sin(l')] - // sin(x) = [-sin(l'), -sin(u')] - // sin(x) = [-sin(l'), sin(-u')] - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::sin(m_lower); - m_lower = -m_lower; - m_upper = -m_upper; - numeric_traits::sin(m_upper); - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - if (m_upper <= pi_half) { - // 2. -pi <= l' <= -1/2 pi <= u' <= 1/2 pi - // sin(x - pi) = [-1, max(sin(l'), sin(u'))] - // = [-1, sin(l')] if l' + u' <= - pi - // = [-1, sin(u')] if l' + u' >= - pi - // sin(x) = [-sin(l'), 1] if l' + u' <= - pi - // = [-sin(u'), 1] if l' + u' >= - pi - if (m_lower + m_upper <= - pi) { - // Nothing - } else { - if (compute_intv) { - m_lower = m_upper; - } - } - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::sin(m_lower); - m_lower = - m_lower; - m_upper = 1.0; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = 0; - } - return; - } - // 3. -pi <= l' <= -1/2 pi <= 1/2 pi <= u' - // sin(x - pi) = [-1, 1] - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = 0; - } - if (compute_intv) { - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); - } - return; - } - if (m_lower <= pi_half) { - if (m_upper <= pi_half) { - // 4. -1/2 pi <= l' <= u' <= 1/2 pi - // sin(x - pi) = [sin(l'), sin(u')] - // sin(x) = [-sin(u'), -sin(l')] - // = [-sin(u'), sin(-l')] - if (compute_intv) { - std::swap(m_lower, m_upper); - m_upper = -m_upper; - numeric_traits::set_rounding(true); - numeric_traits::sin(m_lower); - numeric_traits::sin(m_upper); - m_lower = -m_lower; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - if (m_upper <= pi_half + pi) { - // 5. -1/2 pi <= l' <= 1/2pi <= u' <= 3/2pi - // sin(x - pi) = [min(sin(l'), sin(u')), 1] - // = [sin(l'), 1] if l' + u' <= pi - // = [sin(u'), 1] if l' + u' >= pi - // sin(x) = [-1, sin(-l')] if l' + u' <= pi - // = [-1, sin(-u')] if l' + u' >= pi - if (m_lower + m_upper <= pi) { - if (compute_intv) { - m_upper = - m_lower; - } - } else { - if (compute_intv) { - m_upper = - m_upper; - } - } - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::sin(m_upper); - m_lower = -1.0; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - // 6. -1/2 pi <= l' <= 1/2pi <= 3/2pi <= u' - // sin(x - pi) = [-1, 1] - if (compute_intv) { - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = 0; - } - return; - } - lean_assert(pi_half <= m_lower); - if (m_upper <= pi_half + pi) { - // 7. 1/2pi <= l' <= u' <= 3/2 pi - // sin(x - pi) = [sin(u'), sin(l')] - // sin(x) = [-sin(l'), sin(-u')] - if (compute_intv) { - m_upper = -m_upper; - numeric_traits::set_rounding(true); - numeric_traits::sin(m_lower); - numeric_traits::sin(m_upper); - m_lower = -m_lower; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - if (m_upper <= pi_half + pi_twice) { - // 8. 1/2pi <= l' <= 3/2pi <= u' <= 5/2 pi - // sin(x - pi) = [-1, max(sin(l'), sin(u')] - // = [-1, sin(l')] if l' + u' <= 3pi - // = [-1, sin(u')] if l' + u' >= 3pi - // sin(x) = [-sin(l'), 1] if l' + u' <= 3pi - // = [-sin(u'), 1] if l' + u' >= 3pi - if (m_lower + m_upper <= pi + pi_twice) { - // Nothing - } else { - if (compute_intv) { - m_lower = m_upper; - } - } - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::sin(m_lower); - m_lower = - m_lower; - m_upper = 1.0; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = 0; - } - return; - } - // 9. 1/2pi <= l' <= 5/2pi <= u' - // sin(x - pi) = [-1, 1] - if (compute_intv) { - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = 0; - } - return; -} - -template -template -void interval::cos (interval_deps & deps) { - if (m_lower_inf || m_upper_inf) { - // cos([-oo, c]) = [-1.0, +1.0] - // cos([c, +oo]) = [-1.0, +1.0] - if (compute_intv) { - m_lower = -1.0; - m_upper = 1.0; - m_lower_open = m_upper_open = false; - m_lower_inf = m_upper_inf = false; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = 0; - } - return; - } - - m_lower_open = m_upper_open = false; - m_lower_inf = m_upper_inf = false; - T const pi_twice = numeric_traits::pi_twice(); - fmod(interval(numeric_traits::pi_twice_lower(), numeric_traits::pi_twice_upper())); - if (m_upper - m_lower >= pi_twice) { - // If the input width is bigger than 2pi, - // it covers whole domain and gets [-1.0, 1.0] - if (compute_intv) { - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = 0; - } - return; - } - if (m_lower >= numeric_traits::pi_upper()) { - // If the input is bigger than pi, we handle it recursively by the fact: - // cos(x) = -cos(x - pi) - if (compute_intv) { - *this -= interval(numeric_traits::pi_lower(), numeric_traits::pi_upper()); - } - cos(deps); - neg(); - lean_assert(check_invariant()); - return; - } - - if (m_upper <= numeric_traits::pi_lower()) { - // 0 <= l <= u <= pi - // cos([l, u]) = [cos_d(u), cos_u(l)] - if (compute_intv) { - std::swap(m_lower, m_upper); - numeric_traits::set_rounding(false); - numeric_traits::cos(m_lower); - numeric_traits::set_rounding(true); - numeric_traits::cos(m_upper); - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - - if (m_upper <= numeric_traits::pi_twice_lower()) { - // If the input is [a, b] and a <= pi <= b, - // Pick the tmp = min(a, 2pi - b) and return [-1, cos(tmp)] - if (m_lower + m_upper < numeric_traits::pi_twice()) { - if (compute_intv) { - m_upper = m_lower; - } - } else { - // Nothing - } - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::cos(m_upper); - m_lower = -1.0; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - if (compute_intv) { - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = 0; - } - return; -} - -template -template -void interval::tan(interval_deps & deps) { - if (m_lower_inf || m_upper_inf) { - // tan([-oo, c]) = [-oo, +oo] - // tan([c, +oo]) = [-oo, +oo] - if (compute_intv) { - numeric_traits::reset(m_lower); - numeric_traits::reset(m_upper); - m_lower_open = m_upper_open = true; - m_lower_inf = m_upper_inf = true; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = deps.m_upper_deps = 0; - } - return; - } - - T const pi_half_lower = numeric_traits::pi_half_lower(); - fmod(interval(numeric_traits::pi_lower(), numeric_traits::pi_upper())); - - if (m_lower >= pi_half_lower) { - *this -= interval(numeric_traits::pi_lower(), numeric_traits::pi_upper()); - } - if (m_lower <= - pi_half_lower || m_upper >= pi_half_lower) { - if (compute_intv) { - numeric_traits::reset(m_lower); - numeric_traits::reset(m_upper); - m_lower_open = m_upper_open = true; - m_lower_inf = m_upper_inf = true; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = deps.m_upper_deps = 0; - } - return; - } else { - if (compute_intv) { - numeric_traits::set_rounding(true); - m_lower = -m_lower; - numeric_traits::tan(m_lower); - m_lower = -m_lower; - numeric_traits::tan(m_upper); - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } -} - -template -template -void interval::csc (interval_deps & deps) { - T l; - T u; - if (compute_intv) { - l = m_lower; - u = m_upper; - } - // csc(x) = 1 / sin(x) - if (m_lower_inf || m_upper_inf || (m_upper - m_lower > numeric_traits::pi())) { - // csc([-oo, c]) = [-oo, +oo] - // csc([c, +oo]) = [-oo, +oo] - // if the width is bigger than pi, then the result is [-oo, +oo] - if (compute_intv) { - numeric_traits::reset(m_lower); - numeric_traits::reset(m_upper); - m_lower_open = m_upper_open = true; - m_lower_inf = m_upper_inf = true; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = deps.m_upper_deps = 0; - } - return; - } - T const pi_half = numeric_traits::pi_half(); - T const pi = numeric_traits::pi(); - fmod(interval(numeric_traits::pi_twice_lower(), numeric_traits::pi_twice_upper())); - if (m_upper > numeric_traits::pi_twice() || - (m_lower < pi && pi < m_upper)) { - // l < 2pi < u or l < pi < u - // then the result = [-oo, +oo] - if (compute_intv) { - numeric_traits::reset(m_lower); - numeric_traits::reset(m_upper); - m_lower_open = m_upper_open = true; - m_lower_inf = m_upper_inf = true; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = deps.m_upper_deps = 0; - } - return; - } - - if (m_lower <= pi_half) { - if (m_upper <= pi_half) { - // l <= u <= 1/2 pi - // csc[l, u] = [csc(u), csc(l)] - // = [-csc(-u), csc(l)] - if (compute_intv) { - m_lower = -u; - m_upper = l; - numeric_traits::set_rounding(true); - numeric_traits::csc(m_lower); - numeric_traits::csc(m_upper); - m_lower = -m_lower; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - if (m_upper <= pi) { - // l <= 1/2 pi <= u <= pi - // csc[l, u] = [1, max(csc(l), csc(u))] - // = [1, csc(l)] if l + u <= pi - // = [1, csc(u)] if l + u >= pi - if (m_lower + m_upper < pi) { - if (compute_intv) { - m_upper = l; - } - } else { - // Nothing - if (compute_intv) { - m_upper = u; - } - } - if (compute_intv) { - m_lower = 1.0; - numeric_traits::set_rounding(true); - numeric_traits::csc(m_upper); - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - lean_unreachable(); // LCOV_EXCL_LINE - } - - if (m_lower <= pi && m_upper <= pi) { - // l <= u <= pi - // csc[l, u] = [csc(l), csc(u)] - // = [-csc(-l), csc(u)] - if (compute_intv) { - m_lower = -l; - m_upper = u; - numeric_traits::set_rounding(true); - numeric_traits::csc(m_lower); - numeric_traits::csc(m_upper); - m_lower = -m_lower; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - if (m_lower <= pi + pi_half) { - if (m_upper <= pi + pi_half) { - // l <= u <= 3/2 pi - // csc[l, u] = [csc(l), csc(u)] - // = [-csc(-l), csc(u)] - if (compute_intv) { - m_lower = -l; - m_upper = u; - numeric_traits::set_rounding(true); - numeric_traits::csc(m_lower); - numeric_traits::csc(m_upper); - m_lower = -m_lower; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - // l <= 3/2 pi <= u <= 2pi - // csc[l, u] = [min(csc(l), csc(u)), -1] - // = [csc(l), -1] if l + u <= 3pi - // = [csc(u), -1] if l + u >= 3pi - // - // = [-csc(-l), -1] if l + u <= 3pi - // = [-csc(-u), -1] if l + u >= 3pi - if (m_lower + m_upper < pi + numeric_traits::pi_twice()) { - // Nothing - if (compute_intv) { - m_lower = -l; - } - } else { - if (compute_intv) { - m_lower = -u; - } - } - if (compute_intv) { - m_upper = -1.0; - numeric_traits::set_rounding(true); - numeric_traits::csc(m_lower); - m_lower = -m_lower; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = 0; - } - return; - } - // 3/2pi <= l <= u < 2pi - // csc[l, u] = [csc(u), csc(l)] - // = [-csc(-u), csc(l)] - if (compute_intv) { - m_lower = -u; - m_upper = l; - numeric_traits::set_rounding(true); - numeric_traits::csc(m_lower); - numeric_traits::csc(m_upper); - m_lower = -m_lower; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; -} - -template -template -void interval::sec (interval_deps & deps) { - if (compute_intv) { - *this += interval(numeric_traits::pi_half_lower(), numeric_traits::pi_half_upper()); - } - csc(deps); - return; -} - -template -template -void interval::cot (interval_deps & deps) { - T l; - T u; - if (compute_intv) { - l = m_lower; - u = m_upper; - } - if (m_lower_inf || m_upper_inf) { - // cot([-oo, c]) = [-oo, +oo] - // cot([c, +oo]) = [-oo, +oo] - if (compute_intv) { - numeric_traits::reset(m_lower); - numeric_traits::reset(m_upper); - m_lower_open = m_upper_open = true; - m_lower_inf = m_upper_inf = true; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = deps.m_upper_deps = 0; - } - return; - } - fmod(interval(numeric_traits::pi_lower(), numeric_traits::pi_upper())); - if (m_upper >= numeric_traits::pi()) { - if (compute_intv) { - numeric_traits::reset(m_lower); - numeric_traits::reset(m_upper); - m_lower_open = m_upper_open = true; - m_lower_inf = m_upper_inf = true; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = deps.m_upper_deps = 0; - } - return; - } - - // cot([l, u]) = [cot_d(u), cot_u(l)] - // = [-cot_u(-u), cot_u(l)] - if (compute_intv) { - m_lower = - u; - m_upper = l; - numeric_traits::set_rounding(true); - numeric_traits::cot(m_lower); - numeric_traits::cot(m_upper); - m_lower = - m_lower; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; -} - -template -template -void interval::asin (interval_deps & deps) { - lean_assert(lower_kind() == XN_NUMERAL && upper_kind() == XN_NUMERAL); - lean_assert(-1.0 <= m_lower && m_upper <= 1.0); - - // aisn([l, u]) = [asin_d(l), asin_u(u)] - // = [-asin_u(-l), asin_u(u)] - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::asin(m_upper); - m_lower = -m_lower; - numeric_traits::asin(m_lower); - m_lower = -m_lower; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - deps.m_upper_deps = DEP_IN_UPPER1; - } - return; -} - -template -template -void interval::acos (interval_deps & deps) { - lean_assert(lower_kind() == XN_NUMERAL && upper_kind() == XN_NUMERAL); - lean_assert(-1.0 <= m_lower && m_upper <= 1.0); - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::acos(m_lower); - numeric_traits::set_rounding(false); - numeric_traits::acos(m_upper); - std::swap(m_lower, m_upper); - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1; - } - return; -} - -template -template -void interval::atan (interval_deps & deps) { - if (lower_kind() == XN_MINUS_INFINITY) { - if (compute_intv) { - m_lower = -1.0; - m_lower_open = false; - m_lower_inf = false; - } - if (compute_deps) { - deps.m_lower_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(true); - m_lower = -m_lower; - numeric_traits::atan(m_lower); - m_lower = -m_lower; - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } - - if (upper_kind() == XN_MINUS_INFINITY) { - if (compute_intv) { - m_upper = 1.0; - m_upper_open = false; - m_upper_inf = false; - } - if (compute_deps) { - deps.m_upper_deps = 0; - } - } else { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::atan(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } - if (compute_intv) { - lean_assert(check_invariant()); - } - return; -} - -template -template -void interval::sinh (interval_deps & deps) { - if (lower_kind() == XN_NUMERAL) { - if (compute_intv) { - numeric_traits::set_rounding(true); - m_lower = -m_lower; - numeric_traits::sinh(m_lower); - m_lower = -m_lower; - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } - if (upper_kind() == XN_NUMERAL) { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::sinh(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } - if (compute_intv) { - lean_assert(check_invariant()); - } - return; -} - -template -template -void interval::cosh (interval_deps & deps) { - if (lower_kind() == XN_NUMERAL && upper_kind() == XN_NUMERAL) { - if (numeric_traits::is_pos(m_lower) || numeric_traits::is_zero(m_lower)) { - // [a, b] where 0 <= a <= b - if (compute_intv) { - numeric_traits::set_rounding(false); - numeric_traits::cosh(m_lower); - numeric_traits::set_rounding(true); - numeric_traits::cosh(m_upper); - lean_assert(check_invariant()); - } - if (compute_deps) { - // cos([a, b]) = [cosh(a), cos(b)] - deps.m_lower_deps = DEP_IN_LOWER1; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - if (numeric_traits::is_neg(m_upper) || numeric_traits::is_zero(m_upper)) { - // [a, b] where a <= b < 0 - if (compute_intv) { - std::swap(m_lower, m_upper); - numeric_traits::set_rounding(false); - numeric_traits::cosh(m_lower); - numeric_traits::set_rounding(true); - numeric_traits::cosh(m_upper); - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - deps.m_upper_deps = DEP_IN_LOWER1; - } - return; - } - // [a, b] where a < 0 < b - if (m_lower + m_upper < 0.0) { - if (compute_intv) { - m_upper = m_lower; - } - } else { - // Nothing - } - if (compute_intv) { - m_lower = 1.0; - m_lower_open = false; - numeric_traits::set_rounding(true); - numeric_traits::cosh(m_upper); - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_upper_deps = 0; - deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1; - } - return; - } - if (lower_kind() == XN_NUMERAL) { - // [c, +oo] - lean_assert(upper_kind() == XN_PLUS_INFINITY); - if (numeric_traits::is_pos(m_lower)) { - // [c, +oo] where 0 < c < +oo - if (compute_intv) { - numeric_traits::set_rounding(false); - numeric_traits::cosh(m_lower); - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - deps.m_upper_deps = 0; - } - return; - } else { - // [c, +oo] where c <= 0 < +oo - if (compute_intv) { - m_lower = 1.0; - m_lower_open = false; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = deps.m_upper_deps = 0; - } - return; - } - } - if (upper_kind() == XN_NUMERAL) { - // [-oo, c] - lean_assert(lower_kind() == XN_MINUS_INFINITY); - if (compute_intv) { - m_upper_inf = true; - m_upper_open = true; - } - if (numeric_traits::is_pos(m_upper)) { - // [-oo, c] where -oo < 0 < c - if (compute_intv) { - m_lower = 1.0; - m_lower_open = false; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = deps.m_upper_deps = 0; - } - return; - } else { - // [-oo, c] where -oo < c <= 0 - if (compute_intv) { - m_lower = m_upper; - numeric_traits::set_rounding(false); - numeric_traits::cosh(m_lower); - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_UPPER1; - deps.m_upper_deps = 0; - } - return; - } - } - lean_assert(lower_kind() == XN_MINUS_INFINITY && upper_kind() == XN_PLUS_INFINITY); - // cosh((-oo, +oo)) = [1.0, +oo) - if (compute_intv) { - m_upper_open = true; - m_upper_inf = true; - m_lower = 1.0; - m_lower_open = false; - m_lower_inf = false; - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = 0; - deps.m_upper_deps = 0; - } - return; -} - -template -template -void interval::tanh (interval_deps & deps) { - if (compute_deps) { - deps.m_lower_deps = deps.m_upper_deps = 0; - } - - if (lower_kind() == XN_NUMERAL) { - if (compute_intv) { - numeric_traits::set_rounding(true); - m_lower = -m_lower; - numeric_traits::tanh(m_lower); - m_lower = -m_lower; - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } - if (upper_kind() == XN_NUMERAL) { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::tanh(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } - if (compute_intv) { - lean_assert(check_invariant()); - } - return; -} - -template -template -void interval::asinh(interval_deps & deps) { - if (compute_deps) { - deps.m_lower_deps = deps.m_upper_deps = 0; - } - if (lower_kind() == XN_NUMERAL) { - if (compute_intv) { - numeric_traits::set_rounding(true); - m_lower = -m_lower; - numeric_traits::asinh(m_lower); - m_lower = -m_lower; - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - } - if (upper_kind() == XN_NUMERAL) { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::asinh(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } - if (compute_intv) { - lean_assert(check_invariant()); - } - return; -} - -template -template -void interval::acosh(interval_deps & deps) { - lean_assert(lower_kind() == XN_NUMERAL && m_lower >= 1.0); - if (compute_intv) { - numeric_traits::set_rounding(false); - numeric_traits::acosh(m_lower); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - } - if (upper_kind() == XN_NUMERAL) { - if (compute_intv) { - numeric_traits::set_rounding(true); - numeric_traits::acosh(m_upper); - } - if (compute_deps) { - deps.m_upper_deps = DEP_IN_UPPER1; - } - } else { - // upper_kind() == +oo - if (compute_deps) { - deps.m_upper_deps = 0; - } - } - if (compute_intv) { - lean_assert(check_invariant()); - } - return; -} - -template -template -void interval::atanh(interval_deps & deps) { - lean_assert(lower_kind() == XN_NUMERAL && m_lower >= -1.0); - lean_assert(upper_kind() == XN_NUMERAL && m_upper <= 1.0); - - if (compute_intv) { - numeric_traits::set_rounding(true); - m_lower = -m_lower; - numeric_traits::atanh(m_lower); - m_lower = -m_lower; - numeric_traits::set_rounding(true); - numeric_traits::atanh(m_upper); - lean_assert(check_invariant()); - } - if (compute_deps) { - deps.m_lower_deps = DEP_IN_LOWER1; - deps.m_upper_deps = DEP_IN_UPPER1; - } - return; -} - -template void interval::exp_jst(interval_deps & deps) { - exp(deps); - return; -} -template void interval::exp2_jst(interval_deps & deps) { - exp2(deps); - return; -} -template void interval::exp10_jst(interval_deps & deps) { - exp10(deps); - return; -} -template void interval::log_jst(interval_deps & deps) { - log(deps); - return; -} -template void interval::log2_jst(interval_deps & deps) { - log2(deps); - return; -} -template void interval::log10_jst(interval_deps & deps) { - log10(deps); - return; -} -template void interval::sin_jst(interval_deps & deps) { - sin(deps); - return; -} -template void interval::cos_jst(interval_deps & deps) { - cos(deps); - return; -} -template void interval::tan_jst(interval_deps & deps) { - tan(deps); - return; -} -template void interval::csc_jst(interval_deps & deps) { - csc(deps); - return; -} -template void interval::sec_jst(interval_deps & deps) { - sec(deps); - return; -} -template void interval::cot_jst(interval_deps & deps) { - cot(deps); - return; -} -template void interval::asin_jst(interval_deps & deps) { - asin(deps); - return; -} -template void interval::acos_jst(interval_deps & deps) { - acos(deps); - return; -} -template void interval::atan_jst(interval_deps & deps) { - atan(deps); - return; -} -template void interval::sinh_jst(interval_deps & deps) { - sinh(deps); - return; -} -template void interval::cosh_jst(interval_deps & deps) { - cosh(deps); - return; -} -template void interval::tanh_jst(interval_deps & deps) { - tanh(deps); - return; -} -template void interval::asinh_jst(interval_deps & deps) { - asinh(deps); - return; -} -template void interval::acosh_jst(interval_deps & deps) { - acosh(deps); - return; -} -template void interval::atanh_jst(interval_deps & deps) { - atanh(deps); - return; -} -} diff --git a/src/util/interval/interval.h b/src/util/interval/interval.h deleted file mode 100644 index 914b5a3b74..0000000000 --- a/src/util/interval/interval.h +++ /dev/null @@ -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 -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::set_rounding(true); } - static void round_to_minus_inf() { numeric_traits::set_rounding(false); } - static void reset(T & v) { numeric_traits::reset(v); } - static void inv(T & v) { numeric_traits::inv(v); } - static void neg(T & v) { numeric_traits::neg(v); } - static bool is_zero(T const & v) { return numeric_traits::is_zero(v); } - static void power(T & v, unsigned k) { return numeric_traits::power(v, k); } - void _swap(interval & b); - bool _eq(interval const & b) const; - -public: - template 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 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 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 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 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 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 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 void set_lower(T2 const & n) { m_lower = n; } - template 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 void neg(interval_deps & deps = dummy); - void neg_jst(interval_deps & deps) { neg(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 - interval & add(interval const & o, interval_deps & deps = dummy); - template - interval & sub(interval const & o, interval_deps & deps = dummy); - template - interval & mul(interval const & o, interval_deps & deps = dummy); - template - 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 void inv(interval_deps & deps = dummy); - void inv_jst (interval_deps & deps) { inv(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 - 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 void exp(interval_deps & deps = dummy); - template void exp2(interval_deps & deps = dummy); - template void exp10(interval_deps & deps = dummy); - template void log(interval_deps & deps = dummy); - template void log2(interval_deps & deps = dummy); - template void log10(interval_deps & deps = dummy); - template void sin(interval_deps & deps = dummy); - template void cos(interval_deps & deps = dummy); - template void tan(interval_deps & deps = dummy); - template void csc(interval_deps & deps = dummy); - template void sec(interval_deps & deps = dummy); - template void cot(interval_deps & deps = dummy); - template void asin(interval_deps & deps = dummy); - template void acos(interval_deps & deps = dummy); - template void atan(interval_deps & deps = dummy); - template void sinh(interval_deps & deps = dummy); - template void cosh(interval_deps & deps = dummy); - template void tanh(interval_deps & deps = dummy); - template void asinh(interval_deps & deps = dummy); - template void acosh(interval_deps & deps = dummy); - template 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; - } -}; - -} diff --git a/src/util/interval/interval_instances.cpp b/src/util/interval/interval_instances.cpp deleted file mode 100644 index 0c8f6ecff9..0000000000 --- a/src/util/interval/interval_instances.cpp +++ /dev/null @@ -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; -template void interval::neg(interval_deps &); -template void interval::neg(interval_deps &); -template void interval::inv(interval_deps &); -template void interval::power(unsigned, interval_deps &); - -template class interval; -template void interval::neg(interval_deps &); -template void interval::inv(interval_deps &); -template void interval::power(unsigned, interval_deps &); -template void interval::exp(interval_deps &); -template void interval::exp2(interval_deps &); -template void interval::exp10(interval_deps &); -template void interval::log(interval_deps &); -template void interval::log2(interval_deps &); -template void interval::log10(interval_deps &); -template void interval::sin(interval_deps &); -template void interval::cos(interval_deps &); -template void interval::tan(interval_deps &); -template void interval::asin(interval_deps &); -template void interval::acos(interval_deps &); -template void interval::atan(interval_deps &); -template void interval::sinh(interval_deps &); -template void interval::cosh(interval_deps &); -template void interval::tanh(interval_deps &); -template void interval::csc(interval_deps &); -template void interval::sec(interval_deps &); -template void interval::cot(interval_deps &); -template void interval::asinh(interval_deps &); -template void interval::acosh(interval_deps &); -template void interval::atanh(interval_deps &); - -template class interval; -template void interval::neg(interval_deps &); -template void interval::inv(interval_deps &); -template void interval::power(unsigned, interval_deps &); -template void interval::exp(interval_deps &); -template void interval::exp2(interval_deps &); -template void interval::exp10(interval_deps &); -template void interval::log(interval_deps &); -template void interval::log2(interval_deps &); -template void interval::log10(interval_deps &); -template void interval::sin(interval_deps &); -template void interval::cos(interval_deps &); -template void interval::tan(interval_deps &); -template void interval::asin(interval_deps &); -template void interval::acos(interval_deps &); -template void interval::atan(interval_deps &); -template void interval::sinh(interval_deps &); -template void interval::cosh(interval_deps &); -template void interval::tanh(interval_deps &); -template void interval::csc(interval_deps &); -template void interval::sec(interval_deps &); -template void interval::cot(interval_deps &); -template void interval::asinh(interval_deps &); -template void interval::acosh(interval_deps &); -template void interval::atanh(interval_deps &); - -template class interval; -template void interval::neg(interval_deps &); -template void interval::inv(interval_deps &); -template void interval::power(unsigned, interval_deps &); -template void interval::exp(interval_deps &); -template void interval::exp2(interval_deps &); -template void interval::exp10(interval_deps &); -template void interval::log(interval_deps &); -template void interval::log2(interval_deps &); -template void interval::log10(interval_deps &); -template void interval::sin(interval_deps &); -template void interval::cos(interval_deps &); -template void interval::tan(interval_deps &); -template void interval::asin(interval_deps &); -template void interval::acos(interval_deps &); -template void interval::atan(interval_deps &); -template void interval::sinh(interval_deps &); -template void interval::cosh(interval_deps &); -template void interval::tanh(interval_deps &); -template void interval::csc(interval_deps &); -template void interval::sec(interval_deps &); -template void interval::cot(interval_deps &); -template void interval::asinh(interval_deps &); -template void interval::acosh(interval_deps &); -template void interval::atanh(interval_deps &); -} - -void print(lean::interval const & i) { std::cout << i << std::endl; } -void print(lean::interval const & i) { std::cout << i << std::endl; } diff --git a/src/util/numerics/CMakeLists.txt b/src/util/numerics/CMakeLists.txt index 2006ed0ee6..1819d63feb 100644 --- a/src/util/numerics/CMakeLists.txt +++ b/src/util/numerics/CMakeLists.txt @@ -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) diff --git a/src/util/numerics/double.cpp b/src/util/numerics/double.cpp index 143852064d..727fba68bd 100644 --- a/src/util/numerics/double.cpp +++ b/src/util/numerics/double.cpp @@ -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::g_zero = 0.0; double numeric_traits::g_one = 1.0; + +double numeric_traits::log(double d) { + return std::log(d); +} }; diff --git a/src/util/numerics/double.h b/src/util/numerics/double.h index 45847fab54..67719732ad 100644 --- a/src/util/numerics/double.h +++ b/src/util/numerics/double.h @@ -6,11 +6,9 @@ Author: Soonho Kong */ #pragma once #include -#include -#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 { 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); }; } diff --git a/src/util/numerics/float.cpp b/src/util/numerics/float.cpp index d66af90006..07f96b7800 100644 --- a/src/util/numerics/float.cpp +++ b/src/util/numerics/float.cpp @@ -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); } diff --git a/src/util/numerics/float.h b/src/util/numerics/float.h index bf70d5faaf..aaf2c83e7c 100644 --- a/src/util/numerics/float.h +++ b/src/util/numerics/float.h @@ -6,11 +6,9 @@ Author: Soonho Kong */ #pragma once #include -#include -#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 { 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()); } }; } diff --git a/src/util/numerics/init_module.cpp b/src/util/numerics/init_module.cpp index 8fe04a1489..3b4eabe11f 100644 --- a/src/util/numerics/init_module.cpp +++ b/src/util/numerics/init_module.cpp @@ -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(); diff --git a/src/util/numerics/mpfp.h b/src/util/numerics/mpfp.h deleted file mode 100644 index ab9f9deb1b..0000000000 --- a/src/util/numerics/mpfp.h +++ /dev/null @@ -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 -#include -#include -#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; - 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(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 { -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(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(); -} diff --git a/src/util/numerics/numeric_traits.h b/src/util/numerics/numeric_traits.h index 53633c5909..978dfa8c0a 100644 --- a/src/util/numerics/numeric_traits.h +++ b/src/util/numerics/numeric_traits.h @@ -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); - }