Implement dependencies on interval functions (exp, log, and trigonometric functions)
This commit is contained in:
Soonho Kong
parent
4a4f7eb9e2
commit
176b1fccf7
2 changed files with 1155 additions and 376 deletions
|
|
@ -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<typename T>
|
||||
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<bool compute_intv = true, bool compute_deps = false> void neg(interval_deps & deps = dummy);
|
||||
void neg_jst(interval_deps & deps);
|
||||
friend interval<T> neg(interval<T> o) { o.neg(); return o; }
|
||||
friend interval<T> neg_jst(interval<T> o, interval_deps & deps) { o.neg(deps); return o; }
|
||||
|
||||
interval & operator+=(interval<T> const & o);
|
||||
interval & operator-=(interval<T> const & o);
|
||||
|
|
@ -159,50 +192,136 @@ public:
|
|||
friend interval<T> inv(interval<T> 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<bool compute_intv = true, bool compute_deps = false> void exp(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void exp2(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void exp10(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void log(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void log2(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void log10(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void sin(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void cos(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void tan(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void csc(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void sec(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void cot(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void asin(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void acos(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void atan(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void sinh(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void cosh(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void tanh(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void asinh(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void acosh(interval_deps & deps = dummy);
|
||||
template<bool compute_intv = true, bool compute_deps = false> void atanh(interval_deps & deps = dummy);
|
||||
|
||||
void exp_jst (interval_deps & deps);
|
||||
void exp2_jst (interval_deps & deps);
|
||||
void exp10_jst(interval_deps & deps);
|
||||
void log_jst (interval_deps & deps);
|
||||
void log2_jst (interval_deps & deps);
|
||||
void log10_jst(interval_deps & deps);
|
||||
void sin_jst(interval_deps & deps);
|
||||
void cos_jst(interval_deps & deps);
|
||||
void tan_jst(interval_deps & deps);
|
||||
void csc_jst(interval_deps & deps);
|
||||
void sec_jst(interval_deps & deps);
|
||||
void cot_jst(interval_deps & deps);
|
||||
void asin_jst(interval_deps & deps);
|
||||
void acos_jst(interval_deps & deps);
|
||||
void atan_jst(interval_deps & deps);
|
||||
void sinh_jst(interval_deps & deps);
|
||||
void cosh_jst(interval_deps & deps);
|
||||
void tanh_jst(interval_deps & deps);
|
||||
void asinh_jst(interval_deps & deps);
|
||||
void acosh_jst(interval_deps & deps);
|
||||
void atanh_jst(interval_deps & deps);
|
||||
|
||||
friend interval<T> power(interval<T> o, unsigned k) { o.power(k); return o; }
|
||||
|
||||
friend interval<T> exp (interval<T> o) { o.exp(); return o; }
|
||||
friend interval<T> exp (interval<T> o, interval_deps & deps) { o.exp(deps); return o; }
|
||||
friend interval<T> exp_jst(interval<T> o, interval_deps & deps) { o.exp_jst(deps); return o; }
|
||||
|
||||
friend interval<T> exp2 (interval<T> o) { o.exp2(); return o; }
|
||||
friend interval<T> exp2 (interval<T> o, interval_deps & deps) { o.exp2(deps); return o; }
|
||||
friend interval<T> exp2_jst(interval<T> o, interval_deps & deps) { o.exp2_jst(deps); return o; }
|
||||
|
||||
friend interval<T> exp10(interval<T> o) { o.exp10(); return o; }
|
||||
friend interval<T> exp10(interval<T> o, interval_deps & deps) { o.exp10(deps); return o; }
|
||||
friend interval<T> exp10_jst(interval<T> o, interval_deps & deps) { o.exp10(deps); return o; }
|
||||
|
||||
friend interval<T> log (interval<T> o) { o.log(); return o; }
|
||||
friend interval<T> log (interval<T> o, interval_deps & deps) { o.log(deps); return o; }
|
||||
friend interval<T> log_jst(interval<T> o, interval_deps & deps) { o.log_jst(deps); return o; }
|
||||
|
||||
friend interval<T> log2 (interval<T> o) { o.log2(); return o; }
|
||||
friend interval<T> log2 (interval<T> o, interval_deps & deps) { o.log2(deps); return o; }
|
||||
friend interval<T> log2_jst(interval<T> o, interval_deps & deps) { o.log2_jst(deps); return o; }
|
||||
|
||||
friend interval<T> log10(interval<T> o) { o.log10(); return o; }
|
||||
friend interval<T> log10(interval<T> o, interval_deps & deps) { o.log10(deps); return o; }
|
||||
friend interval<T> log10_jst(interval<T> o, interval_deps & deps) { o.log10_jst(deps); return o; }
|
||||
|
||||
friend interval<T> sin (interval<T> o) { o.sin(); return o; }
|
||||
friend interval<T> sin (interval<T> o, interval_deps & deps) { o.sin(deps); return o; }
|
||||
friend interval<T> sin_jst(interval<T> o, interval_deps & deps) { o.sin_jst(deps); return o; }
|
||||
|
||||
friend interval<T> cos (interval<T> o) { o.cos(); return o; }
|
||||
friend interval<T> cos (interval<T> o, interval_deps & deps) { o.cos(deps); return o; }
|
||||
friend interval<T> cos_jst(interval<T> o, interval_deps & deps) { o.cos_jst(deps); return o; }
|
||||
|
||||
friend interval<T> tan (interval<T> o) { o.tan(); return o; }
|
||||
friend interval<T> tan (interval<T> o, interval_deps & deps) { o.tan(deps); return o; }
|
||||
friend interval<T> tan_jst(interval<T> o, interval_deps & deps) { o.tan_jst(deps); return o; }
|
||||
|
||||
friend interval<T> csc (interval<T> o) { o.csc(); return o; }
|
||||
friend interval<T> csc (interval<T> o, interval_deps & deps) { o.csc(deps); return o; }
|
||||
friend interval<T> csc_jst(interval<T> o, interval_deps & deps) { o.csc_jst(deps); return o; }
|
||||
|
||||
friend interval<T> sec (interval<T> o) { o.sec(); return o; }
|
||||
friend interval<T> sec (interval<T> o, interval_deps & deps) { o.sec(deps); return o; }
|
||||
friend interval<T> sec_jst(interval<T> o, interval_deps & deps) { o.sec_jst(deps); return o; }
|
||||
|
||||
friend interval<T> cot (interval<T> o) { o.cot(); return o; }
|
||||
friend interval<T> cot (interval<T> o, interval_deps & deps) { o.cot(deps); return o; }
|
||||
friend interval<T> cot_jst(interval<T> o, interval_deps & deps) { o.cot_jst(deps); return o; }
|
||||
|
||||
friend interval<T> asin (interval<T> o) { o.asin(); return o; }
|
||||
friend interval<T> asin (interval<T> o, interval_deps & deps) { o.asin(deps); return o; }
|
||||
friend interval<T> asin_jst(interval<T> o, interval_deps & deps) { o.asin_jst(deps); return o; }
|
||||
|
||||
friend interval<T> acos (interval<T> o) { o.acos(); return o; }
|
||||
friend interval<T> acos (interval<T> o, interval_deps & deps) { o.acos(deps); return o; }
|
||||
friend interval<T> acos_jst(interval<T> o, interval_deps & deps) { o.acos_jst(deps); return o; }
|
||||
|
||||
friend interval<T> atan (interval<T> o) { o.atan(); return o; }
|
||||
friend interval<T> atan (interval<T> o, interval_deps & deps) { o.atan(deps); return o; }
|
||||
friend interval<T> atan_jst(interval<T> o, interval_deps & deps) { o.atan_jst(deps); return o; }
|
||||
|
||||
friend interval<T> sinh (interval<T> o) { o.sinh(); return o; }
|
||||
friend interval<T> sinh (interval<T> o, interval_deps & deps) { o.sinh(deps); return o; }
|
||||
friend interval<T> sinh_jst(interval<T> o, interval_deps & deps) { o.sinh_jst(deps); return o; }
|
||||
|
||||
friend interval<T> cosh (interval<T> o) { o.cosh(); return o; }
|
||||
friend interval<T> cosh (interval<T> o, interval_deps & deps) { o.cosh(deps); return o; }
|
||||
friend interval<T> cosh_jst(interval<T> o, interval_deps & deps) { o.cosh(); return o; }
|
||||
|
||||
friend interval<T> tanh (interval<T> o) { o.tanh(); return o; }
|
||||
friend interval<T> tanh (interval<T> o, interval_deps & deps) { o.tanh(deps); return o; }
|
||||
friend interval<T> tanh_jst(interval<T> o, interval_deps & deps) { o.tanh_jst(deps); return o; }
|
||||
|
||||
friend interval<T> asinh(interval<T> o) { o.asinh(); return o; }
|
||||
friend interval<T> asinh(interval<T> o, interval_deps & deps) { o.asinh(deps); return o; }
|
||||
friend interval<T> asinh_jst(interval<T> o, interval_deps & deps) { o.asinh_jst(deps); return o; }
|
||||
|
||||
friend interval<T> acosh(interval<T> o) { o.acosh(); return o; }
|
||||
friend interval<T> acosh(interval<T> o, interval_deps & deps) { o.acosh(deps); return o; }
|
||||
friend interval<T> acosh_jst(interval<T> o, interval_deps & deps) { o.acosh_jst(deps); return o; }
|
||||
|
||||
friend interval<T> atanh(interval<T> o) { o.atanh(); return o; }
|
||||
friend interval<T> atanh(interval<T> o, interval_deps & deps) { o.atanh(deps); return o; }
|
||||
friend interval<T> atanh_jst(interval<T> o, interval_deps & deps) { o.atanh_jst(deps); return o; }
|
||||
|
||||
friend interval<T> operator+(interval<T> a, interval<T> const & b) { return a += b; }
|
||||
friend interval<T> operator-(interval<T> a, interval<T> const & b) { return a -= b; }
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
Loading…
Reference in a new issue