From 176b1fccf7b85b07c2e5e2c82e9dd22d8ce7c2f3 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Mon, 19 Aug 2013 17:04:41 -0700 Subject: [PATCH] Implement dependencies on interval functions (exp, log, and trigonometric functions) --- src/interval/interval.h | 163 ++++- src/interval/interval_def.h | 1368 ++++++++++++++++++++++++++--------- 2 files changed, 1155 insertions(+), 376 deletions(-) diff --git a/src/interval/interval.h b/src/interval/interval.h index 163a3c74d..83638dcbd 100644 --- a/src/interval/interval.h +++ b/src/interval/interval.h @@ -11,6 +11,36 @@ Author: Leonardo de Moura namespace lean { +#define DEP_IN_LOWER1 1 +#define DEP_IN_UPPER1 2 +#define DEP_IN_LOWER2 4 +#define DEP_IN_UPPER2 8 + +typedef 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; @@ -19,6 +49,7 @@ class interval { 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; } @@ -137,8 +168,10 @@ public: void set_is_lower_inf(bool v) { m_lower_inf = v; } void set_is_upper_inf(bool v) { m_upper_inf = v; } - void neg(); + template void neg(interval_deps & deps = dummy); + void neg_jst(interval_deps & 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); @@ -159,50 +192,136 @@ public: friend interval inv(interval o, T y) { o.fmod(y); return o; } void power(unsigned n); - void exp (); - void exp2 (); - void exp10(); - void log (); - void log2 (); - void log10(); - void sin (); - void cos (); - void tan (); - void csc (); - void sec (); - void cot (); - void asin (); - void acos (); - void atan (); - void sinh (); - void cosh (); - void tanh (); - void asinh(); - void acosh(); - void atanh(); + + 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 power(interval o, unsigned k) { o.power(k); return o; } + 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(); 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; } diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h index 505c80b34..1957d07d9 100644 --- a/src/interval/interval_def.h +++ b/src/interval/interval_def.h @@ -15,6 +15,9 @@ Author: Leonardo de Moura namespace lean { +template +interval_deps interval::dummy; + template void interval::set_closed_endpoints() { m_lower_open = false; @@ -159,51 +162,79 @@ bool interval::before(interval const & b) const { } template -void interval::neg() { +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) - 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_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| - swap(m_upper, m_lower); - neg(m_upper); - m_upper_inf = false; - m_upper_open = m_lower_open; + 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; + 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| - swap(m_lower, m_upper); - neg(m_lower); - neg(m_upper); + 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; + 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; + } } } - lean_assert(check_invariant()); + if(compute_intv) { + lean_assert(check_invariant()); + } } +template void interval::neg_jst(interval_deps & deps) { + neg(deps); + return; +} template interval & interval::operator+=(interval const & o) { @@ -885,132 +916,260 @@ template void interval::fmod(T y) { *this -= n * y; } -template void interval::exp() { +template +template +void interval::exp(interval_deps & deps) { if(m_lower_inf) { - numeric_traits::reset(m_lower); + if(compute_intv) { + numeric_traits::reset(m_lower); + } + if(compute_deps) { + deps.m_lower_deps = 0; + } } else { - numeric_traits::set_rounding(false); - numeric_traits::exp(m_lower); + 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) { - // Nothing to do + if(compute_deps) { + deps.m_lower_deps = 0; + } } else { - numeric_traits::set_rounding(true); - numeric_traits::exp(m_upper); + 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 void interval::exp2() { + +template +template +void interval::exp2(interval_deps & deps) { if(m_lower_inf) { - numeric_traits::reset(m_lower); + if(compute_intv) { + numeric_traits::reset(m_lower); + } + if(compute_deps) { + deps.m_lower_deps = 0; + } } else { - numeric_traits::set_rounding(false); - numeric_traits::exp2(m_lower); + 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) { - // Nothing to do + if(compute_deps) { + deps.m_lower_deps = 0; + } } else { - numeric_traits::set_rounding(true); - numeric_traits::exp2(m_upper); + 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 void interval::exp10() { + +template +template +void interval::exp10(interval_deps & deps) { if(m_lower_inf) { - numeric_traits::reset(m_lower); + if(compute_intv) { + numeric_traits::reset(m_lower); + } + if(compute_deps) { + deps.m_lower_deps = 0; + } } else { - numeric_traits::set_rounding(false); - numeric_traits::exp10(m_lower); + 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) { - // Nothing to do + if(compute_deps) { + deps.m_lower_deps = 0; + } } else { - numeric_traits::set_rounding(true); - numeric_traits::exp10(m_upper); + 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 void interval::log() { + +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()) { - numeric_traits::set_rounding(false); - numeric_traits::log(m_lower); + if(compute_intv) { + numeric_traits::set_rounding(false); + numeric_traits::log(m_lower); + } + if(compute_deps) { + deps.m_lower_deps = DEP_IN_LOWER1; + } } else { - numeric_traits::reset(m_lower); - m_lower_inf = true; + 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 { - numeric_traits::set_rounding(true); - numeric_traits::log(m_upper); + 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 void interval::log2() { + +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()) { - numeric_traits::set_rounding(false); - numeric_traits::log2(m_lower); + if(compute_intv) { + numeric_traits::set_rounding(false); + numeric_traits::log2(m_lower); + } + if(compute_deps) { + deps.m_lower_deps = DEP_IN_LOWER1; + } } else { - numeric_traits::reset(m_lower); - m_lower_inf = true; + 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 { - numeric_traits::set_rounding(true); - numeric_traits::log2(m_upper); + 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 void interval::log10() { + +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()) { - numeric_traits::set_rounding(false); - numeric_traits::log10(m_lower); + if(compute_intv) { + numeric_traits::set_rounding(false); + numeric_traits::log10(m_lower); + } + if(compute_deps) { + deps.m_lower_deps = DEP_IN_LOWER1; + } } else { - numeric_traits::reset(m_lower); - m_lower_inf = true; + 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 { - numeric_traits::set_rounding(true); - numeric_traits::log10(m_upper); + 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 void interval::sin() { + +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] - 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_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; } @@ -1022,9 +1181,15 @@ template void interval::sin() { 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] - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); + 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; } @@ -1041,12 +1206,18 @@ template void interval::sin() { // sin(x - pi) = [sin(u'), sin(l')] // sin(x) = [-sin(l'), -sin(u')] // sin(x) = [-sin(l'), sin(-u')] - 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_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; + deps.m_lower_deps = DEP_IN_UPPER1; + } return; } if(m_upper <= pi_half) { @@ -1058,21 +1229,37 @@ template void interval::sin() { // = [-sin(u'), 1] if l' + u' >= - pi if(m_lower + m_upper <= - pi) { // Nothing + if(compute_deps) { + deps.m_lower_deps = DEP_IN_LOWER1; + } } else { - m_lower = m_upper; + if(compute_intv) { + m_lower = m_upper; + } + if(compute_deps) { + deps.m_lower_deps = DEP_IN_UPPER1; + } + } + 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()); } - numeric_traits::set_rounding(true); - numeric_traits::sin(m_lower); - m_lower = - m_lower; - m_upper = 1.0; - lean_assert(check_invariant()); return; } // 3. -pi <= l' <= -1/2 pi <= 1/2 pi <= u' // sin(x - pi) = [-1, 1] - 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; + } + if(compute_intv) { + m_lower = -1.0; + m_upper = 1.0; + lean_assert(check_invariant()); + } return; } if(m_lower <= pi_half) { @@ -1081,13 +1268,19 @@ template void interval::sin() { // sin(x - pi) = [sin(l'), sin(u')] // sin(x) = [-sin(u'), -sin(l')] // = [-sin(u'), sin(-l')] - 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_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_UPPER1; + deps.m_upper_deps = DEP_IN_LOWER1; + } return; } if(m_upper <= pi_half + pi) { @@ -1098,21 +1291,42 @@ template void interval::sin() { // sin(x) = [-1, sin(-l')] if l' + u' <= pi // = [-1, sin(-u')] if l' + u' >= pi if(m_lower + m_upper <= pi) { - m_upper = - m_lower; + if(compute_intv) { + m_upper = - m_lower; + } + if(compute_deps) { + deps.m_upper_deps = DEP_IN_LOWER1; + } } else { - m_upper = - m_upper; + if(compute_intv) { + m_upper = - m_upper; + } + if(compute_deps) { + deps.m_upper_deps = DEP_IN_UPPER1; + } + } + 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; } - numeric_traits::set_rounding(true); - numeric_traits::sin(m_upper); - m_lower = -1.0; - lean_assert(check_invariant()); return; } // 6. -1/2 pi <= l' <= 1/2pi <= 3/2pi <= u' // sin(x - pi) = [-1, 1] - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); + 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); @@ -1120,12 +1334,18 @@ template void interval::sin() { // 7. 1/2pi <= l' <= u' <= 3/2 pi // sin(x - pi) = [sin(u'), sin(l')] // sin(x) = [-sin(l'), sin(-u')] - 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_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; + deps.m_upper_deps = DEP_IN_UPPER1; + } return; } if(m_upper <= pi_half + pi_twice) { @@ -1137,33 +1357,60 @@ template void interval::sin() { // = [-sin(u'), 1] if l' + u' >= 3pi if(m_lower + m_upper <= pi + pi_twice) { // Nothing + if(compute_deps) { + deps.m_lower_deps = DEP_IN_LOWER1; + } } else { - m_lower = m_upper; + if(compute_intv) { + m_lower = m_upper; + } + if(compute_deps) { + deps.m_upper_deps = DEP_IN_UPPER1; + } + } + 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_upper_deps = 0; } - numeric_traits::set_rounding(true); - numeric_traits::sin(m_lower); - m_lower = - m_lower; - m_upper = 1.0; - lean_assert(check_invariant()); return; } // 9. 1/2pi <= l' <= 5/2pi <= u' // sin(x - pi) = [-1, 1] - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); + 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 void interval::cos () { +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] - 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_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; } @@ -1174,17 +1421,28 @@ template void interval::cos () { 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] - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); + 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) - *this -= interval(numeric_traits::pi_lower(), numeric_traits::pi_upper()); - cos(); - neg(); + if(compute_intv) { + *this -= interval(numeric_traits::pi_lower(), numeric_traits::pi_upper()); + } + cos(deps); + neg(); + if(compute_deps) { + std::swap(deps.m_lower_deps, deps.m_upper_deps); + } lean_assert(check_invariant()); return; } @@ -1192,43 +1450,75 @@ template void interval::cos () { if (m_upper <= numeric_traits::pi_lower()) { // 0 <= l <= u <= pi // cos([l, u]) = [cos_d(u), cos_u(l)] - 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_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_UPPER1; + deps.m_upper_deps = DEP_IN_LOWER1; + } 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)] - numeric_traits::set_rounding(false); - static thread_local T tmp; - tmp = numeric_traits::pi_twice_lower() - m_upper; - m_upper = tmp < m_lower ? tmp : m_lower; - numeric_traits::set_rounding(true); - numeric_traits::cos(m_upper); - m_lower = -1.0; - lean_assert(check_invariant()); + if(m_lower + m_upper < numeric_traits::pi_twice()) { + if(compute_intv) { + m_upper = m_lower; + } + if(compute_deps) { + deps.m_lower_deps = 0; + deps.m_upper_deps = DEP_IN_LOWER1; + } + } else { + // Nothing + if(compute_deps) { + deps.m_lower_deps = 0; + deps.m_upper_deps = DEP_IN_UPPER1; + } + } + if(compute_intv) { + numeric_traits::set_rounding(true); + numeric_traits::cos(m_upper); + m_lower = -1.0; + lean_assert(check_invariant()); + } return; } - m_lower = -1.0; - m_upper = 1.0; - lean_assert(check_invariant()); + 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 void interval::tan() { +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] - 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_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; } @@ -1239,37 +1529,57 @@ template void interval::tan() { *this -= interval(numeric_traits::pi_lower(), numeric_traits::pi_upper()); } if (m_lower <= - pi_half_lower || m_upper >= pi_half_lower) { - 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_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 { - numeric_traits::set_rounding(false); - numeric_traits::tan(m_lower); - numeric_traits::set_rounding(true); - numeric_traits::tan(m_upper); - lean_assert(check_invariant()); + if(compute_intv) { + numeric_traits::set_rounding(false); + numeric_traits::tan(m_lower); + numeric_traits::set_rounding(true); + numeric_traits::tan(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::csc () { +template +template +void interval::csc (interval_deps & deps) { static thread_local T l; static thread_local T u; - l = m_lower; - u = m_upper; + 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] - 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_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(); @@ -1279,11 +1589,16 @@ template void interval::csc () { (m_lower < pi && 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()); + 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; } @@ -1292,13 +1607,19 @@ template void interval::csc () { // l <= u <= 1/2 pi // csc[l, u] = [csc(u), csc(l)] // = [-csc(-u), csc(l)] - 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_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_UPPER1; + deps.m_upper_deps = DEP_IN_LOWER1; + } return; } if (m_upper <= pi) { @@ -1307,15 +1628,33 @@ template void interval::csc () { // = [1, csc(l)] if l + u <= pi // = [1, csc(u)] if l + u >= pi if (m_lower + m_upper < pi) { - m_upper = l; + if(compute_intv) { + m_upper = l; + } + if(compute_deps) { + deps.m_lower_deps = 0; + deps.m_upper_deps = DEP_IN_LOWER1; + } } else { // Nothing - m_upper = u; + if(compute_intv) { + m_upper = u; + } + if(compute_deps) { + deps.m_lower_deps = 0; + deps.m_upper_deps = DEP_IN_UPPER1; + } + } + 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_UPPER1; } - m_lower = 1.0; - numeric_traits::set_rounding(true); - numeric_traits::csc(m_upper); - lean_assert(check_invariant()); return; } lean_unreachable(); @@ -1326,20 +1665,7 @@ template void interval::csc () { // l <= u <= pi // csc[l, u] = [csc(l), csc(u)] // = [-csc(-l), csc(u)] - 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()); - 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); @@ -1347,6 +1673,31 @@ template void interval::csc () { numeric_traits::csc(m_upper); 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; + } + 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; + deps.m_upper_deps = DEP_IN_UPPER1; + } return; } // l <= 3/2 pi <= u <= 2pi @@ -1358,165 +1709,296 @@ template void interval::csc () { // = [-csc(-u), -1] if l + u >= 3pi if (m_lower + m_upper < pi + numeric_traits::pi_twice()) { // Nothing - m_lower = -l; + if(compute_intv) { + m_lower = -l; + } + if(compute_deps) { + deps.m_lower_deps = DEP_IN_LOWER1; + } } else { - m_lower = -u; + if(compute_intv) { + m_lower = -u; + } + if(compute_deps) { + deps.m_lower_deps = DEP_IN_UPPER1; + } + } + 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_upper_deps = 0; } - m_upper = -1.0; - numeric_traits::set_rounding(true); - numeric_traits::csc(m_lower); - m_lower = -m_lower; - lean_assert(check_invariant()); return; } // 3/2pi <= l <= u < 2pi // csc[l, u] = [csc(u), csc(l)] // = [-csc(-u), csc(l)] - 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_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_UPPER1; + deps.m_upper_deps = DEP_IN_LOWER1; + } return; } -template void interval::sec () { - *this += interval(numeric_traits::pi_half_lower(), numeric_traits::pi_half_upper()); - csc(); +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 void interval::cot () { +template +template +void interval::cot (interval_deps & deps) { static thread_local T l; static thread_local T u; - l = m_lower; - u = m_upper; + 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] - 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_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())); -// fmod(numeric_traits::pi_lower()); 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()); + 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)] - 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_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_UPPER1; + deps.m_upper_deps = DEP_IN_LOWER1; + } return; } -template void interval::asin () { +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)] - 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_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 void interval::acos () { + +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); - 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_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 void interval::atan () { + +template +template +void interval::atan (interval_deps & deps) { if(lower_kind() == XN_MINUS_INFINITY) { - m_lower = -1.0; - m_lower_open = false; - m_lower_inf = false; + if(compute_intv) { + m_lower = -1.0; + m_lower_open = false; + m_lower_inf = false; + } + if(compute_deps) { + deps.m_lower_deps = 0; + } } else { - numeric_traits::set_rounding(true); - m_lower = -m_lower; - numeric_traits::atan(m_lower); - m_lower = -m_lower; + 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) { - m_upper = 1.0; - m_upper_open = false; - m_upper_inf = false; + if(compute_intv) { + m_upper = 1.0; + m_upper_open = false; + m_upper_inf = false; + } + if(compute_deps) { + deps.m_upper_deps = 0; + } } else { - numeric_traits::set_rounding(true); - numeric_traits::atan(m_upper); + 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()); } - lean_assert(check_invariant()); return; } -template void interval::sinh () { + +template +template +void interval::sinh (interval_deps & deps) { if(lower_kind() == XN_NUMERAL) { - numeric_traits::set_rounding(true); - m_lower = -m_lower; - numeric_traits::sinh(m_lower); - m_lower = -m_lower; + 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) { - numeric_traits::set_rounding(true); - numeric_traits::sinh(m_upper); + 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()); } - lean_assert(check_invariant()); return; } -template void interval::cosh () { + +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 - 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_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) { + deps.m_lower_deps = DEP_IN_LOWER1; + deps.m_upper_deps = DEP_IN_UPPER1; + } return; } if(numeric_traits::is_neg(m_upper) || numeric_traits::is_zero(m_upper)) { // [a, b] where a <= b < 0 - 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_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_UPPER1; + deps.m_upper_deps = DEP_IN_LOWER1; + } return; } // [a,b] where a < 0 < b - m_lower = 1.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()); + if(m_lower + m_upper < 0.0) { + if(compute_intv) { + m_upper = m_lower; + } + if(compute_deps) { + deps.m_lower_deps = 0; + deps.m_upper_deps = DEP_IN_LOWER1; + } + } else { + // Nothing + if(compute_deps) { + deps.m_upper_deps = 0; + deps.m_upper_deps = DEP_IN_UPPER1; + } + } + 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()); + } return; } if(lower_kind() == XN_NUMERAL) { @@ -1524,101 +2006,279 @@ template void interval::cosh () { lean_assert(upper_kind() == XN_PLUS_INFINITY); if(numeric_traits::is_pos(m_lower)) { // [c, +oo] where 0 < c < +oo - numeric_traits::set_rounding(false); - numeric_traits::cosh(m_lower); - lean_assert(check_invariant()); + 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 - m_lower = 1.0; - m_lower_open = false; - lean_assert(check_invariant()); + 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); - m_upper_inf = true; - m_upper_open = true; + if(compute_intv) { + m_upper_inf = true; + m_upper_open = true; + } if(numeric_traits::is_pos(m_upper)) { // [-oo, c] where -oo < 0 < c - m_lower = 1.0; - m_lower_open = false; - lean_assert(check_invariant()); + 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 - m_lower = m_upper; - numeric_traits::set_rounding(false); - numeric_traits::cosh(m_lower); - lean_assert(check_invariant()); + 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)) = [0, +oo) - m_upper_open = true; - m_upper_inf = true; - m_lower = 1.0; - m_lower_open = false; - m_lower_inf = false; - lean_assert(check_invariant()); + // 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 void interval::tanh () { + +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) { - numeric_traits::set_rounding(true); - m_lower = -m_lower; - numeric_traits::tanh(m_lower); - m_lower = -m_lower; + 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) { - numeric_traits::set_rounding(true); - numeric_traits::tanh(m_upper); + 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()); } - lean_assert(check_invariant()); return; } -template void interval::asinh() { + +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) { - numeric_traits::set_rounding(true); - m_lower = -m_lower; - numeric_traits::asinh(m_lower); - m_lower = -m_lower; + 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) { - numeric_traits::set_rounding(true); - numeric_traits::asinh(m_upper); + 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()); } - lean_assert(check_invariant()); return; } -template void interval::acosh() { + +template +template +void interval::acosh(interval_deps & deps) { lean_assert(lower_kind() == XN_NUMERAL && m_lower >= 1.0); - numeric_traits::set_rounding(false); - numeric_traits::acosh(m_lower); - if(upper_kind() == XN_NUMERAL) { - numeric_traits::set_rounding(true); - numeric_traits::acosh(m_upper); + 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()); } - lean_assert(check_invariant()); return; } -template void interval::atanh() { + +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(lower_kind() == XN_NUMERAL) { + + if(compute_intv) { numeric_traits::set_rounding(true); m_lower = -m_lower; numeric_traits::atanh(m_lower); m_lower = -m_lower; - } - if(upper_kind() == XN_NUMERAL) { numeric_traits::set_rounding(true); numeric_traits::atanh(m_upper); + lean_assert(check_invariant()); } - 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; } }