feat(numerics): add zero() method to all numeric_traits

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

src/tests/util/numerics/CMakeLists.txt

@@ -22,3 +22,6 @@ add_test(xnumeral ${CMAKE_CURRENT_BINARY_DIR}/xnumeral)
 add_executable(primes primes.cpp)
 target_link_libraries(primes ${EXTRA_LIBS})
 add_test(primes ${CMAKE_CURRENT_BINARY_DIR}/primes)
+add_executable(numeric_traits numeric_traits.cpp)
+target_link_libraries(numeric_traits ${EXTRA_LIBS})
+add_test(numeric_traits ${CMAKE_CURRENT_BINARY_DIR}/numeric_traits)

src/tests/util/numerics/numeric_traits.cpp

@@ -0,0 +1,41 @@
+/*
+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 "util/test.h"
+#include "util/numerics/mpq.h"
+#include "util/numerics/mpz.h"
+#include "util/numerics/mpbq.h"
+#include "util/numerics/double.h"
+#include "util/numerics/float.h"
+#include "util/numerics/mpfp.h"
+using namespace lean;
+
+template<typename T>
+void tst_num(T const & a) {
+    std::cout << "value:           " << a << "\n";
+    std::cout << "is value zero:   " << std::boolalpha << numeric_traits<T>::is_zero(a) << "\n";
+    std::cout << "zero:            " << numeric_traits<T>::zero() << "\n";
+    std::cout << "is type precise: " << std::boolalpha << numeric_traits<T>::precise() << "\n";
+    std::cout << "typeid:          " << typeid(T).name() << "\n";
+    std::cout << "\n";
+}
+
+static void tst1() {
+    tst_num(mpq(1,2));
+    tst_num(mpq(0));
+    tst_num(mpz(3));
+    tst_num(mpz(0));
+    tst_num(mpfp(2.0));
+    tst_num(mpfp(0.0));
+    tst_num(mpfp(0.0, 512));
+    tst_num(mpbq(3));
+    tst_num(1.0);
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}

src/util/numerics/double.cpp

@@ -24,5 +24,8 @@ void double_abs(double & v)   { v = std::abs(v); }
 void double_ceil(double & v)  { v = std::ceil(v); }
 void double_floor(double & v) { v = std::floor(v); }
 
-
+static double g_zero = 0.0;
+double const & numeric_traits<double>::zero() {
+    return g_zero;
+}
 };

src/util/numerics/double.h

@@ -41,6 +41,7 @@ public:
     static void neg(double & v) { v = -v; }
     static void inv(double & v) { v = 1.0/v; }
     static void reset(double & v) { v = 0.0; }
+    static double const & zero();
 
     static void power(double & v, unsigned k) { double_power(v, k); }
     static void abs(double & v) { double_abs(v); }

src/util/numerics/float.cpp

@@ -24,4 +24,8 @@ void float_abs(float & v)   { v = std::abs(v); }
 void float_ceil(float & v)  { v = std::ceil(v); }
 void float_floor(float & v) { v = std::floor(v); }
 
+static float g_zero = 0.0;
+float const & zero() {
+    return g_zero;
+}
 };

src/util/numerics/float.h

@@ -41,6 +41,7 @@ public:
     static void neg(float & v) { v = -v; }
     static void inv(float & v) { v = 1.0/v; }
     static void reset(float & v) { v = 0.0; }
+    static float const & zero();
 
     static void power(float & v, unsigned k) { float_power(v, k); }
     static void abs(float & v) { float_abs(v); }

src/util/numerics/mpbq.cpp

@@ -348,6 +348,11 @@ void display_decimal(std::ostream & out, mpbq const & a, unsigned prec) {
     }
 }
 
+static mpbq g_zero;
+mpbq const & numeric_traits<mpbq>::zero() {
+    lean_assert(is_zero(g_zero));
+    return g_zero;
+}
 }
 
 void print(lean::mpbq const & n) { std::cout << n << std::endl; }

src/util/numerics/mpbq.h

@@ -276,6 +276,7 @@ public:
     static void set_rounding(bool plus_inf) { rnd = plus_inf; }
     static void neg(mpbq & v) { v.neg(); }
     static void reset(mpbq & v) { v = 0; }
+    static mpbq const & zero();
     // v <- v^k
     static void power(mpbq & v, unsigned k) { _power(v, v, k); }
 

src/util/numerics/mpfp.cpp

@@ -49,6 +49,12 @@ std::ostream & operator<<(std::ostream & out, mpfp const & v) {
     out << str;
     return out;
 }
+
+static mpfp g_zero(0.0);
+mpfp const & numeric_traits<mpfp>::zero() {
+    lean_assert(is_zero(g_zero));
+    return g_zero;
+}
 }
 
 void print(lean::mpfp const & v) { std::cout << v << std::endl; }

src/util/numerics/mpfp.h

@@ -497,7 +497,7 @@ template<>
 class numeric_traits<mpfp> {
 public:
     static mpfr_rnd_t rnd() { return get_mpfp_rnd(); }
-    static bool precise() { return true; }
+    static bool precise() { return false; }
     static bool is_zero(mpfp const &  v) { return v.is_zero(); }
     static bool is_pos(mpfp const & v) { return v.is_pos(); }
     static bool is_neg(mpfp const & v) { return v.is_neg(); }
@@ -505,6 +505,8 @@ public:
     static void neg(mpfp & v) { v.neg(); }
     static void inv(mpfp & v) { v.inv(); }
     static void reset(mpfp & v) { v = 0.0; }
+    static mpfp const & zero();
+
     // v <- v^k
     static void power(mpfp & v, unsigned k) { v.power(static_cast<unsigned long>(k)); }
     static void abs(mpfp & v) { v.abs(); }

src/util/numerics/mpq.cpp

@@ -115,6 +115,13 @@ void display_decimal(std::ostream & out, mpq const & a, unsigned prec) {
     }
     out << "?";
 }
+
+static mpq g_zero;
+
+mpq const & numeric_traits<mpq>::zero() {
+    lean_assert(is_zero(g_zero));
+    return g_zero;
+}
 }
 
 void print(lean::mpq const & v) { std::cout << v << std::endl; }

src/util/numerics/mpq.h

@@ -231,6 +231,7 @@ public:
     static void neg(mpq & v) { v.neg(); }
     static void inv(mpq & v) { v.inv(); }
     static void reset(mpq & v) { v = 0; }
+    static mpq const & zero();
 
     static void power(mpq & v, unsigned k) { _power(v, v, k); }
     static void abs(mpq & v) { v.abs(); }

src/util/numerics/mpz.cpp

@@ -75,6 +75,12 @@ std::ostream & operator<<(std::ostream & out, mpz const & v) {
     return out;
 }
 
+static mpz g_zero;
+
+mpz const & numeric_traits<mpz>::zero() {
+    lean_assert(is_zero(g_zero));
+    return g_zero;
+}
 }
 
 void print(lean::mpz const & n) { std::cout << n << std::endl; }

src/util/numerics/mpz.h

@@ -232,6 +232,6 @@ public:
     static void reset(mpz & v) { v = 0; }
     // v <- v^k
     static void power(mpz & v, unsigned k) { _power(v, v, k); }
+    static mpz const & zero();
 };
-
 }