From f2ff0712249dde9f394d15de99ab01b8d40c831c Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 7 Oct 2015 20:17:04 +0100
Subject: [PATCH 1/2] Bugfix for mpf to_ieee_bv
---
src/util/mpf.cpp | 9 +++++++--
src/util/mpf.h | 1 +
2 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 855668e5a..e56e0ce87 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -1176,12 +1176,14 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
SASSERT(!is_nan(x) && !is_inf(x));
SASSERT(exp(x) < INT_MAX);
-
+
unsigned sbits = x.get_sbits();
unsigned ebits = x.get_ebits();
+ scoped_mpz biased_exp(m_mpz_manager);
+ m_mpz_manager.set(biased_exp, bias_exp(ebits, exp(x)));
m_mpz_manager.set(o, sgn(x));
m_mpz_manager.mul2k(o, ebits);
- m_mpz_manager.add(o, (int)exp(x), o);
+ m_mpz_manager.add(o, biased_exp, o);
m_mpz_manager.mul2k(o, sbits - 1);
m_mpz_manager.add(o, sig(x), o);
}
@@ -1519,6 +1521,9 @@ mpf_exp_t mpf_manager::mk_max_exp(unsigned ebits) {
return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, false));
}
+mpf_exp_t mpf_manager::bias_exp(unsigned ebits, mpf_exp_t unbiased_exponent) {
+ return unbiased_exponent + m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false));
+}
mpf_exp_t mpf_manager::unbias_exp(unsigned ebits, mpf_exp_t biased_exponent) {
return biased_exponent - m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false));
}
diff --git a/src/util/mpf.h b/src/util/mpf.h
index 1e934275f..0e9d3e89c 100644
--- a/src/util/mpf.h
+++ b/src/util/mpf.h
@@ -197,6 +197,7 @@ public:
mpf_exp_t mk_max_exp(unsigned ebits);
mpf_exp_t mk_min_exp(unsigned ebits);
+ mpf_exp_t bias_exp(unsigned ebits, mpf_exp_t unbiased_exponent);
mpf_exp_t unbias_exp(unsigned ebits, mpf_exp_t biased_exponent);
/**
From fcf036695e603a8b927676d4e3661c492837f7e9 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 7 Oct 2015 20:17:04 +0100
Subject: [PATCH 2/2] Bugfix for mpf to_ieee_bv
---
src/util/mpf.cpp | 9 +++++++--
src/util/mpf.h | 1 +
2 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 855668e5a..e56e0ce87 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -1176,12 +1176,14 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
SASSERT(!is_nan(x) && !is_inf(x));
SASSERT(exp(x) < INT_MAX);
-
+
unsigned sbits = x.get_sbits();
unsigned ebits = x.get_ebits();
+ scoped_mpz biased_exp(m_mpz_manager);
+ m_mpz_manager.set(biased_exp, bias_exp(ebits, exp(x)));
m_mpz_manager.set(o, sgn(x));
m_mpz_manager.mul2k(o, ebits);
- m_mpz_manager.add(o, (int)exp(x), o);
+ m_mpz_manager.add(o, biased_exp, o);
m_mpz_manager.mul2k(o, sbits - 1);
m_mpz_manager.add(o, sig(x), o);
}
@@ -1519,6 +1521,9 @@ mpf_exp_t mpf_manager::mk_max_exp(unsigned ebits) {
return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, false));
}
+mpf_exp_t mpf_manager::bias_exp(unsigned ebits, mpf_exp_t unbiased_exponent) {
+ return unbiased_exponent + m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false));
+}
mpf_exp_t mpf_manager::unbias_exp(unsigned ebits, mpf_exp_t biased_exponent) {
return biased_exponent - m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false));
}
diff --git a/src/util/mpf.h b/src/util/mpf.h
index 1e934275f..0e9d3e89c 100644
--- a/src/util/mpf.h
+++ b/src/util/mpf.h
@@ -197,6 +197,7 @@ public:
mpf_exp_t mk_max_exp(unsigned ebits);
mpf_exp_t mk_min_exp(unsigned ebits);
+ mpf_exp_t bias_exp(unsigned ebits, mpf_exp_t unbiased_exponent);
mpf_exp_t unbias_exp(unsigned ebits, mpf_exp_t biased_exponent);
/**