From c5db989e385d2454267b3d8c8692c83f2bbb32ca Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Thu, 15 Aug 2013 14:38:50 -0700 Subject: [PATCH] Add csc, sec, cot to interval & add tests for them --- src/interval/interval.h | 4 +- src/interval/interval_def.h | 144 ++++++++++++++++++++++++- src/tests/interval/double_interval.cpp | 111 +++++++++++++++++++ src/tests/interval/float_interval.cpp | 111 +++++++++++++++++++ src/tests/interval/mpfp_interval.cpp | 111 +++++++++++++++++++ 5 files changed, 476 insertions(+), 5 deletions(-) diff --git a/src/interval/interval.h b/src/interval/interval.h index 28f51a138..163a3c74d 100644 --- a/src/interval/interval.h +++ b/src/interval/interval.h @@ -168,8 +168,8 @@ public: void sin (); void cos (); void tan (); - void sec (); void csc (); + void sec (); void cot (); void asin (); void acos (); @@ -191,8 +191,8 @@ public: friend interval sin (interval o) { o.sin(); return o; } friend interval cos (interval o) { o.cos(); return o; } friend interval tan (interval o) { o.tan(); return o; } - friend interval sec (interval o) { o.sec(); return o; } friend interval csc (interval o) { o.csc(); return o; } + friend interval sec (interval o) { o.sec(); return o; } friend interval cot (interval o) { o.cot(); return o; } friend interval asin (interval o) { o.asin(); return o; } friend interval acos (interval o) { o.acos(); return o; } diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h index 9842d2418..91d95b5bf 100644 --- a/src/interval/interval_def.h +++ b/src/interval/interval_def.h @@ -1250,9 +1250,147 @@ 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::csc () { + // 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] + 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()); + return; + } + fmod(interval(numeric_traits::pi_twice_lower(), numeric_traits::pi_twice_upper())); + if(m_upper > numeric_traits::pi_twice() || + (m_lower < numeric_traits::pi() && numeric_traits::pi() < m_upper)) { + // l < 2pi < u or l < pi < u + // then the result = [-oo, +oo] + 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()); + return; + } + + if (m_lower <= numeric_traits::pi_half()) { + if (m_upper <= numeric_traits::pi_half()) { + // l <= u <= 1/2 pi + // csc[l, u] = [csc(u), csc(l)] + std::swap(m_lower, m_upper); + numeric_traits::set_rounding(false); + numeric_traits::csc(m_lower); + numeric_traits::set_rounding(true); + numeric_traits::csc(m_upper); + lean_assert(check_invariant()); + return; + } + if (m_upper <= numeric_traits::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 < numeric_traits::pi()) { + m_upper = m_lower; + } else { + // Nothing + } + m_lower = 1.0; + numeric_traits::set_rounding(true); + numeric_traits::csc(m_upper); + lean_assert(check_invariant()); + return; + } + lean_unreachable(); + return; + } + + if (m_lower <= numeric_traits::pi() && m_upper <= numeric_traits::pi()) { + // l <= u <= pi + // csc[l, u] = [csc(l), csc(u)] + numeric_traits::set_rounding(false); + numeric_traits::csc(m_lower); + numeric_traits::set_rounding(true); + numeric_traits::csc(m_upper); + lean_assert(check_invariant()); + return; + } + if (m_lower <= numeric_traits::pi() + numeric_traits::pi_half()) { + if (m_upper <= numeric_traits::pi() + numeric_traits::pi_half()) { + // l <= u <= 3/2 pi + // csc[l, u] = [csc(l), csc(u)] + numeric_traits::set_rounding(false); + numeric_traits::csc(m_lower); + numeric_traits::set_rounding(true); + numeric_traits::csc(m_upper); + lean_assert(check_invariant()); + 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 + if (m_lower + m_upper < numeric_traits::pi() + numeric_traits::pi_twice()) { + // Nothing + } else { + m_lower = m_upper; + } + m_upper = -1.0; + numeric_traits::set_rounding(false); + numeric_traits::csc(m_lower); + lean_assert(check_invariant()); + return; + } + // 3/2pi <= l <= u < 2pi + lean_assert(numeric_traits::pi_half() + numeric_traits::pi() < m_lower); + lean_assert(m_upper < numeric_traits::pi_twice()); + std::swap(m_lower, m_upper); + numeric_traits::set_rounding(false); + numeric_traits::csc(m_lower); + numeric_traits::set_rounding(true); + numeric_traits::csc(m_upper); + lean_assert(check_invariant()); + return; +} + +template void interval::sec () { + *this += numeric_traits::pi_half(); + csc(); + return; +} + +template void interval::cot () { + if(m_lower_inf || m_upper_inf) { + // cot([-oo, c]) = [-oo, +oo] + // cot([c, +oo]) = [-oo, +oo] + 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()); + return; + } + fmod(interval(numeric_traits::pi_lower(), numeric_traits::pi_upper())); + if (m_upper >= numeric_traits::pi()) { + 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()); + return; + } + std::swap(m_lower, m_upper); + numeric_traits::set_rounding(false); + numeric_traits::cot(m_lower); + numeric_traits::set_rounding(true); + numeric_traits::cot(m_upper); + lean_assert(check_invariant()); + 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); diff --git a/src/tests/interval/double_interval.cpp b/src/tests/interval/double_interval.cpp index 6ad14eee8..abbd72125 100644 --- a/src/tests/interval/double_interval.cpp +++ b/src/tests/interval/double_interval.cpp @@ -855,6 +855,117 @@ static void double_interval_trans() { check_uop(double, tanh, ozero_ninf); check_uop(double, tanh, czero_pinf); check_uop(double, tanh, czero_ninf); + + cout << "=====================" << endl; + check_uop(double, csc, i1); + check_uop(double, csc, i2); + check_uop(double, csc, i3); + check_uop(double, csc, i4); + check_uop(double, csc, i5); + check_uop(double, csc, i6); + check_uop(double, csc, i7); + check_uop(double, csc, i8); + check_uop(double, csc, i9); + check_uop(double, csc, i10); + check_uop(double, csc, i11); + check_uop(double, csc, i12); + check_uop(double, csc, i13); + check_uop(double, csc, i14); + check_uop(double, csc, i15); + check_uop(double, csc, oi1); + check_uop(double, csc, oi2); + check_uop(double, csc, oi3); + check_uop(double, csc, oi4); + check_uop(double, csc, oi5); + check_uop(double, csc, oi6); + check_uop(double, csc, oi7); + check_uop(double, csc, oi8); + check_uop(double, csc, oi9); + check_uop(double, csc, oi10); + check_uop(double, csc, oi11); + check_uop(double, csc, oi12); + check_uop(double, csc, oi13); + check_uop(double, csc, oi14); + check_uop(double, csc, oi15); + check_uop(double, csc, inf); + check_uop(double, csc, ozero_pinf); + check_uop(double, csc, ozero_ninf); + check_uop(double, csc, czero_pinf); + check_uop(double, csc, czero_ninf); + + cout << "=====================" << endl; + check_uop(double, sec, i1); + check_uop(double, sec, i2); + check_uop(double, sec, i3); + check_uop(double, sec, i4); + check_uop(double, sec, i5); + check_uop(double, sec, i6); + check_uop(double, sec, i7); + check_uop(double, sec, i8); + check_uop(double, sec, i9); + check_uop(double, sec, i10); + check_uop(double, sec, i11); + check_uop(double, sec, i12); + check_uop(double, sec, i13); + check_uop(double, sec, i14); + check_uop(double, sec, i15); + check_uop(double, sec, oi1); + check_uop(double, sec, oi2); + check_uop(double, sec, oi3); + check_uop(double, sec, oi4); + check_uop(double, sec, oi5); + check_uop(double, sec, oi6); + check_uop(double, sec, oi7); + check_uop(double, sec, oi8); + check_uop(double, sec, oi9); + check_uop(double, sec, oi10); + check_uop(double, sec, oi11); + check_uop(double, sec, oi12); + check_uop(double, sec, oi13); + check_uop(double, sec, oi14); + check_uop(double, sec, oi15); + check_uop(double, sec, inf); + check_uop(double, sec, ozero_pinf); + check_uop(double, sec, ozero_ninf); + check_uop(double, sec, czero_pinf); + check_uop(double, sec, czero_ninf); + + cout << "=====================" << endl; + check_uop(double, cot, i1); + check_uop(double, cot, i2); + check_uop(double, cot, i3); + check_uop(double, cot, i4); + check_uop(double, cot, i5); + check_uop(double, cot, i6); + check_uop(double, cot, i7); + check_uop(double, cot, i8); + check_uop(double, cot, i9); + check_uop(double, cot, i10); + check_uop(double, cot, i11); + check_uop(double, cot, i12); + check_uop(double, cot, i13); + check_uop(double, cot, i14); + check_uop(double, cot, i15); + check_uop(double, cot, oi1); + check_uop(double, cot, oi2); + check_uop(double, cot, oi3); + check_uop(double, cot, oi4); + check_uop(double, cot, oi5); + check_uop(double, cot, oi6); + check_uop(double, cot, oi7); + check_uop(double, cot, oi8); + check_uop(double, cot, oi9); + check_uop(double, cot, oi10); + check_uop(double, cot, oi11); + check_uop(double, cot, oi12); + check_uop(double, cot, oi13); + check_uop(double, cot, oi14); + check_uop(double, cot, oi15); + check_uop(double, cot, inf); + check_uop(double, cot, ozero_pinf); + check_uop(double, cot, ozero_ninf); + check_uop(double, cot, czero_pinf); + check_uop(double, cot, czero_ninf); } int main() { diff --git a/src/tests/interval/float_interval.cpp b/src/tests/interval/float_interval.cpp index 211836a9e..8bb0f3746 100644 --- a/src/tests/interval/float_interval.cpp +++ b/src/tests/interval/float_interval.cpp @@ -855,6 +855,117 @@ static void float_interval_trans() { check_uop(float, tanh, ozero_ninf); check_uop(float, tanh, czero_pinf); check_uop(float, tanh, czero_ninf); + + cout << "=====================" << endl; + check_uop(float, csc, i1); + check_uop(float, csc, i2); + check_uop(float, csc, i3); + check_uop(float, csc, i4); + check_uop(float, csc, i5); + check_uop(float, csc, i6); + check_uop(float, csc, i7); + check_uop(float, csc, i8); + check_uop(float, csc, i9); + check_uop(float, csc, i10); + check_uop(float, csc, i11); + check_uop(float, csc, i12); + check_uop(float, csc, i13); + check_uop(float, csc, i14); + check_uop(float, csc, i15); + check_uop(float, csc, oi1); + check_uop(float, csc, oi2); + check_uop(float, csc, oi3); + check_uop(float, csc, oi4); + check_uop(float, csc, oi5); + check_uop(float, csc, oi6); + check_uop(float, csc, oi7); + check_uop(float, csc, oi8); + check_uop(float, csc, oi9); + check_uop(float, csc, oi10); + check_uop(float, csc, oi11); + check_uop(float, csc, oi12); + check_uop(float, csc, oi13); + check_uop(float, csc, oi14); + check_uop(float, csc, oi15); + check_uop(float, csc, inf); + check_uop(float, csc, ozero_pinf); + check_uop(float, csc, ozero_ninf); + check_uop(float, csc, czero_pinf); + check_uop(float, csc, czero_ninf); + + cout << "=====================" << endl; + check_uop(float, sec, i1); + check_uop(float, sec, i2); + check_uop(float, sec, i3); + check_uop(float, sec, i4); + check_uop(float, sec, i5); + check_uop(float, sec, i6); + check_uop(float, sec, i7); + check_uop(float, sec, i8); + check_uop(float, sec, i9); + check_uop(float, sec, i10); + check_uop(float, sec, i11); + check_uop(float, sec, i12); + check_uop(float, sec, i13); + check_uop(float, sec, i14); + check_uop(float, sec, i15); + check_uop(float, sec, oi1); + check_uop(float, sec, oi2); + check_uop(float, sec, oi3); + check_uop(float, sec, oi4); + check_uop(float, sec, oi5); + check_uop(float, sec, oi6); + check_uop(float, sec, oi7); + check_uop(float, sec, oi8); + check_uop(float, sec, oi9); + check_uop(float, sec, oi10); + check_uop(float, sec, oi11); + check_uop(float, sec, oi12); + check_uop(float, sec, oi13); + check_uop(float, sec, oi14); + check_uop(float, sec, oi15); + check_uop(float, sec, inf); + check_uop(float, sec, ozero_pinf); + check_uop(float, sec, ozero_ninf); + check_uop(float, sec, czero_pinf); + check_uop(float, sec, czero_ninf); + + cout << "=====================" << endl; + check_uop(float, cot, i1); + check_uop(float, cot, i2); + check_uop(float, cot, i3); + check_uop(float, cot, i4); + check_uop(float, cot, i5); + check_uop(float, cot, i6); + check_uop(float, cot, i7); + check_uop(float, cot, i8); + check_uop(float, cot, i9); + check_uop(float, cot, i10); + check_uop(float, cot, i11); + check_uop(float, cot, i12); + check_uop(float, cot, i13); + check_uop(float, cot, i14); + check_uop(float, cot, i15); + check_uop(float, cot, oi1); + check_uop(float, cot, oi2); + check_uop(float, cot, oi3); + check_uop(float, cot, oi4); + check_uop(float, cot, oi5); + check_uop(float, cot, oi6); + check_uop(float, cot, oi7); + check_uop(float, cot, oi8); + check_uop(float, cot, oi9); + check_uop(float, cot, oi10); + check_uop(float, cot, oi11); + check_uop(float, cot, oi12); + check_uop(float, cot, oi13); + check_uop(float, cot, oi14); + check_uop(float, cot, oi15); + check_uop(float, cot, inf); + check_uop(float, cot, ozero_pinf); + check_uop(float, cot, ozero_ninf); + check_uop(float, cot, czero_pinf); + check_uop(float, cot, czero_ninf); } int main() { diff --git a/src/tests/interval/mpfp_interval.cpp b/src/tests/interval/mpfp_interval.cpp index b48188a57..27bf2c4b9 100644 --- a/src/tests/interval/mpfp_interval.cpp +++ b/src/tests/interval/mpfp_interval.cpp @@ -855,6 +855,117 @@ static void mpfp_interval_trans() { check_uop(mpfp, tanh, ozero_ninf); check_uop(mpfp, tanh, czero_pinf); check_uop(mpfp, tanh, czero_ninf); + + cout << "=====================" << endl; + check_uop(mpfp, csc, i1); + check_uop(mpfp, csc, i2); + check_uop(mpfp, csc, i3); + check_uop(mpfp, csc, i4); + check_uop(mpfp, csc, i5); + check_uop(mpfp, csc, i6); + check_uop(mpfp, csc, i7); + check_uop(mpfp, csc, i8); + check_uop(mpfp, csc, i9); + check_uop(mpfp, csc, i10); + check_uop(mpfp, csc, i11); + check_uop(mpfp, csc, i12); + check_uop(mpfp, csc, i13); + check_uop(mpfp, csc, i14); + check_uop(mpfp, csc, i15); + check_uop(mpfp, csc, oi1); + check_uop(mpfp, csc, oi2); + check_uop(mpfp, csc, oi3); + check_uop(mpfp, csc, oi4); + check_uop(mpfp, csc, oi5); + check_uop(mpfp, csc, oi6); + check_uop(mpfp, csc, oi7); + check_uop(mpfp, csc, oi8); + check_uop(mpfp, csc, oi9); + check_uop(mpfp, csc, oi10); + check_uop(mpfp, csc, oi11); + check_uop(mpfp, csc, oi12); + check_uop(mpfp, csc, oi13); + check_uop(mpfp, csc, oi14); + check_uop(mpfp, csc, oi15); + check_uop(mpfp, csc, inf); + check_uop(mpfp, csc, ozero_pinf); + check_uop(mpfp, csc, ozero_ninf); + check_uop(mpfp, csc, czero_pinf); + check_uop(mpfp, csc, czero_ninf); + + cout << "=====================" << endl; + check_uop(mpfp, sec, i1); + check_uop(mpfp, sec, i2); + check_uop(mpfp, sec, i3); + check_uop(mpfp, sec, i4); + check_uop(mpfp, sec, i5); + check_uop(mpfp, sec, i6); + check_uop(mpfp, sec, i7); + check_uop(mpfp, sec, i8); + check_uop(mpfp, sec, i9); + check_uop(mpfp, sec, i10); + check_uop(mpfp, sec, i11); + check_uop(mpfp, sec, i12); + check_uop(mpfp, sec, i13); + check_uop(mpfp, sec, i14); + check_uop(mpfp, sec, i15); + check_uop(mpfp, sec, oi1); + check_uop(mpfp, sec, oi2); + check_uop(mpfp, sec, oi3); + check_uop(mpfp, sec, oi4); + check_uop(mpfp, sec, oi5); + check_uop(mpfp, sec, oi6); + check_uop(mpfp, sec, oi7); + check_uop(mpfp, sec, oi8); + check_uop(mpfp, sec, oi9); + check_uop(mpfp, sec, oi10); + check_uop(mpfp, sec, oi11); + check_uop(mpfp, sec, oi12); + check_uop(mpfp, sec, oi13); + check_uop(mpfp, sec, oi14); + check_uop(mpfp, sec, oi15); + check_uop(mpfp, sec, inf); + check_uop(mpfp, sec, ozero_pinf); + check_uop(mpfp, sec, ozero_ninf); + check_uop(mpfp, sec, czero_pinf); + check_uop(mpfp, sec, czero_ninf); + + cout << "=====================" << endl; + check_uop(mpfp, cot, i1); + check_uop(mpfp, cot, i2); + check_uop(mpfp, cot, i3); + check_uop(mpfp, cot, i4); + check_uop(mpfp, cot, i5); + check_uop(mpfp, cot, i6); + check_uop(mpfp, cot, i7); + check_uop(mpfp, cot, i8); + check_uop(mpfp, cot, i9); + check_uop(mpfp, cot, i10); + check_uop(mpfp, cot, i11); + check_uop(mpfp, cot, i12); + check_uop(mpfp, cot, i13); + check_uop(mpfp, cot, i14); + check_uop(mpfp, cot, i15); + check_uop(mpfp, cot, oi1); + check_uop(mpfp, cot, oi2); + check_uop(mpfp, cot, oi3); + check_uop(mpfp, cot, oi4); + check_uop(mpfp, cot, oi5); + check_uop(mpfp, cot, oi6); + check_uop(mpfp, cot, oi7); + check_uop(mpfp, cot, oi8); + check_uop(mpfp, cot, oi9); + check_uop(mpfp, cot, oi10); + check_uop(mpfp, cot, oi11); + check_uop(mpfp, cot, oi12); + check_uop(mpfp, cot, oi13); + check_uop(mpfp, cot, oi14); + check_uop(mpfp, cot, oi15); + check_uop(mpfp, cot, inf); + check_uop(mpfp, cot, ozero_pinf); + check_uop(mpfp, cot, ozero_ninf); + check_uop(mpfp, cot, czero_pinf); + check_uop(mpfp, cot, czero_ninf); } int main() {