michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add inv method to interval

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-19 09:47:26 -07:00
parent a376e478f8
commit 7f3bd4f254
3 changed files with 123 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/interval/interval.h
View file

@ -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<T>::set_rounding(true); }
static void round_to_minus_inf() { numeric_traits<T>::set_rounding(false); }
static void reset(T & v) { numeric_traits<T>::reset(v); }
static void inv(T & v) { numeric_traits<T>::inv(v); }
void _swap(interval & b);
bool _eq(interval const & b) const;
public:
template<typename T2> interval & operator=(T2 const & n) { m_lower = n; m_upper = n; set_closed_endpoints(); return *this; }
@ -39,10 +43,11 @@ public:
template<typename T2> 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<typename T2> 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<T> & a, interval<T> & 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<T> const & a, interval<T> const & b) { return a._eq(b); }
friend bool operator!=(interval<T> const & a, interval<T> 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<typename T2> void set_lower(T2 const & n) { m_lower = n; }
template<typename T2> 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<T> inv(interval<T> 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; }

109
src/interval/interval_def.h
View file

@ -72,15 +72,15 @@ interval<T>::~interval() {
}
template<typename T>
void swap(interval<T> & a, interval<T> & b) {
void interval<T>::_swap(interval<T> & 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<typename T>
@ -90,6 +90,24 @@ bool interval<T>::contains_zero() const {
(is_upper_pos() || (is_upper_zero() && !is_upper_open()));
}
template<typename T>
bool interval<T>::_eq(interval<T> 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<typename T>
bool interval<T>::before(interval<T> 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<typename T>
interval<T> & interval<T>::operator+=(interval<T> const & o) {
xnumeral_kind new_l_kind, new_u_kind;
@ -312,6 +330,82 @@ interval<T> & interval<T>::operator/=(interval<T> const & o) {
return *this;
}
template<typename T>
void interval<T>::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<typename T>
bool interval<T>::check_invariant() const {
lean_assert(!m_lower_inf || m_lower_open);
@ -337,3 +431,4 @@ void interval<T>::display(std::ostream & out) const {
}

1
src/tests/interval/interval.cpp
View file

@ -12,6 +12,7 @@ using namespace lean;
void tst1() {
interval<mpq> t(1, 3);
std::cout << t + interval<mpq>(2, 4, false, true) << "\n";
std::cout << t << " --> " << inv(t) << "\n";
}
int main() {