Add interval template

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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)
 

src/interval/CMakeLists.txt

@@ -0,0 +1 @@
+add_library(interval interval.cpp)

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<mpq>;
+template class interval<double>;
+
+}
+
+void pp(lean::interval<lean::mpq> const & i) { std::cout << i << std::endl; }
+void pp(lean::interval<double> const & i) { std::cout << i << std::endl; }

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<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;
+    }
+};
+
+}

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 <utility>
+#include "interval.h"
+
+namespace lean {
+
+template<typename T>
+void interval<T>::set_closed_endpoints() {
+    m_lower_open = false;
+    m_upper_open = false;
+    m_lower_inf  = false;
+    m_upper_inf  = false;
+}
+
+template<typename T>
+interval<T> & interval<T>::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<typename T>
+interval<T> & interval<T>::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<typename T>
+interval<T>::interval():
+    m_lower(0),
+    m_upper(0) {
+    set_closed_endpoints();
+}
+
+template<typename T>
+interval<T>::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<typename T>
+interval<T>::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<typename T>
+interval<T>::~interval() {
+}
+
+template<typename T>
+void swap(interval<T> & a, interval<T> & 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<typename T>
+bool interval<T>::contains_zero() const {
+    return 
+        (is_lower_neg() || (is_lower_zero() && !is_lower_open())) &&
+        (is_upper_pos() || (is_upper_zero() && !is_upper_open()));
+}
+
+template<typename T>
+interval<T> & interval<T>::operator+=(interval<T> 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<typename T>
+interval<T> & interval<T>::operator-=(interval<T> 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<typename T>
+interval<T> & interval<T>::operator*=(interval<T> const & o) {
+    using std::swap;
+    interval<T> const & i1 = *this;
+    interval<T> 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<typename T>
+interval<T> & interval<T>::operator/=(interval<T> const & o) {
+    // TODO
+    return *this;
+}
+
+template<typename T>
+bool interval<T>::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<typename T>
+void interval<T>::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 ? ")" : "]");
+}
+
+
+}

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);
     }
 }
 

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(); }
 

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; }

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<unsigned>(mpz_get_si(m_val)); }
 
@@ -63,7 +63,7 @@ public:
     unsigned int get_unsigned_int() const { lean_assert(is_unsigned_int()); return static_cast<unsigned>(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; }

src/numerics/xnumeral.h

@@ -71,7 +71,6 @@ void neg(T & a, xnumeral_kind & ak) {
 
 template<typename T>
 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<typename T>
 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<typename T>
@@ -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<typename T>
 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<typename T>
 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<typename T>
 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<typename T>

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)

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<mpq> t(1, 3);
+    std::cout << t + interval<mpq>(2, 4, false, true) << "\n";
+}
+
+int main() {
+    continue_on_violation(true);
+    tst1();
+    return 0;
+}