diff --git a/.gitignore b/.gitignore
index 88ccbb56f..e189a9569 100644
--- a/.gitignore
+++ b/.gitignore
@@ -76,6 +76,3 @@ src/api/ml/z3.mllib
*.bak
doc/api
doc/code
-.vs
-examples/**/obj
-CMakeSettings.json
diff --git a/.travis.yml b/.travis.yml
index 12e62ed3d..9ec6132b6 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -20,7 +20,7 @@ env:
# 64-bit UBSan Debug build
- LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP
# 64-bit ASan Debug build
- - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so
+ - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so
# Build for running unit tests under ASan/UBSan
# FIXME: We should really be doing a debug build but the unit tests run too
# slowly when we do that.
@@ -85,7 +85,6 @@ matrix:
osx_image: xcode8.3
# Note: Apple Clang does not support OpenMP
env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 DOTNET_BINDINGS=0
-
script:
# Use `travis_wait` when doing LTO builds because this configuration will
# have long link times during which it will not show any output which
diff --git a/cmake/modules/DotnetImports.props.in b/cmake/modules/DotnetImports.props.in
deleted file mode 100644
index 090d46502..000000000
--- a/cmake/modules/DotnetImports.props.in
+++ /dev/null
@@ -1,8 +0,0 @@
-
-
- ${_DN_OUTPUT_PATH}/
- ${_DN_XPLAT_LIB_DIR}/
- ${_DN_VERSION}
- ${_DN_CUSTOM_BUILDPROPS}
-
-
diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake
deleted file mode 100644
index 98c5f2079..000000000
--- a/cmake/modules/FindDotnet.cmake
+++ /dev/null
@@ -1,471 +0,0 @@
-#.rst
-# FindDotnet
-# ----------
-#
-# Find DotNet executable, and initialize functions for adding dotnet projects.
-#
-# Results are reported in the following variables::
-#
-# DOTNET_FOUND - True if dotnet executable is found
-# DOTNET_EXE - Dotnet executable
-# DOTNET_VERSION - Dotnet version as reported by dotnet executable
-# NUGET_EXE - Nuget executable (WIN32 only)
-# NUGET_CACHE_PATH - Nuget package cache path
-#
-# The following functions are defined to add dotnet/msbuild projects:
-#
-# ADD_DOTNET -- add a project to be built by dotnet.
-#
-# ```
-# ADD_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP]
-# [CONFIG configuration]
-# [PLATFORM platform]
-# [PACKAGE output_nuget_packages... ]
-# [VERSION nuget_package_version]
-# [DEPENDS depend_nuget_packages... ]
-# [OUTPUT_PATH output_path relative to cmake binary output dir]
-# [CUSTOM_BUILDPROPS value....]
-# [SOURCES additional_file_dependencies... ]
-# [ARGUMENTS additional_build_args...]
-# [PACK_ARGUMENTS additional_pack_args...])
-# ```
-#
-# RUN_DOTNET -- Run a project with `dotnet run`. The `OUTPUT` argument represents artifacts
-# produced by running the .NET program, and can be consumed from other build steps.
-#
-# ```
-# RUN_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP]
-# [ARGUMENTS program_args...]
-# [OUTPUT outputs...]
-# [CONFIG configuration]
-# [PLATFORM platform]
-# [DEPENDS depend_nuget_packages... ]
-# [OUTPUT_PATH output_path relative to cmake binary output dir]
-# [CUSTOM_BUILDPROPS value....]
-# [SOURCES additional_file_dependencies... ])
-# ```
-#
-# ADD_MSBUILD -- add a project to be built by msbuild. Windows-only. When building in Unix systems, msbuild targets are skipped.
-#
-# ```
-# ADD_MSBUILD( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP]
-# [CONFIG configuration]
-# [PLATFORM platform]
-# [PACKAGE output_nuget_packages... ]
-# [DEPENDS depend_nuget_packages... ]
-# [CUSTOM_BUILDPROPS value....]
-# [SOURCES additional_file_dependencies... ]
-# [ARGUMENTS additional_build_args...]
-# [PACK_ARGUMENTS additional_pack_args...])
-# ```
-#
-# SMOKETEST_DOTNET -- add a dotnet smoke test project to the build. The project will be run during a build,
-# and if the program fails to build or run, the build fails. Currently only .NET Core App framework is supported.
-# Multiple smoke tests will be run one-by-one to avoid global resource conflicts.
-#
-# SMOKETEST_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP]
-# [ARGUMENTS program_args...]
-# [CONFIG configuration]
-# [PLATFORM platform]
-# [DEPENDS depend_nuget_packages... ]
-# [OUTPUT_PATH output_path relative to cmake binary output dir]
-# [CUSTOM_BUILDPROPS value....]
-# [SOURCES additional_file_dependencies... ])
-#
-# For all the above functions, `RELEASE|DEBUG` overrides `CONFIG`, `X86|X64|ANYCPU` overrides PLATFORM.
-# For Unix systems, the target framework defaults to `netstandard2.0`, unless `NETCOREAPP` is specified.
-# For Windows, the project is built as-is, allowing multi-targeting.
-#
-#
-# DOTNET_REGISTER_LOCAL_REPOSITORY -- register a local NuGet package repository.
-#
-# ```
-# DOTNET_REGISTER_LOCAL_REPOSITORY(repo_name repo_path)
-# ```
-#
-# TEST_DOTNET -- add a dotnet test project to ctest. The project will be run with `dotnet test`,
-# and trx test reports will be generated in the build directory. For Windows, all target frameworks
-# are tested against. For other platforms, only .NET Core App is tested against.
-# Test failures will not fail the build.
-# Tests are only run with `ctest -C `, not with `cmake --build ...`
-#
-# ```
-# TEST_DOTNET(
-# [ARGUMENTS additional_dotnet_test_args...]
-# [OUTPUT_PATH output_path relative to cmake binary output dir])
-# ```
-#
-# GEN_DOTNET_PROPS -- Generates a Directory.Build.props file. The created file is populated with MSBuild properties:
-# - DOTNET_PACKAGE_VERSION: a version string that can be referenced in the actual project file as $(DOTNET_PACKAGE_VERSION).
-# The version string value can be set with PACKAGE_VERSION argument, and defaults to '1.0.0'.
-# - XPLAT_LIB_DIR: points to the cmake build root directory.
-# - OutputPath: Points to the cmake binary directory (overridden by OUTPUT_PATH, relatively). Therefore, projects built without cmake will consistently output
-# to the cmake build directory.
-# - Custom properties can be injected with XML_INJECT argument, which injects an arbitrary string into the project XML file.
-#
-# ```
-# GEN_DOTNET_PROPS(
-# [PACKAGE_VERSION version]
-# [XML_INJECT xml_injection])
-# ```
-#
-# Require 3.5 for batch copy multiple files
-
-cmake_minimum_required(VERSION 3.5.0)
-
-IF(DOTNET_FOUND)
- RETURN()
-ENDIF()
-
-SET(NUGET_CACHE_PATH "~/.nuget/packages")
-FIND_PROGRAM(DOTNET_EXE dotnet)
-SET(DOTNET_MODULE_DIR ${CMAKE_CURRENT_LIST_DIR})
-
-IF(NOT DOTNET_EXE)
- SET(DOTNET_FOUND FALSE)
- IF(Dotnet_FIND_REQUIRED)
- MESSAGE(SEND_ERROR "Command 'dotnet' is not found.")
- ENDIF()
- RETURN()
-ENDIF()
-
-EXECUTE_PROCESS(
- COMMAND ${DOTNET_EXE} --version
- OUTPUT_VARIABLE DOTNET_VERSION
- OUTPUT_STRIP_TRAILING_WHITESPACE
-)
-
-IF(WIN32)
- FIND_PROGRAM(NUGET_EXE nuget PATHS ${CMAKE_BINARY_DIR}/tools)
- IF(NUGET_EXE)
- MESSAGE("-- Found nuget: ${NUGET_EXE}")
- ELSE()
- SET(NUGET_EXE ${CMAKE_BINARY_DIR}/tools/nuget.exe)
- MESSAGE("-- Downloading nuget...")
- FILE(DOWNLOAD https://dist.nuget.org/win-x86-commandline/latest/nuget.exe ${NUGET_EXE})
- MESSAGE("nuget.exe downloaded and saved to ${NUGET_EXE}")
- ENDIF()
-ENDIF()
-
-FUNCTION(DOTNET_REGISTER_LOCAL_REPOSITORY repo_name repo_path)
- MESSAGE("-- Registering NuGet local repository '${repo_name}' at '${repo_path}'.")
- GET_FILENAME_COMPONENT(repo_path ${repo_path} ABSOLUTE)
- IF(WIN32)
- STRING(REPLACE "/" "\\" repo_path ${repo_path})
- EXECUTE_PROCESS(COMMAND ${NUGET_EXE} sources list OUTPUT_QUIET)
- EXECUTE_PROCESS(COMMAND ${NUGET_EXE} sources Remove -Name "${repo_name}" OUTPUT_QUIET ERROR_QUIET)
- EXECUTE_PROCESS(COMMAND ${NUGET_EXE} sources Add -Name "${repo_name}" -Source "${repo_path}")
- ELSE()
- GET_FILENAME_COMPONENT(nuget_config ~/.nuget/NuGet/NuGet.Config ABSOLUTE)
- EXECUTE_PROCESS(COMMAND ${DOTNET_EXE} nuget locals all --list OUTPUT_QUIET)
- EXECUTE_PROCESS(COMMAND sed -i "/${repo_name}/d" "${nuget_config}")
- EXECUTE_PROCESS(COMMAND sed -i "s## \\n #g" "${nuget_config}")
- ENDIF()
-ENDFUNCTION()
-
-FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
- CMAKE_PARSE_ARGUMENTS(
- # prefix
- _DN
- # options (flags)
- "RELEASE;DEBUG;X86;X64;ANYCPU;NETCOREAPP"
- # oneValueArgs
- "CONFIG;PLATFORM;VERSION;OUTPUT_PATH"
- # multiValueArgs
- "PACKAGE;DEPENDS;ARGUMENTS;PACK_ARGUMENTS;OUTPUT;SOURCES;CUSTOM_BUILDPROPS"
- # the input arguments
- ${arguments})
-
- GET_FILENAME_COMPONENT(_DN_abs_proj "${_DN_PROJECT}" ABSOLUTE)
- GET_FILENAME_COMPONENT(_DN_proj_dir "${_DN_abs_proj}" DIRECTORY)
- GET_FILENAME_COMPONENT(_DN_projname "${_DN_PROJECT}" NAME)
- STRING(REGEX REPLACE "\\.[^.]*$" "" _DN_projname_noext ${_DN_projname})
-
- FILE(GLOB_RECURSE DOTNET_deps
- ${_DN_proj_dir}/*.cs
- ${_DN_proj_dir}/*.fs
- ${_DN_proj_dir}/*.vb
- ${_DN_proj_dir}/*.xaml
- ${_DN_proj_dir}/*.resx
- ${_DN_proj_dir}/*.xml
- ${_DN_proj_dir}/*.*proj
- ${_DN_proj_dir}/*.cs
- ${_DN_proj_dir}/*.config)
- LIST(APPEND DOTNET_deps ${_DN_SOURCES})
- SET(_DN_deps "")
- FOREACH(dep ${DOTNET_deps})
- IF(NOT dep MATCHES /obj/ AND NOT dep MATCHES /bin/)
- LIST(APPEND _DN_deps ${dep})
- ENDIF()
- ENDFOREACH()
-
-
- IF(_DN_RELEASE)
- SET(_DN_CONFIG Release)
- ELSEIF(_DN_DEBUG)
- SET(_DN_CONFIG Debug)
- ENDIF()
-
- IF(NOT _DN_CONFIG)
- SET(_DN_CONFIG "$<$:Debug>$<$>:Release>")
- ENDIF()
-
- # If platform is not specified, do not pass the Platform property.
- # dotnet will pick the default Platform.
-
- IF(_DN_X86)
- SET(_DN_PLATFORM x86)
- ELSEIF(_DN_X64)
- SET(_DN_PLATFORM x64)
- ELSEIF(_DN_ANYCPU)
- SET(_DN_PLATFORM "AnyCPU")
- ENDIF()
-
- # If package version is not set, first fallback to DOTNET_PACKAGE_VERSION
- # If again not set, defaults to 1.0.0
- IF(NOT _DN_VERSION)
- SET(_DN_VERSION ${DOTNET_PACKAGE_VERSION})
- ENDIF()
- IF(NOT _DN_VERSION)
- SET(_DN_VERSION "1.0.0")
- ENDIF()
-
- # Set the output path to the binary directory.
- # Build outputs in separated output directories prevent overwriting.
- # Later we then copy the outputs to the destination.
-
- IF(NOT _DN_OUTPUT_PATH)
- SET(_DN_OUTPUT_PATH ${_DN_projname_noext})
- ENDIF()
-
- GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_BINARY_DIR}/${_DN_OUTPUT_PATH} ABSOLUTE)
-
- # In a cmake build, the XPLAT libraries are always copied over.
- # Set the proper directory for .NET projects.
- SET(_DN_XPLAT_LIB_DIR ${CMAKE_BINARY_DIR})
-
- SET(DOTNET_PACKAGES ${_DN_PACKAGE} PARENT_SCOPE)
- SET(DOTNET_CONFIG ${_DN_CONFIG} PARENT_SCOPE)
- SET(DOTNET_PLATFORM ${_DN_PLATFORM} PARENT_SCOPE)
- SET(DOTNET_DEPENDS ${_DN_DEPENDS} PARENT_SCOPE)
- SET(DOTNET_PROJNAME ${_DN_projname_noext} PARENT_SCOPE)
- SET(DOTNET_PROJPATH ${_DN_abs_proj} PARENT_SCOPE)
- SET(DOTNET_PROJDIR ${_DN_proj_dir} PARENT_SCOPE)
- SET(DOTNET_ARGUMENTS ${_DN_ARGUMENTS} PARENT_SCOPE)
- SET(DOTNET_RUN_OUTPUT ${_DN_OUTPUT} PARENT_SCOPE)
- SET(DOTNET_PACKAGE_VERSION ${_DN_VERSION} PARENT_SCOPE)
- SET(DOTNET_OUTPUT_PATH ${_DN_OUTPUT_PATH} PARENT_SCOPE)
- SET(DOTNET_deps ${_DN_deps} PARENT_SCOPE)
-
- IF(_DN_PLATFORM)
- SET(_DN_PLATFORM_PROP "/p:Platform=${_DN_PLATFORM}")
- ENDIF()
-
- IF(_DN_NETCOREAPP)
- SET(_DN_BUILD_OPTIONS -f netcoreapp2.0)
- SET(_DN_PACK_OPTIONS /p:TargetFrameworks=netcoreapp2.0)
- ELSEIF(UNIX)
- # Unix builds default to netstandard2.0
- SET(_DN_BUILD_OPTIONS -f netstandard2.0)
- SET(_DN_PACK_OPTIONS /p:TargetFrameworks=netstandard2.0)
- ENDIF()
-
- SET(_DN_IMPORT_PROP ${CMAKE_CURRENT_BINARY_DIR}/${_DN_projname}.imports.props)
- CONFIGURE_FILE(${DOTNET_MODULE_DIR}/DotnetImports.props.in ${_DN_IMPORT_PROP})
- SET(_DN_IMPORT_ARGS "/p:DirectoryBuildPropsPath=${_DN_IMPORT_PROP}")
-
- SET(DOTNET_IMPORT_PROPERTIES ${_DN_IMPORT_ARGS} PARENT_SCOPE)
- SET(DOTNET_BUILD_PROPERTIES ${_DN_PLATFORM_PROP} ${_DN_IMPORT_ARGS} PARENT_SCOPE)
- SET(DOTNET_BUILD_OPTIONS ${_DN_BUILD_OPTIONS} PARENT_SCOPE)
- SET(DOTNET_PACK_OPTIONS --include-symbols ${_DN_PACK_OPTIONS} ${_DN_PACK_ARGUMENTS} PARENT_SCOPE)
-
-ENDFUNCTION()
-
-MACRO(ADD_DOTNET_DEPENDENCY_TARGETS tgt)
- FOREACH(pkg_dep ${DOTNET_DEPENDS})
- ADD_DEPENDENCIES(${tgt}_${DOTNET_PROJNAME} PKG_${pkg_dep})
- MESSAGE(" ${DOTNET_PROJNAME} <- ${pkg_dep}")
- ENDFOREACH()
-
- FOREACH(pkg ${DOTNET_PACKAGES})
- STRING(TOLOWER ${pkg} pkg_lowercase)
- GET_FILENAME_COMPONENT(cache_path ${NUGET_CACHE_PATH}/${pkg_lowercase} ABSOLUTE)
- IF(WIN32)
- SET(rm_command powershell -NoLogo -NoProfile -NonInteractive -Command "Remove-Item -Recurse -Force -ErrorAction Ignore '${cache_path}'\; exit 0")
- ELSE()
- SET(rm_command rm -rf ${cache_path})
- ENDIF()
- ADD_CUSTOM_TARGET(
- DOTNET_PURGE_${pkg}
- COMMAND ${CMAKE_COMMAND} -E echo "======= [x] Purging nuget package cache for ${pkg}"
- COMMAND ${rm_command}
- DEPENDS ${DOTNET_deps}
- )
- ADD_DEPENDENCIES(${tgt}_${DOTNET_PROJNAME} DOTNET_PURGE_${pkg})
- # Add a target for the built package -- this can be referenced in
- # another project.
- ADD_CUSTOM_TARGET(PKG_${pkg})
- ADD_DEPENDENCIES(PKG_${pkg} ${tgt}_${DOTNET_PROJNAME})
- MESSAGE("==== ${DOTNET_PROJNAME} -> ${pkg}")
- ENDFOREACH()
-ENDMACRO()
-
-MACRO(DOTNET_BUILD_COMMANDS)
- IF(${DOTNET_IS_MSBUILD})
- SET(build_dotnet_cmds
- COMMAND ${CMAKE_COMMAND} -E echo "======= Building msbuild project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]"
- COMMAND ${NUGET_EXE} restore -Force ${DOTNET_PROJPATH}
- COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}"
- COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Build ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}" ${DOTNET_ARGUMENTS})
- SET(build_dotnet_type "msbuild")
- ELSE()
- SET(build_dotnet_cmds
- COMMAND ${CMAKE_COMMAND} -E echo "======= Building .NET project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]"
- COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES}
- COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES}
- COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS} ${DOTNET_ARGUMENTS})
- SET(build_dotnet_type "dotnet")
- ENDIF()
-
- # DOTNET_OUTPUTS refer to artifacts produced, that the BUILD_proj_name target depends on.
- SET(DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp)
- LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${DOTNET_OUTPUTS})
- IF(NOT "${DOTNET_PACKAGES}" STREQUAL "")
- MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (version ${DOTNET_PACKAGE_VERSION})")
- FOREACH(pkg ${DOTNET_PACKAGES})
- LIST(APPEND DOTNET_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg)
- LIST(APPEND DOTNET_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg)
- LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E remove ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg)
- LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E remove ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg)
- ENDFOREACH()
- LIST(APPEND build_dotnet_cmds COMMAND ${DOTNET_EXE} pack --no-build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_PACK_OPTIONS})
- ELSE()
- MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (no nupkg)")
- ENDIF()
-
- ADD_CUSTOM_COMMAND(
- OUTPUT ${DOTNET_OUTPUTS}
- DEPENDS ${DOTNET_deps}
- ${build_dotnet_cmds}
- )
- ADD_CUSTOM_TARGET(
- BUILD_${DOTNET_PROJNAME} ALL
- DEPENDS ${DOTNET_OUTPUTS})
-
-ENDMACRO()
-
-FUNCTION(ADD_DOTNET DOTNET_PROJECT)
- DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}")
- SET(DOTNET_IS_MSBUILD FALSE)
- DOTNET_BUILD_COMMANDS()
- ADD_DOTNET_DEPENDENCY_TARGETS(BUILD)
-ENDFUNCTION()
-
-FUNCTION(ADD_MSBUILD DOTNET_PROJECT)
- IF(NOT WIN32)
- MESSAGE("-- Building non-Win32, skipping ${DOTNET_PROJECT}")
- RETURN()
- ENDIF()
-
- DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}")
- SET(DOTNET_IS_MSBUILD TRUE)
- DOTNET_BUILD_COMMANDS()
- ADD_DOTNET_DEPENDENCY_TARGETS(BUILD)
-ENDFUNCTION()
-
-FUNCTION(RUN_DOTNET DOTNET_PROJECT)
- DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN};NETCOREAPP")
- MESSAGE("-- Adding dotnet run project ${DOTNET_PROJECT}")
- FILE(MAKE_DIRECTORY ${DOTNET_OUTPUT_PATH})
- ADD_CUSTOM_COMMAND(
- OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT}
- DEPENDS ${DOTNET_deps}
- COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES}
- COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES}
- COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS}
- # XXX tfm
- COMMAND ${DOTNET_EXE} ${DOTNET_OUTPUT_PATH}/netcoreapp2.0/${DOTNET_PROJNAME}.dll ${DOTNET_ARGUMENTS}
- COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp
- WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH})
- ADD_CUSTOM_TARGET(
- RUN_${DOTNET_PROJNAME}
- DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT})
- ADD_DOTNET_DEPENDENCY_TARGETS(RUN)
-ENDFUNCTION()
-
-FUNCTION(TEST_DOTNET DOTNET_PROJECT)
- DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}")
- MESSAGE("-- Adding dotnet test project ${DOTNET_PROJECT}")
- IF(WIN32)
- SET(test_framework_args "")
- ELSE()
- SET(test_framework_args -f netcoreapp2.0)
- ENDIF()
-
- ADD_TEST(NAME ${DOTNET_PROJNAME}
- COMMAND ${DOTNET_EXE} test ${test_framework_args} --results-directory "${CMAKE_BINARY_DIR}" --logger trx ${DOTNET_ARGUMENTS}
- WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH})
-
-ENDFUNCTION()
-
-SET_PROPERTY(GLOBAL PROPERTY DOTNET_LAST_SMOKETEST "")
-
-FUNCTION(SMOKETEST_DOTNET DOTNET_PROJECT)
- MESSAGE("-- Adding dotnet smoke test project ${DOTNET_PROJECT}")
- IF(WIN32)
- RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}")
- ELSE()
- RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}")
- ENDIF()
-
- DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}")
- ADD_CUSTOM_TARGET(
- SMOKETEST_${DOTNET_PROJNAME}
- ALL
- DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp)
- ADD_DOTNET_DEPENDENCY_TARGETS(SMOKETEST)
- GET_PROPERTY(_dn_last_smoketest GLOBAL PROPERTY DOTNET_LAST_SMOKETEST)
- IF(_dn_last_smoketest)
- MESSAGE("${_dn_last_smoketest} -> SMOKETEST_${DOTNET_PROJNAME}")
- ADD_DEPENDENCIES(SMOKETEST_${DOTNET_PROJNAME} ${_dn_last_smoketest})
- ENDIF()
- # Chain the smoke tests together so they are executed sequentially
- SET_PROPERTY(GLOBAL PROPERTY DOTNET_LAST_SMOKETEST SMOKETEST_${DOTNET_PROJNAME})
-
-ENDFUNCTION()
-
-SET(DOTNET_IMPORTS_TEMPLATE ${CMAKE_CURRENT_LIST_DIR}/DotnetImports.props.in)
-
-FUNCTION(GEN_DOTNET_PROPS target_props_file)
- CMAKE_PARSE_ARGUMENTS(
- # prefix
- _DNP
- # options (flags)
- ""
- # oneValueArgs
- "PACKAGE_VERSION;XML_INJECT"
- # multiValueArgs
- ""
- # the input arguments
- ${ARGN})
-
- IF(NOT _DNP_PACKAGE_VERSION)
- SET(_DNP_PACKAGE_VERSION 1.0.0)
- ENDIF()
-
- IF(_DNP_XML_INJECT)
- SET(_DN_CUSTOM_BUILDPROPS ${_DNP_XML_INJECT})
- ENDIF()
-
- SET(_DN_OUTPUT_PATH ${CMAKE_BINARY_DIR})
- SET(_DN_XPLAT_LIB_DIR ${CMAKE_BINARY_DIR})
- SET(_DN_VERSION ${_DNP_PACKAGE_VERSION})
- CONFIGURE_FILE(${DOTNET_IMPORTS_TEMPLATE} ${target_props_file})
- UNSET(_DN_OUTPUT_PATH)
- UNSET(_DN_XPLAT_LIB_DIR)
- UNSET(_DN_VERSION)
-ENDFUNCTION()
-
-
-MESSAGE("-- Found .NET toolchain: ${DOTNET_EXE} (version ${DOTNET_VERSION})")
-SET(DOTNET_FOUND TRUE)
diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
index 6012bb25f..87e3c8d67 100644
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
@@ -32,6 +32,7 @@ RUN apt-get update && \
libomp-dev \
llvm-3.9 \
make \
+ mono-devel \
ninja-build \
python3 \
python3-setuptools \
@@ -47,6 +48,4 @@ RUN useradd -m user && \
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
USER user
WORKDIR /home/user
-# TODO .NET core does not support Linux x86 yet, disable it for now.
-# see: https://github.com/dotnet/coreclr/issues/9265
-ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer DOTNET_BINDINGS=0
+ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer
diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
index 9c6bdc054..c963ce255 100644
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
@@ -2,10 +2,9 @@ FROM ubuntu:14.04
RUN apt-get update && \
apt-get -y --no-install-recommends install \
- apt-transport-https \
binutils \
clang-3.9 \
- curl \
+ cmake \
doxygen \
default-jdk \
gcc-multilib \
@@ -19,20 +18,13 @@ RUN apt-get update && \
lib32gomp1 \
llvm-3.9 \
make \
+ mono-devel \
ninja-build \
python3 \
python3-setuptools \
python2.7 \
python-setuptools
-RUN curl -SL https://packages.microsoft.com/config/ubuntu/14.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \
- dpkg -i packages-microsoft-prod.deb && \
- apt-get update && \
- apt-get -y --no-install-recommends install dotnet-sdk-2.1
-
-RUN curl -SL https://cmake.org/files/v3.12/cmake-3.12.0-Linux-x86_64.sh --output cmake-3.12.0-Linux-x86_64.sh && \
- sh cmake-3.12.0-Linux-x86_64.sh --prefix=/usr/local --exclude-subdir
-
# Create `user` user for container with password `user`. and give it
# password-less sudo access
RUN useradd -m user && \
diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
index f4d9c873a..08686e275 100644
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
@@ -2,12 +2,10 @@ FROM ubuntu:16.04
RUN apt-get update && \
apt-get -y --no-install-recommends install \
- apt-transport-https \
binutils \
clang \
clang-3.9 \
cmake \
- curl \
doxygen \
default-jdk \
gcc-multilib \
@@ -22,6 +20,7 @@ RUN apt-get update && \
libomp-dev \
llvm-3.9 \
make \
+ mono-devel \
ninja-build \
python3 \
python3-setuptools \
@@ -29,11 +28,6 @@ RUN apt-get update && \
python-setuptools \
sudo
-RUN curl -SL https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \
- dpkg -i packages-microsoft-prod.deb && \
- apt-get update && \
- apt-get -y --no-install-recommends install dotnet-sdk-2.1
-
# Create `user` user for container with password `user`. and give it
# password-less sudo access
RUN useradd -m user && \
diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh
index a149a1d83..687efebb4 100755
--- a/contrib/ci/scripts/test_z3_examples_cmake.sh
+++ b/contrib/ci/scripts/test_z3_examples_cmake.sh
@@ -88,14 +88,11 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
fi
if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
+ # Build .NET example
+ # FIXME: Move compliation step into CMake target
+ mcs ${Z3_SRC_DIR}/examples/dotnet/Program.cs /target:exe /out:dotnet_test.exe /reference:Microsoft.Z3.dll /r:System.Numerics.dll
# Run .NET example
- if [ "X${ASAN_BUILD}" = "X1" ]; then
- # The dotnet test get stuck on ASAN
- # so don't run it for now.
- echo "Skipping .NET example under ASan build"
- else
- run_quiet run_non_native_binding dotnet ${Z3_BUILD_DIR}/dotnet/netcoreapp2.0/dotnet.dll
- fi
+ run_quiet run_non_native_binding mono ./dotnet_test.exe
fi
if [ "X${JAVA_BINDINGS}" = "X1" ]; then
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 5d06029f9..6c50320ed 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -112,10 +112,3 @@ set_target_properties(z3_tptp5 PROPERTIES EXCLUDE_FROM_ALL TRUE)
if (BUILD_PYTHON_BINDINGS)
add_subdirectory(python)
endif()
-
-################################################################################
-# Build dotnet examples
-################################################################################
-if (BUILD_DOTNET_BINDINGS)
- add_subdirectory(dotnet)
-endif()
\ No newline at end of file
diff --git a/examples/dotnet/CMakeLists.txt b/examples/dotnet/CMakeLists.txt
deleted file mode 100644
index 108326f83..000000000
--- a/examples/dotnet/CMakeLists.txt
+++ /dev/null
@@ -1,34 +0,0 @@
-find_package(Dotnet REQUIRED)
-
-if("${TARGET_ARCHITECTURE}" STREQUAL "i686")
- set(Z3_DOTNET_PLATFORM "x86")
-else()
- set(Z3_DOTNET_PLATFORM "AnyCPU")
-endif()
-
-configure_file(${CMAKE_CURRENT_SOURCE_DIR}/dotnet.csproj dotnet.csproj COPYONLY)
-configure_file(${CMAKE_CURRENT_SOURCE_DIR}/Program.cs Program.cs COPYONLY)
-
-ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/dotnet.csproj
- PLATFORM ${Z3_DOTNET_PLATFORM}
- NETCOREAPP
- CUSTOM_BUILDPROPS "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}"
- DEPENDS Microsoft.Z3)
-
-if(UNIX AND NOT APPLE)
- set(z3_dotnet_native_lib ${CMAKE_BINARY_DIR}/libz3.so)
- set(z3_dotnet_test_manual_copy_deps
- ${CMAKE_BINARY_DIR}/Microsoft.Z3/netstandard2.0/Microsoft.Z3.dll
- ${z3_dotnet_native_lib}
- )
-
- add_custom_target(
- z3_dotnet_test_manual_copy_assembly_hack ALL
- COMMAND ${CMAKE_COMMAND} -E copy ${z3_dotnet_test_manual_copy_deps} ${CMAKE_BINARY_DIR}/dotnet/netcoreapp2.0/
- # hack the libz3 entry in deps so it's easy enough for dotnet to reach it...
- COMMAND sed \"s/runtimes\\/.*libz3\\.so/libz3.so/\" -i ${CMAKE_BINARY_DIR}/dotnet/netcoreapp2.0/dotnet.deps.json
- )
-
- add_dependencies(z3_dotnet_test_manual_copy_assembly_hack BUILD_dotnet)
-endif()
-
diff --git a/examples/dotnet/README b/examples/dotnet/README
index b42156761..3f7e989df 100644
--- a/examples/dotnet/README
+++ b/examples/dotnet/README
@@ -1,6 +1,7 @@
Small example using the .Net bindings.
+This example is only built if you have Visual Studio.
To build the example execute
make examples
in the build directory.
-It will create a .net core 2.0 app.
+It will create the executable dotnet_example.exe
diff --git a/examples/dotnet/dotnet.csproj b/examples/dotnet/dotnet.csproj
deleted file mode 100644
index 7776259ea..000000000
--- a/examples/dotnet/dotnet.csproj
+++ /dev/null
@@ -1,12 +0,0 @@
-
-
-
- Exe
- netcoreapp2.0
-
-
-
-
-
-
-
diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index 3ff1a484a..20621e4fc 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -1,10 +1,12 @@
-find_package(Dotnet REQUIRED)
+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")
@@ -125,64 +127,160 @@ endforeach()
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES
"${Z3_DOTNET_CONST_FILE}"
"${Z3_DOTNET_NATIVE_FILE}"
+ "${Z3_DOTNET_ASSEMBLY_INFO_FILE}"
)
-
-# Generate items
-set(Z3_DOTNET_COMPILE_ITEMS "")
-foreach(csfile ${Z3_DOTNET_ASSEMBLY_SOURCES})
- set(Z3_DOTNET_COMPILE_ITEMS "${Z3_DOTNET_COMPILE_ITEMS}\n ")
+# ``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()
-
-# FindDotnet.cmake forwards CMake build type to MSBuild.
-# And thus we can put the conditional properties in the project file.
-# Note, nuget package file names do not have the ${VER_REV} part.
-
-set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}")
-if("${TARGET_ARCHITECTURE}" STREQUAL "i686")
- set(Z3_DOTNET_PLATFORM "x86")
+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"
+ )
+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()
- set(Z3_DOTNET_PLATFORM "AnyCPU")
+ message(FATAL_ERROR "Unknown .NET toolchain")
endif()
-# TODO conditional for signing. we can then enable the ``Release_delaysign`` configuration
+# 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"
+)
-configure_file(${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in ${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj)
-ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj
- VERSION ${Z3_DOTNET_NUPKG_VERSION}
- PLATFORM ${Z3_DOTNET_PLATFORM}
- SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in
- ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.props
- ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.targets
- ${Z3_DOTNET_ASSEMBLY_SOURCES}
- PACKAGE Microsoft.Z3
- PACK_ARGUMENTS "/p:_DN_CMAKE_CONFIG=$"
- )
-add_dependencies(BUILD_Microsoft.Z3 libz3)
+# 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
+ "$<$:/debug+>"
+ "$<$:/debug:full>"
+ "$<$:/optimize->"
+ # This has to be quoted otherwise the ``;`` is interpreted as a command separator
+ "$<$:\"/define:DEBUG$TRACE\">"
+ # Release flags, expands to nothing if we are doing a debug build
+ "$<$>:/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 ``$`` 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 BUILD_Microsoft.Z3)
-
-# Register the local nupkg repo
-set(Z3_DOTNET_LOCALREPO_NAME "Microsoft Z3 Local Repository")
-DOTNET_REGISTER_LOCAL_REPOSITORY(${Z3_DOTNET_LOCALREPO_NAME} ${CMAKE_BINARY_DIR})
+add_custom_target(build_z3_dotnet_bindings
+ ALL
+ DEPENDS
+ "${Z3_DOTNET_ASSEMBLY_DLL}"
+)
###############################################################################
-# Install: register a local nuget repo and install our package.
-# the build step depends on the 'purge' target, making sure that
-# a user will always restore the freshly-built package.
+# 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(INSTALL_DOTNET_BINDINGS)
- install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.${Z3_DOTNET_NUPKG_VERSION}.nupkg" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
- # move the local repo to the installation directory (cancel the build-time repo)
- install(CODE "include(${CMAKE_CURRENT_LIST_DIR}/../../../cmake/modules/FindDotnet.cmake)\n DOTNET_REGISTER_LOCAL_REPOSITORY(\"${Z3_DOTNET_LOCALREPO_NAME}\" ${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/z3.nuget)")
- install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.xml" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
-# TODO GAC?
-# set(GAC_PKG_NAME "Microsoft.Z3.Sharp")
-# set(PREFIX "${CMAKE_INSTALL_PREFIX}")
-# set(VERSION "${Z3_VERSION}")
+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()
-
diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj
new file mode 100644
index 000000000..045c610dd
--- /dev/null
+++ b/src/api/dotnet/Microsoft.Z3.csproj
@@ -0,0 +1,418 @@
+
+
+
+ Debug
+ AnyCPU
+ 8.0.30703
+ 2.0
+ {EC3DB697-B734-42F7-9468-5B62821EEB5A}
+ Library
+ Properties
+ Microsoft.Z3
+ Microsoft.Z3
+ v4.0
+ 512
+ Client
+ 0
+
+
+ true
+ full
+ false
+ ..\Debug\
+ DEBUG;TRACE
+ prompt
+ 4
+ true
+ ..\Debug\Microsoft.Z3.XML
+ False
+ False
+ True
+ False
+ False
+ True
+ False
+ True
+ True
+ False
+ False
+ False
+ True
+ False
+ False
+ False
+ True
+ False
+ False
+ True
+ True
+ True
+ False
+ False
+
+
+
+
+
+
+ True
+ Full
+ %28none%29
+ 2
+
+
+ pdbonly
+ true
+ ..\external\
+
+
+ prompt
+ 4
+ true
+ ..\external\Microsoft.Z3.xml
+ AnyCPU
+
+
+ ..\external\
+ true
+ ..\external\Microsoft.Z3.xml
+ true
+ pdbonly
+ AnyCPU
+ bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ true
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ true
+ false
+
+
+ true
+ ..\x64\Debug\
+ DEBUG;TRACE
+ true
+ full
+ x64
+ ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ true
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ true
+ True
+ False
+ True
+ False
+ False
+ False
+ False
+ False
+ False
+ False
+ False
+ False
+ False
+ False
+ False
+ False
+ True
+ False
+ False
+ True
+ False
+ False
+ False
+
+
+
+
+
+
+ False
+ Full
+ %28none%29
+ 0
+ ..\x64\Debug\Microsoft.Z3.XML
+
+
+ ..\x64\external_64\
+ true
+ ..\x64\external_64\Microsoft.Z3.xml
+ true
+ pdbonly
+ x64
+ ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ true
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ True
+ False
+ True
+ False
+ False
+ True
+ True
+ True
+ False
+ False
+ False
+ True
+ True
+ False
+ False
+ False
+ True
+ False
+ False
+ True
+ True
+ False
+ False
+
+
+
+
+ -repro
+
+ True
+ Full
+ %28none%29
+ 2
+
+
+ ..\x64\external\
+ true
+ ..\x64\external\Microsoft.Z3.XML
+ true
+ pdbonly
+ x64
+ bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ true
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ true
+
+
+ false
+
+
+
+
+
+
+ false
+
+
+ ..\Release_delaysign\
+ true
+ ..\Release_delaysign\Microsoft.Z3.XML
+ true
+ pdbonly
+ AnyCPU
+ ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ true
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ true
+ DELAYSIGN
+
+
+ bin\x64\Release_delaysign\
+ true
+ bin\x64\Release_delaysign\Microsoft.Z3.XML
+ true
+ pdbonly
+ x64
+ ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ true
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ true
+
+
+ true
+ ..\x86\Debug\
+ DEBUG;TRACE
+ true
+ full
+ x86
+ ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ ..\x86\Debug\Microsoft.Z3.XML
+
+
+ bin\x86\Release\
+ true
+ bin\x86\Release\Microsoft.Z3.xml
+ true
+ pdbonly
+ x86
+ ..\external\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+
+
+ bin\x86\external\
+ true
+ bin\x86\external\Microsoft.Z3.XML
+ true
+ pdbonly
+ x86
+ bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ true
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ true
+
+
+ bin\x86\Release_delaysign\
+ DELAYSIGN
+ true
+ bin\x86\Release_delaysign\Microsoft.Z3.XML
+ true
+ pdbonly
+ x86
+ ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ true
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ true
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in
deleted file mode 100644
index fc6d6a978..000000000
--- a/src/api/dotnet/Microsoft.Z3.csproj.in
+++ /dev/null
@@ -1,95 +0,0 @@
-
-
-
-
-
- Microsoft.Z3
- Microsoft.Z3
- Microsoft.Z3
-
- Z3 .NET Interface
- Z3 .NET Interface
-
- Z3
-
- Z3 is a satisfiability modulo theories solver from Microsoft Research.
- .NET Interface to the Z3 Theorem Prover
-
- Copyright (C) 2006-2019 Microsoft Corporation
- Copyright (C) 2006-2019 Microsoft Corporation
-
- Microsoft Corporation
- Microsoft Corporation
-
- @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@
- @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@
-
- @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@
- @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@
-
- ${DOTNET_PACKAGE_VERSION}
- smt constraint solver theorem prover
-
- Microsoft
- Microsoft
-
-
-
-
- false
- false
-
-
-
- DELAYSIGN
- true
- true
-
-
-
-
-
- netstandard2.0;net45
- library
- True
- 1701,1702
- 4
- true
- $(OutputPath)\Microsoft.Z3.xml
-
-
-
-
-${Z3_DOTNET_COMPILE_ITEMS}
-
-
-
-
-
- build
-
-
- build
-
-
-
-
-
-
-
-
- runtimes\win-x64\native
-
-
- runtimes\linux-x64\native
-
-
-
-
-
-
- runtimes\win-x86\native
-
-
-
-
diff --git a/src/api/dotnet/Microsoft.Z3.props b/src/api/dotnet/Microsoft.Z3.props
deleted file mode 100644
index a5db71359..000000000
--- a/src/api/dotnet/Microsoft.Z3.props
+++ /dev/null
@@ -1,23 +0,0 @@
-
-
-
-
-
- true
- true
- true
-
-
- $(MSBuildThisFileDirectory)..\
- $(Z3_PACKAGE_PATH)runtimes\win-x64\native\libz3.dll
- $(Z3_PACKAGE_PATH)runtimes\win-x86\native\libz3.dll
- $(Z3_PACKAGE_PATH)runtimes\linux-x64\native\libz3.so
-
-
-
-
-
- false
-
-
-
diff --git a/src/api/dotnet/Microsoft.Z3.targets b/src/api/dotnet/Microsoft.Z3.targets
deleted file mode 100644
index 38e56b350..000000000
--- a/src/api/dotnet/Microsoft.Z3.targets
+++ /dev/null
@@ -1,11 +0,0 @@
-
-
-
-
-
- %(RecursiveDir)%(FileName)%(Extension)
- PreserveNewest
-
-
-
-
diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs.in b/src/api/dotnet/Properties/AssemblyInfo.cs.in
new file mode 100644
index 000000000..e5a85f16f
--- /dev/null
+++ b/src/api/dotnet/Properties/AssemblyInfo.cs.in
@@ -0,0 +1,38 @@
+using System;
+using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+using System.Security.Permissions;
+
+// General Information about an assembly is controlled through the following
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("Z3 .NET Interface")]
+[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("Microsoft Corporation")]
+[assembly: AssemblyProduct("Z3")]
+[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible
+// to COM components. If you need to access a type in this assembly from
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// The following GUID is for the ID of the typelib if this project is exposed to COM
+[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")]
+
+// Version information for an assembly consists of the following four values:
+//
+// Major Version
+// Minor Version
+// Build Number
+// Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers
+// by using the '*' as shown below:
+// [assembly: AssemblyVersion("4.2.0.0")]
+[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")]
+[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")]
diff --git a/src/api/dotnet/core/README.txt b/src/api/dotnet/core/README.txt
new file mode 100644
index 000000000..fa274f72b
--- /dev/null
+++ b/src/api/dotnet/core/README.txt
@@ -0,0 +1,15 @@
+Z3 API for .NET Core
+
+Z3's .NET API uses Code Contracts, which are not included in .NET Core. The
+enclosed file called DummyContracts.cs provides stubs for the Code Contracts
+functions, so that the API will compile, but not perform any contract
+checking. To build this using .NET core, run (in this directory):
+
+dotnet restore
+dotnet build core.csproj -c Release
+
+If you are building with the cmake system, you should first
+copy over files that are produced by the compiler into
+this directory. You need to copy over Native.cs and Enumeration.cs
+
+-- good luck!
diff --git a/src/api/dotnet/core/core.csproj b/src/api/dotnet/core/core.csproj
new file mode 100644
index 000000000..5fa3275cf
--- /dev/null
+++ b/src/api/dotnet/core/core.csproj
@@ -0,0 +1,18 @@
+
+
+
+ netcoreapp1.0
+ $(DefineConstants);DOTNET_CORE
+ portable
+ Microsoft.Z3
+ Library
+ core
+ $(PackageTargetFallback);dnxcore50
+ 1.0.4
+
+
+
+
+
+
+