From 5063c8cfa1e9e06ff3106f239ca6683a90db806f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Jul 2013 20:21:41 -0700 Subject: [PATCH] Add interval template Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 3 + src/interval/CMakeLists.txt | 1 + src/interval/interval.cpp | 18 ++ src/interval/interval.h | 96 +++++++++ src/interval/interval_def.h | 339 ++++++++++++++++++++++++++++++ src/numerics/mpbq.cpp | 8 +- src/numerics/mpbq.h | 4 +- src/numerics/mpq.h | 8 +- src/numerics/mpz.h | 4 +- src/numerics/xnumeral.h | 13 +- src/tests/interval/CMakeLists.txt | 3 + src/tests/interval/interval.cpp | 21 ++ 12 files changed, 499 insertions(+), 19 deletions(-) create mode 100644 src/interval/CMakeLists.txt create mode 100644 src/interval/interval.cpp create mode 100644 src/interval/interval.h create mode 100644 src/interval/interval_def.h create mode 100644 src/tests/interval/CMakeLists.txt create mode 100644 src/tests/interval/interval.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c5ee4c6956..b44c4a1d93 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -50,10 +50,13 @@ mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES) include_directories(${LEAN_SOURCE_DIR}/util) include_directories(${LEAN_SOURCE_DIR}/numerics) +include_directories(${LEAN_SOURCE_DIR}/interval) add_subdirectory(util) add_subdirectory(numerics) +add_subdirectory(interval) set(EXTRA_LIBS ${EXTRA_LIBS} util numerics ${GMP_LIBRARIES}) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread") add_subdirectory(shell) add_subdirectory(tests/numerics) +add_subdirectory(tests/interval) diff --git a/src/interval/CMakeLists.txt b/src/interval/CMakeLists.txt new file mode 100644 index 0000000000..9cc261e8f4 --- /dev/null +++ b/src/interval/CMakeLists.txt @@ -0,0 +1 @@ +add_library(interval interval.cpp) diff --git a/src/interval/interval.cpp b/src/interval/interval.cpp new file mode 100644 index 0000000000..7b7ab18aca --- /dev/null +++ b/src/interval/interval.cpp @@ -0,0 +1,18 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "interval_def.h" +#include "mpq.h" + +namespace lean { + +template class interval; +template class interval; + +} + +void pp(lean::interval const & i) { std::cout << i << std::endl; } +void pp(lean::interval const & i) { std::cout << i << std::endl; } diff --git a/src/interval/interval.h b/src/interval/interval.h new file mode 100644 index 0000000000..7bfde2610d --- /dev/null +++ b/src/interval/interval.h @@ -0,0 +1,96 @@ +/* +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 +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::set_rounding(true); } + static void round_to_minus_inf() { numeric_traits::set_rounding(false); } + +public: + template 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 interval(T2 const & n):m_lower(n), m_upper(n) { set_closed_endpoints();} + interval(interval const & n); + interval(interval && n); + 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; + } + + ~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 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; } + 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; + } +}; + +} diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h new file mode 100644 index 0000000000..f2c2a2e556 --- /dev/null +++ b/src/interval/interval_def.h @@ -0,0 +1,339 @@ +/* +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 +#include "interval.h" + +namespace lean { + +template +void interval::set_closed_endpoints() { + m_lower_open = false; + m_upper_open = false; + m_lower_inf = false; + m_upper_inf = false; +} + +template +interval & interval::operator=(interval const & n) { + m_lower = n.m_lower; + m_upper = n.m_upper; + m_lower_open = n.m_lower_open; + m_upper_open = n.m_upper_open; + m_lower_inf = n.m_lower_inf; + m_upper_inf = n.m_upper_inf; + return *this; +} + +template +interval & interval::operator=(interval && n) { + m_lower = std::move(n.m_lower); + m_upper = std::move(n.m_upper); + m_lower_open = n.m_lower_open; + m_upper_open = n.m_upper_open; + m_lower_inf = n.m_lower_inf; + m_upper_inf = n.m_upper_inf; + return *this; +} + +template +interval::interval(): + m_lower(0), + m_upper(0) { + set_closed_endpoints(); +} + +template +interval::interval(interval const & n): + m_lower(n.m_lower), + m_upper(n.m_upper), + m_lower_open(n.m_lower_open), + m_upper_open(n.m_upper_open), + m_lower_inf(n.m_lower_inf), + m_upper_inf(n.m_upper_inf) { +} + +template +interval::interval(interval && n): + m_lower(std::move(n.m_lower)), + m_upper(std::move(n.m_upper)), + m_lower_open(n.m_lower_open), + m_upper_open(n.m_upper_open), + m_lower_inf(n.m_lower_inf), + m_upper_inf(n.m_upper_inf) { +} + +template +interval::~interval() { +} + +template +void swap(interval & a, interval & b) { + using std::swap; + swap(a.m_lower, b.m_lower); + swap(a.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; +} + +template +bool interval::contains_zero() const { + return + (is_lower_neg() || (is_lower_zero() && !is_lower_open())) && + (is_upper_pos() || (is_upper_zero() && !is_upper_open())); +} + +template +interval & interval::operator+=(interval const & o) { + xnumeral_kind new_l_kind, new_u_kind; + round_to_minus_inf(); + add(m_lower, new_l_kind, m_lower, lower_kind(), o.m_lower, o.lower_kind()); + round_to_plus_inf(); + add(m_upper, new_u_kind, m_upper, upper_kind(), o.m_upper, o.upper_kind()); + m_lower_inf = new_l_kind == XN_MINUS_INFINITY; + m_upper_inf = new_u_kind == XN_PLUS_INFINITY; + m_lower_open = m_lower_open || o.m_lower_open; + m_upper_open = m_upper_open || o.m_upper_open; + lean_assert(check_invariant()); + return *this; +} + +template +interval & interval::operator-=(interval const & o) { + xnumeral_kind new_l_kind, new_u_kind; + round_to_minus_inf(); + sub(m_lower, new_l_kind, m_lower, lower_kind(), o.m_upper, o.upper_kind()); + round_to_plus_inf(); + add(m_upper, new_u_kind, m_upper, upper_kind(), o.m_lower, o.lower_kind()); + m_lower_inf = new_l_kind == XN_MINUS_INFINITY; + m_upper_inf = new_u_kind == XN_PLUS_INFINITY; + m_lower_open = m_lower_open || o.m_upper_open; + m_upper_open = m_upper_open || o.m_lower_open; + lean_assert(check_invariant()); + return *this; +} + +template +interval & interval::operator*=(interval const & o) { + using std::swap; + interval const & i1 = *this; + interval const & i2 = o; +#if LEAN_DEBUG || LEAN_TRACE + bool i1_contains_zero = i1.contains_zero(); + bool i2_contains_zero = i2.contains_zero(); +#endif + if (i1.is_zero()) { + return *this; + } + if (i2.is_zero()) { + *this = i2; + return *this; + } + + T const & a = i1.m_lower; xnumeral_kind a_k = i1.lower_kind(); + T const & b = i1.m_upper; xnumeral_kind b_k = i1.upper_kind(); + T const & c = i2.m_lower; xnumeral_kind c_k = i2.lower_kind(); + T const & d = i2.m_upper; xnumeral_kind d_k = i2.upper_kind(); + + bool a_o = i1.is_lower_open(); + bool b_o = i1.is_upper_open(); + bool c_o = i2.is_lower_open(); + bool d_o = i2.is_upper_open(); + + static thread_local T new_l_val; + static thread_local T new_u_val; + xnumeral_kind new_l_kind, new_u_kind; + + if (i1.is_N()) { + if (i2.is_N()) { + // x <= b <= 0, y <= d <= 0 --> b*d <= x*y + // a <= x <= b <= 0, c <= y <= d <= 0 --> x*y <= a*c (we can use the fact that x or y is always negative (i.e., b is neg or d is neg)) + set_is_lower_open((i1.is_N0() || i2.is_N0()) ? false : (b_o || d_o)); + set_is_upper_open(a_o || c_o); + // if b = 0 (and the interval is closed), then the lower bound is closed + + round_to_minus_inf(); + mul(new_l_val, new_l_kind, b, b_k, d, d_k); + round_to_plus_inf(); + mul(new_u_val, new_u_kind, a, a_k, c, c_k); + } + else if (i2.is_M()) { + // a <= x <= b <= 0, y <= d, d > 0 --> a*d <= x*y (uses the fact that b is not positive) + // a <= x <= b <= 0, c <= y, c < 0 --> x*y <= a*c (uses the fact that b is not positive) + set_is_lower_open(a_o || d_o); + set_is_upper_open(a_o || c_o); + + round_to_minus_inf(); + mul(new_l_val, new_l_kind, a, a_k, d, d_k); + round_to_plus_inf(); + mul(new_u_val, new_u_kind, a, a_k, c, c_k); + } + else { + // a <= x <= b <= 0, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that x is neg (b is not positive) or y is pos (c is not negative)) + // x <= b <= 0, 0 <= c <= y --> x*y <= b*c + lean_assert(i2.is_P()); + + // must update upper_is_open first, since value of is_N0(i1) and is_P0(i2) may be affected by update + set_is_upper_open((i1.is_N0() || i2.is_P0()) ? false : (b_o || c_o)); + set_is_lower_open(a_o || d_o); + + round_to_minus_inf(); + mul(new_l_val, new_l_kind, a, a_k, d, d_k); + round_to_plus_inf(); + mul(new_u_val, new_u_kind, b, b_k, c, c_k); + } + } + else if (i1.is_M()) { + if (i2.is_N()) { + // b > 0, x <= b, c <= y <= d <= 0 --> b*c <= x*y (uses the fact that d is not positive) + // a < 0, a <= x, c <= y <= d <= 0 --> x*y <= a*c (uses the fact that d is not positive) + set_is_lower_open(b_o || c_o); + set_is_upper_open(a_o || c_o); + + round_to_minus_inf(); + mul(new_l_val, new_l_kind, b, b_k, c, c_k); + round_to_plus_inf(); + mul(new_u_val, new_u_kind, a, a_k, c, c_k); + } + else if (i2.is_M()) { + static thread_local T ad; xnumeral_kind ad_k; + static thread_local T bc; xnumeral_kind bc_k; + static thread_local T ac; xnumeral_kind ac_k; + static thread_local T bd; xnumeral_kind bd_k; + + bool ad_o = a_o || d_o; + bool bc_o = b_o || c_o; + bool ac_o = a_o || c_o; + bool bd_o = b_o || d_o; + + round_to_minus_inf(); + mul(ad, ad_k, a, a_k, d, d_k); + mul(bc, bc_k, b, b_k, c, c_k); + round_to_plus_inf(); + mul(ac, ac_k, a, a_k, c, c_k); + mul(bd, bd_k, b, b_k, d, d_k); + + if (lt(ad, ad_k, bc, bc_k) || (eq(ad, ad_k, bc, bc_k) && !ad_o && bc_o)) { + swap(new_l_val, ad); + new_l_kind = ad_k; + set_is_lower_open(ad_o); + } + else { + swap(new_l_val, bc); + new_l_kind = bc_k; + set_is_lower_open(bc_o); + } + + + if (gt(ac, ac_k, bd, bd_k) || (eq(ac, ac_k, bd, bd_k) && !ac_o && bd_o)) { + swap(new_u_val, ac); + new_u_kind = ac_k; + set_is_upper_open(ac_o); + } + else { + swap(new_u_val, bd); + new_u_kind = bd_k; + set_is_upper_open(bd_o); + } + } + else { + // a < 0, a <= x, 0 <= c <= y <= d --> a*d <= x*y (uses the fact that c is not negative) + // b > 0, x <= b, 0 <= c <= y <= d --> x*y <= b*d (uses the fact that c is not negative) + lean_assert(i2.is_P()); + + set_is_lower_open(a_o || d_o); + set_is_upper_open(b_o || d_o); + + round_to_minus_inf(); + mul(new_l_val, new_l_kind, a, a_k, d, d_k); + round_to_plus_inf(); + mul(new_u_val, new_u_kind, b, b_k, d, d_k); + } + } + else { + lean_assert(i1.is_P()); + if (i2.is_N()) { + // 0 <= a <= x <= b, c <= y <= d <= 0 --> x*y <= b*c (uses the fact that x is pos (a is not neg) or y is neg (d is not pos)) + // 0 <= a <= x, y <= d <= 0 --> a*d <= x*y + + // must update upper_is_open first, since value of is_P0(i1) and is_N0(i2) may be affected by update + set_is_upper_open((i1.is_P0() || i2.is_N0()) ? false : a_o || d_o); + set_is_lower_open(b_o || c_o); + + round_to_minus_inf(); + mul(new_l_val, new_l_kind, b, b_k, c, c_k); + round_to_plus_inf(); + mul(new_u_val, new_u_kind, a, a_k, d, d_k); + } + else if (i2.is_M()) { + // 0 <= a <= x <= b, c <= y --> b*c <= x*y (uses the fact that a is not negative) + // 0 <= a <= x <= b, y <= d --> x*y <= b*d (uses the fact that a is not negative) + set_is_lower_open(b_o || c_o); + set_is_upper_open(b_o || d_o); + + round_to_minus_inf(); + mul(new_l_val, new_l_kind, b, b_k, c, c_k); + round_to_plus_inf(); + mul(new_u_val, new_u_kind, b, b_k, d, d_k); + } + else { + lean_assert(i2.is_P()); + // 0 <= a <= x, 0 <= c <= y --> a*c <= x*y + // x <= b, y <= d --> x*y <= b*d (uses the fact that x is pos (a is not negative) or y is pos (c is not negative)) + + set_is_lower_open((i1.is_P0() || i2.is_P0()) ? false : a_o || c_o); + set_is_upper_open(b_o || d_o); + + round_to_minus_inf(); + mul(new_l_val, new_l_kind, a, a_k, c, c_k); + round_to_plus_inf(); + mul(new_u_val, new_u_kind, b, b_k, d, d_k); + } + } + + swap(m_lower, new_l_val); + swap(m_upper, new_u_val); + set_is_lower_inf(new_l_kind == XN_MINUS_INFINITY); + set_is_upper_inf(new_u_kind == XN_PLUS_INFINITY); + lean_assert(!(i1_contains_zero || i2_contains_zero) || contains_zero()); + return *this; +} + +template +interval & interval::operator/=(interval const & o) { + // TODO + return *this; +} + +template +bool interval::check_invariant() const { + lean_assert(!m_lower_inf || m_lower_open); + lean_assert(!m_upper_inf || m_upper_open); + if (eq(m_lower, lower_kind(), m_upper, upper_kind())) { + lean_assert(!is_lower_open()); + lean_assert(!is_upper_open()); + } + else { + lean_assert(lt(m_lower, lower_kind(), m_upper, upper_kind())); + } + return true; +} + +template +void interval::display(std::ostream & out) const { + out << (m_lower_open ? "(" : "["); + ::lean::display(out, m_lower, lower_kind()); + out << ", "; + ::lean::display(out, m_upper, upper_kind()); + out << (m_upper_open ? ")" : "]"); +} + + +} diff --git a/src/numerics/mpbq.cpp b/src/numerics/mpbq.cpp index 707dbd6979..0eb284b9dd 100644 --- a/src/numerics/mpbq.cpp +++ b/src/numerics/mpbq.cpp @@ -268,11 +268,11 @@ void refine_upper(mpq const & q, mpbq & l, mpbq & u) { mid = l + u; div2(mid); if (mid > q) { - u.swap(mid); + swap(u, mid); lean_assert(l < q && q < u); return; } - l.swap(mid); + swap(l, mid); } } @@ -284,11 +284,11 @@ void refine_lower(mpq const & q, mpbq & l, mpbq & u) { mid = l + u; div2(mid); if (mid < q) { - l.swap(mid); + swap(l, mid); lean_assert(l < q && q < u); return; } - u.swap(mid); + swap(u, mid); } } diff --git a/src/numerics/mpbq.h b/src/numerics/mpbq.h index 5eaf44383c..2a2c6116fe 100644 --- a/src/numerics/mpbq.h +++ b/src/numerics/mpbq.h @@ -28,11 +28,11 @@ public: ~mpbq() {} mpbq & operator=(mpbq const & v) { m_num = v.m_num; m_k = v.m_k; return *this; } - mpbq & operator=(mpbq && v) { swap(v); return *this; } + mpbq & operator=(mpbq && v) { swap(*this, v); return *this; } mpbq & operator=(unsigned int v) { m_num = v; m_k = 0; return *this; } mpbq & operator=(int v) { m_num = v; m_k = 0; return *this; } - void swap(mpbq & o) { m_num.swap(o.m_num); std::swap(m_k, o.m_k); } + friend void swap(mpbq & a, mpbq & b) { swap(a.m_num, b.m_num); std::swap(a.m_k, b.m_k); } unsigned hash() const { return m_num.hash(); } diff --git a/src/numerics/mpq.h b/src/numerics/mpq.h index 654ba934ca..729d204d65 100644 --- a/src/numerics/mpq.h +++ b/src/numerics/mpq.h @@ -17,13 +17,13 @@ class mpq { static mpz_t const & zval(mpz const & v) { return v.m_val; } static mpz_t & zval(mpz & v) { return v.m_val; } public: - void swap(mpq & v) { mpq_swap(m_val, v.m_val); } - void swap_numerator(mpz & v) { mpz_swap(mpq_numref(m_val), v.m_val); mpq_canonicalize(m_val); } - void swap_denominator(mpz & v) { mpz_swap(mpq_denref(m_val), v.m_val); mpq_canonicalize(m_val); } + friend void swap(mpq & a, mpq & b) { mpq_swap(a.m_val, b.m_val); } + friend void swap_numerator(mpq & a, mpz & b) { mpz_swap(mpq_numref(a.m_val), b.m_val); mpq_canonicalize(a.m_val); } + friend void swap_denominator(mpq & a, mpz & b) { mpz_swap(mpq_denref(a.m_val), b.m_val); mpq_canonicalize(a.m_val); } mpq & operator=(mpz const & v) { mpq_set_z(m_val, v.m_val); return *this; } mpq & operator=(mpq const & v) { mpq_set(m_val, v.m_val); return *this; } - mpq & operator=(mpq && v) { swap(v); return *this; } + mpq & operator=(mpq && v) { swap(*this, v); return *this; } mpq & operator=(char const * v) { mpq_set_str(m_val, v, 10); return *this; } mpq & operator=(unsigned long int v) { mpq_set_ui(m_val, v, 1u); return *this; } mpq & operator=(long int v) { mpq_set_si(m_val, v, 1); return *this; } diff --git a/src/numerics/mpz.h b/src/numerics/mpz.h index 18825ebb04..8d4aae8516 100644 --- a/src/numerics/mpz.h +++ b/src/numerics/mpz.h @@ -31,7 +31,7 @@ public: mpz(mpz && s):mpz() { mpz_swap(m_val, s.m_val); } ~mpz() { mpz_clear(m_val); } - void swap(mpz & o) { mpz_swap(m_val, o.m_val); } + friend void swap(mpz & a, mpz & b) { mpz_swap(a.m_val, b.m_val); } unsigned hash() const { return static_cast(mpz_get_si(m_val)); } @@ -63,7 +63,7 @@ public: unsigned int get_unsigned_int() const { lean_assert(is_unsigned_int()); return static_cast(get_unsigned_long_int()); } mpz & operator=(mpz const & v) { mpz_set(m_val, v.m_val); return *this; } - mpz & operator=(mpz && v) { swap(v); return *this; } + mpz & operator=(mpz && v) { swap(*this, v); return *this; } mpz & operator=(char const * v) { mpz_set_str(m_val, v, 10); return *this; } mpz & operator=(unsigned long int v) { mpz_set_ui(m_val, v); return *this; } mpz & operator=(long int v) { mpz_set_si(m_val, v); return *this; } diff --git a/src/numerics/xnumeral.h b/src/numerics/xnumeral.h index 598443f23f..303b10a3ae 100644 --- a/src/numerics/xnumeral.h +++ b/src/numerics/xnumeral.h @@ -71,7 +71,6 @@ void neg(T & a, xnumeral_kind & ak) { template void inv(T & a, xnumeral_kind & ak) { - lean_assert(numeral_manager::field()); switch (ak) { case XN_MINUS_INFINITY: ak = XN_NUMERAL; @@ -175,7 +174,7 @@ void div(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b, } else { rk = XN_NUMERAL; - c = a / b; + r = a / b; } } @@ -209,7 +208,7 @@ bool eq(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { template bool neq(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { - return !eq(m, a, ak, b, bk); + return !eq(a, ak, b, bk); } template @@ -226,7 +225,7 @@ bool lt(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { case XN_PLUS_INFINITY: return true; default: - UNREACHABLE(); + lean_unreachable(); return false; } case XN_PLUS_INFINITY: @@ -239,17 +238,17 @@ bool lt(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { template bool gt(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { - return lt(m, b, bk, a, ak); + return lt(b, bk, a, ak); } template bool le(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { - return !gt(m, a, ak, b, bk); + return !gt(a, ak, b, bk); } template bool ge(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { - return !lt(m, a, ak, b, bk); + return !lt(a, ak, b, bk); } template diff --git a/src/tests/interval/CMakeLists.txt b/src/tests/interval/CMakeLists.txt new file mode 100644 index 0000000000..4352214255 --- /dev/null +++ b/src/tests/interval/CMakeLists.txt @@ -0,0 +1,3 @@ +add_executable(test_interval interval.cpp) +target_link_libraries(test_interval ${EXTRA_LIBS}) +add_test(interval ${CMAKE_CURRENT_BINARY_DIR}/test_interval) diff --git a/src/tests/interval/interval.cpp b/src/tests/interval/interval.cpp new file mode 100644 index 0000000000..18ce7784cd --- /dev/null +++ b/src/tests/interval/interval.cpp @@ -0,0 +1,21 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "interval_def.h" +#include "test.h" +#include "mpq.h" +using namespace lean; + +void tst1() { + interval t(1, 3); + std::cout << t + interval(2, 4, false, true) << "\n"; +} + +int main() { + continue_on_violation(true); + tst1(); + return 0; +}