Merge pull request #539 from delcypher/cmake_dotnet_bindings

[CMake] Teach CMake to build .NET bindings

.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

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

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.
 

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

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

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

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

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

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

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
 ###############################################################################

scripts/mk_util.py

@@ -2739,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)
-
+    full_path_api_files = []
-    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')
-
     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)
-
+        full_path_api_files.append(api_file)
-        api = open(api_file, 'r')
+    generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, dotnet.src_dir)
-
-        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()
     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):