From 707dbd4173a6dff25d4b4212df64240406c01824 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 17 Oct 2016 16:19:27 +0100 Subject: [PATCH 1/6] Bugfix for bv2fpa (model) conversion. Relates to #740 --- src/ast/fpa/bv2fpa_converter.cpp | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index fb3af396c..50f13aeee 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -316,13 +316,21 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model app * a2 = to_app(val->get_arg(2)); expr_ref v0(m), v1(m), v2(m); +#ifdef Z3DEBUG v0 = mc->get_const_interp(a0->get_decl()); v1 = mc->get_const_interp(a1->get_decl()); v2 = mc->get_const_interp(a2->get_decl()); +#else + expr * bv = mc->get_const_interp(to_app(to_app(a0)->get_arg(0))->get_decl()); + unsigned bv_sz = m_bv_util.get_bv_size(bv); + v0 = m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv); + v1 = m_bv_util.mk_extract(bv_sz-2, sbits-1, bv); + v2 = m_bv_util.mk_extract(sbits-2, 0, bv); +#endif - if (!v0) v0 = m_bv_util.mk_numeral(0, 1); - if (!v1) v1 = m_bv_util.mk_numeral(0, ebits); - if (!v2) v2 = m_bv_util.mk_numeral(0, sbits-1); + if (!v0) v0 = m_bv_util.mk_numeral(0, 1); + if (!v1) v1 = m_bv_util.mk_numeral(0, ebits); + if (!v2) v2 = m_bv_util.mk_numeral(0, sbits-1); expr_ref sgn(m), exp(m), sig(m); m_th_rw(v0, sgn); From 2f6ef0f3be4ba96dd09c7f1c7c13d88bc77f19c7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 17 Oct 2016 16:33:09 +0100 Subject: [PATCH 2/6] Removed unnecessary variables. --- src/ast/fpa/fpa2bv_converter.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 05c45c925..da473f993 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3295,8 +3295,6 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg void fpa2bv_converter::mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 0); - unsigned ebits = f->get_parameter(0).get_int(); - unsigned sbits = f->get_parameter(1).get_int(); unsigned width = m_bv_util.get_bv_size(f->get_range()); if (m_hi_fp_unspecified) @@ -3326,8 +3324,6 @@ expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 0); - unsigned ebits = f->get_parameter(0).get_int(); - unsigned sbits = f->get_parameter(1).get_int(); unsigned width = m_bv_util.get_bv_size(f->get_range()); if (m_hi_fp_unspecified) @@ -3339,7 +3335,7 @@ void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * m_uf2bvuf.insert(f, fd); m.inc_ref(f); m.inc_ref(fd); - } + } result = m.mk_const(fd); } From 4ef55505e7f8ca5b35b88ec1c2e1a2c331460d40 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 17 Oct 2016 17:12:04 +0100 Subject: [PATCH 3/6] [CMake] Fix #763 reported by @jirislaby. `INTERFACE` was the not appropriate usage requirement to use. However it only caused a problem when USE_LIB_GMP was enabled. With `INTERFACE` `-lgmp` was not specified on the link line so `libz3.so` did not have a reference to the library and linking against `libz3.so` by clients would fail with missing references to symbols in `libgmp`. --- contrib/cmake/src/CMakeLists.txt | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index cba30c46f..f12c56f8e 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -136,9 +136,10 @@ if (NOT MSVC) set_target_properties(libz3 PROPERTIES OUTPUT_NAME z3) endif() -# Using INTERFACE means that targets that try link against libz3 will -# automatically link against the libs in Z3_DEPENDENT_LIBS -target_link_libraries(libz3 INTERFACE ${Z3_DEPENDENT_LIBS}) +# The `PRIVATE` usage requirement is specified so that when building Z3 as a +# shared library the dependent libraries are specified on the link command line +# so that if those are also shared libraries they are referenced by `libz3.so`. +target_link_libraries(libz3 PRIVATE ${Z3_DEPENDENT_LIBS}) z3_append_linker_flag_list_to_target(libz3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) From 03071db3eda047743442f1160af28f223ddb6608 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 17 Oct 2016 18:00:08 +0100 Subject: [PATCH 4/6] [CMake] Fix building the examples when libz3 is built as a static library. --- contrib/cmake/examples/c++/CMakeLists.txt | 5 +++++ contrib/cmake/examples/c/CMakeLists.txt | 6 ++++++ 2 files changed, 11 insertions(+) diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/contrib/cmake/examples/c++/CMakeLists.txt index 85bbd77c7..fdc5cf387 100644 --- a/contrib/cmake/examples/c++/CMakeLists.txt +++ b/contrib/cmake/examples/c++/CMakeLists.txt @@ -1,4 +1,9 @@ +# FIXME: We should build this as an external project and consume +# Z3 as `find_package(z3 CONFIG)`. add_executable(cpp_example EXCLUDE_FROM_ALL example.cpp) target_link_libraries(cpp_example PRIVATE libz3) target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++") +if (NOT BUILD_LIBZ3_SHARED) + z3_append_linker_flag_list_to_target(cpp_example ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) +endif() diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/contrib/cmake/examples/c/CMakeLists.txt index 1a14573ac..fc6eaee18 100644 --- a/contrib/cmake/examples/c/CMakeLists.txt +++ b/contrib/cmake/examples/c/CMakeLists.txt @@ -1,3 +1,9 @@ +# FIXME: We should build this as an external project and consume +# Z3 as `find_package(z3 CONFIG)`. add_executable(c_example EXCLUDE_FROM_ALL test_capi.c) target_link_libraries(c_example PRIVATE libz3) target_include_directories(c_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") +# This is needed for when libz3 is built as a static library +if (NOT BUILD_LIBZ3_SHARED) + z3_append_linker_flag_list_to_target(c_example ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}) +endif() From 462d3e8e8b6ac0f8319bd0f8e73aa82e85d02e1a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 17 Oct 2016 18:15:31 +0100 Subject: [PATCH 5/6] [CMake] Unbreak building the .NET bindings. 7fefe40f210300dc073c93b2889be274bd92da62 broke building the .NET bindings by renaming the signing key without updating the CMake build. --- contrib/cmake/src/api/dotnet/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contrib/cmake/src/api/dotnet/CMakeLists.txt b/contrib/cmake/src/api/dotnet/CMakeLists.txt index 7440f021b..93f5929d9 100644 --- a/contrib/cmake/src/api/dotnet/CMakeLists.txt +++ b/contrib/cmake/src/api/dotnet/CMakeLists.txt @@ -156,7 +156,7 @@ elseif (DOTNET_TOOLCHAIN_IS_MONO) # We need to give the assembly a strong name so that it can be installed # into the GAC. list(APPEND CSC_FLAGS - "/keyfile:${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.mono.snk" + "/keyfile:${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.snk" ) else() message(FATAL_ERROR "Unknown .NET toolchain") From 289e51f4557baebb08ea37f951bf92fc01b3c1ef Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 17 Oct 2016 18:30:49 +0100 Subject: [PATCH 6/6] [CMake] Fix building the Java bindings. This was broken due to 495ef0f055f300089ec57f7aa71c2cc48d0fd402 and a914822346179531cf36c79809e5f01842267c84 adding and removing source files without updating the CMake build. --- contrib/cmake/src/api/java/CMakeLists.txt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/contrib/cmake/src/api/java/CMakeLists.txt index 6e16ddb74..b34277266 100644 --- a/contrib/cmake/src/api/java/CMakeLists.txt +++ b/contrib/cmake/src/api/java/CMakeLists.txt @@ -110,7 +110,9 @@ set(Z3_JAVA_JAR_SOURCE_FILES BitVecSort.java BoolExpr.java BoolSort.java + ConstructorDecRefQueue.java Constructor.java + ConstructorListDecRefQueue.java ConstructorList.java Context.java DatatypeExpr.java @@ -136,7 +138,6 @@ set(Z3_JAVA_JAR_SOURCE_FILES GoalDecRefQueue.java Goal.java IDecRefQueue.java - IDisposable.java InterpolationContext.java IntExpr.java IntNum.java