From c581990f67a3f099d577e3810249582907ada551 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Jul 2013 10:29:33 -0700 Subject: [PATCH] Clean white-spaces Signed-off-by: Leonardo de Moura --- src/interval/interval.cpp | 4 +- src/interval/interval.h | 10 +-- src/interval/interval_def.h | 61 ++++++++-------- src/numerics/gmp_init.cpp | 9 ++- src/numerics/mpbq.cpp | 24 +++---- src/numerics/mpbq.h | 120 ++++++++++++++++---------------- src/numerics/mpq.cpp | 5 +- src/numerics/mpz.cpp | 12 ++-- src/numerics/mpz.h | 84 +++++++++++----------- src/numerics/numeric_traits.cpp | 6 +- src/numerics/numeric_traits.h | 4 +- src/numerics/xnumeral.h | 10 +-- src/shell/lean.cpp | 2 +- src/tests/interval/interval.cpp | 4 +- src/tests/numerics/mpq.cpp | 4 +- src/util/debug.cpp | 4 +- src/util/debug.h | 8 +-- src/util/exception.cpp | 4 +- src/util/exception.h | 4 +- src/util/name.cpp | 22 +++--- src/util/name.h | 4 +- src/util/rc.h | 4 +- src/util/test.h | 7 +- src/util/trace.cpp | 11 ++- src/util/trace.h | 8 +-- src/util/verbosity.cpp | 4 +- src/util/verbosity.h | 6 +- 27 files changed, 219 insertions(+), 226 deletions(-) diff --git a/src/interval/interval.cpp b/src/interval/interval.cpp index 7b7ab18aca..51dde8db35 100644 --- a/src/interval/interval.cpp +++ b/src/interval/interval.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include "interval_def.h" #include "mpq.h" diff --git a/src/interval/interval.h b/src/interval/interval.h index 2f0f1d6a5b..331719b40c 100644 --- a/src/interval/interval.h +++ b/src/interval/interval.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once #include "numeric_traits.h" @@ -35,7 +35,7 @@ public: 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); @@ -48,7 +48,7 @@ public: ~interval(); 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()); } bool is_lower_zero() const { return ::lean::is_zero(m_lower, lower_kind()); } @@ -102,7 +102,7 @@ public: 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) { diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h index 057187cb23..2d22cf2d6f 100644 --- a/src/interval/interval_def.h +++ b/src/interval/interval_def.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once #include @@ -49,8 +49,8 @@ interval::interval(): template interval::interval(interval const & n): - m_lower(n.m_lower), - m_upper(n.m_upper), + 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), @@ -59,8 +59,8 @@ interval::interval(interval const & n): template interval::interval(interval && n): - m_lower(std::move(n.m_lower)), - m_upper(std::move(n.m_upper)), + 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), @@ -78,21 +78,21 @@ void interval::_swap(interval & b) { swap(m_upper, b.m_upper); unsigned 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_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; + tmp = m_upper_open; m_upper_open = b.m_upper_open; b.m_upper_open = tmp; } template bool interval::contains_zero() const { - return + return (is_lower_neg() || (is_lower_zero() && !is_lower_open())) && (is_upper_pos() || (is_upper_zero() && !is_upper_open())); } template bool interval::_eq(interval const & b) const { - return + 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()) && @@ -104,7 +104,7 @@ 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 m_upper < b.m_lower || (is_upper_open() && return true; } @@ -197,11 +197,11 @@ interval & interval::operator*=(interval const & o) { // 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 + + // 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(); @@ -213,7 +213,7 @@ interval & interval::operator*=(interval const & o) { // 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); + 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); @@ -230,7 +230,7 @@ interval & interval::operator*=(interval const & 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); @@ -249,7 +249,7 @@ interval & interval::operator*=(interval const & o) { 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; @@ -267,7 +267,7 @@ interval & interval::operator*=(interval const & o) { lean_assert(i2.is_P()); set_is_lower_open(a_o || d_o); - set_is_upper_open(b_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); @@ -276,12 +276,12 @@ interval & interval::operator*=(interval const & o) { } } else { - lean_assert(i1.is_P()); + 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 + + // 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); @@ -303,7 +303,7 @@ interval & interval::operator*=(interval const & o) { } else { lean_assert(i2.is_P()); - // 0 <= a <= x, 0 <= c <= y --> a*c <= x*y + // 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); @@ -340,18 +340,18 @@ void interval::inv() { 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_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); @@ -366,9 +366,9 @@ void interval::inv() { 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_inf(false); set_is_lower_open(new_l_open); } else if (is_N1()) { @@ -396,8 +396,8 @@ void interval::inv() { set_is_lower_inf(false); set_is_lower_open(is_upper_open()); } - - swap(m_upper, new_u_val); + + swap(m_upper, new_u_val); set_is_upper_inf(false); set_is_upper_open(new_u_open); } @@ -431,4 +431,3 @@ void interval::display(std::ostream & out) const { } - diff --git a/src/numerics/gmp_init.cpp b/src/numerics/gmp_init.cpp index 386c96d344..e2b9b874c7 100644 --- a/src/numerics/gmp_init.cpp +++ b/src/numerics/gmp_init.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include #include @@ -12,7 +12,7 @@ extern "C" void * cxx_malloc(size_t size) { void * p = malloc(size); if (p != 0 || size == 0) return p; - + throw std::bad_alloc(); } @@ -20,7 +20,7 @@ extern "C" void * cxx_realloc(void * q, size_t, size_t new_size) { void* p = realloc(q, new_size); if (p != 0 || new_size == 0) return p; - + throw std::bad_alloc(); } @@ -36,4 +36,3 @@ public: }; gmp_init g_gmp_init; - diff --git a/src/numerics/mpbq.cpp b/src/numerics/mpbq.cpp index 0eb284b9dd..2cec33cb20 100644 --- a/src/numerics/mpbq.cpp +++ b/src/numerics/mpbq.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include #include "mpbq.h" @@ -59,7 +59,7 @@ int cmp(mpbq const & a, mpq const & b) { // tmp1 <- numerator(a)*denominator(b) denominator(tmp1, b); tmp1 *= a.m_num; // tmp2 <- numerator(b)*denominator(a) - numerator(tmp2, b); mul2k(tmp2, tmp2, a.m_k); + numerator(tmp2, b); mul2k(tmp2, tmp2, a.m_k); return tmp1 < tmp2; } } @@ -83,7 +83,7 @@ mpbq & mpbq::operator+=(mpbq const & a) { return *this; } -template +template mpbq & mpbq::add_int(T const & a) { if (m_k == 0) { m_num += a; @@ -97,7 +97,7 @@ mpbq & mpbq::add_int(T const & a) { } normalize(); return *this; -} +} mpbq & mpbq::operator+=(unsigned a) { return add_int(a); } mpbq & mpbq::operator+=(int a) { return add_int(a); } @@ -120,7 +120,7 @@ mpbq & mpbq::operator-=(mpbq const & a) { return *this; } -template +template mpbq & mpbq::sub_int(T const & a) { if (m_k == 0) { m_num -= a; @@ -134,7 +134,7 @@ mpbq & mpbq::sub_int(T const & a) { } normalize(); return *this; -} +} mpbq & mpbq::operator-=(unsigned a) { return sub_int(a); } mpbq & mpbq::operator-=(int a) { return sub_int(a); } @@ -150,12 +150,12 @@ mpbq & mpbq::operator*=(mpbq const & a) { return *this; } -template +template mpbq & mpbq::mul_int(T const & a) { m_num *= a; normalize(); return *this; -} +} mpbq & mpbq::operator*=(unsigned a) { return mul_int(a); } mpbq & mpbq::operator*=(int a) { return mul_int(a); } @@ -263,7 +263,7 @@ bool root_upper(mpbq & a, mpbq const & b, unsigned n) { void refine_upper(mpq const & q, mpbq & l, mpbq & u) { lean_assert(l < q && q < u); lean_assert(!q.get_denominator().is_power_of_two()); - mpbq mid; + mpbq mid; while (true) { mid = l + u; div2(mid); @@ -279,7 +279,7 @@ void refine_upper(mpq const & q, mpbq & l, mpbq & u) { void refine_lower(mpq const & q, mpbq & l, mpbq & u) { lean_assert(l < q && q < u); lean_assert(!q.get_denominator().is_power_of_two()); - mpbq mid; + mpbq mid; while (true) { mid = l + u; div2(mid); @@ -293,7 +293,7 @@ void refine_lower(mpq const & q, mpbq & l, mpbq & u) { } bool lt_1div2k(mpbq const & a, unsigned k) { - if (a.m_num.is_nonpos()) + if (a.m_num.is_nonpos()) return true; if (a.m_k <= k) { // since a.m_num >= 1 diff --git a/src/numerics/mpbq.h b/src/numerics/mpbq.h index 2a2c6116fe..68b7c61b8c 100644 --- a/src/numerics/mpbq.h +++ b/src/numerics/mpbq.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once #include "mpz.h" @@ -10,7 +10,7 @@ Author: Leonardo de Moura namespace lean { -// Multiple precision binary rationals +// Multiple precision binary rationals class mpbq { mpz m_num; unsigned m_k; @@ -38,7 +38,7 @@ public: int sgn() const { return m_num.sgn(); } friend int sgn(mpbq const & a) { return a.sgn(); } - bool is_pos() const { return sgn() > 0; } + bool is_pos() const { return sgn() > 0; } bool is_neg() const { return sgn() < 0; } bool is_zero() const { return sgn() == 0; } bool is_nonpos() const { return !is_pos(); } @@ -53,52 +53,52 @@ public: mpz const & get_numerator() const { return m_num; } unsigned get_k() const { return m_k; } bool is_integer() const { return m_k == 0; } - + friend int cmp(mpbq const & a, mpbq const & b); friend int cmp(mpbq const & a, mpz const & b); friend int cmp(mpbq const & a, mpq const & b); friend int cmp(mpbq const & a, unsigned b) { return cmp(a, mpbq(b)); } friend int cmp(mpbq const & a, int b) { return cmp(a, mpbq(b)); } - friend bool operator<(mpbq const & a, mpbq const & b) { return cmp(a, b) < 0; } - friend bool operator<(mpbq const & a, mpz const & b) { return cmp(a, b) < 0; } - friend bool operator<(mpbq const & a, mpq const & b) { return cmp(a, b) < 0; } - friend bool operator<(mpbq const & a, unsigned b) { return cmp(a, b) < 0; } - friend bool operator<(mpbq const & a, int b) { return cmp(a, b) < 0; } - friend bool operator<(mpz const & a, mpbq const & b) { return cmp(b, a) > 0; } - friend bool operator<(mpq const & a, mpbq const & b) { return cmp(b, a) > 0; } - friend bool operator<(unsigned a, mpbq const & b) { return cmp(b, a) > 0; } - friend bool operator<(int a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator<(mpbq const & a, mpbq const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpbq const & a, mpz const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpbq const & a, mpq const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpbq const & a, unsigned b) { return cmp(a, b) < 0; } + friend bool operator<(mpbq const & a, int b) { return cmp(a, b) < 0; } + friend bool operator<(mpz const & a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator<(mpq const & a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator<(unsigned a, mpbq const & b) { return cmp(b, a) > 0; } + friend bool operator<(int a, mpbq const & b) { return cmp(b, a) > 0; } - friend bool operator>(mpbq const & a, mpbq const & b) { return cmp(a, b) > 0; } - friend bool operator>(mpbq const & a, mpz const & b) { return cmp(a, b) > 0; } - friend bool operator>(mpbq const & a, mpq const & b) { return cmp(a, b) > 0; } - friend bool operator>(mpbq const & a, unsigned b) { return cmp(a, b) > 0; } - friend bool operator>(mpbq const & a, int b) { return cmp(a, b) > 0; } - friend bool operator>(mpz const & a, mpbq const & b) { return cmp(b, a) < 0; } - friend bool operator>(mpq const & a, mpbq const & b) { return cmp(b, a) < 0; } - friend bool operator>(unsigned a, mpbq const & b) { return cmp(b, a) < 0; } - friend bool operator>(int a, mpbq const & b) { return cmp(b, a) < 0; } + friend bool operator>(mpbq const & a, mpbq const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpbq const & a, mpz const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpbq const & a, mpq const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpbq const & a, unsigned b) { return cmp(a, b) > 0; } + friend bool operator>(mpbq const & a, int b) { return cmp(a, b) > 0; } + friend bool operator>(mpz const & a, mpbq const & b) { return cmp(b, a) < 0; } + friend bool operator>(mpq const & a, mpbq const & b) { return cmp(b, a) < 0; } + friend bool operator>(unsigned a, mpbq const & b) { return cmp(b, a) < 0; } + friend bool operator>(int a, mpbq const & b) { return cmp(b, a) < 0; } - friend bool operator<=(mpbq const & a, mpbq const & b) { return cmp(a, b) <= 0; } - friend bool operator<=(mpbq const & a, mpz const & b) { return cmp(a, b) <= 0; } - friend bool operator<=(mpbq const & a, mpq const & b) { return cmp(a, b) <= 0; } - friend bool operator<=(mpbq const & a, unsigned b) { return cmp(a, b) <= 0; } - friend bool operator<=(mpbq const & a, int b) { return cmp(a, b) <= 0; } - friend bool operator<=(mpz const & a, mpbq const & b) { return cmp(b, a) >= 0; } - friend bool operator<=(mpq const & a, mpbq const & b) { return cmp(b, a) >= 0; } - friend bool operator<=(unsigned a, mpbq const & b) { return cmp(b, a) >= 0; } - friend bool operator<=(int a, mpbq const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(mpbq const & a, mpbq const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpbq const & a, mpz const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpbq const & a, mpq const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpbq const & a, unsigned b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpbq const & a, int b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpz const & a, mpbq const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(mpq const & a, mpbq const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(unsigned a, mpbq const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(int a, mpbq const & b) { return cmp(b, a) >= 0; } - friend bool operator>=(mpbq const & a, mpbq const & b) { return cmp(a, b) >= 0; } - friend bool operator>=(mpbq const & a, mpz const & b) { return cmp(a, b) >= 0; } - friend bool operator>=(mpbq const & a, mpq const & b) { return cmp(a, b) >= 0; } - friend bool operator>=(mpbq const & a, unsigned b) { return cmp(a, b) >= 0; } - friend bool operator>=(mpbq const & a, int b) { return cmp(a, b) >= 0; } - friend bool operator>=(mpz const & a, mpbq const & b) { return cmp(b, a) <= 0; } - friend bool operator>=(mpq const & a, mpbq const & b) { return cmp(b, a) <= 0; } - friend bool operator>=(unsigned a, mpbq const & b) { return cmp(b, a) <= 0; } - friend bool operator>=(int a, mpbq const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(mpbq const & a, mpbq const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpbq const & a, mpz const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpbq const & a, mpq const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpbq const & a, unsigned b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpbq const & a, int b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpz const & a, mpbq const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(mpq const & a, mpbq const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(unsigned a, mpbq const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(int a, mpbq const & b) { return cmp(b, a) <= 0; } friend bool operator==(mpbq const & a, mpbq const & b) { return a.m_k == b.m_k && a.m_num == b.m_num; } friend bool operator==(mpbq const & a, mpz const & b) { return a.is_integer() && a.m_num == b; } @@ -132,28 +132,28 @@ public: mpbq & operator*=(unsigned a); mpbq & operator*=(int a); - friend mpbq operator+(mpbq a, mpbq const & b) { return a += b; } - friend mpbq operator+(mpbq a, mpz const & b) { return a += b; } - friend mpbq operator+(mpbq a, unsigned b) { return a += b; } - friend mpbq operator+(mpbq a, int b) { return a += b; } + friend mpbq operator+(mpbq a, mpbq const & b) { return a += b; } + friend mpbq operator+(mpbq a, mpz const & b) { return a += b; } + friend mpbq operator+(mpbq a, unsigned b) { return a += b; } + friend mpbq operator+(mpbq a, int b) { return a += b; } friend mpbq operator+(mpz const & a, mpbq b) { return b += a; } - friend mpbq operator+(unsigned a, mpbq b) { return b += a; } - friend mpbq operator+(int a, mpbq b) { return b += a; } + friend mpbq operator+(unsigned a, mpbq b) { return b += a; } + friend mpbq operator+(int a, mpbq b) { return b += a; } - friend mpbq operator-(mpbq a, mpbq const & b) { return a -= b; } - friend mpbq operator-(mpbq a, mpz const & b) { return a -= b; } - friend mpbq operator-(mpbq a, unsigned b) { return a -= b; } - friend mpbq operator-(mpbq a, int b) { return a -= b; } + friend mpbq operator-(mpbq a, mpbq const & b) { return a -= b; } + friend mpbq operator-(mpbq a, mpz const & b) { return a -= b; } + friend mpbq operator-(mpbq a, unsigned b) { return a -= b; } + friend mpbq operator-(mpbq a, int b) { return a -= b; } friend mpbq operator-(mpz const & a, mpbq b) { b.neg(); return b += a; } - friend mpbq operator-(unsigned a, mpbq b) { b.neg(); return b += a; } - friend mpbq operator-(int a, mpbq b) { b.neg(); return b += a; } + friend mpbq operator-(unsigned a, mpbq b) { b.neg(); return b += a; } + friend mpbq operator-(int a, mpbq b) { b.neg(); return b += a; } friend mpbq operator*(mpbq a, mpbq const & b) { return a *= b; } friend mpbq operator*(mpbq a, mpz const & b) { return a *= b; } - friend mpbq operator*(mpbq a, unsigned b) { return a *= b; } - friend mpbq operator*(mpbq a, int b) { return a *= b; } + friend mpbq operator*(mpbq a, unsigned b) { return a *= b; } + friend mpbq operator*(mpbq a, int b) { return a *= b; } friend mpbq operator*(mpz const & a, mpbq b) { return b *= a; } - friend mpbq operator*(unsigned a, mpbq b) { return b *= a; } + friend mpbq operator*(unsigned a, mpbq b) { return b *= a; } friend mpbq operator*(int a, mpbq b) { return b *= a; } mpbq & operator++() { return operator+=(1); } @@ -174,7 +174,7 @@ public: Remark: mlog2(b) = log2(-b) Examples: - + 5/2^3 log2(5) - 3 = -1 21/2^2 log2(21) - 2 = 2 -3/2^4 log2(3) - 4 + 1 = -2 @@ -196,7 +196,7 @@ public: friend void mul2k(mpbq & a, unsigned k); // a <- b * 2^k friend void mul2k(mpbq & a, mpbq const & b, unsigned k) { a = b; mul2k(a, k); } - + // a <- a/2 friend void div2(mpbq & a) { bool old_k_zero = (a.m_k == 0); a.m_k++; if (old_k_zero) a.normalize(); } // a <- a/2^k @@ -206,7 +206,7 @@ public: /** \brief Return true if b^{1/n} is a binary rational, and store the result in a. - Otherwise, return false and return an lower bound based on the integer root of the + Otherwise, return false and return an lower bound based on the integer root of the numerator and denominator/n */ friend bool root_lower(mpbq & a, mpbq const & b, unsigned n); @@ -216,7 +216,7 @@ public: \brief Given a rational q which cannot be represented as a binary rational, and an interval (l, u) s.t. l < q < u. This method stores in u, a u' s.t. q < u' < u. - In the refinement process, the lower bound l may be also refined to l' + In the refinement process, the lower bound l may be also refined to l' s.t. l < l' < q */ friend void refine_upper(mpq const & q, mpbq & l, mpbq & u); diff --git a/src/numerics/mpq.cpp b/src/numerics/mpq.cpp index 842a95378e..e0d3a235c1 100644 --- a/src/numerics/mpq.cpp +++ b/src/numerics/mpq.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include "mpq.h" @@ -102,4 +102,3 @@ void display_decimal(std::ostream & out, mpq const & a, unsigned prec) { } void pp(lean::mpq const & v) { std::cout << v << std::endl; } - diff --git a/src/numerics/mpz.cpp b/src/numerics/mpz.cpp index 7b244e2c07..c9527d50e1 100644 --- a/src/numerics/mpz.cpp +++ b/src/numerics/mpz.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include #include "mpz.h" @@ -40,8 +40,8 @@ bool mpz::is_power_of_two(unsigned & shift) const { return false; } } - -mpz operator%(mpz const & a, mpz const & b) { + +mpz operator%(mpz const & a, mpz const & b) { mpz r(rem(a, b)); if (r.is_neg()) { if (b.is_pos()) @@ -52,9 +52,9 @@ mpz operator%(mpz const & a, mpz const & b) { return r; } -bool root(mpz & root, mpz const & a, unsigned k) { +bool root(mpz & root, mpz const & a, unsigned k) { static thread_local mpz rem; - mpz_rootrem(root.m_val, rem.m_val, a.m_val, k); + mpz_rootrem(root.m_val, rem.m_val, a.m_val, k); return rem.is_zero(); } diff --git a/src/numerics/mpz.h b/src/numerics/mpz.h index 8d4aae8516..8904de9e0b 100644 --- a/src/numerics/mpz.h +++ b/src/numerics/mpz.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once #include @@ -22,7 +22,7 @@ class mpz { mpz(__mpz_struct const * v) { mpz_init_set(m_val, v); } public: mpz() { mpz_init(m_val); } - mpz(char const * v) { mpz_init_set_str(m_val, const_cast(v), 10); } + mpz(char const * v) { mpz_init_set_str(m_val, const_cast(v), 10); } mpz(unsigned long int v) { mpz_init_set_ui(m_val, v); } mpz(long int v) { mpz_init_set_si(m_val, v); } mpz(unsigned int v) { mpz_init_set_ui(m_val, v); } @@ -37,12 +37,12 @@ public: int sgn() const { return mpz_sgn(m_val); } friend int sgn(mpz const & a) { return a.sgn(); } - bool is_pos() const { return sgn() > 0; } + bool is_pos() const { return sgn() > 0; } bool is_neg() const { return sgn() < 0; } bool is_zero() const { return sgn() == 0; } bool is_nonpos() const { return !is_pos(); } bool is_nonneg() const { return !is_neg(); } - + void neg() { mpz_neg(m_val, m_val); } friend mpz neg(mpz a) { a.neg(); return a; } @@ -74,29 +74,29 @@ public: friend int cmp(mpz const & a, unsigned b) { return mpz_cmp_ui(a.m_val, b); } friend int cmp(mpz const & a, int b) { return mpz_cmp_si(a.m_val, b); } - friend bool operator<(mpz const & a, mpz const & b) { return cmp(a, b) < 0; } - friend bool operator<(mpz const & a, unsigned b) { return cmp(a, b) < 0; } - friend bool operator<(mpz const & a, int b) { return cmp(a, b) < 0; } - friend bool operator<(unsigned a, mpz const & b) { return cmp(b, a) > 0; } - friend bool operator<(int a, mpz const & b) { return cmp(b, a) > 0; } + friend bool operator<(mpz const & a, mpz const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpz const & a, unsigned b) { return cmp(a, b) < 0; } + friend bool operator<(mpz const & a, int b) { return cmp(a, b) < 0; } + friend bool operator<(unsigned a, mpz const & b) { return cmp(b, a) > 0; } + friend bool operator<(int a, mpz const & b) { return cmp(b, a) > 0; } - friend bool operator>(mpz const & a, mpz const & b) { return cmp(a, b) > 0; } - friend bool operator>(mpz const & a, unsigned b) { return cmp(a, b) > 0; } - friend bool operator>(mpz const & a, int b) { return cmp(a, b) > 0; } - friend bool operator>(unsigned a, mpz const & b) { return cmp(b, a) < 0; } - friend bool operator>(int a, mpz const & b) { return cmp(b, a) < 0; } + friend bool operator>(mpz const & a, mpz const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpz const & a, unsigned b) { return cmp(a, b) > 0; } + friend bool operator>(mpz const & a, int b) { return cmp(a, b) > 0; } + friend bool operator>(unsigned a, mpz const & b) { return cmp(b, a) < 0; } + friend bool operator>(int a, mpz const & b) { return cmp(b, a) < 0; } - friend bool operator<=(mpz const & a, mpz const & b) { return cmp(a, b) <= 0; } - friend bool operator<=(mpz const & a, unsigned b) { return cmp(a, b) <= 0; } - friend bool operator<=(mpz const & a, int b) { return cmp(a, b) <= 0; } - friend bool operator<=(unsigned a, mpz const & b) { return cmp(b, a) >= 0; } - friend bool operator<=(int a, mpz const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(mpz const & a, mpz const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpz const & a, unsigned b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpz const & a, int b) { return cmp(a, b) <= 0; } + friend bool operator<=(unsigned a, mpz const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(int a, mpz const & b) { return cmp(b, a) >= 0; } - friend bool operator>=(mpz const & a, mpz const & b) { return cmp(a, b) >= 0; } - friend bool operator>=(mpz const & a, unsigned b) { return cmp(a, b) >= 0; } - friend bool operator>=(mpz const & a, int b) { return cmp(a, b) >= 0; } - friend bool operator>=(unsigned a, mpz const & b) { return cmp(b, a) <= 0; } - friend bool operator>=(int a, mpz const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(mpz const & a, mpz const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpz const & a, unsigned b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpz const & a, int b) { return cmp(a, b) >= 0; } + friend bool operator>=(unsigned a, mpz const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(int a, mpz const & b) { return cmp(b, a) <= 0; } friend bool operator==(mpz const & a, mpz const & b) { return cmp(a, b) == 0; } friend bool operator==(mpz const & a, unsigned b) { return cmp(a, b) == 0; } @@ -109,7 +109,7 @@ public: friend bool operator!=(mpz const & a, int b) { return cmp(a, b) != 0; } friend bool operator!=(unsigned a, mpz const & b) { return cmp(b, a) != 0; } friend bool operator!=(int a, mpz const & b) { return cmp(b, a) != 0; } - + mpz & operator+=(mpz const & o) { mpz_add(m_val, m_val, o.m_val); return *this; } mpz & operator+=(unsigned u) { mpz_add_ui(m_val, m_val, u); return *this; } mpz & operator+=(int u) { if (u >= 0) mpz_add_ui(m_val, m_val, u); else mpz_sub_ui(m_val, m_val, u); return *this; } @@ -128,28 +128,28 @@ public: friend mpz rem(mpz const & a, mpz const & b) { mpz r; mpz_tdiv_r(r.m_val, a.m_val, b.m_val); return r; } mpz & operator%=(mpz const & o) { mpz r(*this % o); mpz_swap(m_val, r.m_val); return *this; } - friend mpz operator+(mpz a, mpz const & b) { return a += b; } - friend mpz operator+(mpz a, unsigned b) { return a += b; } - friend mpz operator+(mpz a, int b) { return a += b; } - friend mpz operator+(unsigned a, mpz b) { return b += a; } - friend mpz operator+(int a, mpz b) { return b += a; } + friend mpz operator+(mpz a, mpz const & b) { return a += b; } + friend mpz operator+(mpz a, unsigned b) { return a += b; } + friend mpz operator+(mpz a, int b) { return a += b; } + friend mpz operator+(unsigned a, mpz b) { return b += a; } + friend mpz operator+(int a, mpz b) { return b += a; } - friend mpz operator-(mpz a, mpz const & b) { return a -= b; } - friend mpz operator-(mpz a, unsigned b) { return a -= b; } - friend mpz operator-(mpz a, int b) { return a -= b; } - friend mpz operator-(unsigned a, mpz b) { b.neg(); return b += a; } - friend mpz operator-(int a, mpz b) { b.neg(); return b += a; } + friend mpz operator-(mpz a, mpz const & b) { return a -= b; } + friend mpz operator-(mpz a, unsigned b) { return a -= b; } + friend mpz operator-(mpz a, int b) { return a -= b; } + friend mpz operator-(unsigned a, mpz b) { b.neg(); return b += a; } + friend mpz operator-(int a, mpz b) { b.neg(); return b += a; } friend mpz operator*(mpz a, mpz const & b) { return a *= b; } - friend mpz operator*(mpz a, unsigned b) { return a *= b; } - friend mpz operator*(mpz a, int b) { return a *= b; } - friend mpz operator*(unsigned a, mpz b) { return b *= a; } + friend mpz operator*(mpz a, unsigned b) { return a *= b; } + friend mpz operator*(mpz a, int b) { return a *= b; } + friend mpz operator*(unsigned a, mpz b) { return b *= a; } friend mpz operator*(int a, mpz b) { return b *= a; } - friend mpz operator/(mpz a, mpz const & b) { return a /= b; } + friend mpz operator/(mpz a, mpz const & b) { return a /= b; } friend mpz operator/(mpz a, unsigned b) { return a /= b; } friend mpz operator/(mpz a, int b) { return a /= b; } - friend mpz operator/(unsigned a, mpz const & b) { mpz r(a); return r /= b; } + friend mpz operator/(unsigned a, mpz const & b) { mpz r(a); return r /= b; } friend mpz operator/(int a, mpz const & b) { mpz r(a); return r /= b; } friend mpz operator%(mpz const & a, mpz const & b); @@ -215,7 +215,7 @@ public: friend void lcm(mpz & l, mpz const & a, mpz const & b) { mpz_lcm(l.m_val, a.m_val, b.m_val); } friend mpz lcm(mpz const & a, mpz const & b) { mpz l; lcm(l, a, b); return l; } - friend std::ostream & operator<<(std::ostream & out, mpz const & v); + friend std::ostream & operator<<(std::ostream & out, mpz const & v); }; template<> diff --git a/src/numerics/numeric_traits.cpp b/src/numerics/numeric_traits.cpp index f4befa2946..ec2893079b 100644 --- a/src/numerics/numeric_traits.cpp +++ b/src/numerics/numeric_traits.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include #include @@ -10,7 +10,7 @@ Author: Leonardo de Moura namespace lean { -void set_processor_rounding(bool plus_inf) { +void set_processor_rounding(bool plus_inf) { if (plus_inf) std::fesetround(FE_UPWARD); else diff --git a/src/numerics/numeric_traits.h b/src/numerics/numeric_traits.h index 214f5e71b4..451bc49ab6 100644 --- a/src/numerics/numeric_traits.h +++ b/src/numerics/numeric_traits.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once diff --git a/src/numerics/xnumeral.h b/src/numerics/xnumeral.h index 303b10a3ae..b59711b544 100644 --- a/src/numerics/xnumeral.h +++ b/src/numerics/xnumeral.h @@ -1,15 +1,15 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once #include #include "numeric_traits.h" #include "debug.h" - + namespace lean { // Goodies (templates) for computing with extended numeral. @@ -38,8 +38,8 @@ bool is_neg(T const & a, xnumeral_kind ak) { return ak == XN_MINUS_INFINITY || (ak == XN_NUMERAL && numeric_traits::is_neg(a)); } -inline bool is_infinite(xnumeral_kind ak) { - return ak != XN_NUMERAL; +inline bool is_infinite(xnumeral_kind ak) { + return ak != XN_NUMERAL; } template diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 08fe041550..12c49ff962 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -30,7 +30,7 @@ void tst3() { lean::mpbq n2(2); lean_assert(n1 < n2); }}); - + std::thread t2([](){ for (unsigned i = 0; i < 10000000; i++) { lean::mpbq n1(500000001,3); diff --git a/src/tests/interval/interval.cpp b/src/tests/interval/interval.cpp index 3c04aac493..f9bd3da4e7 100644 --- a/src/tests/interval/interval.cpp +++ b/src/tests/interval/interval.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include "interval_def.h" #include "test.h" diff --git a/src/tests/numerics/mpq.cpp b/src/tests/numerics/mpq.cpp index ad9977e8fe..4bc73df0f7 100644 --- a/src/tests/numerics/mpq.cpp +++ b/src/tests/numerics/mpq.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include #include "test.h" diff --git a/src/util/debug.cpp b/src/util/debug.cpp index e3f95d72d5..ad99e0c381 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include "debug.h" #include diff --git a/src/util/debug.h b/src/util/debug.h index 7d96975506..f7dfd59034 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once @@ -13,7 +13,7 @@ Author: Leonardo de Moura #ifdef LEAN_DEBUG #define DEBUG_CODE(CODE) CODE #else -#define DEBUG_CODE(CODE) +#define DEBUG_CODE(CODE) #endif #define lean_assert(COND) DEBUG_CODE({if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }}) @@ -39,7 +39,7 @@ void disable_debug(char const * tag); bool is_debug_enabled(char const * tag); void invoke_debugger(); // support for testing -void continue_on_violation(bool flag); +void continue_on_violation(bool flag); bool has_violations(); } diff --git a/src/util/exception.cpp b/src/util/exception.cpp index 092a185385..d8950d6138 100644 --- a/src/util/exception.cpp +++ b/src/util/exception.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include "exception.h" diff --git a/src/util/exception.h b/src/util/exception.h index 6e30220ad9..e596ce956f 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once #include diff --git a/src/util/name.cpp b/src/util/name.cpp index 38e66f0a20..9b6f93c0ef 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include #include "name.h" @@ -21,7 +21,7 @@ struct name::imp { char * m_str; unsigned m_k; }; - + void dealloc() { imp * curr = this; while (true) { @@ -45,7 +45,7 @@ struct name::imp { display_core(out, sep, p->m_prefix); out << sep; } - if (p->m_is_string) + if (p->m_is_string) out << p->m_str; else out << p->m_k; @@ -103,7 +103,7 @@ name::~name() { } name & name::operator=(name const & other) { - if (other.m_imp) + if (other.m_imp) other.m_imp->inc_ref(); if (m_imp) m_imp->dec_ref(); @@ -121,9 +121,9 @@ name & name::operator=(name && other) { } name::kind name::get_kind() const { - if (m_imp == nullptr) + if (m_imp == nullptr) return kind::ANONYMOUS; - else + else return m_imp->m_is_string ? kind::STRING : kind::NUMERAL; } @@ -174,10 +174,10 @@ name name::get_prefix() const { static unsigned num_digits(unsigned k) { if (k == 0) return 1; - int r = 0; - while (k != 0) { - k /= 10; - r++; + int r = 0; + while (k != 0) { + k /= 10; + r++; } return r; } diff --git a/src/util/name.h b/src/util/name.h index ab0bf1fd8c..ba90b3ba27 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once #include diff --git a/src/util/rc.h b/src/util/rc.h index 5a760efad6..d60776bb22 100644 --- a/src/util/rc.h +++ b/src/util/rc.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once diff --git a/src/util/test.h b/src/util/test.h index 152c402098..c9151a68c5 100644 --- a/src/util/test.h +++ b/src/util/test.h @@ -1,13 +1,12 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once // always define LEAN_DEBUG for unit-tests #ifndef LEAN_DEBUG #define LEAN_DEBUG -#endif +#endif #include "debug.h" - diff --git a/src/util/trace.cpp b/src/util/trace.cpp index 29cf2348fa..c3eac10ffb 100644 --- a/src/util/trace.cpp +++ b/src/util/trace.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include "trace.h" @@ -12,7 +12,7 @@ Author: Leonardo de Moura #ifndef LEAN_TRACE_OUT #define LEAN_TRACE_OUT ".lean_trace" -#endif +#endif namespace lean { @@ -20,7 +20,7 @@ namespace lean { std::ofstream tout(LEAN_TRACE_OUT); std::mutex trace_mutex; #endif - + static std::unique_ptr> g_enabled_trace_tags; void enable_trace(char const * tag) { @@ -30,7 +30,7 @@ void enable_trace(char const * tag) { } void disable_trace(char const * tag) { - if (g_enabled_trace_tags) + if (g_enabled_trace_tags) g_enabled_trace_tags->erase(tag); } @@ -39,4 +39,3 @@ bool is_trace_enabled(char const * tag) { } } - diff --git a/src/util/trace.h b/src/util/trace.h index 14032c08f0..e8de5e140e 100644 --- a/src/util/trace.h +++ b/src/util/trace.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once @@ -10,12 +10,12 @@ Author: Leonardo de Moura #include #include namespace lean { -extern std::ofstream tout; +extern std::ofstream tout; extern std::mutex trace_mutex; } #define TRACE_CODE(CODE) { std::lock_guard _lean_trace_lock_(lean::trace_mutex); CODE } #else -#define TRACE_CODE(CODE) +#define TRACE_CODE(CODE) #endif #define lean_trace(TAG, CODE) TRACE_CODE(if (lean::is_trace_enabled(TAG)) { lean::tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE lean::tout << "------------------------------------------------\n"; lean::tout.flush(); }) diff --git a/src/util/verbosity.cpp b/src/util/verbosity.cpp index 53ec8e271d..f63f1d8f3b 100644 --- a/src/util/verbosity.cpp +++ b/src/util/verbosity.cpp @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #include "verbosity.h" diff --git a/src/util/verbosity.h b/src/util/verbosity.h index d564b9325a..298611a80e 100644 --- a/src/util/verbosity.h +++ b/src/util/verbosity.h @@ -1,8 +1,8 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Leonardo de Moura +Author: Leonardo de Moura */ #pragma once #include @@ -14,5 +14,3 @@ std::ostream& verbose_stream(); void set_verbose_stream(std::ostream& s); #define lean_verbose(LVL, CODE) { if (get_verbosity_level() >= LVL) { CODE } } } - -