From 7768aa5487f357f020682b45a49b87567eb98dbb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Oct 2015 10:35:48 -0700 Subject: [PATCH 1/3] compiler warning by daniel j h Signed-off-by: Nikolaj Bjorner --- src/ast/ast.h | 2 +- src/muz/rel/dl_sparse_table.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index deddd3cad..32a5c78ba 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -523,7 +523,7 @@ public: /** The ids of expressions and declarations are in different ranges. */ -const unsigned c_first_decl_id = (1 << 31); +const unsigned c_first_decl_id = (1u << 31u); /** \brief Superclass for function declarations and sorts. diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h index 95dccdf89..a45f4e6c6 100644 --- a/src/muz/rel/dl_sparse_table.h +++ b/src/muz/rel/dl_sparse_table.h @@ -350,7 +350,7 @@ namespace datalog { *ptr&=m_write_mask; *ptr|=val< { From 2912c355e223dd3b49534c1392dae7a5513fdf9e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Oct 2015 10:54:19 -0700 Subject: [PATCH 2/3] remove reinterpret_cast. Issue #229, issue #24 Signed-off-by: Nikolaj Bjorner --- src/interp/iz3foci.cpp | 21 ++++++++++----------- src/muz/pdr/pdr_util.cpp | 2 +- src/muz/rel/dl_sparse_table.cpp | 2 +- src/muz/rel/tbv.cpp | 2 +- src/util/hwf.h | 4 ++-- 5 files changed, 15 insertions(+), 16 deletions(-) diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp index e0773209b..3a873de2c 100755 --- a/src/interp/iz3foci.cpp +++ b/src/interp/iz3foci.cpp @@ -19,7 +19,6 @@ #include #include -#include #include "iz3hash.h" #include "foci2.h" @@ -197,7 +196,7 @@ public: std::cerr << "iZ3: unsupported Z3 operator in expression\n "; print_expr(std::cerr,t); std::cerr << "\n"; - assert(0 && "iZ3: unsupported Z3 operator"); + SASSERT(0 && "iZ3: unsupported Z3 operator"); } } return res; @@ -272,7 +271,7 @@ public: } break; default: - assert("unknown built-in op"); + SASSERT(false && "unknown built-in op"); } } else if(foci->get_int(i,nval)){ @@ -280,15 +279,15 @@ public: } else if(foci->get_func(i,f)){ if(f == select_op){ - assert(n == 2); + SASSERT(n == 2); res = make(Select,args[0],args[1]); } else if(f == store_op){ - assert(n == 3); + SASSERT(n == 3); res = make(Store,args[0],args[1],args[2]); } else if(f == mod_op){ - assert(n == 2); + SASSERT(n == 2); res = make(Mod,args[0],args[1]); } else { @@ -298,20 +297,20 @@ public: if(bar.second){ std::cout << "unknown function symbol:\n"; foci->show_ast(i); - assert(0); + SASSERT(0); } res = make(func_decl,args); } } else { std::cerr << "iZ3: unknown FOCI expression kind\n"; - assert(0 && "iZ3: unknown FOCI expression kind"); + SASSERT(0 && "iZ3: unknown FOCI expression kind"); } return res; } int interpolate(const std::vector &cnsts, std::vector &itps){ - assert((int)cnsts.size() == frames); + SASSERT((int)cnsts.size() == frames); std::string lia("lia"); #ifdef _FOCI2 foci = foci2::create(lia); @@ -320,7 +319,7 @@ public: #endif if(!foci){ std::cerr << "iZ3: cannot find foci lia solver.\n"; - assert(0); + SASSERT(0); } select_op = foci->mk_func("select"); store_op = foci->mk_func("store"); @@ -335,7 +334,7 @@ public: } int res = foci->interpolate(foci_cnsts, foci_itps, foci_parents); if(res == 0){ - assert((int)foci_itps.size() == frames-1); + SASSERT((int)foci_itps.size() == frames-1); itps.resize(frames-1); for(int i = 0; i < frames-1; i++){ // foci->show_ast(foci_itps[i]); diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp index f8758d997..9af3ea8b4 100644 --- a/src/muz/pdr/pdr_util.cpp +++ b/src/muz/pdr/pdr_util.cpp @@ -73,7 +73,7 @@ namespace pdr { } std::string pp_cube(unsigned sz, app * const * lits, ast_manager& m) { - return pp_cube(sz, reinterpret_cast(lits), m); + return pp_cube(sz, (expr * const *)(lits), m); } std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& m) { diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp index 2c806971f..24fda3e96 100644 --- a/src/muz/rel/dl_sparse_table.cpp +++ b/src/muz/rel/dl_sparse_table.cpp @@ -293,7 +293,7 @@ namespace datalog { void key_to_reserve(const key_value & key) const { m_keys.ensure_reserve(); - m_keys.write_into_reserve(reinterpret_cast(key.c_ptr())); + m_keys.write_into_reserve((char *)(key.c_ptr())); } offset_vector & get_matching_offset_vector(const key_value & key) { diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 6e030a823..568f63f51 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -43,7 +43,7 @@ void tbv_manager::reset() { m.reset(); } tbv* tbv_manager::allocate() { - tbv* r = reinterpret_cast(m.allocate()); + tbv* r = static_cast(m.allocate()); DEBUG_CODE( if (s_debug_alloc) { TRACE("doc", tout << allocated_tbvs.size() << " " << r << "\n";); diff --git a/src/util/hwf.h b/src/util/hwf.h index 7b17553d2..d2055d56e 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -131,11 +131,11 @@ public: return (x.get_raw() & 0x8000000000000000ull) != 0; } - const uint64 sig(hwf const & x) const { + uint64 sig(hwf const & x) const { return x.get_raw() & 0x000FFFFFFFFFFFFFull; } - const int exp(hwf const & x) const { + int exp(hwf const & x) const { return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023; } From 1bb9864d0f27b634249427c09640197737ac266a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Oct 2015 11:24:22 -0700 Subject: [PATCH 3/3] comment out diverging portion of unit test. Issue #210 Signed-off-by: Nikolaj Bjorner --- src/test/expr_substitution.cpp | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/src/test/expr_substitution.cpp b/src/test/expr_substitution.cpp index 8af3f7197..fdf1d6dc2 100644 --- a/src/test/expr_substitution.cpp +++ b/src/test/expr_substitution.cpp @@ -47,16 +47,23 @@ void tst_expr_substitution() { expr_substitution subst(m); th_rewriter rw(m); + std::cout << mk_pp(c, m) << "\n"; + // normalizing c does not help. rw(c, d, pr); - subst.insert(b, d); - rw.set_substitution(&subst); + std::cout << mk_pp(d, m) << "\n"; + + +// This portion diverges. It attempts to replace x by (bvadd #xfc x), which contains x. +// subst.insert(b, d); + +// std::cout << mk_pp(a, m) << "\n"; +// rw.set_substitution(&subst); +// enable_trace("th_rewriter_step"); +// rw(a, new_a, pr); - enable_trace("th_rewriter_step"); - rw(a, new_a, pr); - - std::cout << mk_pp(new_a, m) << "\n"; +// std::cout << mk_pp(new_a, m) << "\n"; }