diff --git a/.gitignore b/.gitignore
index e189a9569..88ccbb56f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -76,3 +76,6 @@ src/api/ml/z3.mllib
*.bak
doc/api
doc/code
+.vs
+examples/**/obj
+CMakeSettings.json
diff --git a/.travis.yml b/.travis.yml
index 9ec6132b6..12e62ed3d 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,6 +85,7 @@ 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
new file mode 100644
index 000000000..090d46502
--- /dev/null
+++ b/cmake/modules/DotnetImports.props.in
@@ -0,0 +1,8 @@
+
+
+ ${_DN_OUTPUT_PATH}/
+ ${_DN_XPLAT_LIB_DIR}/
+ ${_DN_VERSION}
+ ${_DN_CUSTOM_BUILDPROPS}
+
+
diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake
new file mode 100644
index 000000000..98c5f2079
--- /dev/null
+++ b/cmake/modules/FindDotnet.cmake
@@ -0,0 +1,471 @@
+#.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 87e3c8d67..6012bb25f 100644
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
@@ -32,7 +32,6 @@ RUN apt-get update && \
libomp-dev \
llvm-3.9 \
make \
- mono-devel \
ninja-build \
python3 \
python3-setuptools \
@@ -48,4 +47,6 @@ RUN useradd -m user && \
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
USER user
WORKDIR /home/user
-ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer
+# 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
diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
index c963ce255..9c6bdc054 100644
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
@@ -2,9 +2,10 @@ FROM ubuntu:14.04
RUN apt-get update && \
apt-get -y --no-install-recommends install \
+ apt-transport-https \
binutils \
clang-3.9 \
- cmake \
+ curl \
doxygen \
default-jdk \
gcc-multilib \
@@ -18,13 +19,20 @@ 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 08686e275..f4d9c873a 100644
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
@@ -2,10 +2,12 @@ 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 \
@@ -20,7 +22,6 @@ RUN apt-get update && \
libomp-dev \
llvm-3.9 \
make \
- mono-devel \
ninja-build \
python3 \
python3-setuptools \
@@ -28,6 +29,11 @@ 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 687efebb4..a149a1d83 100755
--- a/contrib/ci/scripts/test_z3_examples_cmake.sh
+++ b/contrib/ci/scripts/test_z3_examples_cmake.sh
@@ -88,11 +88,14 @@ 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
- run_quiet run_non_native_binding mono ./dotnet_test.exe
+ 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
fi
if [ "X${JAVA_BINDINGS}" = "X1" ]; then
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 6c50320ed..5d06029f9 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -112,3 +112,10 @@ 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
new file mode 100644
index 000000000..108326f83
--- /dev/null
+++ b/examples/dotnet/CMakeLists.txt
@@ -0,0 +1,34 @@
+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 3f7e989df..b42156761 100644
--- a/examples/dotnet/README
+++ b/examples/dotnet/README
@@ -1,7 +1,6 @@
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 the executable dotnet_example.exe
+It will create a .net core 2.0 app.
diff --git a/examples/dotnet/dotnet.csproj b/examples/dotnet/dotnet.csproj
new file mode 100644
index 000000000..7776259ea
--- /dev/null
+++ b/examples/dotnet/dotnet.csproj
@@ -0,0 +1,12 @@
+
+
+
+ Exe
+ netcoreapp2.0
+
+
+
+
+
+
+
diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index 20621e4fc..3ff1a484a 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -1,12 +1,10 @@
-find_package(DotNetToolchain REQUIRED)
+find_package(Dotnet 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")
@@ -127,160 +125,64 @@ endforeach()
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}")
+
+# Generate items
+set(Z3_DOTNET_COMPILE_ITEMS "")
+foreach(csfile ${Z3_DOTNET_ASSEMBLY_SOURCES})
+ set(Z3_DOTNET_COMPILE_ITEMS "${Z3_DOTNET_COMPILE_ITEMS}\n ")
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"
- )
-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"
- )
+
+# 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")
else()
- message(FATAL_ERROR "Unknown .NET toolchain")
+ set(Z3_DOTNET_PLATFORM "AnyCPU")
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"
-)
+# TODO conditional for signing. we can then enable the ``Release_delaysign`` configuration
-# 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}\""
-)
+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)
# Convenient top-level target
-add_custom_target(build_z3_dotnet_bindings
- ALL
- DEPENDS
- "${Z3_DOTNET_ASSEMBLY_DLL}"
-)
+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})
###############################################################################
-# Install
+# 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.
###############################################################################
option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install target" ON)
-set(GAC_PKG_NAME "Microsoft.Z3.Sharp")
-set(PREFIX "${CMAKE_INSTALL_PREFIX}")
-set(VERSION "${Z3_VERSION}")
-set(Z3_DOTNET_PKGCONFIG_FILE "${CMAKE_CURRENT_BINARY_DIR}/Microsoft.Z3.Sharp.pc")
-configure_file("Microsoft.Z3.Sharp.pc.in" "${Z3_DOTNET_PKGCONFIG_FILE}" @ONLY)
-if (DOTNET_TOOLCHAIN_IS_MONO)
- message(STATUS "Emitting install rules for .NET bindings")
- # Install pkgconfig file for the assembly. This is needed by Monodevelop
- # to find the assembly
- install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}")
-
- # Configure the install and uninstall scripts.
- # Note: If multi-configuration generator support is ever fixed then these
- # scripts will be broken.
- configure_file(cmake_install_gac.cmake.in cmake_install_gac.cmake @ONLY)
- configure_file(cmake_uninstall_gac.cmake.in cmake_uninstall_gac.cmake @ONLY)
-
- # Tell CMake to Invoke a script to install assembly to the GAC during install
- install(SCRIPT "${CMAKE_CURRENT_BINARY_DIR}/cmake_install_gac.cmake")
-
- # Add custom target to uninstall the assembly from the GAC
- add_custom_target(remove_dotnet_dll_from_gac
- COMMAND "${CMAKE_COMMAND}" "-P" "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall_gac.cmake"
- COMMENT "Uninstalling ${Z3_DOTNET_ASSEMBLY_NAME} from the GAC"
- ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
- )
- add_dependencies(uninstall remove_dotnet_dll_from_gac)
-
-elseif(DOTNET_TOOLCHAIN_IS_WINDOWS)
- # Don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead just copy into
- # installation directory.
- install(FILES "${Z3_DOTNET_ASSEMBLY_DLL}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
- install(FILES "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
-else()
- message(FATAL_ERROR "Unknown .NET toolchain")
+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}")
endif()
+
diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj
deleted file mode 100644
index 045c610dd..000000000
--- a/src/api/dotnet/Microsoft.Z3.csproj
+++ /dev/null
@@ -1,418 +0,0 @@
-
-
-
- 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
new file mode 100644
index 000000000..fc6d6a978
--- /dev/null
+++ b/src/api/dotnet/Microsoft.Z3.csproj.in
@@ -0,0 +1,95 @@
+
+
+
+
+
+ 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
new file mode 100644
index 000000000..a5db71359
--- /dev/null
+++ b/src/api/dotnet/Microsoft.Z3.props
@@ -0,0 +1,23 @@
+
+
+
+
+
+ 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
new file mode 100644
index 000000000..38e56b350
--- /dev/null
+++ b/src/api/dotnet/Microsoft.Z3.targets
@@ -0,0 +1,11 @@
+
+
+
+
+
+ %(RecursiveDir)%(FileName)%(Extension)
+ PreserveNewest
+
+
+
+
diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs.in b/src/api/dotnet/Properties/AssemblyInfo.cs.in
deleted file mode 100644
index e5a85f16f..000000000
--- a/src/api/dotnet/Properties/AssemblyInfo.cs.in
+++ /dev/null
@@ -1,38 +0,0 @@
-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
deleted file mode 100644
index fa274f72b..000000000
--- a/src/api/dotnet/core/README.txt
+++ /dev/null
@@ -1,15 +0,0 @@
-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
deleted file mode 100644
index 5fa3275cf..000000000
--- a/src/api/dotnet/core/core.csproj
+++ /dev/null
@@ -1,18 +0,0 @@
-
-
-
- netcoreapp1.0
- $(DefineConstants);DOTNET_CORE
- portable
- Microsoft.Z3
- Library
- core
- $(PackageTargetFallback);dnxcore50
- 1.0.4
-
-
-
-
-
-
-