From 7f3bd4f254a8be6950b9f8cef169f4ea59b41f66 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Jul 2013 09:47:26 -0700 Subject: [PATCH] Add inv method to interval Signed-off-by: Leonardo de Moura --- src/interval/interval.h | 22 ++++++- src/interval/interval_def.h | 109 ++++++++++++++++++++++++++++++-- src/tests/interval/interval.cpp | 1 + 3 files changed, 123 insertions(+), 9 deletions(-) diff --git a/src/interval/interval.h b/src/interval/interval.h index 7bfde2610d..2f0f1d6a5b 100644 --- a/src/interval/interval.h +++ b/src/interval/interval.h @@ -20,11 +20,15 @@ class interval { unsigned m_upper_inf:1; 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; } + 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); } + 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; } @@ -39,10 +43,11 @@ public: 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; } + template interval(bool l_open, T2 const & l, T2 const & u, bool u_open):interval(l, u, l_open, u_open) {} ~interval(); - friend void swap(interval & a, interval & b); + friend void swap(interval & a, interval & b) { a._swap(b); } 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()); } @@ -54,6 +59,8 @@ public: 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; } bool is_P() const { return is_lower_pos() || is_lower_zero(); } bool is_P0() const { return is_lower_zero() && !is_lower_open(); } @@ -66,6 +73,14 @@ public: bool contains_zero() const; + 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; } @@ -78,6 +93,9 @@ public: interval & operator*=(interval const & o); interval & operator/=(interval const & o); + void inv(); + friend interval inv(interval o) { o.inv(); 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; } diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h index f2c2a2e556..057187cb23 100644 --- a/src/interval/interval_def.h +++ b/src/interval/interval_def.h @@ -72,15 +72,15 @@ interval::~interval() { } template -void swap(interval & a, interval & b) { +void interval::_swap(interval & b) { using std::swap; - swap(a.m_lower, b.m_lower); - swap(a.m_upper, b.m_upper); + swap(m_lower, b.m_lower); + swap(m_upper, b.m_upper); unsigned tmp; - tmp = a.m_lower_inf; a.m_lower_inf = b.m_lower_inf; b.m_lower_inf = tmp; - tmp = a.m_upper_inf; a.m_upper_inf = b.m_upper_inf; b.m_upper_inf = tmp; - tmp = a.m_lower_open; a.m_lower_open = b.m_lower_open; b.m_lower_open = tmp; - tmp = a.m_upper_open; a.m_upper_open = b.m_upper_open; b.m_upper_open = 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 @@ -90,6 +90,24 @@ bool interval::contains_zero() const { (is_upper_pos() || (is_upper_zero() && !is_upper_open())); } +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 { + // TODO + //if (is_upper_inf() || b.lower_is_inf()) + // return false; + // return m_upper < b.m_lower || (is_upper_open() && + return true; +} + template interval & interval::operator+=(interval const & o) { xnumeral_kind new_l_kind, new_u_kind; @@ -312,6 +330,82 @@ interval & interval::operator/=(interval const & o) { return *this; } +template +void interval::inv() { + // If the interval [l,u] does not contain 0, then 1/[l,u] = [1/u, 1/l] + lean_assert(!contains_zero()); + + using std::swap; + + static thread_local T new_l_val; + static thread_local 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) + + 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); + } + else if (is_N1()) { + // x <= u < 0 --> 1/u <= 1/x + // l <= x <= u < 0 --> 1/l <= 1/x (use lower and upper bounds) + 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); + } + else { + lean_unreachable(); + } +} + template bool interval::check_invariant() const { lean_assert(!m_lower_inf || m_lower_open); @@ -337,3 +431,4 @@ void interval::display(std::ostream & out) const { } + diff --git a/src/tests/interval/interval.cpp b/src/tests/interval/interval.cpp index 18ce7784cd..3c04aac493 100644 --- a/src/tests/interval/interval.cpp +++ b/src/tests/interval/interval.cpp @@ -12,6 +12,7 @@ using namespace lean; void tst1() { interval t(1, 3); std::cout << t + interval(2, 4, false, true) << "\n"; + std::cout << t << " --> " << inv(t) << "\n"; } int main() {