mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-06-13 19:03:45 -07:00
commit 7023af4528
101 changed files with 35 additions and 317 deletions
Download patch file Download diff file Expand all files Collapse all files

74
src/api/CMakeLists.txt Normal file
View file

@ -0,0 +1,74 @@
set(generated_files
api_commands.cpp
api_log_macros.cpp
api_log_macros.h
)
# Sanity check
foreach (gen_file ${generated_files})
if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}")
message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${gen_files}\""
${z3_polluted_tree_msg})
endif()
endforeach()
set(full_path_generated_files "")
foreach (gen_file ${generated_files})
list(APPEND full_path_generated_files "${CMAKE_CURRENT_BINARY_DIR}/${gen_file}")
endforeach()
add_custom_command(OUTPUT ${generated_files}
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--api_output_dir"
"${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating ${generated_files}"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
VERBATIM
)
z3_add_component(api
SOURCES
api_algebraic.cpp
api_arith.cpp
api_array.cpp
api_ast.cpp
api_ast_map.cpp
api_ast_vector.cpp
api_bv.cpp
api_config_params.cpp
api_context.cpp
api_datalog.cpp
api_datatype.cpp
api_fpa.cpp
api_goal.cpp
api_interp.cpp
api_log.cpp
api_model.cpp
api_numeral.cpp
api_opt.cpp
api_params.cpp
api_parsers.cpp
api_pb.cpp
api_polynomial.cpp
api_quant.cpp
api_rcf.cpp
api_seq.cpp
api_solver.cpp
api_stats.cpp
api_tactic.cpp
z3_replayer.cpp
${full_path_generated_files}
COMPONENT_DEPENDENCIES
interp
opt
portfolio
realclosure
smtparser
)

13
src/api/dll/CMakeLists.txt Normal file
View file

@ -0,0 +1,13 @@
set(api_dll_deps api extra_cmds sat)
z3_add_component(api_dll
SOURCES
dll.cpp
"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
COMPONENT_DEPENDENCIES
${api_dll_deps}
)
z3_add_install_tactic_rule(${api_dll_deps})
z3_add_memory_initializer_rule(${api_dll_deps})
z3_add_gparams_register_modules_rule(${api_dll_deps})

291
src/api/dotnet/CMakeLists.txt Normal file
View file

