mirror of
https://github.com/Z3Prover/z3
synced 2025-04-26 18:45:33 +00:00
api: dotnet: switch to multi-targeting project and modern cmake-dotnet
integration.
This commit is contained in:
Yatao Li
parent
1e11b62bc6
commit
c77af6b75f
20 changed files with 438 additions and 1311 deletions
7
cmake/modules/DotnetImports.props.in
Normal file
7
cmake/modules/DotnetImports.props.in
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
<Project>
|
||||
<PropertyGroup>
|
||||
<OutputPath>${_DN_OUTPUT_PATH}/</OutputPath>
|
||||
<XPLAT_LIB_DIR>${XPLAT_LIB_DIR}/</XPLAT_LIB_DIR>
|
||||
<DOTNET_PACKAGE_VERSION>${_DN_VERSION}</DOTNET_PACKAGE_VERSION>
|
||||
</PropertyGroup>
|
||||
</Project>
|
||||
304
cmake/modules/FindDotnet.cmake
Normal file
304
cmake/modules/FindDotnet.cmake
Normal file
|
|
@ -0,0 +1,304 @@
|
|||
#.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... ])
|
||||
# ```
|
||||
#
|
||||
# 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>
|
||||
# [ARGUMENTS program_args...]
|
||||
# [OUTPUT outputs...])
|
||||
# ```
|
||||
#
|
||||
# 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... ])
|
||||
# ```
|
||||
#
|
||||
# DOTNET_REGISTER_LOCAL_REPOSITORY -- register a local NuGet package repository.
|
||||
#
|
||||
# ```
|
||||
# DOTNET_REGISTER_LOCAL_REPOSITORY(repo_name repo_path)
|
||||
# ```
|
||||
#
|
||||
# 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.
|
||||
#
|
||||
# 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)
|
||||
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)
|
||||
FILE(GLOB_RECURSE DOTNET_deps *.cs *.fs *.xaml *.csproj *.fsproj *.tsl)
|
||||
LIST(FILTER DOTNET_deps EXCLUDE REGEX /obj/)
|
||||
CMAKE_PARSE_ARGUMENTS(
|
||||
# prefix
|
||||
_DN
|
||||
# options (flags)
|
||||
"RELEASE;DEBUG;X86;X64;ANYCPU;NETCOREAPP"
|
||||
# oneValueArgs
|
||||
"CONFIG;PLATFORM;VERSION"
|
||||
# multiValueArgs
|
||||
"PACKAGE;DEPENDS;ARGUMENTS;OUTPUT"
|
||||
# the input arguments
|
||||
${arguments})
|
||||
|
||||
GET_FILENAME_COMPONENT(_DN_abs_proj "${_DN_PROJECT}" ABSOLUTE)
|
||||
GET_FILENAME_COMPONENT(_DN_proj_dir "${_DN_PROJECT}" DIRECTORY)
|
||||
GET_FILENAME_COMPONENT(_DN_projname "${DOTNET_PROJECT}" NAME)
|
||||
STRING(REGEX REPLACE "\\.[^.]*$" "" _DN_projname_noext ${_DN_projname})
|
||||
|
||||
IF(_DN_RELEASE)
|
||||
SET(_DN_CONFIG Release)
|
||||
ELSEIF(_DN_DEBUG)
|
||||
SET(_DN_CONFIG Debug)
|
||||
ENDIF()
|
||||
|
||||
IF(NOT _DN_CONFIG)
|
||||
SET(_DN_CONFIG $<CONFIG>)
|
||||
IF(_DN_CONFIG STREQUAL "RelWithDebInfo" OR _DN_CONFIG STREQUAL "RelMinSize" OR NOT _DN_CONFIG)
|
||||
SET(_DN_CONFIG "Release")
|
||||
ENDIF()
|
||||
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 "Any CPU")
|
||||
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()
|
||||
|
||||
GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_CURRENT_BINARY_DIR}/bin ABSOLUTE)
|
||||
|
||||
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_RUN_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 ${DOTNET_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(DOTNET_BUILD_PROPERTIES ${_DN_PLATFORM_PROP} ${_DN_TFMS_PROP} "/p:DirectoryBuildPropsPath=${_DN_IMPORT_PROP}" "/p:DOTNET_PACKAGE_VERSION=${_DN_VERSION}" PARENT_SCOPE)
|
||||
SET(DOTNET_BUILD_OPTIONS ${_DN_BUILD_OPTIONS} PARENT_SCOPE)
|
||||
SET(DOTNET_PACK_OPTIONS ${_DN_PACK_OPTIONS} PARENT_SCOPE)
|
||||
|
||||
ENDFUNCTION()
|
||||
|
||||
MACRO(ADD_DOTNET_DEPENDENCY_TARGETS)
|
||||
FOREACH(pkg_dep ${DOTNET_DEPENDS})
|
||||
ADD_DEPENDENCIES(BUILD_${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(BUILD_${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} BUILD_${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 ${DOTNET_PROJPATH}
|
||||
COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean /p:Configuration="${DOTNET_CONFIG}"
|
||||
COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Build ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}")
|
||||
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}
|
||||
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})
|
||||
SET(build_dotnet_type "dotnet")
|
||||
ENDIF()
|
||||
|
||||
IF(NOT "${DOTNET_PACKAGES}" STREQUAL "")
|
||||
MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (version ${DOTNET_PACKAGE_VERSION})")
|
||||
SET(_DOTNET_OUTPUTS "")
|
||||
FOREACH(pkg ${DOTNET_PACKAGES})
|
||||
LIST(APPEND _DOTNET_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.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})
|
||||
LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E copy ${_DOTNET_OUTPUTS} ${CMAKE_BINARY_DIR})
|
||||
ELSE()
|
||||
|
||||
MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (no nupkg)")
|
||||
SET(_DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp)
|
||||
LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${_DOTNET_OUTPUTS})
|
||||
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()
|
||||
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()
|
||||
ENDFUNCTION()
|
||||
|
||||
FUNCTION(RUN_DOTNET DOTNET_PROJECT)
|
||||
DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}")
|
||||
ADD_CUSTOM_COMMAND(
|
||||
OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT}
|
||||
DEPENDS ${DOTNET_deps}
|
||||
COMMAND ${DOTNET_EXE} run ${DOTNET_RUN_ARGUMENTS}
|
||||
COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp
|
||||
WORKING_DIRECTORY ${DOTNET_PROJDIR})
|
||||
ADD_CUSTOM_TARGET(
|
||||
RUN_${DOTNET_PROJNAME}
|
||||
DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT})
|
||||
ADD_DEPENDENCIES(RUN_${DOTNET_PROJNAME} BUILD_${DOTNET_PROJNAME})
|
||||
ENDFUNCTION()
|
||||
|
||||
MESSAGE("-- Found .NET toolchain: ${DOTNET_EXE} (version ${DOTNET_VERSION})")
|
||||
SET(DOTNET_FOUND TRUE)
|
||||
|
|
@ -1,12 +1,10 @@
|
|||
find_package(DotNetToolchain REQUIRED)
|
||||
find_package(Dotnet REQUIRED)
|
||||
|
||||
# Configure AssemblyInfo.cs
|
||||
set(VER_MAJOR "${Z3_VERSION_MAJOR}")
|
||||
set(VER_MINOR "${Z3_VERSION_MINOR}")
|
||||
set(VER_BUILD "${Z3_VERSION_PATCH}")
|
||||
set(VER_REVISION "${Z3_VERSION_TWEAK}")
|
||||
set(Z3_DOTNET_ASSEMBLY_INFO_FILE "${CMAKE_CURRENT_BINARY_DIR}/Properties/AssemblyInfo.cs")
|
||||
configure_file("Properties/AssemblyInfo.cs.in" "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" @ONLY)
|
||||
|
||||
# Generate Native.cs
|
||||
set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs")
|
||||
|
|
@ -127,165 +125,33 @@ endforeach()
|
|||
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES
|
||||
"${Z3_DOTNET_CONST_FILE}"
|
||||
"${Z3_DOTNET_NATIVE_FILE}"
|
||||
"${Z3_DOTNET_ASSEMBLY_INFO_FILE}"
|
||||
)
|
||||
|
||||
# ``csc.exe`` doesn't like UNIX style paths so convert them
|
||||
# if necessary first to native paths.
|
||||
set(Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "")
|
||||
foreach (csfile_path ${Z3_DOTNET_ASSEMBLY_SOURCES})
|
||||
file(TO_NATIVE_PATH "${csfile_path}" csfile_path_native)
|
||||
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "${csfile_path_native}")
|
||||
|
||||
# Generate <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}\" />")
|
||||
endforeach()
|
||||
|
||||
set(CSC_FLAGS "")
|
||||
if (DOTNET_TOOLCHAIN_IS_WINDOWS)
|
||||
# FIXME: Why use these flags?
|
||||
# Note these flags have been copied from the Python build system.
|
||||
list(APPEND CSC_FLAGS
|
||||
"/noconfig"
|
||||
"/nostdlib+"
|
||||
"/reference:mscorlib.dll"
|
||||
)
|
||||
# FIXME: This flag only works when the working directory of csc.exe is
|
||||
# the directory containing the ``libz3`` target. I can't get this to work
|
||||
# correctly with multi-configuration generators (i.e. Visual Studio) so
|
||||
# just don't set the flag for now.
|
||||
#list(APPEND CSC_FLAGS "/linkresource:$<TARGET_FILE_NAME:libz3>")
|
||||
elseif (DOTNET_TOOLCHAIN_IS_MONO)
|
||||
# We need to give the assembly a strong name so that it can be installed
|
||||
# into the GAC.
|
||||
list(APPEND CSC_FLAGS
|
||||
"/keyfile:${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.snk"
|
||||
)
|
||||
else()
|
||||
message(FATAL_ERROR "Unknown .NET toolchain")
|
||||
endif()
|
||||
|
||||
# Common flags
|
||||
list(APPEND CSC_FLAGS
|
||||
"/unsafe+"
|
||||
"/nowarn:1701,1702"
|
||||
"/errorreport:prompt"
|
||||
"/warn:4"
|
||||
"/reference:System.Core.dll"
|
||||
"/reference:System.dll"
|
||||
"/reference:System.Numerics.dll"
|
||||
"/filealign:512" # Why?
|
||||
"/target:library"
|
||||
)
|
||||
# FindDotnet.cmake forwards CMake build type to MSBuild.
|
||||
# And thus we can put the conditional properties in the project file.
|
||||
|
||||
# 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+>"
|
||||
)
|
||||
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
|
||||
# note, nuget package file names do not have the ${VER_REV} part.
|
||||
VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}"
|
||||
PACKAGE Microsoft.Z3)
|
||||
|
||||
# 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}\""
|
||||
)
|
||||
add_custom_command(
|
||||
OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/buildtimestamp
|
||||
DEPENDS ${Z3_DOTNET_ASSEMBLY_SOURCES} ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in
|
||||
COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/buildtimestamp)
|
||||
add_custom_target(Z3_DOTNET_BUILD_DUMMY ALL DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/buildtimestamp)
|
||||
add_dependencies(BUILD_Microsoft.Z3 Z3_DOTNET_BUILD_DUMMY libz3)
|
||||
|
||||
# Convenient top-level target
|
||||
add_custom_target(build_z3_dotnet_bindings
|
||||
ALL
|
||||
DEPENDS
|
||||
"${Z3_DOTNET_ASSEMBLY_DLL}"
|
||||
)
|
||||
add_custom_target(build_z3_dotnet_bindings ALL DEPENDS BUILD_Microsoft.Z3)
|
||||
|
||||
###############################################################################
|
||||
# Install
|
||||
###############################################################################
|
||||
option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install target" ON)
|
||||
set(GAC_PKG_NAME "Microsoft.Z3.Sharp")
|
||||
set(PREFIX "${CMAKE_INSTALL_PREFIX}")
|
||||
set(VERSION "${Z3_VERSION}")
|
||||
set(Z3_DOTNET_PKGCONFIG_FILE "${CMAKE_CURRENT_BINARY_DIR}/Microsoft.Z3.Sharp.pc")
|
||||
configure_file("Microsoft.Z3.Sharp.pc.in" "${Z3_DOTNET_PKGCONFIG_FILE}" @ONLY)
|
||||
|
||||
if (DOTNET_TOOLCHAIN_IS_MONO)
|
||||
message(STATUS "Emitting install rules for .NET bindings")
|
||||
# Install pkgconfig file for the assembly. This is needed by Monodevelop
|
||||
# to find the assembly
|
||||
install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}")
|
||||
|
||||
# Configure the install and uninstall scripts.
|
||||
# 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()
|
||||
#TODO install
|
||||
|
|
|
|||
|
|
@ -1,417 +0,0 @@
|
|||
<?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="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="InterpolationContext.cs" />
|
||||
<Compile Include="IntExpr.cs" />
|
||||
<Compile Include="IntNum.cs" />
|
||||
<Compile Include="IntSort.cs" />
|
||||
<Compile Include="IntSymbol.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>
|
||||
73
src/api/dotnet/Microsoft.Z3.csproj.in
Normal file
73
src/api/dotnet/Microsoft.Z3.csproj.in
Normal file
|
|
@ -0,0 +1,73 @@
|
|||
<Project Sdk="Microsoft.Net.Sdk">
|
||||
|
||||
<!-- Package metadata properties -->
|
||||
<PropertyGroup>
|
||||
|
||||
<PackageId>Microsoft.Z3</PackageId>
|
||||
<AssemblyName>Microsoft.Z3</AssemblyName>
|
||||
|
||||
<Title>Z3 .NET Interface</Title>
|
||||
<AssemblyTitle>Z3 .NET Interface</AssemblyTitle>
|
||||
|
||||
<AssemblyProduct>Z3</AssemblyProduct>
|
||||
|
||||
<Description>.NET Interface to the Z3 Theorem Prover</Description>
|
||||
<AssemblyDescription>.NET Interface to the Z3 Theorem Prover</AssemblyDescription>
|
||||
|
||||
<Copyright>Copyright (C) 2006-2015 Microsoft Corporation</Copyright>
|
||||
<AssemblyCopyright>Copyright (C) 2006-2015 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>
|
||||
</PropertyGroup>
|
||||
|
||||
<!-- Build properties -->
|
||||
<PropertyGroup>
|
||||
<!-- Add net40;net35 only if the appropriate SDKs are installed. -->
|
||||
<!-- Also, in xplat builds, netfx TFMs are not available. -->
|
||||
<TargetFrameworks>netstandard2.0;net461;net45</TargetFrameworks>
|
||||
<OutputTypeEx>library</OutputTypeEx>
|
||||
<AllowUnsafeBlocks>True</AllowUnsafeBlocks>
|
||||
<NoWarn>1701,1702</NoWarn>
|
||||
<Warn>4</Warn>
|
||||
<DefineConstants Condition="'$(TargetFramework)'=='net35'">FRAMEWORK_LT_4</DefineConstants>
|
||||
</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>
|
||||
|
||||
<!-- Native binaries -->
|
||||
<ItemGroup>
|
||||
<!-- FIXME configuration fixed to Release -->
|
||||
<Content Include="${CMAKE_BINARY_DIR}/Release/libz3.dll" Condition="Exists('${CMAKE_BINARY_DIR}/Release/libz3.dll')">
|
||||
<PackagePath>runtimes\win-x64\native</PackagePath>
|
||||
</Content>
|
||||
<!-- TODO XPlat support -->
|
||||
</ItemGroup>
|
||||
|
||||
<!-- NuGet package references -->
|
||||
<ItemGroup Condition="'$(TargetFramework)'=='net35'">
|
||||
<PackageReference Include="Code.Contract" Version="1.0.0"/>
|
||||
</ItemGroup>
|
||||
|
||||
</Project>
|
||||
22
src/api/dotnet/Microsoft.Z3.props
Normal file
22
src/api/dotnet/Microsoft.Z3.props
Normal file
|
|
@ -0,0 +1,22 @@
|
|||
<?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 for a tools\ directory which will contain Trinity.TSL.Compiler.exe. -->
|
||||
<Z3_PACKAGE_PATH Condition="('$(Z3_PACKAGE_PATH)' == '')">$(MSBuildThisFileDirectory)..\..\</Z3_PACKAGE_PATH>
|
||||
<Z3_NATIVE_LIB_PATH Condition="'$(IsWindows)' == 'true'">$(Z3_PACKAGE_PATH)runtimes\win-x64\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>
|
||||
11
src/api/dotnet/Microsoft.Z3.targets
Normal file
11
src/api/dotnet/Microsoft.Z3.targets
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
|
||||
|
||||
<ItemGroup Condition="'$(TargetFramework)' != 'netstandard2.0'">
|
||||
<None Include="$(Z3_NATIVE_LIB_PATH)">
|
||||
<Link>%(RecursiveDir)%(FileName)%(Extension)</Link>
|
||||
<CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
|
||||
</None>
|
||||
</ItemGroup>
|
||||
|
||||
</Project>
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
using System;
|
||||
using System.Reflection;
|
||||
using System.Runtime.CompilerServices;
|
||||
using System.Runtime.InteropServices;
|
||||
using System.Security.Permissions;
|
||||
|
||||
// General Information about an assembly is controlled through the following
|
||||
// set of attributes. Change these attribute values to modify the information
|
||||
// associated with an assembly.
|
||||
[assembly: AssemblyTitle("Z3 .NET Interface")]
|
||||
[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")]
|
||||
[assembly: AssemblyConfiguration("")]
|
||||
[assembly: AssemblyCompany("Microsoft Corporation")]
|
||||
[assembly: AssemblyProduct("Z3")]
|
||||
[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")]
|
||||
[assembly: AssemblyTrademark("")]
|
||||
[assembly: AssemblyCulture("")]
|
||||
|
||||
// Setting ComVisible to false makes the types in this assembly not visible
|
||||
// to COM components. If you need to access a type in this assembly from
|
||||
// COM, set the ComVisible attribute to true on that type.
|
||||
[assembly: ComVisible(false)]
|
||||
|
||||
// The following GUID is for the ID of the typelib if this project is exposed to COM
|
||||
[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")]
|
||||
|
||||
// Version information for an assembly consists of the following four values:
|
||||
//
|
||||
// Major Version
|
||||
// Minor Version
|
||||
// Build Number
|
||||
// Revision
|
||||
//
|
||||
// You can specify all the values or you can default the Build and Revision Numbers
|
||||
// by using the '*' as shown below:
|
||||
// [assembly: AssemblyVersion("4.2.0.0")]
|
||||
[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")]
|
||||
[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")]
|
||||
|
|
@ -1,65 +0,0 @@
|
|||
/*++
|
||||
Copyright (<c>) 2016 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
Contracts.cs
|
||||
|
||||
Abstract:
|
||||
|
||||
Z3 Managed API: Dummy Code Contracts class for .NET
|
||||
frameworks that don't support them (e.g., CoreCLR).
|
||||
|
||||
Author:
|
||||
|
||||
Christoph Wintersteiger (cwinter) 2016-10-06
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
|
||||
namespace System.Diagnostics.Contracts
|
||||
{
|
||||
public class ContractClass : Attribute
|
||||
{
|
||||
public ContractClass(Type t) { }
|
||||
}
|
||||
|
||||
public class ContractClassFor : Attribute
|
||||
{
|
||||
public ContractClassFor(Type t) { }
|
||||
}
|
||||
|
||||
public class ContractInvariantMethod : Attribute
|
||||
{
|
||||
public ContractInvariantMethod() { }
|
||||
}
|
||||
|
||||
public class ContractVerification : Attribute
|
||||
{
|
||||
public ContractVerification(bool b) { }
|
||||
}
|
||||
|
||||
public class Pure : Attribute { }
|
||||
|
||||
public static class Contract
|
||||
{
|
||||
[Conditional("false")]
|
||||
public static void Ensures(bool b) { }
|
||||
[Conditional("false")]
|
||||
public static void Requires(bool b) { }
|
||||
[Conditional("false")]
|
||||
public static void Assume(bool b, string msg) { }
|
||||
[Conditional("false")]
|
||||
public static void Assert(bool b) { }
|
||||
public static bool ForAll(bool b) { return true; }
|
||||
public static bool ForAll(Object c, Func<Object, bool> p) { return true; }
|
||||
public static bool ForAll(int from, int to, Predicate<int> p) { return true; }
|
||||
[Conditional("false")]
|
||||
public static void Invariant(bool b) { }
|
||||
public static T[] Result<T>() { return new T[1]; }
|
||||
[Conditional("false")]
|
||||
public static void EndContractBlock() { }
|
||||
public static T ValueAtReturn<T>(out T v) { T[] t = new T[1]; v = t[0]; return v; }
|
||||
}
|
||||
}
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
Z3 API for .NET Core
|
||||
|
||||
Z3's .NET API uses Code Contracts, which are not included in .NET Core. The
|
||||
enclosed file called DummyContracts.cs provides stubs for the Code Contracts
|
||||
functions, so that the API will compile, but not perform any contract
|
||||
checking. To build this using .NET core, run (in this directory):
|
||||
|
||||
dotnet restore
|
||||
dotnet build project.json
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
{
|
||||
"version": "1.0.0-*",
|
||||
"buildOptions": {
|
||||
"debugType": "portable",
|
||||
"emitEntryPoint": false,
|
||||
"outputName": "Microsoft.Z3",
|
||||
"compile": [ "../*.cs", "*.cs" ],
|
||||
"define": ["DOTNET_CORE"]
|
||||
},
|
||||
"dependencies": { },
|
||||
"frameworks": {
|
||||
"netcoreapp1.0": {
|
||||
"dependencies": {
|
||||
"Microsoft.NETCore.App": {
|
||||
"type": "platform",
|
||||
"version": "1.0.1"
|
||||
}
|
||||
},
|
||||
"imports": "dnxcore50"
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
<?xml version="1.0" encoding="utf-8" ?>
|
||||
<configuration>
|
||||
<startup>
|
||||
<supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.5.2" />
|
||||
</startup>
|
||||
</configuration>
|
||||
|
|
@ -1,78 +0,0 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project ToolsVersion="14.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
|
||||
<Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
|
||||
<PropertyGroup>
|
||||
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
|
||||
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
|
||||
<ProjectGuid>{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}</ProjectGuid>
|
||||
<OutputType>Exe</OutputType>
|
||||
<AppDesignerFolder>Properties</AppDesignerFolder>
|
||||
<RootNamespace>Example</RootNamespace>
|
||||
<AssemblyName>Example</AssemblyName>
|
||||
<TargetFrameworkVersion>v4.5.2</TargetFrameworkVersion>
|
||||
<FileAlignment>512</FileAlignment>
|
||||
<AutoGenerateBindingRedirects>true</AutoGenerateBindingRedirects>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
|
||||
<PlatformTarget>AnyCPU</PlatformTarget>
|
||||
<DebugSymbols>true</DebugSymbols>
|
||||
<DebugType>full</DebugType>
|
||||
<Optimize>false</Optimize>
|
||||
<OutputPath>bin\Debug\</OutputPath>
|
||||
<DefineConstants>TRACE;DEBUG;FRAMEWORK_LT_4</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
|
||||
<PlatformTarget>AnyCPU</PlatformTarget>
|
||||
<DebugType>pdbonly</DebugType>
|
||||
<Optimize>true</Optimize>
|
||||
<OutputPath>bin\Release\</OutputPath>
|
||||
<DefineConstants>TRACE;FRAMEWORK_LT_4</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x64'">
|
||||
<DebugSymbols>true</DebugSymbols>
|
||||
<OutputPath>bin\x64\Debug\</OutputPath>
|
||||
<DefineConstants>TRACE;DEBUG;FRAMEWORK_LT_4</DefineConstants>
|
||||
<DebugType>full</DebugType>
|
||||
<PlatformTarget>x64</PlatformTarget>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
|
||||
<Prefer32Bit>true</Prefer32Bit>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x64'">
|
||||
<OutputPath>bin\x64\Release\</OutputPath>
|
||||
<DefineConstants>TRACE;FRAMEWORK_LT_4</DefineConstants>
|
||||
<Optimize>true</Optimize>
|
||||
<DebugType>pdbonly</DebugType>
|
||||
<PlatformTarget>x64</PlatformTarget>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
|
||||
<Prefer32Bit>true</Prefer32Bit>
|
||||
</PropertyGroup>
|
||||
<ItemGroup>
|
||||
<Compile Include="..\..\..\..\..\examples\dotnet\Program.cs">
|
||||
<Link>Program.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="Properties\AssemblyInfo.cs" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<None Include="App.config" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<ProjectReference Include="..\Microsoft.Z3.NET35.csproj">
|
||||
<Project>{ec3db697-b734-42f7-9468-5b62821eeb5a}</Project>
|
||||
<Name>Microsoft.Z3.NET35</Name>
|
||||
</ProjectReference>
|
||||
</ItemGroup>
|
||||
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
|
||||
<!-- 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>
|
||||
|
|
@ -1,36 +0,0 @@
|
|||
using System.Reflection;
|
||||
using System.Runtime.CompilerServices;
|
||||
using System.Runtime.InteropServices;
|
||||
|
||||
// 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("Example")]
|
||||
[assembly: AssemblyDescription("")]
|
||||
[assembly: AssemblyConfiguration("")]
|
||||
[assembly: AssemblyCompany("")]
|
||||
[assembly: AssemblyProduct("Example")]
|
||||
[assembly: AssemblyCopyright("Copyright © 2017")]
|
||||
[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("2a8e577b-7b6d-4ca9-832a-ca2eec314812")]
|
||||
|
||||
// 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("1.0.*")]
|
||||
[assembly: AssemblyVersion("1.0.0.0")]
|
||||
[assembly: AssemblyFileVersion("1.0.0.0")]
|
||||
|
|
@ -1,347 +0,0 @@
|
|||
<?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>v3.5</TargetFrameworkVersion>
|
||||
<FileAlignment>512</FileAlignment>
|
||||
<TargetFrameworkProfile>
|
||||
</TargetFrameworkProfile>
|
||||
<CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
|
||||
<DebugSymbols>true</DebugSymbols>
|
||||
<DebugType>full</DebugType>
|
||||
<Optimize>false</Optimize>
|
||||
<OutputPath>Debug\</OutputPath>
|
||||
<DefineConstants>TRACE;DEBUG;FRAMEWORK_LT_4</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>Release\</OutputPath>
|
||||
<DefineConstants>FRAMEWORK_LT_4</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
|
||||
<DocumentationFile>Release\Microsoft.Z3.xml</DocumentationFile>
|
||||
<PlatformTarget>x86</PlatformTarget>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup>
|
||||
<SignAssembly>true</SignAssembly>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup>
|
||||
<AssemblyOriginatorKeyFile>
|
||||
</AssemblyOriginatorKeyFile>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup>
|
||||
<DelaySign>false</DelaySign>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x64'">
|
||||
<DebugSymbols>true</DebugSymbols>
|
||||
<OutputPath>bin\x64\Debug\</OutputPath>
|
||||
<DefineConstants>TRACE;DEBUG;FRAMEWORK_LT_4</DefineConstants>
|
||||
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
|
||||
<DocumentationFile>Debug\Microsoft.Z3.XML</DocumentationFile>
|
||||
<DebugType>full</DebugType>
|
||||
<PlatformTarget>x64</PlatformTarget>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x64'">
|
||||
<OutputPath>bin\x64\Release\</OutputPath>
|
||||
<DefineConstants>FRAMEWORK_LT_4</DefineConstants>
|
||||
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
|
||||
<DocumentationFile>Release\Microsoft.Z3.xml</DocumentationFile>
|
||||
<Optimize>true</Optimize>
|
||||
<DebugType>pdbonly</DebugType>
|
||||
<PlatformTarget>x64</PlatformTarget>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
|
||||
</PropertyGroup>
|
||||
<ItemGroup>
|
||||
<Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
|
||||
<HintPath>packages\Code.Contract.1.0.0\lib\net35\Microsoft.Contracts.dll</HintPath>
|
||||
<Private>True</Private>
|
||||
</Reference>
|
||||
<Reference Include="System" />
|
||||
<Reference Include="System.Core" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<Compile Include="..\AlgebraicNum.cs">
|
||||
<Link>AlgebraicNum.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ApplyResult.cs">
|
||||
<Link>ApplyResult.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ArithExpr.cs">
|
||||
<Link>ArithExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ArithSort.cs">
|
||||
<Link>ArithSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ArrayExpr.cs">
|
||||
<Link>ArrayExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ArraySort.cs">
|
||||
<Link>ArraySort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\AST.cs">
|
||||
<Link>AST.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ASTMap.cs">
|
||||
<Link>ASTMap.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ASTVector.cs">
|
||||
<Link>ASTVector.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\BitVecExpr.cs">
|
||||
<Link>BitVecExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\BitVecNum.cs">
|
||||
<Link>BitVecNum.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\BitVecSort.cs">
|
||||
<Link>BitVecSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\BoolExpr.cs">
|
||||
<Link>BoolExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\BoolSort.cs">
|
||||
<Link>BoolSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Constructor.cs">
|
||||
<Link>Constructor.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ConstructorList.cs">
|
||||
<Link>ConstructorList.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Context.cs">
|
||||
<Link>Context.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\DatatypeExpr.cs">
|
||||
<Link>DatatypeExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\DatatypeSort.cs">
|
||||
<Link>DatatypeSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Deprecated.cs">
|
||||
<Link>Deprecated.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Enumerations.cs">
|
||||
<Link>Enumerations.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\EnumSort.cs">
|
||||
<Link>EnumSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Expr.cs">
|
||||
<Link>Expr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FiniteDomainExpr.cs">
|
||||
<Link>FiniteDomainExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FiniteDomainNum.cs">
|
||||
<Link>FiniteDomainNum.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FiniteDomainSort.cs">
|
||||
<Link>FiniteDomainSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Fixedpoint.cs">
|
||||
<Link>Fixedpoint.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FPExpr.cs">
|
||||
<Link>FPExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FPNum.cs">
|
||||
<Link>FPNum.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FPRMExpr.cs">
|
||||
<Link>FPRMExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FPRMNum.cs">
|
||||
<Link>FPRMNum.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FPRMSort.cs">
|
||||
<Link>FPRMSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FPSort.cs">
|
||||
<Link>FPSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FuncDecl.cs">
|
||||
<Link>FuncDecl.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\FuncInterp.cs">
|
||||
<Link>FuncInterp.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Global.cs">
|
||||
<Link>Global.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Goal.cs">
|
||||
<Link>Goal.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\IDecRefQueue.cs">
|
||||
<Link>IDecRefQueue.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\InterpolationContext.cs">
|
||||
<Link>InterpolationContext.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\IntExpr.cs">
|
||||
<Link>IntExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\IntNum.cs">
|
||||
<Link>IntNum.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\IntSort.cs">
|
||||
<Link>IntSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\IntSymbol.cs">
|
||||
<Link>IntSymbol.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ListSort.cs">
|
||||
<Link>ListSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Log.cs">
|
||||
<Link>Log.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Model.cs">
|
||||
<Link>Model.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Native.cs">
|
||||
<Link>Native.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Optimize.cs">
|
||||
<Link>Optimize.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ParamDescrs.cs">
|
||||
<Link>ParamDescrs.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Params.cs">
|
||||
<Link>Params.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Pattern.cs">
|
||||
<Link>Pattern.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Probe.cs">
|
||||
<Link>Probe.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Quantifier.cs">
|
||||
<Link>Quantifier.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RatNum.cs">
|
||||
<Link>RatNum.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RealExpr.cs">
|
||||
<Link>RealExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RealSort.cs">
|
||||
<Link>RealSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ReExpr.cs">
|
||||
<Link>ReExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RelationSort.cs">
|
||||
<Link>RelationSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\ReSort.cs">
|
||||
<Link>ReSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\SeqExpr.cs">
|
||||
<Link>SeqExpr.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\SeqSort.cs">
|
||||
<Link>SeqSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\SetSort.cs">
|
||||
<Link>SetSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Solver.cs">
|
||||
<Link>Solver.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Sort.cs">
|
||||
<Link>Sort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Statistics.cs">
|
||||
<Link>Statistics.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Status.cs">
|
||||
<Link>Status.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\StringSymbol.cs">
|
||||
<Link>StringSymbol.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Symbol.cs">
|
||||
<Link>Symbol.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Tactic.cs">
|
||||
<Link>Tactic.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\TupleSort.cs">
|
||||
<Link>TupleSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\UninterpretedSort.cs">
|
||||
<Link>UninterpretedSort.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Version.cs">
|
||||
<Link>Version.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Z3Exception.cs">
|
||||
<Link>Z3Exception.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\Z3Object.cs">
|
||||
<Link>Z3Object.cs</Link>
|
||||
</Compile>
|
||||
<Compile Include="Properties\AssemblyInfo.cs" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<WCFMetadata Include="Service References\" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<None Include="packages.config" />
|
||||
</ItemGroup>
|
||||
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
|
||||
</Project>
|
||||
|
|
@ -1,48 +0,0 @@
|
|||
|
||||
Microsoft Visual Studio Solution File, Format Version 12.00
|
||||
# Visual Studio 14
|
||||
VisualStudioVersion = 14.0.25420.1
|
||||
MinimumVisualStudioVersion = 10.0.40219.1
|
||||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Microsoft.Z3.NET35", "Microsoft.Z3.NET35.csproj", "{EC3DB697-B734-42F7-9468-5B62821EEB5A}"
|
||||
EndProject
|
||||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Example", "Example\Example.csproj", "{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}"
|
||||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|Any CPU = Debug|Any CPU
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|Any CPU = Release|Any CPU
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.ActiveCfg = Debug|Any CPU
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.Build.0 = Debug|Any CPU
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.ActiveCfg = Debug|Any CPU
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.Build.0 = Debug|Any CPU
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.ActiveCfg = Release|x64
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.Build.0 = Release|x64
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.ActiveCfg = Release|Any CPU
|
||||
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.Build.0 = Release|Any CPU
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.ActiveCfg = Debug|Any CPU
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.Build.0 = Debug|Any CPU
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.ActiveCfg = Debug|Any CPU
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.Build.0 = Debug|Any CPU
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.ActiveCfg = Release|x64
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.Build.0 = Release|x64
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.ActiveCfg = Release|Any CPU
|
||||
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.Build.0 = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(SolutionProperties) = preSolution
|
||||
HideSolutionNode = FALSE
|
||||
EndGlobalSection
|
||||
EndGlobal
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
using System;
|
||||
using System.Reflection;
|
||||
using System.Runtime.CompilerServices;
|
||||
using System.Runtime.InteropServices;
|
||||
using System.Security.Permissions;
|
||||
|
||||
// General Information about an assembly is controlled through the following
|
||||
// set of attributes. Change these attribute values to modify the information
|
||||
// associated with an assembly.
|
||||
[assembly: AssemblyTitle("Z3 .NET Interface")]
|
||||
[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")]
|
||||
[assembly: AssemblyConfiguration("")]
|
||||
[assembly: AssemblyCompany("Microsoft Corporation")]
|
||||
[assembly: AssemblyProduct("Z3")]
|
||||
[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")]
|
||||
[assembly: AssemblyTrademark("")]
|
||||
[assembly: AssemblyCulture("")]
|
||||
|
||||
// Setting ComVisible to false makes the types in this assembly not visible
|
||||
// to COM components. If you need to access a type in this assembly from
|
||||
// COM, set the ComVisible attribute to true on that type.
|
||||
[assembly: ComVisible(false)]
|
||||
|
||||
// The following GUID is for the ID of the typelib if this project is exposed to COM
|
||||
[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")]
|
||||
|
||||
// Version information for an assembly consists of the following four values:
|
||||
//
|
||||
// Major Version
|
||||
// Minor Version
|
||||
// Build Number
|
||||
// Revision
|
||||
//
|
||||
// You can specify all the values or you can default the Build and Revision Numbers
|
||||
// by using the '*' as shown below:
|
||||
// [assembly: AssemblyVersion("4.2.0.0")]
|
||||
[assembly: AssemblyVersion("4.5.1.6031")]
|
||||
[assembly: AssemblyFileVersion("4.5.1.6031")]
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
using System;
|
||||
using System.Reflection;
|
||||
using System.Runtime.CompilerServices;
|
||||
using System.Runtime.InteropServices;
|
||||
using System.Security.Permissions;
|
||||
|
||||
// General Information about an assembly is controlled through the following
|
||||
// set of attributes. Change these attribute values to modify the information
|
||||
// associated with an assembly.
|
||||
[assembly: AssemblyTitle("Z3 .NET Interface")]
|
||||
[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")]
|
||||
[assembly: AssemblyConfiguration("")]
|
||||
[assembly: AssemblyCompany("Microsoft Corporation")]
|
||||
[assembly: AssemblyProduct("Z3")]
|
||||
[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")]
|
||||
[assembly: AssemblyTrademark("")]
|
||||
[assembly: AssemblyCulture("")]
|
||||
|
||||
// Setting ComVisible to false makes the types in this assembly not visible
|
||||
// to COM components. If you need to access a type in this assembly from
|
||||
// COM, set the ComVisible attribute to true on that type.
|
||||
[assembly: ComVisible(false)]
|
||||
|
||||
// The following GUID is for the ID of the typelib if this project is exposed to COM
|
||||
[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")]
|
||||
|
||||
// Version information for an assembly consists of the following four values:
|
||||
//
|
||||
// Major Version
|
||||
// Minor Version
|
||||
// Build Number
|
||||
// Revision
|
||||
//
|
||||
// You can specify all the values or you can default the Build and Revision Numbers
|
||||
// by using the '*' as shown below:
|
||||
// [assembly: AssemblyVersion("4.2.0.0")]
|
||||
[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")]
|
||||
[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")]
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
The default Z3 bindings for .NET are built for the .NET framework version 4.
|
||||
Should the need arise, it is also possible to build them for .NET 3.5; the
|
||||
instructions are as follows:
|
||||
|
||||
In the project properties of Microsoft.Z3.csproj:
|
||||
- Under 'Application': Change Target framework to .NET Framework 3.5
|
||||
- Under 'Build': Add FRAMEWORK_LT_4 to the condidional compilation symbols
|
||||
- Remove the reference to System.Numerics
|
||||
- Install the NuGet Package "Microsoft Code Contracts for Net3.5":
|
||||
In the Package Manager Console enter Install-Package Code.Contract
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<packages>
|
||||
<package id="Code.Contract" version="1.0.0" targetFramework="net35" />
|
||||
</packages>
|
||||
Loading…
Add table
Add a link
Reference in a new issue