97 lines
3.8 KiB
C
97 lines
3.8 KiB
C
|
/*
|
||
|
|
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||
|
|
|
||
|
|
Author: Leonardo de Moura
|
||
|
|
*/
|
||
|
|
#pragma once
|
||
|
|
#include "numeric_traits.h"
|
||
|
|
#include "xnumeral.h"
|
||
|
|
|
||
|
|
namespace lean {
|
||
|
|
|
||
|
|
template<typename T>
|
||
|
|
class interval {
|
||
|
|
T m_lower;
|
||
|
|
T m_upper;
|
||
|
|
unsigned m_lower_open:1;
|
||
|
|
unsigned m_upper_open:1;
|
||
|
|
unsigned m_lower_inf:1;
|
||
|
|
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; }
|
||
|
|
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); }
|
||
|
|
|
||
|
|
public:
|
||
|
|
template<typename T2> interval & operator=(T2 const & n) { m_lower = n; m_upper = n; set_closed_endpoints(); return *this; }
|
||
|
|
interval & operator=(T const & n);
|
||
|
|
interval & operator=(interval const & n);
|
||
|
|
interval & operator=(interval && n);
|
||
|
|
|
||
|
|
interval();
|
||
|
|
template<typename T2> interval(T2 const & n):m_lower(n), m_upper(n) { set_closed_endpoints();}
|
||
|
|
interval(interval const & n);
|
||
|
|
interval(interval && n);
|
||
|
|
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;
|
||
|
|
}
|
||
|
|
|
||
|
|
~interval();
|
||
|
|
|
||
|
|
friend void swap(interval & a, interval & 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()); }
|
||
|
|
bool is_lower_zero() const { return ::lean::is_zero(m_lower, lower_kind()); }
|
||
|
|
|
||
|
|
bool is_upper_neg() const { return ::lean::is_neg(m_upper, upper_kind()); }
|
||
|
|
bool is_upper_pos() const { return ::lean::is_pos(m_upper, upper_kind()); }
|
||
|
|
bool is_upper_zero() const { return ::lean::is_zero(m_upper, upper_kind()); }
|
||
|
|
|
||
|
|
bool is_lower_open() const { return m_lower_open; }
|
||
|
|
bool is_upper_open() const { return m_upper_open; }
|
||
|
|
|
||
|
|
bool is_P() const { return is_lower_pos() || is_lower_zero(); }
|
||
|
|
bool is_P0() const { return is_lower_zero() && !is_lower_open(); }
|
||
|
|
bool is_P1() const { return is_lower_pos() || (is_lower_zero() && is_lower_open()); }
|
||
|
|
bool is_N() const { return is_upper_neg() || is_upper_zero(); }
|
||
|
|
bool is_N0() const { return is_upper_zero() && !is_upper_open(); }
|
||
|
|
bool is_N1() const { return is_upper_neg() || (is_upper_zero() && is_upper_open()); }
|
||
|
|
bool is_M() const { return is_lower_neg() && is_upper_pos(); }
|
||
|
|
bool is_zero() const { return is_lower_zero() && is_upper_zero(); }
|
||
|
|
|
||
|
|
bool contains_zero() 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; }
|
||
|
|
void set_is_upper_open(bool v) { m_upper_open = v; }
|
||
|
|
void set_is_lower_inf(bool v) { m_lower_inf = v; }
|
||
|
|
void set_is_upper_inf(bool v) { m_upper_inf = v; }
|
||
|
|
|
||
|
|
interval & operator+=(interval const & o);
|
||
|
|
interval & operator-=(interval const & o);
|
||
|
|
interval & operator*=(interval const & o);
|
||
|
|
interval & operator/=(interval const & 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; }
|
||
|
|
friend interval operator/(interval a, interval const & b) { return a /= b; }
|
||
|
|
|
||
|
|
bool check_invariant() const;
|
||
|
|
|
||
|
|
void display(std::ostream & out) const;
|
||
|
|
|
||
|
|
friend std::ostream & operator<<(std::ostream & out, interval const & n) {
|
||
|
|
n.display(out);
|
||
|
|
return out;
|
||
|
|
}
|
||
|
|
};
|
||
|
|
|
||
|
|
}
|