@ -0,0 +1,291 @@
find_package(DotNetToolchain REQUIRED)
# Configure AssemblyInfo.cs
set(VER_MAJOR "${Z3_VERSION_MAJOR}")
set(VER_MINOR "${Z3_VERSION_MINOR}")
set(VER_BUILD "${Z3_VERSION_PATCH}")
set(VER_REVISION "${Z3_VERSION_TWEAK}")
set(Z3_DOTNET_ASSEMBLY_INFO_FILE "${CMAKE_CURRENT_BINARY_DIR}/Properties/AssemblyInfo.cs")
configure_file("Properties/AssemblyInfo.cs.in" "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" @ONLY)
# Generate Native.cs
set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs")
add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--dotnet-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating ${Z3_DOTNET_NATIVE_FILE}"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
# Generate Enumerations.cs
set(Z3_DOTNET_CONST_FILE "${CMAKE_CURRENT_BINARY_DIR}/Enumerations.cs")
add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--dotnet-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating ${Z3_DOTNET_CONST_FILE}"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
AlgebraicNum.cs
ApplyResult.cs
ArithExpr.cs
ArithSort.cs
ArrayExpr.cs
ArraySort.cs
AST.cs
ASTMap.cs
ASTVector.cs
BitVecExpr.cs
BitVecNum.cs
BitVecSort.cs
BoolExpr.cs
BoolSort.cs
Constructor.cs
ConstructorList.cs
Context.cs
DatatypeExpr.cs
DatatypeSort.cs
Deprecated.cs
EnumSort.cs
Expr.cs
FiniteDomainExpr.cs
FiniteDomainNum.cs
FiniteDomainSort.cs
Fixedpoint.cs
FPExpr.cs
FPNum.cs
FPRMExpr.cs
FPRMNum.cs
FPRMSort.cs
FPSort.cs
FuncDecl.cs
FuncInterp.cs
Global.cs
Goal.cs
IDecRefQueue.cs
InterpolationContext.cs
IntExpr.cs
IntNum.cs
IntSort.cs
IntSymbol.cs
ListSort.cs
Log.cs
Model.cs
Optimize.cs
ParamDescrs.cs
Params.cs
Pattern.cs
Probe.cs
Quantifier.cs
RatNum.cs
RealExpr.cs
RealSort.cs
ReExpr.cs
RelationSort.cs
ReSort.cs
SeqExpr.cs
SeqSort.cs
SetSort.cs
Solver.cs
Sort.cs
Statistics.cs
Status.cs
StringSymbol.cs
Symbol.cs
Tactic.cs
TupleSort.cs
UninterpretedSort.cs
Version.cs
Z3Exception.cs
Z3Object.cs
)
set(Z3_DOTNET_ASSEMBLY_SOURCES "")
# Make paths to source files absolute
foreach (csfile ${Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE})
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES "${CMAKE_CURRENT_SOURCE_DIR}/${csfile}")
endforeach()
# Add generated files
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES
"${Z3_DOTNET_CONST_FILE}"
"${Z3_DOTNET_NATIVE_FILE}"
"${Z3_DOTNET_ASSEMBLY_INFO_FILE}"
)
# ``csc.exe`` doesn't like UNIX style paths so convert them
# if necessary first to native paths.
set(Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "")
foreach (csfile_path ${Z3_DOTNET_ASSEMBLY_SOURCES})
file(TO_NATIVE_PATH "${csfile_path}" csfile_path_native)
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "${csfile_path_native}")
endforeach()
set(CSC_FLAGS "")
if (DOTNET_TOOLCHAIN_IS_WINDOWS)
# FIXME: Why use these flags?
# Note these flags have been copied from the Python build system.
list(APPEND CSC_FLAGS
"/noconfig"
"/nostdlib+"
"/reference:mscorlib.dll"
)
# FIXME: This flag only works when the working directory of csc.exe is
# the directory containing the ``libz3`` target. I can't get this to work
# correctly with multi-configuration generators (i.e. Visual Studio) so
# just don't set the flag for now.
#list(APPEND CSC_FLAGS "/linkresource:$<TARGET_FILE_NAME:libz3>")
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.snk"
)
else()
message(FATAL_ERROR "Unknown .NET toolchain")
endif()
# Common flags
list(APPEND CSC_FLAGS
"/unsafe+"
"/nowarn:1701,1702"
"/errorreport:prompt"
"/warn:4"
"/reference:System.Core.dll"
"/reference:System.dll"
"/reference:System.Numerics.dll"
"/filealign:512" # Why?
"/target:library"
)
# Set the build type flags. The build type for the assembly roughly corresponds
# with the native code build type.
list(APPEND CSC_FLAGS
# Debug flags, expands to nothing if we aren't doing a debug build
"$<$<CONFIG:Debug>:/debug+>"
"$<$<CONFIG:Debug>:/debug:full>"
"$<$<CONFIG:Debug>:/optimize->"
# This has to be quoted otherwise the ``;`` is interpreted as a command separator
"$<$<CONFIG:Debug>:\"/define:DEBUG$<SEMICOLON>TRACE\">"
# Release flags, expands to nothing if we are doing a debug build
"$<$<NOT:$<CONFIG:Debug>>:/optimize+>"
)
# Mono's gacutil crashes when trying to install an assembly if we set the
# platform in some cases, so only set it on Windows. This bug has been
# reported at https://bugzilla.xamarin.com/show_bug.cgi?id=39955 . However mono
# ignores the platform of an assembly when running it (
# http://lists.ximian.com/pipermail/mono-devel-list/2015-November/043370.html )
# so this shouldn't matter in practice.
if (DOTNET_TOOLCHAIN_IS_WINDOWS)
# Set platform for assembly
if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
list(APPEND CSC_FLAGS "/platform:x64")
elseif ("${TARGET_ARCHITECTURE}" STREQUAL "i686")
list(APPEND CSC_FLAGS "/platform:x86")
endif()
endif()
# FIXME: Ideally we should emit files into a configuration specific directory
# when using multi-configuration generators so that the files generated by each
# configuration don't clobber each other. Unfortunately the ``get_property()``
# command only works correctly for single configuration generators so we can't
# use it. We also can't use ``$<TARGET_FILE_DIR:libz3>`` because the ``OUTPUT``
# argument to ``add_custom_commands()`` won't accept it.
# See http://public.kitware.com/pipermail/cmake/2016-March/063101.html
#
# For now just output file to the root binary directory like the Python build
# system does and emit a warning when appropriate.
if (DEFINED CMAKE_CONFIGURATION_TYPES)
# Multi-configuration build (e.g. Visual Studio and Xcode).
message(WARNING "You are using a multi-configuration generator. The build rules for"
" the \".NET\" bindings currently do not emit files per configuration so previously"
" generated files for other configurations will be overwritten.")
endif()
set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_BINARY_DIR}")
set(Z3_DOTNET_ASSEMBLY_NAME "Microsoft.Z3.dll")
set(Z3_DOTNET_ASSEMBLY_DLL "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/${Z3_DOTNET_ASSEMBLY_NAME}")
# csc.exe doesn't work with UNIX style paths so convert to native path
file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL}" Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH)
set(Z3_DOTNET_ASSEMBLY_DLL_DOC "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/Microsoft.Z3.xml")
file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH)
add_custom_command(OUTPUT "${Z3_DOTNET_ASSEMBLY_DLL}" "${Z3_DOTNET_ASSEMBLY_DLL_DOC}"
COMMAND
"${DOTNET_CSC_EXECUTABLE}"
${CSC_FLAGS}
"/out:${Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH}"
"/doc:${Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH}"
${Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH}
DEPENDS
${Z3_DOTNET_ASSEMBLY_SOURCES}
libz3
WORKING_DIRECTORY "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}"
COMMENT "Building \"${Z3_DOTNET_ASSEMBLY_DLL}\""
)
# Convenient top-level target
add_custom_target(build_z3_dotnet_bindings
ALL
DEPENDS
"${Z3_DOTNET_ASSEMBLY_DLL}"
)
###############################################################################
# Install
###############################################################################
option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install target" ON)
set(GAC_PKG_NAME "Microsoft.Z3.Sharp")
set(PREFIX "${CMAKE_INSTALL_PREFIX}")
set(VERSION "${Z3_VERSION}")
set(Z3_DOTNET_PKGCONFIG_FILE "${CMAKE_CURRENT_BINARY_DIR}/Microsoft.Z3.Sharp.pc")
configure_file("Microsoft.Z3.Sharp.pc.in" "${Z3_DOTNET_PKGCONFIG_FILE}" @ONLY)
if (DOTNET_TOOLCHAIN_IS_MONO)
message(STATUS "Emitting install rules for .NET bindings")
# Install pkgconfig file for the assembly. This is needed by Monodevelop
# to find the assembly
install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}")
# Configure the install and uninstall scripts.
# Note: If multi-configuration generator support is ever fixed then these
# scripts will be broken.
configure_file(cmake_install_gac.cmake.in cmake_install_gac.cmake @ONLY)
configure_file(cmake_uninstall_gac.cmake.in cmake_uninstall_gac.cmake @ONLY)
# Tell CMake to Invoke a script to install assembly to the GAC during install
install(SCRIPT "${CMAKE_CURRENT_BINARY_DIR}/cmake_install_gac.cmake")
# Add custom target to uninstall the assembly from the GAC
add_custom_target(remove_dotnet_dll_from_gac
COMMAND "${CMAKE_COMMAND}" "-P" "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall_gac.cmake"
COMMENT "Uninstalling ${Z3_DOTNET_ASSEMBLY_NAME} from the GAC"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
add_dependencies(uninstall remove_dotnet_dll_from_gac)
elseif(DOTNET_TOOLCHAIN_IS_WINDOWS)
# Don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead just copy into
# installation directory.
install(FILES "${Z3_DOTNET_ASSEMBLY_DLL}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
install(FILES "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
else()
message(FATAL_ERROR "Unknown .NET toolchain")
endif()

18
src/api/dotnet/cmake_install_gac.cmake.in Normal file
View file

@ -0,0 +1,18 @@
# Install assembly to the GAC
set(GAC_ROOT "$ENV{DESTDIR}@CMAKE_INSTALL_FULL_LIBDIR@")
execute_process(COMMAND
"@DOTNET_GACUTIL_EXECUTABLE@"
"-i"
"@Z3_DOTNET_ASSEMBLY_DLL@"
"-f"
"-package" "@GAC_PKG_NAME@"
"-root" "${GAC_ROOT}"
WORKING_DIRECTORY "@CMAKE_CURRENT_BINARY_DIR@"
RESULT_VARIABLE gacutil_exit_code
)
if ("${gacutil_exit_code}" EQUAL 0)
message(STATUS "Installed \"@Z3_DOTNET_ASSEMBLY_DLL@\" to the GAC")
else()
message(FATAL_ERROR "Failed to install \"@Z3_DOTNET_ASSEMBLY_DLL@\" to the GAC")
endif()

20
src/api/dotnet/cmake_uninstall_gac.cmake.in Normal file
View file

@ -0,0 +1,20 @@
# Uninstall assembly from the GAC
set(GAC_ROOT "$ENV{DESTDIR}@CMAKE_INSTALL_FULL_LIBDIR@")
execute_process(COMMAND
"@DOTNET_GACUTIL_EXECUTABLE@"
# Note ``-us`` takes assembly file name rather than
# ``-u`` which takes an assembly display name
"-us"
"@Z3_DOTNET_ASSEMBLY_NAME@"
"-f"
"-package" "@GAC_PKG_NAME@"
"-root" "${GAC_ROOT}"
WORKING_DIRECTORY "@CMAKE_CURRENT_BINARY_DIR@"
RESULT_VARIABLE gacutil_exit_code
)
if ("${gacutil_exit_code}" EQUAL 0)
message(STATUS "Uninstalled \"@Z3_DOTNET_ASSEMBLY_NAME@\" from the GAC")
else()
message(FATAL_ERROR "Failed to uninstall \"@Z3_DOTNET_ASSEMBLY_NAME@\" from the GAC")
endif()

236
src/api/java/CMakeLists.txt Normal file
View file

@ -0,0 +1,236 @@
find_package(Java REQUIRED)
find_package(JNI REQUIRED)
include(UseJava)
# Sanity check for dirty source tree
foreach (file_name "enumerations" "Native.cpp" "Native.java")
if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${file_name}")
message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${file_name}\""
${z3_polluted_tree_msg})
endif()
endforeach()
set(Z3_JAVA_PACKAGE_NAME "com.microsoft.z3")
# Rule to generate ``Native.java`` and ``Native.cpp``
set(Z3_JAVA_NATIVE_JAVA "${CMAKE_CURRENT_BINARY_DIR}/Native.java")
set(Z3_JAVA_NATIVE_CPP "${CMAKE_CURRENT_BINARY_DIR}/Native.cpp")
add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--java-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
"--java-package-name"
${Z3_JAVA_PACKAGE_NAME}
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\""
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
# Add rule to build native code that provides a bridge between
# ``Native.java`` and libz3's interfac3.
add_library(z3java SHARED ${Z3_JAVA_NATIVE_CPP})
target_link_libraries(z3java PRIVATE libz3)
# FIXME:
# Not sure if using all the flags used by the Z3 components is really necessary
# here. At the bare minimum setting _AMD64_ depending on the target is
# necessary but seeing as the Python build system uses all the flags used for building
# Z3's components to build ``Native.cpp`` lets do the same for now.
target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
target_include_directories(z3java PRIVATE
"${CMAKE_SOURCE_DIR}/src/api"
"${CMAKE_BINARY_DIR}/src/api"
${JNI_INCLUDE_DIRS}
)
# FIXME: Should this library have SONAME and VERSION set?
# This prevents CMake from automatically defining ``z3java_EXPORTS``
set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")
# Rule to generate the ``com.microsoft.z3.enumerations`` package
# FIXME: This list of files is fragile
set(Z3_JAVA_ENUMERATION_PACKAGE_FILES
Z3_ast_kind.java
Z3_ast_print_mode.java
Z3_decl_kind.java
Z3_error_code.java
Z3_goal_prec.java
Z3_lbool.java
Z3_param_kind.java
Z3_parameter_kind.java
Z3_sort_kind.java
Z3_symbol_kind.java
)
set(Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH "")
foreach (enum_file ${Z3_JAVA_ENUMERATION_PACKAGE_FILES})
list(APPEND Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH
"${CMAKE_CURRENT_BINARY_DIR}/enumerations/${enum_file}"
)
endforeach()
add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--java-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
"--java-package-name"
${Z3_JAVA_PACKAGE_NAME}
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating ${Z3_JAVA_PACKAGE_NAME}.enumerations package"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
set(Z3_JAVA_JAR_SOURCE_FILES
AlgebraicNum.java
ApplyResultDecRefQueue.java
ApplyResult.java
ArithExpr.java
ArithSort.java
ArrayExpr.java
ArraySort.java
ASTDecRefQueue.java
AST.java
AstMapDecRefQueue.java
ASTMap.java
AstVectorDecRefQueue.java
ASTVector.java
BitVecExpr.java
BitVecNum.java
BitVecSort.java
BoolExpr.java
BoolSort.java
ConstructorDecRefQueue.java
Constructor.java
ConstructorListDecRefQueue.java
ConstructorList.java
Context.java
DatatypeExpr.java
DatatypeSort.java
EnumSort.java
Expr.java
FiniteDomainExpr.java
FiniteDomainNum.java
FiniteDomainSort.java
FixedpointDecRefQueue.java
Fixedpoint.java
FPExpr.java
FPNum.java
FPRMExpr.java
FPRMNum.java
FPRMSort.java
FPSort.java
FuncDecl.java
FuncInterpDecRefQueue.java
FuncInterpEntryDecRefQueue.java
FuncInterp.java
Global.java
GoalDecRefQueue.java
Goal.java
IDecRefQueue.java
InterpolationContext.java
IntExpr.java
IntNum.java
IntSort.java
IntSymbol.java
ListSort.java
Log.java
ModelDecRefQueue.java
Model.java
OptimizeDecRefQueue.java
Optimize.java
ParamDescrsDecRefQueue.java
ParamDescrs.java
ParamsDecRefQueue.java
Params.java
Pattern.java
ProbeDecRefQueue.java
Probe.java
Quantifier.java
RatNum.java
RealExpr.java
RealSort.java
ReExpr.java
RelationSort.java
ReSort.java
SeqExpr.java
SeqSort.java
SetSort.java
SolverDecRefQueue.java
Solver.java
Sort.java
StatisticsDecRefQueue.java
Statistics.java
Status.java
StringSymbol.java
Symbol.java
TacticDecRefQueue.java
Tactic.java
TupleSort.java
UninterpretedSort.java
Version.java
Z3Exception.java
Z3Object.java
)
set(Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "")
foreach (java_src_file ${Z3_JAVA_JAR_SOURCE_FILES})
list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "${CMAKE_CURRENT_SOURCE_DIR}/${java_src_file}")
endforeach()
# Add generated files to list
list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH
${Z3_JAVA_NATIVE_JAVA}
${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
)
# Convenient top-level target
add_custom_target(build_z3_java_bindings
ALL
DEPENDS
z3java
z3JavaJar
)
# Rule to build ``com.microsoft.z3.jar``
# TODO: Should we set ``CMAKE_JNI_TARGET`` to ``TRUE``?
add_jar(z3JavaJar
SOURCES ${Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH}
OUTPUT_NAME ${Z3_JAVA_PACKAGE_NAME}
OUTPUT_DIR "${CMAKE_BINARY_DIR}"
VERSION "${Z3_VERSION}"
)
###############################################################################
# Install
###############################################################################
option(INSTALL_JAVA_BINDINGS "Install Java bindings when invoking install target" ON)
if (INSTALL_JAVA_BINDINGS)
# Provide cache variables for the install locations that the user can change.
# This defaults to ``/usr/local/java`` which seems to be the location for ``.jar``
# files on Linux distributions
set(Z3_JAVA_JAR_INSTALLDIR
"${CMAKE_INSTALL_DATAROOTDIR}/java"
CACHE
PATH
"Directory to install Z3 Java jar file relative to install prefix"
)
# FIXME: I don't think this the right installation location
set(Z3_JAVA_JNI_LIB_INSTALLDIR
"${CMAKE_INSTALL_LIBDIR}"
CACHE
PATH
"Directory to install Z3 Java JNI bridge library relative to install prefix"
)
install(TARGETS z3java DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}")
# Note: Don't use ``DESTINATION`` here as the version of ``UseJava.cmake`` shipped
# with CMake 2.8.12.2 handles that incorrectly.
install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}")
endif()

