diff --git a/README-CMake.md b/README-CMake.md
index 2cec1653a..0943e7a7d 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -279,6 +279,10 @@ The following useful options can be passed to CMake whilst configuring.
* ``INSTALL_DOTNET_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOTNET_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's .NET bindings.
* ``DOTNET_CSC_EXECUTABLE`` - STRING. The path to the C# compiler to use. Only relevant if ``BUILD_DOTNET_BINDINGS`` is set to ``TRUE``.
* ``DOTNET_GACUTIL_EXECUTABLE`` - STRING. The path to the gacutil program to use. Only relevant if ``BUILD_DOTNET_BINDINGS`` is set to ``TRUE``.
+* ``BUILD_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Java bindings will be built.
+* ``INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings.
+* ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
+* ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.
@@ -286,8 +290,29 @@ Example
```
cmake -DCMAKE_BUILD_TYPE=Release -DENABLE_TRACING=FALSE ../
+
```
+## Z3 API Bindings
+
+Z3 exposes various language bindings for its API. Below are some notes on building
+and/or installing these bindings when building Z3 with CMake.
+
+### Java bindings
+
+The CMake build uses the ``FindJava`` and ``FindJNI`` cmake modules to detect the
+installation of Java. If CMake fails to find your installation of Java set the
+``JAVA_HOME`` environment variable when invoking CMake so that it points at the
+correct location. For example
+
+```
+JAVA_HOME=/usr/lib/jvm/default cmake -DBUILD_JAVA_BINDINGS=ON ../
+```
+Note that the built ``.jar`` file is named ``com.microsoft.z3-VERSION.jar``
+where ``VERSION`` is the Z3 version. Under non Windows systems a
+symbolic link named ``com.microsoft.z3.jar`` is provided. This symbolic
+link is not created when building under Windows.
+
## Developer/packager notes
These notes are help developers and packagers of Z3.
diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt
index 13403afb1..574dd1089 100644
--- a/contrib/cmake/src/CMakeLists.txt
+++ b/contrib/cmake/src/CMakeLists.txt
@@ -234,4 +234,16 @@ if (BUILD_DOTNET_BINDINGS)
add_subdirectory(api/dotnet)
endif()
+################################################################################
+# Java bindings
+################################################################################
+option(BUILD_JAVA_BINDINGS "Build Java bindings for Z3" OFF)
+if (BUILD_JAVA_BINDINGS)
+ if (NOT BUILD_LIBZ3_SHARED)
+ message(FATAL_ERROR "The Java bindings will not work with a static libz3. "
+ "You either need to disable BUILD_JAVA_BINDINGS or enable BUILD_LIBZ3_SHARED")
+ endif()
+ add_subdirectory(api/java)
+endif()
+
# TODO: Implement support for other bindigns
diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/contrib/cmake/src/api/java/CMakeLists.txt
new file mode 100644
index 000000000..6e16ddb74
--- /dev/null
+++ b/contrib/cmake/src/api/java/CMakeLists.txt
@@ -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})
+z3_append_linker_flag_list_to_target(z3java ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+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
+ Constructor.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
+ IDisposable.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()
diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py
index 482b13c94..e582d8468 100755
--- a/scripts/mk_consts_files.py
+++ b/scripts/mk_consts_files.py
@@ -17,6 +17,11 @@ def main(args):
parser.add_argument("api_files", nargs="+")
parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None)
parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None)
+ parser.add_argument("--java-output-dir", dest="java_output_dir", default=None)
+ parser.add_argument("--java-package-name",
+ dest="java_package_name",
+ default=None,
+ help="Name to give the Java package (e.g. ``com.microsoft.z3``).")
pargs = parser.parse_args(args)
if not mk_genfile_common.check_files_exist(pargs.api_files):
@@ -41,6 +46,20 @@ def main(args):
logging.info('Generated "{}"'.format(output))
count += 1
+ if pargs.java_output_dir:
+ if pargs.java_package_name == None:
+ logging.error('Java package name must be specified')
+ return 1
+ if not mk_genfile_common.check_dir_exists(pargs.java_output_dir):
+ return 1
+ outputs = mk_genfile_common.mk_z3consts_java_internal(
+ pargs.api_files,
+ pargs.java_package_name,
+ pargs.java_output_dir)
+ for generated_file in outputs:
+ logging.info('Generated "{}"'.format(generated_file))
+ count += 1
+
if count == 0:
logging.info('No files generated. You need to specific an output directory'
' for the relevant langauge bindings')
diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
index 0734d52b0..b8d6ac5e1 100644
--- a/scripts/mk_genfile_common.py
+++ b/scripts/mk_genfile_common.py
@@ -255,6 +255,116 @@ def mk_z3consts_dotnet_internal(api_files, output_dir):
z3consts.close()
return z3consts_output_path
+
+def mk_z3consts_java_internal(api_files, package_name, output_dir):
+ """
+ Generate "com.microsoft.z3.enumerations" package from the list of API
+ header files in ``api_files`` and write the package directory into
+ the ``output_dir`` directory
+
+ Returns a list of the generated java source files.
+ """
+ blank_pat = re.compile("^ *$")
+ comment_pat = re.compile("^ *//.*$")
+ typedef_pat = re.compile("typedef enum *")
+ typedef2_pat = re.compile("typedef enum { *")
+ openbrace_pat = re.compile("{ *")
+ closebrace_pat = re.compile("}.*;")
+
+ DeprecatedEnums = [ 'Z3_search_failure' ]
+ gendir = os.path.join(output_dir, "enumerations")
+ if not os.path.exists(gendir):
+ os.mkdir(gendir)
+
+ generated_enumeration_files = []
+ for api_file in api_files:
+ api = open(api_file, 'r')
+
+ SEARCHING = 0
+ FOUND_ENUM = 1
+ IN_ENUM = 2
+
+ mode = SEARCHING
+ decls = {}
+ idx = 0
+
+ linenum = 1
+ for line in api:
+ m1 = blank_pat.match(line)
+ m2 = comment_pat.match(line)
+ if m1 or m2:
+ # skip blank lines and comments
+ linenum = linenum + 1
+ elif mode == SEARCHING:
+ m = typedef_pat.match(line)
+ if m:
+ mode = FOUND_ENUM
+ m = typedef2_pat.match(line)
+ if m:
+ mode = IN_ENUM
+ decls = {}
+ idx = 0
+ elif mode == FOUND_ENUM:
+ m = openbrace_pat.match(line)
+ if m:
+ mode = IN_ENUM
+ decls = {}
+ idx = 0
+ else:
+ assert False, "Invalid %s, line: %s" % (api_file, linenum)
+ else:
+ assert mode == IN_ENUM
+ words = re.split('[^\-a-zA-Z0-9_]+', line)
+ m = closebrace_pat.match(line)
+ if m:
+ name = words[1]
+ if name not in DeprecatedEnums:
+ efile = open('%s.java' % os.path.join(gendir, name), 'w')
+ generated_enumeration_files.append(efile.name)
+ efile.write('/**\n * Automatically generated file\n **/\n\n')
+ efile.write('package %s.enumerations;\n\n' % package_name)
+
+ efile.write('/**\n')
+ efile.write(' * %s\n' % name)
+ efile.write(' **/\n')
+ efile.write('public enum %s {\n' % name)
+ efile.write
+ first = True
+ # Iterate over key-value pairs ordered by value
+ for k, v in sorted(decls.items(), key=lambda pair: pair[1]):
+ if first:
+ first = False
+ else:
+ efile.write(',\n')
+ efile.write(' %s (%s)' % (k, v))
+ efile.write(";\n")
+ efile.write('\n private final int intValue;\n\n')
+ efile.write(' %s(int v) {\n' % name)
+ efile.write(' this.intValue = v;\n')
+ efile.write(' }\n\n')
+ efile.write(' public static final %s fromInt(int v) {\n' % name)
+ efile.write(' for (%s k: values()) \n' % name)
+ efile.write(' if (k.intValue == v) return k;\n')
+ efile.write(' return values()[0];\n')
+ efile.write(' }\n\n')
+ efile.write(' public final int toInt() { return this.intValue; }\n')
+ # efile.write(';\n %s(int v) {}\n' % name)
+ efile.write('}\n\n')
+ efile.close()
+ mode = SEARCHING
+ else:
+ if words[2] != '':
+ if len(words[2]) > 1 and words[2][1] == 'x':
+ idx = int(words[2], 16)
+ else:
+ idx = int(words[2])
+ decls[words[1]] = idx
+ idx = idx + 1
+ linenum = linenum + 1
+ api.close()
+ return generated_enumeration_files
+
+
###############################################################################
# Functions for generating a "module definition file" for MSVC
###############################################################################
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index be641ba35..38bf2a854 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2753,109 +2753,19 @@ def mk_z3consts_dotnet(api_files):
# Extract enumeration types from z3_api.h, and add Java definitions
def mk_z3consts_java(api_files):
- blank_pat = re.compile("^ *$")
- comment_pat = re.compile("^ *//.*$")
- typedef_pat = re.compile("typedef enum *")
- typedef2_pat = re.compile("typedef enum { *")
- openbrace_pat = re.compile("{ *")
- closebrace_pat = re.compile("}.*;")
-
java = get_component(JAVA_COMPONENT)
-
- DeprecatedEnums = [ 'Z3_search_failure' ]
- gendir = os.path.join(java.src_dir, "enumerations")
- if not os.path.exists(gendir):
- os.mkdir(gendir)
-
+ full_path_api_files = []
for api_file in api_files:
api_file_c = java.find_file(api_file, java.name)
api_file = os.path.join(api_file_c.src_dir, api_file)
-
- api = open(api_file, 'r')
-
- SEARCHING = 0
- FOUND_ENUM = 1
- IN_ENUM = 2
-
- mode = SEARCHING
- decls = {}
- idx = 0
-
- linenum = 1
- for line in api:
- m1 = blank_pat.match(line)
- m2 = comment_pat.match(line)
- if m1 or m2:
- # skip blank lines and comments
- linenum = linenum + 1
- elif mode == SEARCHING:
- m = typedef_pat.match(line)
- if m:
- mode = FOUND_ENUM
- m = typedef2_pat.match(line)
- if m:
- mode = IN_ENUM
- decls = {}
- idx = 0
- elif mode == FOUND_ENUM:
- m = openbrace_pat.match(line)
- if m:
- mode = IN_ENUM
- decls = {}
- idx = 0
- else:
- assert False, "Invalid %s, line: %s" % (api_file, linenum)
- else:
- assert mode == IN_ENUM
- words = re.split('[^\-a-zA-Z0-9_]+', line)
- m = closebrace_pat.match(line)
- if m:
- name = words[1]
- if name not in DeprecatedEnums:
- efile = open('%s.java' % os.path.join(gendir, name), 'w')
- efile.write('/**\n * Automatically generated file\n **/\n\n')
- efile.write('package %s.enumerations;\n\n' % java.package_name)
-
- efile.write('/**\n')
- efile.write(' * %s\n' % name)
- efile.write(' **/\n')
- efile.write('public enum %s {\n' % name)
- efile.write
- first = True
- for k in decls:
- i = decls[k]
- if first:
- first = False
- else:
- efile.write(',\n')
- efile.write(' %s (%s)' % (k, i))
- efile.write(";\n")
- efile.write('\n private final int intValue;\n\n')
- efile.write(' %s(int v) {\n' % name)
- efile.write(' this.intValue = v;\n')
- efile.write(' }\n\n')
- efile.write(' public static final %s fromInt(int v) {\n' % name)
- efile.write(' for (%s k: values()) \n' % name)
- efile.write(' if (k.intValue == v) return k;\n')
- efile.write(' return values()[0];\n')
- efile.write(' }\n\n')
- efile.write(' public final int toInt() { return this.intValue; }\n')
- # efile.write(';\n %s(int v) {}\n' % name)
- efile.write('}\n\n')
- efile.close()
- mode = SEARCHING
- else:
- if words[2] != '':
- if len(words[2]) > 1 and words[2][1] == 'x':
- idx = int(words[2], 16)
- else:
- idx = int(words[2])
- decls[words[1]] = idx
- idx = idx + 1
- linenum = linenum + 1
- api.close()
+ full_path_api_files.append(api_file)
+ generated_files = mk_genfile_common.mk_z3consts_java_internal(
+ full_path_api_files,
+ java.package_name,
+ java.src_dir)
if VERBOSE:
- print("Generated '%s'" % ('%s' % gendir))
+ for generated_file in generated_files:
+ print("Generated '{}'".format(generated_file))
# Extract enumeration types from z3_api.h, and add ML definitions
def mk_z3consts_ml(api_files):