From 89f1541d83ed1a9353624e83ac66685ddef1d2ba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Oct 2015 17:15:45 -0700 Subject: [PATCH 01/10] put break statement in else branh. Issue #230 (broken loop) Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 2 ++ src/util/prime_generator.cpp | 5 ++++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 0f322c6e9..6dab74d9f 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -126,9 +126,11 @@ extern "C" { lbool r = l_undef; cancel_eh eh(*to_optimize_ptr(o)); unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout()); + unsigned rlimit = mk_c(c)->get_rlimit(); api::context::set_interruptable si(*(mk_c(c)), eh); { scoped_timer timer(timeout, &eh); + scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { r = to_optimize_ptr(o)->optimize(); } diff --git a/src/util/prime_generator.cpp b/src/util/prime_generator.cpp index a82400305..0f2441455 100644 --- a/src/util/prime_generator.cpp +++ b/src/util/prime_generator.cpp @@ -67,8 +67,11 @@ void prime_generator::process_next_k_numbers(uint64 k) { if (todo[k1] < p) { m_primes.push_back(todo[k1]); } - break; + else { + break; + } } + std::cout << "TODO:" << k1 << "\n"; unsigned k2 = 0; for (; k1 < todo_sz; k1++, k2++) { todo[k2] = todo[k1]; From 50993582ec0a679cbe9f4bc5cfb3fbf3a827833c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Oct 2015 17:15:54 -0700 Subject: [PATCH 02/10] put break statement in else branh. Issue #230 (broken loop) Signed-off-by: Nikolaj Bjorner --- src/util/prime_generator.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/prime_generator.cpp b/src/util/prime_generator.cpp index 0f2441455..6aef1305b 100644 --- a/src/util/prime_generator.cpp +++ b/src/util/prime_generator.cpp @@ -71,7 +71,6 @@ void prime_generator::process_next_k_numbers(uint64 k) { break; } } - std::cout << "TODO:" << k1 << "\n"; unsigned k2 = 0; for (; k1 < todo_sz; k1++, k2++) { todo[k2] = todo[k1]; From 62a4737d7725cf33e5ee1342152a9c255aa41ae8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Oct 2015 17:30:12 -0700 Subject: [PATCH 03/10] disable code in dl_query that depends on hard-wired file path Signed-off-by: Nikolaj Bjorner --- src/test/dl_query.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index ab5141b18..ae7313e41 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -212,6 +212,7 @@ void tst_dl_query() { //params.m_dl_default_relation = symbol("tr_hashtable"); //dl_query_test_wpa(params); + return; ast_manager m; From 459e456f6646bb93241dd8c979067dc243f6d663 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Oct 2015 17:37:33 -0700 Subject: [PATCH 04/10] disable memory finalization after quant_solve unit test. Related to issue #210 Signed-off-by: Nikolaj Bjorner --- src/test/quant_solve.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index aa1306128..ed332ce26 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -238,6 +238,7 @@ static void test_quant_solve1() { test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))", false); test_quant_solver(m, "(exists ((c Cell)) (= (cell c (cdr c1)) c1))", false); + test_quant_solver(m, "(exists ((t Tuple)) (= (tuple a P r1) t))"); test_quant_solver(m, "(exists ((t Tuple)) (= a (first t)))"); test_quant_solver(m, "(exists ((t Tuple)) (= P (second t)))"); @@ -253,11 +254,13 @@ void tst_quant_solve() { test_quant_solve1(); +#if 0 memory::finalize(); #ifdef _WINDOWS _CrtDumpMemoryLeaks(); #endif exit(0); +#endif } From 4857de6c8116cd6d78c153c6051b5e6d5af10d87 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 4 Oct 2015 15:16:03 +0100 Subject: [PATCH 05/10] 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& 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" Date: Sun, 4 Oct 2015 15:16:41 +0100 Subject: [PATCH 06/10] 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" Date: Sun, 4 Oct 2015 15:21:17 +0100 Subject: [PATCH 07/10] 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 vec(int i, int j) { return nv; } -static vector vec(int i, int j, int k) { - vector nv = vec(i, j); - nv.push_back(R(k)); - return nv; -} +// static vector vec(int i, int j, int k) { +// vector nv = vec(i, j); +// nv.push_back(R(k)); +// return nv; +// } -static vector vec(int i, int j, int k, int l) { - vector nv = vec(i, j, k); - nv.push_back(R(l)); - return nv; -} +// static vector vec(int i, int j, int k, int l) { +// vector nv = vec(i, j, k); +// nv.push_back(R(l)); +// return nv; +// } -static vector vec(int i, int j, int k, int l, int x) { - vector nv = vec(i, j, k, l); - nv.push_back(R(x)); - return nv; -} +/// static vector vec(int i, int j, int k, int l, int x) { +/// vector nv = vec(i, j, k, l); +/// nv.push_back(R(x)); +/// return nv; +/// } -static vector vec(int i, int j, int k, int l, int x, int y) { - vector nv = vec(i, j, k, l, x); - nv.push_back(R(y)); - return nv; -} +// static vector vec(int i, int j, int k, int l, int x, int y) { +// vector nv = vec(i, j, k, l, x); +// nv.push_back(R(y)); +// return nv; +// } -static vector vec(int i, int j, int k, int l, int x, int y, int z) { - vector nv = vec(i, j, k, l, x, y); - nv.push_back(R(z)); - return nv; -} +// static vector vec(int i, int j, int k, int l, int x, int y, int z) { +// vector 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" Date: Sun, 4 Oct 2015 15:22:10 +0100 Subject: [PATCH 08/10] 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" Date: Sun, 4 Oct 2015 15:51:27 +0100 Subject: [PATCH 09/10] 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 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" Date: Sun, 4 Oct 2015 15:52:20 +0100 Subject: [PATCH 10/10] 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(&(X))) -#define DBL(X) (*reinterpret_cast(&(X))) +// #define RAW(X) (*reinterpret_cast(&(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(&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(&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(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(w); + uint64 r = 0; + memcpy(&r, w, sizeof(uint64)); + return r; } template