From 4857de6c8116cd6d78c153c6051b5e6d5af10d87 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 4 Oct 2015 15:16:03 +0100
Subject: [PATCH 1/7] fixed buggy if condition
---
src/test/ddnf.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp
index 8620bd441..d2ca92557 100644
--- a/src/test/ddnf.cpp
+++ b/src/test/ddnf.cpp
@@ -123,7 +123,7 @@ datalog::ddnf_core* populate_ddnf(char const* file, ptr_vector<tbv>& tbvs) {
static void read_args(char ** argv, int argc, int& i) {
- if (argc = i + 2) {
+ if (argc == i + 2) {
g_file = argv[i + 1];
++i;
return;
From fbac183e32ec7e3aedc5f8c44eba544b6113abfd Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 4 Oct 2015 15:16:41 +0100
Subject: [PATCH 2/7] eliminated unused variable
---
src/test/doc.cpp | 1 -
1 file changed, 1 deletion(-)
diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index b2863a629..331901734 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -181,7 +181,6 @@ class test_doc_cls {
expr_ref result(m);
expr_ref_vector conjs(m);
unsigned n = m2.num_tbits();
- tbv_manager& tm = m2.tbvm();
SASSERT(n <= m_vars.size());
for (unsigned i = 0; i < n; ++i) {
switch (t[i]) {
From b20224bc9810bb1557ca29729871ec1f061b1a82 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 4 Oct 2015 15:21:17 +0100
Subject: [PATCH 3/7] Removed or commented unused functions and variables.
---
src/test/simplex.cpp | 52 ++++++++++++++++++++++----------------------
1 file changed, 26 insertions(+), 26 deletions(-)
diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp
index 61ab7180b..3a5e58a4b 100644
--- a/src/test/simplex.cpp
+++ b/src/test/simplex.cpp
@@ -24,35 +24,35 @@ static vector<R> vec(int i, int j) {
return nv;
}
-static vector<R> vec(int i, int j, int k) {
- vector<R> nv = vec(i, j);
- nv.push_back(R(k));
- return nv;
-}
+// static vector<R> vec(int i, int j, int k) {
+// vector<R> nv = vec(i, j);
+// nv.push_back(R(k));
+// return nv;
+// }
-static vector<R> vec(int i, int j, int k, int l) {
- vector<R> nv = vec(i, j, k);
- nv.push_back(R(l));
- return nv;
-}
+// static vector<R> vec(int i, int j, int k, int l) {
+// vector<R> nv = vec(i, j, k);
+// nv.push_back(R(l));
+// return nv;
+// }
-static vector<R> vec(int i, int j, int k, int l, int x) {
- vector<R> nv = vec(i, j, k, l);
- nv.push_back(R(x));
- return nv;
-}
+/// static vector<R> vec(int i, int j, int k, int l, int x) {
+/// vector<R> nv = vec(i, j, k, l);
+/// nv.push_back(R(x));
+/// return nv;
+/// }
-static vector<R> vec(int i, int j, int k, int l, int x, int y) {
- vector<R> nv = vec(i, j, k, l, x);
- nv.push_back(R(y));
- return nv;
-}
+// static vector<R> vec(int i, int j, int k, int l, int x, int y) {
+// vector<R> nv = vec(i, j, k, l, x);
+// nv.push_back(R(y));
+// return nv;
+// }
-static vector<R> vec(int i, int j, int k, int l, int x, int y, int z) {
- vector<R> nv = vec(i, j, k, l, x, y);
- nv.push_back(R(z));
- return nv;
-}
+// static vector<R> vec(int i, int j, int k, int l, int x, int y, int z) {
+// vector<R> nv = vec(i, j, k, l, x, y);
+// nv.push_back(R(z));
+// return nv;
+// }
@@ -148,7 +148,7 @@ void tst_simplex() {
coeffs.push_back(mpz(i+1));
}
- Simplex::row r = S.add_row(1, coeffs.size(), vars.c_ptr(), coeffs.c_ptr());
+ // Simplex::row r = S.add_row(1, coeffs.size(), vars.c_ptr(), coeffs.c_ptr());
is_sat = S.make_feasible();
std::cout << "feasible: " << is_sat << "\n";
S.display(std::cout);
From 32194b3f36c55be35efada11fe9c6aa180fd4a1f Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 4 Oct 2015 15:22:10 +0100
Subject: [PATCH 4/7] Eliminated unused variables.
---
src/tactic/fpa/fpa2bv_model_converter.cpp | 2 --
1 file changed, 2 deletions(-)
diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp
index e4d51ed45..91f7bd3d4 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_model_converter.cpp
@@ -179,8 +179,6 @@ expr_ref fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, func_decl * var,
void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
fpa_util fu(m);
bv_util bu(m);
- unsynch_mpz_manager & mpzm = fu.fm().mpz_manager();
- unsynch_mpq_manager & mpqm = fu.fm().mpq_manager();
TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
for (unsigned i = 0; i < bv_mdl->get_num_constants(); i++)
From c636c87e4d1b3f11acc48118def4355093b4da65 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 4 Oct 2015 15:51:27 +0100
Subject: [PATCH 5/7] Eliminated unused variable
---
src/test/old_interval.cpp | 1 -
1 file changed, 1 deletion(-)
diff --git a/src/test/old_interval.cpp b/src/test/old_interval.cpp
index 91096a629..92064c03e 100644
--- a/src/test/old_interval.cpp
+++ b/src/test/old_interval.cpp
@@ -172,7 +172,6 @@ public:
static void tst2() {
typedef basic_interval_manager<unsynch_mpz_manager, false> mpzi_manager;
- typedef mpzi_manager::interval mpzi;
typedef mpzi_manager::scoped_interval scoped_mpzi;
unsynch_mpz_manager nm;
From 462619690769addb27d957077acd63c0999868cb Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 4 Oct 2015 15:52:20 +0100
Subject: [PATCH 6/7] Eliminated reinterpret_casts. Partially fixes #24, #229.
---
src/util/hwf.cpp | 7 ++++---
src/util/mpfx.cpp | 10 +++++++---
2 files changed, 11 insertions(+), 6 deletions(-)
diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
index 21f1c281f..0c1e2d3de 100644
--- a/src/util/hwf.cpp
+++ b/src/util/hwf.cpp
@@ -85,8 +85,9 @@ hwf_manager::~hwf_manager()
{
}
-#define RAW(X) (*reinterpret_cast<const uint64*>(&(X)))
-#define DBL(X) (*reinterpret_cast<const double*>(&(X)))
+// #define RAW(X) (*reinterpret_cast<const uint64*>(&(X)))
+#define RAW(X) ({ uint64 tmp; memcpy(&tmp, &(X), sizeof(uint64)); tmp; })
+#define DBL(X) ({ double tmp; memcpy(&tmp, &(X), sizeof(double)); tmp; })
void hwf_manager::set(hwf & o, int value) {
o.value = (double) value;
@@ -166,7 +167,7 @@ void hwf_manager::set(hwf & o, bool sign, uint64 significand, int exponent) {
uint64 raw = (sign?0x8000000000000000ull:0);
raw |= (((uint64)exponent) + 1023) << 52;
raw |= significand;
- o.value = *reinterpret_cast<double*>(&raw);
+ memcpy(&o.value, &raw, sizeof(double));
}
void hwf_manager::set(hwf & o, hwf const & x) {
diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp
index c75a43046..f9a51ebd7 100644
--- a/src/util/mpfx.cpp
+++ b/src/util/mpfx.cpp
@@ -199,8 +199,9 @@ void mpfx_manager::set(mpfx & n, uint64 v) {
else {
allocate_if_needed(n);
n.m_sign = 0;
- unsigned * _v = reinterpret_cast<unsigned*>(&v);
unsigned * w = words(n);
+ unsigned * _v = 0;
+ memcpy(_v, &v, sizeof(unsigned*));
for (unsigned i = 0; i < m_total_sz; i++)
w[i] = 0;
w[m_frac_part_sz] = _v[0];
@@ -679,7 +680,8 @@ int64 mpfx_manager::get_int64(mpfx const & n) const {
SASSERT(is_int64(n));
unsigned * w = words(n);
w += m_frac_part_sz;
- uint64 r = *reinterpret_cast<uint64*>(w);
+ uint64 r = 0;
+ memcpy(&r, w, sizeof(uint64));
if (r == 0x8000000000000000ull) {
SASSERT(is_neg(n));
return INT64_MIN;
@@ -693,7 +695,9 @@ uint64 mpfx_manager::get_uint64(mpfx const & n) const {
SASSERT(is_uint64(n));
unsigned * w = words(n);
w += m_frac_part_sz;
- return *reinterpret_cast<uint64*>(w);
+ uint64 r = 0;
+ memcpy(&r, w, sizeof(uint64));
+ return r;
}
template<bool SYNCH>
From f11502e0ac8539a7e83a1cce0ae86f44ec620a7c Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 4 Oct 2015 16:41:28 +0100
Subject: [PATCH 7/7] reinterpret_cast fixes for the Windows compiler.
---
src/util/hwf.cpp | 5 ++---
src/util/mpfx.cpp | 3 ++-
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
index 0c1e2d3de..3963836f2 100644
--- a/src/util/hwf.cpp
+++ b/src/util/hwf.cpp
@@ -85,9 +85,8 @@ hwf_manager::~hwf_manager()
{
}
-// #define RAW(X) (*reinterpret_cast<const uint64*>(&(X)))
-#define RAW(X) ({ uint64 tmp; memcpy(&tmp, &(X), sizeof(uint64)); tmp; })
-#define DBL(X) ({ double tmp; memcpy(&tmp, &(X), sizeof(double)); tmp; })
+uint64 RAW(double X) { uint64 tmp; memcpy(&tmp, &(X), sizeof(uint64)); return tmp; }
+double DBL(uint64 X) { double tmp; memcpy(&tmp, &(X), sizeof(double)); return tmp; }
void hwf_manager::set(hwf & o, int value) {
o.value = (double) value;
diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp
index f9a51ebd7..41ed93617 100644
--- a/src/util/mpfx.cpp
+++ b/src/util/mpfx.cpp
@@ -200,8 +200,9 @@ void mpfx_manager::set(mpfx & n, uint64 v) {
allocate_if_needed(n);
n.m_sign = 0;
unsigned * w = words(n);
+ uint64 * _vp = &v;
unsigned * _v = 0;
- memcpy(_v, &v, sizeof(unsigned*));
+ memcpy(&_v, &_vp, sizeof(unsigned*));
for (unsigned i = 0; i < m_total_sz; i++)
w[i] = 0;
w[m_frac_part_sz] = _v[0];