diff --git a/.gitignore b/.gitignore
index 80a50ea9f..fcff2132d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -84,3 +84,5 @@ src/CMakeLists.txt
src/*/CMakeLists.txt
src/*/*/CMakeLists.txt
src/*/*/*/CMakeLists.txt
+src/api/dotnet/cmake_install_gac.cmake.in
+src/api/dotnet/cmake_uninstall_gac.cmake.in
diff --git a/CMakeLists.txt b/CMakeLists.txt
index df6d528b0..ee0810295 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -323,9 +323,35 @@ message(STATUS "Z3_DEPENDENT_EXTRA_C_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_C_LINK_FLA
# Z3 installation locations
################################################################################
include(GNUInstallDirs)
+set(CMAKE_INSTALL_PKGCONFIGDIR
+ "${CMAKE_INSTALL_LIBDIR}/pkgconfig"
+ CACHE
+ PATH
+ "Directory to install pkgconfig files"
+)
message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"")
message(STATUS "CMAKE_INSTALL_BINDIR: \"${CMAKE_INSTALL_BINDIR}\"")
message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"")
+message(STATUS "CMAKE_INSTALL_PKGCONFIGDIR: \"${CMAKE_INSTALL_PKGCONFIGDIR}\"")
+
+################################################################################
+# Uninstall rule
+################################################################################
+configure_file(
+ "${CMAKE_SOURCE_DIR}/cmake/cmake_uninstall.cmake.in"
+ "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
+ @ONLY
+)
+
+# Target needs to be declared before the components so that they can add
+# dependencies to this target so they can run their own custom uninstall rules.
+add_custom_target(uninstall
+ COMMAND
+ "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
+ COMMENT "Uninstalling..."
+ ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+ VERBATIM
+)
################################################################################
# CMake build file locations
@@ -362,19 +388,3 @@ if (ENABLE_EXAMPLE_TARGETS)
add_subdirectory(examples)
endif()
-################################################################################
-# Uninstall rule
-################################################################################
-configure_file(
- "${CMAKE_SOURCE_DIR}/cmake/cmake_uninstall.cmake.in"
- "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
- @ONLY
-)
-
-add_custom_target(uninstall
- COMMAND
- "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
- COMMENT "Uninstalling..."
- ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
- VERBATIM
-)
diff --git a/README-CMake.md b/README-CMake.md
index 47ec11a7c..2cec1653a 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -265,14 +265,20 @@ The following useful options can be passed to CMake whilst configuring.
* ``CMAKE_INSTALL_INCLUDEDIR`` - STRING. The path to install z3 include files (relative to ``CMAKE_INSTALL_PREFIX``), e.g. ``include``.
* ``CMAKE_INSTALL_LIBDIR`` - STRING. The path to install z3 libraries (relative to ``CMAKE_INSTALL_PREFIX``), e.g. ``lib``.
* ``CMAKE_INSTALL_PREFIX`` - STRING. The install prefix to use (e.g. ``/usr/local/``).
+* ``CMAKE_INSTALL_PKGCONFIGDIR`` - STRING. The path to install pkgconfig files.
* ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute.
* ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled.
* ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library.
* ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples.
* ``USE_OPENMP`` - BOOL. If set to ``TRUE`` and OpenMP support is detected build with OpenMP support.
* ``USE_LIB_GMP`` - BOOL. If set to ``TRUE`` use the GNU multiple precision library. If set to ``FALSE`` use an internal implementation.
+* ``PYTHON_EXECUTABLE`` - STRING. The python executable to use during the build.
* ``BUILD_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's python bindings will be built.
* ``INSTALL_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_PYTHON_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Python bindings.
+* ``BUILD_DOTNET_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's .NET bindings will be built.
+* ``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``.
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.
diff --git a/contrib/cmake/cmake/modules/FindDotNetToolchain.cmake b/contrib/cmake/cmake/modules/FindDotNetToolchain.cmake
new file mode 100644
index 000000000..abc4ff21c
--- /dev/null
+++ b/contrib/cmake/cmake/modules/FindDotNetToolchain.cmake
@@ -0,0 +1,53 @@
+# Tries to find a working .NET tool chain
+#
+# Once complete this will define
+# DOTNET_TOOLCHAIN_FOUND : BOOL : System has a .NET toolchain
+# DOTNET_CSC_EXECUTABLE - STRING : Path to C# compiler
+# DOTNET_GACUTIL_EXECUTABLE - STRING : Path to gacutil
+# DOTNET_TOOLCHAIN_IS_MONO : BOOL : True if detected .NET toolchain is Mono
+# DOTNET_TOOLCHAIN_IS_WINDOWS : BOOL : True if detected .NET toolchain is native Windows
+include(FindPackageHandleStandardArgs)
+
+find_program(
+ DOTNET_CSC_EXECUTABLE
+ NAMES "csc.exe" "mcs" "dmcs"
+)
+message(STATUS "DOTNET_CSC_EXECUTABLE: \"${DOTNET_CSC_EXECUTABLE}\"")
+
+find_program(
+ DOTNET_GACUTIL_EXECUTABLE
+ NAMES "gacutil.exe" "gacutil"
+)
+message(STATUS "DOTNET_GACUTIL_EXECUTABLE: \"${DOTNET_GACUTIL_EXECUTABLE}\"")
+
+# Try to determine the tool chain vendor
+set(DOTNET_DETERMINED_VENDOR FALSE)
+if (DOTNET_CSC_EXECUTABLE)
+ execute_process(COMMAND "${DOTNET_CSC_EXECUTABLE}" "/help"
+ RESULT_VARIABLE CSC_EXIT_CODE
+ OUTPUT_VARIABLE CSC_STD_OUT
+ )
+ if (${CSC_EXIT_CODE} EQUAL 0)
+ if ("${CSC_STD_OUT}" MATCHES "^Mono[ ]+C#")
+ set(DOTNET_DETERMINED_VENDOR TRUE)
+ set(DOTNET_TOOLCHAIN_IS_MONO TRUE)
+ set(DOTNET_TOOLCHAIN_IS_WINDOWS FALSE)
+ message(STATUS ".NET toolchain is Mono")
+ elseif ("${CSC_STD_OUT}" MATCHES "^Microsoft.+Visual[ ]+C#")
+ set(DOTNET_DETERMINED_VENDOR TRUE)
+ set(DOTNET_TOOLCHAIN_IS_MONO FALSE)
+ set(DOTNET_TOOLCHAIN_IS_WINDOWS TRUE)
+ message(STATUS ".NET toolchain is Windows native")
+ else()
+ message(STATUS ".NET toolchain is unknown")
+ endif()
+ endif()
+endif()
+
+# TODO: Check C# compiler works
+
+find_package_handle_standard_args(DotNetToolChain DEFAULT_MSG
+ DOTNET_CSC_EXECUTABLE
+ DOTNET_GACUTIL_EXECUTABLE
+ DOTNET_DETERMINED_VENDOR
+)
diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt
index 00dd01627..13403afb1 100644
--- a/contrib/cmake/src/CMakeLists.txt
+++ b/contrib/cmake/src/CMakeLists.txt
@@ -222,4 +222,16 @@ if (BUILD_PYTHON_BINDINGS)
add_subdirectory(api/python)
endif()
+################################################################################
+# .NET bindings
+################################################################################
+option(BUILD_DOTNET_BINDINGS "Build .NET bindings for Z3" OFF)
+if (BUILD_DOTNET_BINDINGS)
+ if (NOT BUILD_LIBZ3_SHARED)
+ message(FATAL_ERROR "The .NET bindings will not work with a static libz3. "
+ "You either need to disable BUILD_DOTNET_BINDINGS or enable BUILD_LIBZ3_SHARED")
+ endif()
+ add_subdirectory(api/dotnet)
+endif()
+
# TODO: Implement support for other bindigns
diff --git a/contrib/cmake/src/api/dotnet/CMakeLists.txt b/contrib/cmake/src/api/dotnet/CMakeLists.txt
new file mode 100644
index 000000000..f077b57ce
--- /dev/null
+++ b/contrib/cmake/src/api/dotnet/CMakeLists.txt
@@ -0,0 +1,276 @@
+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.mono.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: 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. For now just output file to the
+# current binary directory.
+# get_property(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR TARGET libz3 PROPERTY LIBRARY_OUTPUT_DIRECTORY)
+set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_CURRENT_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
+ 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)
+ # FIXME: This isn't implemented because I'm not sure how/if the assembly should
+ # be installed to the GAC.
+ message(WARNING "Install of .NET bindings is not implemented for Windows")
+else()
+ message(FATAL_ERROR "Unknown .NET toolchain")
+endif()
diff --git a/contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in b/contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in
new file mode 100644
index 000000000..d49f985c0
--- /dev/null
+++ b/contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in
@@ -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()
diff --git a/contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in b/contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in
new file mode 100644
index 000000000..14683e5b8
--- /dev/null
+++ b/contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in
@@ -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()
diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py
index 2c017bd2c..482b13c94 100755
--- a/scripts/mk_consts_files.py
+++ b/scripts/mk_consts_files.py
@@ -16,6 +16,7 @@ def main(args):
parser = argparse.ArgumentParser(description=__doc__)
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)
pargs = parser.parse_args(args)
if not mk_genfile_common.check_files_exist(pargs.api_files):
@@ -31,6 +32,15 @@ def main(args):
logging.info('Generated "{}"'.format(output))
count += 1
+ if pargs.dotnet_output_dir:
+ if not mk_genfile_common.check_dir_exists(pargs.dotnet_output_dir):
+ return 1
+ output = mk_genfile_common.mk_z3consts_dotnet_internal(
+ pargs.api_files,
+ pargs.dotnet_output_dir)
+ logging.info('Generated "{}"'.format(output))
+ 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 38d173108..0734d52b0 100644
--- a/scripts/mk_genfile_common.py
+++ b/scripts/mk_genfile_common.py
@@ -163,6 +163,98 @@ def mk_z3consts_py_internal(api_files, output_dir):
z3consts.close()
return z3consts_output_path
+def mk_z3consts_dotnet_internal(api_files, output_dir):
+ """
+ Generate ``Enumerations.cs`` from the list of API header files
+ in ``api_files`` and write the output file into
+ the ``output_dir`` directory
+
+ Returns the path to the generated file.
+ """
+ assert os.path.isdir(output_dir)
+ assert isinstance(api_files, list)
+ blank_pat = re.compile("^ *\r?$")
+ 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' ]
+ z3consts = open(os.path.join(output_dir, 'Enumerations.cs'), 'w')
+ z3consts_output_path = z3consts.name
+ z3consts.write('// Automatically generated file\n\n')
+ z3consts.write('using System;\n\n'
+ '#pragma warning disable 1591\n\n'
+ 'namespace Microsoft.Z3\n'
+ '{\n')
+
+ 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:
+ z3consts.write(' /// <summary>%s</summary>\n' % name)
+ z3consts.write(' public enum %s {\n' % name)
+ z3consts.write
+ # Iterate over key-value pairs ordered by value
+ for k, v in sorted(decls.items(), key=lambda pair: pair[1]):
+ z3consts.write(' %s = %s,\n' % (k, v))
+ z3consts.write(' }\n\n')
+ mode = SEARCHING
+ elif len(words) <= 2:
+ assert False, "Invalid %s, line: %s" % (api_file, linenum)
+ 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()
+ z3consts.write('}\n');
+ z3consts.close()
+ return z3consts_output_path
+
###############################################################################
# Functions for generating a "module definition file" for MSVC
###############################################################################
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index e6de3e8ea..be641ba35 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1913,6 +1913,7 @@ class MLComponent(Component):
for m in self.modules:
out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi')
+ out.write(' ' + os.path.join(self.sub_dir, m) + '.cmx')
out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)'))))
out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml$(LIB_EXT)'))))
out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cma'))))
@@ -2013,7 +2014,7 @@ class DotNetExampleComponent(ExampleComponent):
if VS_X64:
out.write(' /platform:x64')
elif VS_ARM:
- out.write(' /platform:arm')
+ out.write(' /platform:arm')
else:
out.write(' /platform:x86')
for csfile in get_cs_files(self.ex_dir):
@@ -2206,7 +2207,7 @@ def mk_config():
static_opt = static_opt + 'd'
config.write(
'AR_FLAGS=/nologo\n'
- 'LINK_FLAGS=/nologo %s\n'
+ 'LINK_FLAGS=/nologo %s\n'
'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
if VS_X64:
config.write(
@@ -2249,7 +2250,7 @@ def mk_config():
'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG))
-
+
# End of Windows VS config.mk
if is_verbose():
@@ -2483,7 +2484,7 @@ def mk_makefile():
print("To build Z3, open a [Visual Studio x64 Command Prompt], then")
elif VS_ARM:
print(" platform: ARM\n")
- print("To build Z3, open a [Visual Studio ARM Command Prompt], then")
+ print("To build Z3, open a [Visual Studio ARM Command Prompt], then")
else:
print(" platform: x86")
print("To build Z3, open a [Visual Studio Command Prompt], then")
@@ -2738,96 +2739,17 @@ def mk_z3consts_py(api_files):
if VERBOSE:
print("Generated '{}".format(generated_file))
-
# Extract enumeration types from z3_api.h, and add .Net definitions
def mk_z3consts_dotnet(api_files):
- blank_pat = re.compile("^ *\r?$")
- comment_pat = re.compile("^ *//.*$")
- typedef_pat = re.compile("typedef enum *")
- typedef2_pat = re.compile("typedef enum { *")
- openbrace_pat = re.compile("{ *")
- closebrace_pat = re.compile("}.*;")
-
dotnet = get_component(DOTNET_COMPONENT)
-
- DeprecatedEnums = [ 'Z3_search_failure' ]
- z3consts = open(os.path.join(dotnet.src_dir, 'Enumerations.cs'), 'w')
- z3consts.write('// Automatically generated file\n\n')
- z3consts.write('using System;\n\n'
- '#pragma warning disable 1591\n\n'
- 'namespace Microsoft.Z3\n'
- '{\n')
-
+ full_path_api_files = []
for api_file in api_files:
api_file_c = dotnet.find_file(api_file, dotnet.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:
- z3consts.write(' /// <summary>%s</summary>\n' % name)
- z3consts.write(' public enum %s {\n' % name)
- z3consts.write
- for k in decls:
- i = decls[k]
- z3consts.write(' %s = %s,\n' % (k, i))
- z3consts.write(' }\n\n')
- mode = SEARCHING
- elif len(words) <= 2:
- assert False, "Invalid %s, line: %s" % (api_file, linenum)
- 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()
- z3consts.write('}\n');
- z3consts.close()
+ full_path_api_files.append(api_file)
+ generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, dotnet.src_dir)
if VERBOSE:
- print("Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs'))
-
+ print("Generated '{}".format(generated_file))
# Extract enumeration types from z3_api.h, and add Java definitions
def mk_z3consts_java(api_files):
@@ -3388,7 +3310,7 @@ class MakeRuleCmd(object):
cls.write_cmd(out, "mkdir -p {install_root}{dir}".format(
install_root=install_root,
dir=dir))
-
+
@classmethod
def _is_path_prefix_of(cls, temp_path, target_as_abs):
"""
@@ -3517,4 +3439,3 @@ def configure_file(template_file_path, output_file_path, substitutions):
if __name__ == '__main__':
import doctest
doctest.testmod()
-