From 105f55c68b4012b3361a0d7cd40ef7a319ecadd1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 16 Oct 2013 16:53:41 -0700
Subject: [PATCH] feat(numerics): add zero() method to all numeric_traits

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/numerics/CMakeLists.txt     |  3 ++
 src/tests/util/numerics/numeric_traits.cpp | 41 ++++++++++++++++++++++
 src/util/numerics/double.cpp               |  5 ++-
 src/util/numerics/double.h                 |  1 +
 src/util/numerics/float.cpp                |  4 +++
 src/util/numerics/float.h                  |  1 +
 src/util/numerics/mpbq.cpp                 |  5 +++
 src/util/numerics/mpbq.h                   |  1 +
 src/util/numerics/mpfp.cpp                 |  6 ++++
 src/util/numerics/mpfp.h                   |  4 ++-
 src/util/numerics/mpq.cpp                  |  7 ++++
 src/util/numerics/mpq.h                    |  1 +
 src/util/numerics/mpz.cpp                  |  6 ++++
 src/util/numerics/mpz.h                    |  2 +-
 14 files changed, 84 insertions(+), 3 deletions(-)
 create mode 100644 src/tests/util/numerics/numeric_traits.cpp

diff --git a/src/tests/util/numerics/CMakeLists.txt b/src/tests/util/numerics/CMakeLists.txt
index 57ca5f7b1..32498b602 100644
--- a/src/tests/util/numerics/CMakeLists.txt
+++ b/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)
diff --git a/src/tests/util/numerics/numeric_traits.cpp b/src/tests/util/numerics/numeric_traits.cpp
new file mode 100644
index 000000000..63e9e22d7
--- /dev/null
+++ b/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;
+}
diff --git a/src/util/numerics/double.cpp b/src/util/numerics/double.cpp
index 87930b928..9c296be3d 100644
--- a/src/util/numerics/double.cpp
+++ b/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;
+}
 };
diff --git a/src/util/numerics/double.h b/src/util/numerics/double.h
index 34305f472..727069584 100644
--- a/src/util/numerics/double.h
+++ b/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); }
diff --git a/src/util/numerics/float.cpp b/src/util/numerics/float.cpp
index 42bdd318d..4a38ab26f 100644
--- a/src/util/numerics/float.cpp
+++ b/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;
+}
 };
diff --git a/src/util/numerics/float.h b/src/util/numerics/float.h
index c33b8f27b..a5c86216a 100644
--- a/src/util/numerics/float.h
+++ b/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); }
diff --git a/src/util/numerics/mpbq.cpp b/src/util/numerics/mpbq.cpp
index 9b6456acf..dbbdd01f1 100644
--- a/src/util/numerics/mpbq.cpp
+++ b/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; }
diff --git a/src/util/numerics/mpbq.h b/src/util/numerics/mpbq.h
index 64fb1ab68..6fd1facbd 100644
--- a/src/util/numerics/mpbq.h
+++ b/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); }
 
diff --git a/src/util/numerics/mpfp.cpp b/src/util/numerics/mpfp.cpp
index c1fbfa2d9..3b8d7aedb 100644
--- a/src/util/numerics/mpfp.cpp
+++ b/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; }
diff --git a/src/util/numerics/mpfp.h b/src/util/numerics/mpfp.h
index 9a72b09d9..73778ec9f 100644
--- a/src/util/numerics/mpfp.h
+++ b/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(); }
diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp
index d03fb5546..d29e7ad4e 100644
--- a/src/util/numerics/mpq.cpp
+++ b/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; }
diff --git a/src/util/numerics/mpq.h b/src/util/numerics/mpq.h
index d87692324..c738f9a32 100644
--- a/src/util/numerics/mpq.h
+++ b/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(); }
diff --git a/src/util/numerics/mpz.cpp b/src/util/numerics/mpz.cpp
index 006514b88..33d9f9de7 100644
--- a/src/util/numerics/mpz.cpp
+++ b/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; }
diff --git a/src/util/numerics/mpz.h b/src/util/numerics/mpz.h
index e9fe1b347..13ad7b8d1 100644
--- a/src/util/numerics/mpz.h
+++ b/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();
 };
-
 }