From ff04c5a2e2d4841c226bf6a470548a0a46f8c48c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Oct 2013 16:35:42 -0700 Subject: [PATCH] test(numerics): add test to make sure that zeros of different precision mpfp numbers are the equal. Signed-off-by: Leonardo de Moura --- src/tests/util/numerics/mpfp.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/tests/util/numerics/mpfp.cpp b/src/tests/util/numerics/mpfp.cpp index aee6cdbe7..15db9c962 100644 --- a/src/tests/util/numerics/mpfp.cpp +++ b/src/tests/util/numerics/mpfp.cpp @@ -37,10 +37,28 @@ static void tst1() { std::cout << "exp(b, UP ) = |" << exp(b, MPFR_RNDU) << "|" << std::endl; std::cout << "exp(b, NEAR) = |" << exp(b, MPFR_RNDN) << "|" << std::endl; std::cout << "exp(b, DOWN) = |" << exp(b, MPFR_RNDD) << "|" << std::endl; + + mpfp d = mpfp(6.141592, 512); + std::cout << "d = |" << d << "|" << std::endl; + std::cout << "exp(d, UP ) = |" << exp(d, MPFR_RNDU) << "|" << std::endl; + std::cout << "exp(d, NEAR) = |" << exp(d, MPFR_RNDN) << "|" << std::endl; + std::cout << "exp(d, DOWN) = |" << exp(d, MPFR_RNDD) << "|" << std::endl; + } +static void tst2() { + mpfp a(10.0, 64); + mpfp b(10.0, 128); + lean_assert(a == b); + for (unsigned i = 16; i < 256; i++) { + for (unsigned j = 16; j < 256; j++) { + lean_assert_eq(mpfp(0.0, i), mpfp(0.0, j)); + } + } +} int main() { tst1(); + tst2(); return has_violations() ? 1 : 0; }