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 @@
-<Project>
- <PropertyGroup>
- <OutputPath>${_DN_OUTPUT_PATH}/</OutputPath>
- <XPLAT_LIB_DIR>${_DN_XPLAT_LIB_DIR}/</XPLAT_LIB_DIR>
- <DOTNET_PACKAGE_VERSION>${_DN_VERSION}</DOTNET_PACKAGE_VERSION>
- ${_DN_CUSTOM_BUILDPROPS}
- </PropertyGroup>
-</Project>
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(<project_file> [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 <CustomProp>value</CustomProp>....]
-# [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(<project_file> [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 <CustomProp>value</CustomProp>....]
-# [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(<project_file> [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP]
-# [CONFIG configuration]
-# [PLATFORM platform]
-# [PACKAGE output_nuget_packages... ]
-# [DEPENDS depend_nuget_packages... ]
-# [CUSTOM_BUILDPROPS <CustomProp>value</CustomProp>....]
-# [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(<project_file> [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 <CustomProp>value</CustomProp>....]
-# [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 <config>`, not with `cmake --build ...`
-#
-# ```
-# TEST_DOTNET(<project_file>
-# [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(<target_props_file>
-# [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#</packageSources># <add key=\\\"${repo_name}\\\" value=\\\"${repo_path}\\\" />\\n </packageSources>#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 "$<$<CONFIG:Debug>:Debug>$<$<NOT:$<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>${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}</Z3_VERSION>"
- 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 @@
-<Project Sdk="Microsoft.NET.Sdk">
-
- <PropertyGroup>
- <OutputType>Exe</OutputType>
- <TargetFramework>netcoreapp2.0</TargetFramework>
- </PropertyGroup>
-
- <ItemGroup>
- <PackageReference Include="Microsoft.Z3" Version="$(Z3_VERSION)" />
- </ItemGroup>
-
-</Project>
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 <Compile Include="files.cs" /> items
-set(Z3_DOTNET_COMPILE_ITEMS "")
-foreach(csfile ${Z3_DOTNET_ASSEMBLY_SOURCES})
- set(Z3_DOTNET_COMPILE_ITEMS "${Z3_DOTNET_COMPILE_ITEMS}\n <Compile Include=\"${csfile}\" />")
+# ``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=$<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
+ "$<$<CONFIG:Debug>:/debug+>"
+ "$<$<CONFIG:Debug>:/debug:full>"
+ "$<$<CONFIG:Debug>:/optimize->"
+ # This has to be quoted otherwise the ``;`` is interpreted as a command separator
+ "$<$<CONFIG:Debug>:\"/define:DEBUG$<SEMICOLON>TRACE\">"
+ # Release flags, expands to nothing if we are doing a debug build
+ "$<$<NOT:$<CONFIG:Debug>>:/optimize+>"
+)
+
+# Mono's gacutil crashes when trying to install an assembly if we set the
+# platform in some cases, so only set it on Windows. This bug has been
+# reported at https://bugzilla.xamarin.com/show_bug.cgi?id=39955 . However mono
+# ignores the platform of an assembly when running it (
+# http://lists.ximian.com/pipermail/mono-devel-list/2015-November/043370.html )
+# so this shouldn't matter in practice.
+if (DOTNET_TOOLCHAIN_IS_WINDOWS)
+ # Set platform for assembly
+ if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+ list(APPEND CSC_FLAGS "/platform:x64")
+ elseif ("${TARGET_ARCHITECTURE}" STREQUAL "i686")
+ list(APPEND CSC_FLAGS "/platform:x86")
+ endif()
+endif()
+
+# FIXME: 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 ``$<TARGET_FILE_DIR:libz3>`` 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 @@
+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProductVersion>8.0.30703</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{EC3DB697-B734-42F7-9468-5B62821EEB5A}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Microsoft.Z3</RootNamespace>
+ <AssemblyName>Microsoft.Z3</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>..\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DocumentationFile>..\Debug\Microsoft.Z3.XML</DocumentationFile>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>True</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsDisjunctiveRequires>True</CodeContractsDisjunctiveRequires>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>2</CodeContractsAnalysisWarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>..\external\</OutputPath>
+ <DefineConstants>
+ </DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'external|AnyCPU' ">
+ <OutputPath>..\external\</OutputPath>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x64'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>..\x64\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DebugType>full</DebugType>
+ <PlatformTarget>x64</PlatformTarget>
+ <CodeAnalysisLogFile>..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsInferRequires>False</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <DocumentationFile>..\x64\Debug\Microsoft.Z3.XML</DocumentationFile>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x64'">
+ <OutputPath>..\x64\external_64\</OutputPath>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>x64</PlatformTarget>
+ <CodeAnalysisLogFile>..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>True</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions>-repro</CodeContractsExtraAnalysisOptions>
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>2</CodeContractsAnalysisWarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external|x64'">
+ <OutputPath>..\x64\external\</OutputPath>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DocumentationFile>..\x64\external\Microsoft.Z3.XML</DocumentationFile>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>x64</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ </PropertyGroup>
+ <PropertyGroup>
+ <SignAssembly>false</SignAssembly>
+ </PropertyGroup>
+ <PropertyGroup>
+ <AssemblyOriginatorKeyFile>
+ </AssemblyOriginatorKeyFile>
+ </PropertyGroup>
+ <PropertyGroup>
+ <DelaySign>false</DelaySign>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|AnyCPU'">
+ <OutputPath>..\Release_delaysign\</OutputPath>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DocumentationFile>..\Release_delaysign\Microsoft.Z3.XML</DocumentationFile>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <DefineConstants>DELAYSIGN</DefineConstants>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|x64'">
+ <OutputPath>bin\x64\Release_delaysign\</OutputPath>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DocumentationFile>bin\x64\Release_delaysign\Microsoft.Z3.XML</DocumentationFile>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>x64</PlatformTarget>
+ <CodeAnalysisLogFile>..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;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</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>..\x86\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DebugType>full</DebugType>
+ <PlatformTarget>x86</PlatformTarget>
+ <CodeAnalysisLogFile>..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <DocumentationFile>..\x86\Debug\Microsoft.Z3.XML</DocumentationFile>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">
+ <OutputPath>bin\x86\Release\</OutputPath>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DocumentationFile>bin\x86\Release\Microsoft.Z3.xml</DocumentationFile>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>x86</PlatformTarget>
+ <CodeAnalysisLogFile>..\external\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external|x86'">
+ <OutputPath>bin\x86\external\</OutputPath>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DocumentationFile>bin\x86\external\Microsoft.Z3.XML</DocumentationFile>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>x86</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|x86'">
+ <OutputPath>bin\x86\Release_delaysign\</OutputPath>
+ <DefineConstants>DELAYSIGN</DefineConstants>
+ <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
+ <DocumentationFile>bin\x86\Release_delaysign\Microsoft.Z3.XML</DocumentationFile>
+ <Optimize>true</Optimize>
+ <DebugType>pdbonly</DebugType>
+ <PlatformTarget>x86</PlatformTarget>
+ <CodeAnalysisLogFile>..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
+ <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Numerics" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="AlgebraicNum.cs" />
+ <Compile Include="ApplyResult.cs" />
+ <Compile Include="ArithExpr.cs" />
+ <Compile Include="ArithSort.cs" />
+ <Compile Include="ArrayExpr.cs" />
+ <Compile Include="ArraySort.cs" />
+ <Compile Include="AST.cs" />
+ <Compile Include="ASTMap.cs" />
+ <Compile Include="ASTVector.cs" />
+ <Compile Include="BitVecExpr.cs" />
+ <Compile Include="BitVecNum.cs" />
+ <Compile Include="BitVecSort.cs" />
+ <Compile Include="BoolExpr.cs" />
+ <Compile Include="BoolSort.cs" />
+ <Compile Include="Constructor.cs" />
+ <Compile Include="ConstructorList.cs" />
+ <Compile Include="DatatypeExpr.cs" />
+ <Compile Include="DatatypeSort.cs" />
+ <Compile Include="Deprecated.cs" />
+ <Compile Include="FiniteDomainExpr.cs" />
+ <Compile Include="FiniteDomainNum.cs" />
+ <Compile Include="FPExpr.cs" />
+ <Compile Include="FPNum.cs" />
+ <Compile Include="FPRMExpr.cs" />
+ <Compile Include="FPRMNum.cs" />
+ <Compile Include="FPRMSort.cs" />
+ <Compile Include="FPSort.cs" />
+ <Compile Include="Global.cs" />
+ <Compile Include="IDecRefQueue.cs" />
+ <Compile Include="Enumerations.cs" />
+ <Compile Include="EnumSort.cs" />
+ <Compile Include="Expr.cs" />
+ <Compile Include="FiniteDomainSort.cs" />
+ <Compile Include="Fixedpoint.cs" />
+ <Compile Include="FuncDecl.cs" />
+ <Compile Include="FuncInterp.cs" />
+ <Compile Include="Goal.cs" />
+ <Compile Include="IntExpr.cs" />
+ <Compile Include="IntNum.cs" />
+ <Compile Include="IntSort.cs" />
+ <Compile Include="IntSymbol.cs" />
+ <Compile Include="Lambda.cs" />
+ <Compile Include="ListSort.cs" />
+ <Compile Include="Model.cs" />
+ <Compile Include="Optimize.cs" />
+ <Compile Include="Params.cs" />
+ <Compile Include="ParamDescrs.cs" />
+ <Compile Include="Pattern.cs" />
+ <Compile Include="RatNum.cs" />
+ <Compile Include="RealExpr.cs" />
+ <Compile Include="RealSort.cs" />
+ <Compile Include="ReExpr.cs" />
+ <Compile Include="RelationSort.cs" />
+ <Compile Include="ReSort.cs" />
+ <Compile Include="SeqExpr.cs" />
+ <Compile Include="SeqSort.cs" />
+ <Compile Include="SetSort.cs" />
+ <Compile Include="Statistics.cs" />
+ <Compile Include="Status.cs" />
+ <Compile Include="Context.cs" />
+ <Compile Include="Probe.cs" />
+ <Compile Include="Solver.cs" />
+ <Compile Include="StringSymbol.cs" />
+ <Compile Include="Tactic.cs" />
+ <Compile Include="TupleSort.cs" />
+ <Compile Include="UninterpretedSort.cs" />
+ <Compile Include="Z3Exception.cs" />
+ <Compile Include="Log.cs" />
+ <Compile Include="Native.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="Quantifier.cs" />
+ <Compile Include="Sort.cs" />
+ <Compile Include="Symbol.cs" />
+ <Compile Include="Version.cs" />
+ <Compile Include="Z3Object.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <WCFMetadata Include="Service References\" />
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <PropertyGroup>
+ <PostBuildEvent>
+ </PostBuildEvent>
+ </PropertyGroup>
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ 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 @@
-<Project Sdk="Microsoft.NET.Sdk">
-
- <!-- Package metadata properties -->
- <PropertyGroup>
-
- <PackageId>Microsoft.Z3</PackageId>
- <AssemblyName>Microsoft.Z3</AssemblyName>
- <RootNamespace>Microsoft.Z3</RootNamespace>
-
- <Title>Z3 .NET Interface</Title>
- <AssemblyTitle>Z3 .NET Interface</AssemblyTitle>
-
- <AssemblyProduct>Z3</AssemblyProduct>
-
- <Description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</Description>
- <AssemblyDescription>.NET Interface to the Z3 Theorem Prover</AssemblyDescription>
-
- <Copyright>Copyright (C) 2006-2019 Microsoft Corporation</Copyright>
- <AssemblyCopyright>Copyright (C) 2006-2019 Microsoft Corporation</AssemblyCopyright>
-
- <Company>Microsoft Corporation</Company>
- <AssemblyCompany>Microsoft Corporation</AssemblyCompany>
-
- <Version>@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@</Version>
- <AssemblyVersion>@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@</AssemblyVersion>
-
- <FileVersion>@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@</FileVersion>
- <AssemblyFileVersion>@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@</AssemblyFileVersion>
-
- <PackageVersion>${DOTNET_PACKAGE_VERSION}</PackageVersion>
- <PackageTags>smt constraint solver theorem prover</PackageTags>
-
- <Authors>Microsoft</Authors>
- <Company>Microsoft</Company>
- </PropertyGroup>
-
- <!-- Code contract & signing properties -->
- <PropertyGroup Condition="'$(Configuration)' != 'Release_delaysign'">
- <SignAssembly>false</SignAssembly>
- <DelaySign>false</DelaySign>
- </PropertyGroup>
-
- <PropertyGroup Condition="'$(Configuration)' == 'Release_delaysign'">
- <DefineConstants>DELAYSIGN</DefineConstants>
- <SignAssembly>true</SignAssembly>
- <DelaySign>true</DelaySign>
- </PropertyGroup>
-
- <!-- Build properties -->
- <PropertyGroup>
- <!-- In *nix builds, netfx TFMs are not available. -->
- <TargetFrameworks>netstandard2.0;net45</TargetFrameworks>
- <OutputTypeEx>library</OutputTypeEx>
- <AllowUnsafeBlocks>True</AllowUnsafeBlocks>
- <NoWarn>1701,1702</NoWarn>
- <Warn>4</Warn>
- <GenerateDocumentationFile>true</GenerateDocumentationFile>
- <DocumentationFile>$(OutputPath)\Microsoft.Z3.xml</DocumentationFile>
- </PropertyGroup>
-
- <!-- Compilation items -->
- <ItemGroup>
-${Z3_DOTNET_COMPILE_ITEMS}
- </ItemGroup>
-
- <!-- Legacy .NET framework native library helper routines -->
- <ItemGroup>
- <Content Include="${CMAKE_CURRENT_LIST_DIR}/Microsoft.Z3.props">
- <PackagePath>build</PackagePath>
- </Content>
- <Content Include="${CMAKE_CURRENT_LIST_DIR}/Microsoft.Z3.targets">
- <PackagePath>build</PackagePath>
- </Content>
- </ItemGroup>
-
- <!-- TODO we may want to pack x64 and x86 native assemblies into a single nupkg -->
-
- <!-- Native binaries x64 -->
- <ItemGroup Condition="'$(Platform)' != 'x86'">
- <Content Include="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/$(_DN_CMAKE_CONFIG)/libz3.dll" Condition="Exists('${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/$(_DN_CMAKE_CONFIG)/libz3.dll')">
- <PackagePath>runtimes\win-x64\native</PackagePath>
- </Content>
- <Content Include="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.so" Condition="Exists('${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.so')">
- <PackagePath>runtimes\linux-x64\native</PackagePath>
- </Content>
- </ItemGroup>
-
- <!-- Native binaries for x86; currently only Windows is supported. -->
- <ItemGroup Condition="'$(Platform)' == 'x86'">
- <Content Include="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/$(_DN_CMAKE_CONFIG)/libz3.dll" Condition="Exists('${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/$(_DN_CMAKE_CONFIG)/libz3.dll')">
- <PackagePath>runtimes\win-x86\native</PackagePath>
- </Content>
- </ItemGroup>
-
-</Project>
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 @@
-<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="12.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
-
- <!-- Paths -->
- <PropertyGroup>
- <IsOSX Condition="'$([System.Runtime.InteropServices.RuntimeInformation]::IsOSPlatform($([System.Runtime.InteropServices.OSPlatform]::OSX)))' == 'true'">true</IsOSX>
- <IsLinux Condition="'$([System.Runtime.InteropServices.RuntimeInformation]::IsOSPlatform($([System.Runtime.InteropServices.OSPlatform]::Linux)))' == 'true'">true</IsLinux>
- <IsWindows Condition="'$([System.Runtime.InteropServices.RuntimeInformation]::IsOSPlatform($([System.Runtime.InteropServices.OSPlatform]::Windows)))' == 'true'">true</IsWindows>
-
- <!-- Probe the package root path -->
- <Z3_PACKAGE_PATH Condition="('$(Z3_PACKAGE_PATH)' == '')">$(MSBuildThisFileDirectory)..\</Z3_PACKAGE_PATH>
- <Z3_NATIVE_LIB_PATH Condition="'$(IsWindows)' == 'true' and '$(Platform)' != 'x86'">$(Z3_PACKAGE_PATH)runtimes\win-x64\native\libz3.dll</Z3_NATIVE_LIB_PATH>
- <Z3_NATIVE_LIB_PATH Condition="'$(IsWindows)' == 'true' and '$(Platform)' == 'x86'">$(Z3_PACKAGE_PATH)runtimes\win-x86\native\libz3.dll</Z3_NATIVE_LIB_PATH>
- <Z3_NATIVE_LIB_PATH Condition="'$(IsLinux)' == 'true'">$(Z3_PACKAGE_PATH)runtimes\linux-x64\native\libz3.so</Z3_NATIVE_LIB_PATH>
- </PropertyGroup>
-
- <!-- Configurations -->
- <PropertyGroup>
- <!-- Disable "prefer 32-bit mode", so that the program runs in 64 bit mode and loads libz3 correctly. -->
- <Prefer32Bit>false</Prefer32Bit>
- </PropertyGroup>
-
-</Project>
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 @@
-<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
-
- <ItemGroup Condition="!$(TargetFramework.Contains('netstandard')) and !$(TargetFramework.Contains('netcoreapp'))">
- <None Include="$(Z3_NATIVE_LIB_PATH)">
- <Link>%(RecursiveDir)%(FileName)%(Extension)</Link>
- <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
- </None>
- </ItemGroup>
-
-</Project>
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 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+ <PropertyGroup>
+ <TargetFramework>netcoreapp1.0</TargetFramework>
+ <DefineConstants>$(DefineConstants);DOTNET_CORE</DefineConstants>
+ <DebugType>portable</DebugType>
+ <AssemblyName>Microsoft.Z3</AssemblyName>
+ <OutputType>Library</OutputType>
+ <PackageId>core</PackageId>
+ <PackageTargetFallback>$(PackageTargetFallback);dnxcore50</PackageTargetFallback>
+ <RuntimeFrameworkVersion>1.0.4</RuntimeFrameworkVersion>
+ </PropertyGroup>
+
+ <ItemGroup>
+ <Compile Include="..\*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
+ </ItemGroup>
+
+</Project>