32
src/api/java/FuncDecl.java
View file

@ -1,6 +1,6 @@
/**
Copyright (c) 2012-2014 Microsoft Corporation
Module Name:
FuncDecl.java
@ -12,8 +12,8 @@ Author:
@author Christoph Wintersteiger (cwinter) 2012-03-15
Notes:
**/
**/
package com.microsoft.z3;
@ -59,6 +59,24 @@ public class FuncDecl extends AST
return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
}
/**
* Translates (copies) the function declaration to the Context {@code ctx}.
* @param ctx A context
*
* @return A copy of the function declaration which is associated with {@code ctx}
* @throws Z3Exception on error
**/
public FuncDecl translate(Context ctx)
{
if (getContext() == ctx) {
return this;
} else {
return new FuncDecl(ctx, Native.translate(getContext().nCtx(),
getNativeObject(), ctx.nCtx()));
}
}
/**
* The arity of the function declaration
**/
@ -68,7 +86,7 @@ public class FuncDecl extends AST
}
/**
* The size of the domain of the function declaration
* The size of the domain of the function declaration
* @see #getArity
**/
public int getDomainSize()
@ -324,7 +342,7 @@ public class FuncDecl extends AST
}
FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
{
super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
AST.arrayLength(domain), AST.arrayToNative(domain),
@ -333,7 +351,7 @@ public class FuncDecl extends AST
}
FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
{
super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
AST.arrayLength(domain), AST.arrayToNative(domain),
@ -351,7 +369,7 @@ public class FuncDecl extends AST
}
/**
* Create expression that applies function to arguments.
* Create expression that applies function to arguments.
**/
public Expr apply(Expr ... args)
{

143
src/api/python/CMakeLists.txt Normal file
View file

@ -0,0 +1,143 @@
message(STATUS "Emitting rules to build Z3 python bindings")
###############################################################################
# Add target to build python bindings for the build directory
###############################################################################
# This allows the python bindings to be used directly from the build directory
set(z3py_files
z3/__init__.py
z3/z3.py
z3/z3num.py
z3/z3poly.py
z3/z3printer.py
z3/z3rcf.py
z3test.py
z3/z3types.py
z3/z3util.py
)
set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}/python")
file(MAKE_DIRECTORY "${z3py_bindings_build_dest}")
file(MAKE_DIRECTORY "${z3py_bindings_build_dest}/z3")
set(build_z3_python_bindings_target_depends "")
foreach (z3py_file ${z3py_files})
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${z3py_file}"
COMMAND "${CMAKE_COMMAND}" "-E" "copy"
"${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
"${z3py_bindings_build_dest}/${z3py_file}"
DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}/${z3py_file}"
)
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/${z3py_file}")
endforeach()
# Generate z3core.py
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--z3py-output-dir"
"${z3py_bindings_build_dest}"
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating z3core.py"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3core.py")
# Generate z3consts.py
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3consts.py"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--z3py-output-dir"
"${z3py_bindings_build_dest}"
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating z3consts.py"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3consts.py")
if (UNIX)
set(LINK_COMMAND "create_symlink")
else()
set(LINK_COMMAND "copy")
endif()
# Link libz3 into the python directory so bindings work out of the box
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
"${CMAKE_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
"${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
DEPENDS libz3
COMMENT "Linking libz3 into python directory"
)
# Convenient top-level target
add_custom_target(build_z3_python_bindings
ALL
DEPENDS
${build_z3_python_bindings_target_depends}
"${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
)
###############################################################################
# Install
###############################################################################
option(INSTALL_PYTHON_BINDINGS "Install Python bindings when invoking install target" ON)
if (INSTALL_PYTHON_BINDINGS)
message(STATUS "Emitting rules to install Z3 python bindings")
# Try to guess the installation path for the bindings
if (NOT DEFINED CMAKE_INSTALL_PYTHON_PKG_DIR)
message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR not set. Trying to guess")
execute_process(
COMMAND "${PYTHON_EXECUTABLE}" "-c"
"import distutils.sysconfig; print(distutils.sysconfig.get_python_lib())"
RESULT_VARIABLE exit_code
OUTPUT_VARIABLE CMAKE_INSTALL_PYTHON_PKG_DIR
OUTPUT_STRIP_TRAILING_WHITESPACE
)
if (NOT ("${exit_code}" EQUAL 0))
message(FATAL_ERROR "Failed to determine your Python package directory")
endif()
message(STATUS "Detected Python package directory: \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
# Set a cache variable that the user can modify if needed
set(CMAKE_INSTALL_PYTHON_PKG_DIR
"${CMAKE_INSTALL_PYTHON_PKG_DIR}"
CACHE PATH
"Path to install python bindings. This can be relative or absolute.")
mark_as_advanced(CMAKE_INSTALL_PYTHON_PKG_DIR)
else()
message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR already set (\"${CMAKE_INSTALL_PYTHON_PKG_DIR}\")"
". Not trying to guess.")
endif()
# Check if path exists under the install prefix if it is absolute. If the
# path is relative it will be installed under the install prefix so there
# if nothing to check
if (IS_ABSOLUTE "${CMAKE_INSTALL_PYTHON_PKG_DIR}")
string(FIND "${CMAKE_INSTALL_PYTHON_PKG_DIR}" "${CMAKE_INSTALL_PREFIX}" position)
if (NOT ("${position}" EQUAL 0))
message(WARNING "The directory to install the python bindings \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\" "
"is not under the install prefix \"${CMAKE_INSTALL_PREFIX}\"."
" Running the install target may lead to a broken installation. "
"To change the install directory modify the CMAKE_INSTALL_PYTHON_PKG_DIR cache variable."
)
endif()
endif()
# Using DESTDIR still seems to work even if we use an absolute path
message(STATUS "Python bindings will be installed to \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
install(FILES ${build_z3_python_bindings_target_depends}
DESTINATION "${CMAKE_INSTALL_PYTHON_PKG_DIR}/z3"
)
else()
message(STATUS "Not emitting rules to install Z3 python bindings")
endif()