Revert "api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration."

.gitignore

@@ -76,6 +76,3 @@ src/api/ml/z3.mllib
 *.bak
 doc/api
 doc/code
-.vs
-examples/**/obj
-CMakeSettings.json

.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

cmake/modules/DotnetImports.props.in

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

cmake/modules/FindDotnet.cmake

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

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.
+ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer
-# see: https://github.com/dotnet/coreclr/issues/9265
-ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer DOTNET_BINDINGS=0

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 && \

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 && \

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
+  run_quiet run_non_native_binding mono ./dotnet_test.exe
-    # 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

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

examples/dotnet/CMakeLists.txt

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

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

examples/dotnet/dotnet.csproj

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

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}"
 )
 
-
+# ``csc.exe`` doesn't like UNIX style paths so convert them
-# Generate <Compile Include="files.cs" /> items
+# if necessary first to native paths.
-set(Z3_DOTNET_COMPILE_ITEMS "")
+set(Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "")
-foreach(csfile ${Z3_DOTNET_ASSEMBLY_SOURCES})
+foreach (csfile_path ${Z3_DOTNET_ASSEMBLY_SOURCES})
-    set(Z3_DOTNET_COMPILE_ITEMS "${Z3_DOTNET_COMPILE_ITEMS}\n    <Compile Include=\"${csfile}\" />")
+  file(TO_NATIVE_PATH "${csfile_path}" csfile_path_native)
+  list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "${csfile_path_native}")
 endforeach()
 
-
+set(CSC_FLAGS "")
-# FindDotnet.cmake forwards CMake build type to MSBuild.
+if (DOTNET_TOOLCHAIN_IS_WINDOWS)
-# And thus we can put the conditional properties in the project file.
+  # FIXME: Why use these flags?
-# Note, nuget package file names do not have the ${VER_REV} part.
+  # Note these flags have been copied from the Python build system.
-
+  list(APPEND CSC_FLAGS
-set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}")
+    "/noconfig"
-if("${TARGET_ARCHITECTURE}" STREQUAL "i686")
+    "/nostdlib+"
-    set(Z3_DOTNET_PLATFORM "x86")
+    "/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)
+# Set the build type flags. The build type for the assembly roughly corresponds
-ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj
+# with the native code build type.
-    VERSION ${Z3_DOTNET_NUPKG_VERSION}
+list(APPEND CSC_FLAGS
-    PLATFORM ${Z3_DOTNET_PLATFORM}
+  # Debug flags, expands to nothing if we aren't doing a debug build
-    SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in 
+  "$<$<CONFIG:Debug>:/debug+>"
-            ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.props
+  "$<$<CONFIG:Debug>:/debug:full>"
-            ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.targets
+  "$<$<CONFIG:Debug>:/optimize->"
-            ${Z3_DOTNET_ASSEMBLY_SOURCES}
+  # This has to be quoted otherwise the ``;`` is interpreted as a command separator
-    PACKAGE Microsoft.Z3
+  "$<$<CONFIG:Debug>:\"/define:DEBUG$<SEMICOLON>TRACE\">"
-    PACK_ARGUMENTS "/p:_DN_CMAKE_CONFIG=$<CONFIG>"
+  # Release flags, expands to nothing if we are doing a debug build
-    )
+  "$<$<NOT:$<CONFIG:Debug>>:/optimize+>"
-add_dependencies(BUILD_Microsoft.Z3 libz3)
+)
+
+# 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)
+add_custom_target(build_z3_dotnet_bindings
-
+  ALL
-# Register the local nupkg repo
+  DEPENDS
-set(Z3_DOTNET_LOCALREPO_NAME "Microsoft Z3 Local Repository")
+    "${Z3_DOTNET_ASSEMBLY_DLL}"
-DOTNET_REGISTER_LOCAL_REPOSITORY(${Z3_DOTNET_LOCALREPO_NAME} ${CMAKE_BINARY_DIR})
+)
 
 ###############################################################################
-# Install: register a local nuget repo and install our package.
+# Install
-#          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(INSTALL_DOTNET_BINDINGS)
+if (DOTNET_TOOLCHAIN_IS_MONO)
-    install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.${Z3_DOTNET_NUPKG_VERSION}.nupkg" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
+  message(STATUS "Emitting install rules for .NET bindings")
-    # move the local repo to the installation directory (cancel the build-time repo)
+  # Install pkgconfig file for the assembly. This is needed by Monodevelop
-    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)")
+  # to find the assembly
-    install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.xml" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
+  install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}")
-# TODO GAC?
+
-#  set(GAC_PKG_NAME "Microsoft.Z3.Sharp")
+  # Configure the install and uninstall scripts.
-#  set(PREFIX "${CMAKE_INSTALL_PREFIX}")
+  # Note: If multi-configuration generator support is ever fixed then these
-#  set(VERSION "${Z3_VERSION}")
+  # 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()
-

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>

src/api/dotnet/Microsoft.Z3.csproj.in

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

src/api/dotnet/Microsoft.Z3.props

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

src/api/dotnet/Microsoft.Z3.targets

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

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@")]

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!

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>