Add precise() to numeric_traits

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

src/numerics/mpbq.h

@@ -246,6 +246,7 @@ public:
 template<>
 class numeric_traits<mpbq> {
 public:
+    static bool precise() { return true; }
     static bool is_zero(mpbq const &  v) { return v.is_zero(); }
     static bool is_pos(mpbq const & v) { return v.is_pos(); }
     static bool is_neg(mpbq const & v) { return v.is_neg(); }

src/numerics/mpq.h

@@ -211,6 +211,7 @@ public:
 template<>
 class numeric_traits<mpq> {
 public:
+    static bool precise() { return true; }
     static bool is_zero(mpq const &  v) { return v.is_zero(); }
     static bool is_pos(mpq const & v) { return v.is_pos(); }
     static bool is_neg(mpq const & v) { return v.is_neg(); }

src/numerics/mpz.h

@@ -221,6 +221,7 @@ public:
 template<>
 class numeric_traits<mpz> {
 public:
+    static bool precise() { return true; }
     static bool is_zero(mpz const & v) { return v.is_zero(); }
     static bool is_pos(mpz const & v) { return v.is_pos(); }
     static bool is_neg(mpz const & v) { return v.is_neg(); }

src/numerics/numeric_traits.h

@@ -18,6 +18,7 @@ void double_power(double & v, unsigned k);
 template<>
 class numeric_traits<double> {
 public:
+    static bool precise() { return false; }
     static bool is_zero(double v) { return v == 0.0; }
     static bool is_pos(double v) { return v > 0.0; }
     static bool is_neg(double v) { return v < 0.0; }