From 49b8bde67cb2530a8963edaab651154763b8bad3 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Wed, 14 Aug 2013 12:08:24 -0700 Subject: [PATCH] Add asin, acos, atan, sinh, cosh, tanh to interval --- src/interval/interval.h | 1 + src/interval/interval_def.h | 148 +++++++++++++++++++++++++++++++++--- 2 files changed, 140 insertions(+), 9 deletions(-) diff --git a/src/interval/interval.h b/src/interval/interval.h index 58f60c141..71747f2f3 100644 --- a/src/interval/interval.h +++ b/src/interval/interval.h @@ -3,6 +3,7 @@ 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 "numeric_traits.h" diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h index f4ea08210..050c69589 100644 --- a/src/interval/interval_def.h +++ b/src/interval/interval_def.h @@ -3,6 +3,7 @@ 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 @@ -12,7 +13,6 @@ Author: Leonardo de Moura #include "trace.h" #include "mpz.h" - namespace lean { template @@ -398,7 +398,7 @@ interval & interval::operator*=(interval const & o) { mul(new_u_val, new_u_kind, b, b_k, d, d_k); } else { lean_assert(i2.is_P()); - // 0 <= a <= x, 0 <= c <= y --> a*c <= x*y + // 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)) set_is_lower_open((i1.is_P0() || i2.is_P0()) ? false : a_o || c_o); @@ -1105,14 +1105,144 @@ template void interval::tan() { template void interval::sec () { /* TODO */ lean_unreachable(); return; } template void interval::csc () { /* TODO */ lean_unreachable(); return; } template void interval::cot () { /* TODO */ lean_unreachable(); return; } -template void interval::asin () { /* TODO */ lean_unreachable(); return; } -template void interval::acos () { /* TODO */ lean_unreachable(); return; } -template void interval::atan () { /* TODO */ lean_unreachable(); return; } -template void interval::sinh () { /* TODO */ lean_unreachable(); return; } -template void interval::cosh () { /* TODO */ lean_unreachable(); return; } -template void interval::tanh () { /* TODO */ lean_unreachable(); return; } +template void interval::asin () { + lean_assert(lower_kind() == XN_NUMERAL && upper_kind() == XN_NUMERAL); + lean_assert(-1.0 <= m_lower && m_upper <= 1.0); + numeric_traits::set_rounding(false); + numeric_traits::asin(m_lower); + numeric_traits::set_rounding(true); + numeric_traits::asin(m_upper); + lean_assert(check_invariant()); + return; +} +template void interval::acos () { + lean_assert(lower_kind() == XN_NUMERAL && upper_kind() == XN_NUMERAL); + lean_assert(-1.0 <= m_lower && m_upper <= 1.0); + 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()); + return; +} +template void interval::atan () { + if(lower_kind() == XN_MINUS_INFINITY) { + m_lower = -1.0; + m_lower_open = false; + m_lower_inf = false; + } else { + numeric_traits::set_rounding(false); + numeric_traits::atan(m_lower); + } + + if(upper_kind() == XN_MINUS_INFINITY) { + m_upper = 1.0; + m_upper_open = false; + m_upper_inf = false; + } else { + numeric_traits::set_rounding(true); + numeric_traits::atan(m_upper); + } + lean_assert(check_invariant()); + return; +} +template void interval::sinh () { + if(lower_kind() == XN_NUMERAL) { + numeric_traits::set_rounding(false); + numeric_traits::sinh(m_lower); + } + if(upper_kind() == XN_NUMERAL) { + numeric_traits::set_rounding(true); + numeric_traits::sinh(m_upper); + } + lean_assert(check_invariant()); + return; +} +template void interval::cosh () { + 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 + numeric_traits::set_rounding(false); + numeric_traits::cosh(m_lower); + numeric_traits::set_rounding(true); + numeric_traits::cosh(m_lower); + lean_assert(check_invariant()); + return; + } + if(numeric_traits::is_neg(m_upper) || numeric_traits::is_zero(m_upper)) { + // [a, b] where a <= b < 0 + numeric_traits::set_rounding(true); + numeric_traits::cosh(m_lower); + numeric_traits::set_rounding(false); + numeric_traits::cosh(m_lower); + std::swap(m_lower, m_upper); + lean_assert(check_invariant()); + return; + } + // [a,b] where a < 0 < b + m_lower = 0.0; + m_lower_open = false; + m_upper = m_upper > m_lower ? m_upper : m_lower; + numeric_traits::set_rounding(true); + numeric_traits::cosh(m_upper); + lean_assert(check_invariant()); + return; + } + if(lower_kind() == XN_NUMERAL) { + m_upper_open = false; + m_upper_inf = true; + // [-oo, c] + if(numeric_traits::is_neg(m_upper)) { + m_lower = m_upper; + numeric_traits::set_rounding(false); + numeric_traits::cosh(m_lower); + lean_assert(check_invariant()); + return; + } else { + m_lower = 0.0; + m_lower_open = false; + lean_assert(check_invariant()); + return; + } + } + if(upper_kind() == XN_NUMERAL) { + // [c,+oo] + if(numeric_traits::is_neg(m_upper)) { + m_lower = 0.0; + m_lower_open = false; + lean_assert(check_invariant()); + return; + } else { + numeric_traits::set_rounding(false); + numeric_traits::cosh(m_lower); + lean_assert(check_invariant()); + return; + } + } + lean_assert(lower_kind() == XN_MINUS_INFINITY && upper_kind() == XN_PLUS_INFINITY); + // cosh((-oo, +oo)) = [0, +oo) + m_upper_open = true; + m_upper_inf = true; + m_lower = 0.0; + m_lower_open = false; + m_lower_inf = false; + lean_assert(check_invariant()); + return; +} +template void interval::tanh () { + if(lower_kind() == XN_NUMERAL) { + numeric_traits::set_rounding(false); + numeric_traits::tanh(m_lower); + } + if(upper_kind() == XN_NUMERAL) { + numeric_traits::set_rounding(true); + numeric_traits::tanh(m_upper); + } + lean_assert(check_invariant()); + return; +} template void interval::asinh() { /* TODO */ lean_unreachable(); return; } template void interval::acosh() { /* TODO */ lean_unreachable(); return; } template void interval::atanh() { /* TODO */ lean_unreachable(); return; } - }