Merge branch 'master' of https://github.com/Z3Prover/z3

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()

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()

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
+# The `PRIVATE` usage requirement is specified so that when building Z3 as a
-# automatically link against the libs in Z3_DEPENDENT_LIBS
+# shared library the dependent libraries are specified on the link command line
-target_link_libraries(libz3 INTERFACE ${Z3_DEPENDENT_LIBS})
+# 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})
 

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")

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

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 (!v0) v0 = m_bv_util.mk_numeral(0, 1);
-		if (!v1) v1 = m_bv_util.mk_numeral(0, ebits);
+        if (!v1) v1 = m_bv_util.mk_numeral(0, ebits);
-		if (!v2) v2 = m_bv_util.mk_numeral(0, sbits-1);
+        if (!v2) v2 = m_bv_util.mk_numeral(0, sbits-1);
 
 		expr_ref sgn(m), exp(m), sig(m);
 		m_th_rw(v0, sgn);

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);
 	}