diff --git a/cmake/modules/DotnetImports.props.in b/cmake/modules/DotnetImports.props.in new file mode 100644 index 000000000..fba9ae301 --- /dev/null +++ b/cmake/modules/DotnetImports.props.in @@ -0,0 +1,7 @@ + + + ${_DN_OUTPUT_PATH}/ + ${XPLAT_LIB_DIR}/ + ${_DN_VERSION} + + diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake new file mode 100644 index 000000000..a3d0c2dd1 --- /dev/null +++ b/cmake/modules/FindDotnet.cmake @@ -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( [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( +# [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( [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## \\n #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 $) + 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) diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 50f643c8d..987ef3dff 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -1,12 +1,10 @@ -find_package(DotNetToolchain REQUIRED) +find_package(Dotnet REQUIRED) # Configure AssemblyInfo.cs set(VER_MAJOR "${Z3_VERSION_MAJOR}") set(VER_MINOR "${Z3_VERSION_MINOR}") set(VER_BUILD "${Z3_VERSION_PATCH}") set(VER_REVISION "${Z3_VERSION_TWEAK}") -set(Z3_DOTNET_ASSEMBLY_INFO_FILE "${CMAKE_CURRENT_BINARY_DIR}/Properties/AssemblyInfo.cs") -configure_file("Properties/AssemblyInfo.cs.in" "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" @ONLY) # Generate Native.cs set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs") @@ -127,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 items +set(Z3_DOTNET_COMPILE_ITEMS "") +foreach(csfile ${Z3_DOTNET_ASSEMBLY_SOURCES}) + set(Z3_DOTNET_COMPILE_ITEMS "${Z3_DOTNET_COMPILE_ITEMS}\n ") endforeach() -set(CSC_FLAGS "") -if (DOTNET_TOOLCHAIN_IS_WINDOWS) - # FIXME: Why use these flags? - # Note these flags have been copied from the Python build system. - list(APPEND CSC_FLAGS - "/noconfig" - "/nostdlib+" - "/reference:mscorlib.dll" - ) - # 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:$") -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 - "$<$:/debug+>" - "$<$:/debug:full>" - "$<$:/optimize->" - # This has to be quoted otherwise the ``;`` is interpreted as a command separator - "$<$:\"/define:DEBUG$TRACE\">" - # Release flags, expands to nothing if we are doing a debug build - "$<$>:/optimize+>" -) +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 ``$`` 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 diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj deleted file mode 100644 index cde8b78c9..000000000 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ /dev/null @@ -1,417 +0,0 @@ - - - - Debug - AnyCPU - 8.0.30703 - 2.0 - {EC3DB697-B734-42F7-9468-5B62821EEB5A} - Library - Properties - Microsoft.Z3 - Microsoft.Z3 - v4.0 - 512 - Client - 0 - - - true - full - false - ..\Debug\ - DEBUG;TRACE - prompt - 4 - true - ..\Debug\Microsoft.Z3.XML - False - False - True - False - False - True - False - True - True - False - False - False - True - False - False - False - True - False - False - True - True - True - False - False - - - - - - - True - Full - %28none%29 - 2 - - - pdbonly - true - ..\external\ - - - prompt - 4 - true - ..\external\Microsoft.Z3.xml - AnyCPU - - - ..\external\ - true - ..\external\Microsoft.Z3.xml - true - pdbonly - AnyCPU - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - false - - - true - ..\x64\Debug\ - DEBUG;TRACE - true - full - x64 - ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - True - False - True - False - False - False - False - False - False - False - False - False - False - False - False - False - True - False - False - True - False - False - False - - - - - - - False - Full - %28none%29 - 0 - ..\x64\Debug\Microsoft.Z3.XML - - - ..\x64\external_64\ - true - ..\x64\external_64\Microsoft.Z3.xml - true - pdbonly - x64 - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - True - False - True - False - False - True - True - True - False - False - False - True - True - False - False - False - True - False - False - True - True - False - False - - - - - -repro - - True - Full - %28none%29 - 2 - - - ..\x64\external\ - true - ..\x64\external\Microsoft.Z3.XML - true - pdbonly - x64 - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - - - false - - - - - - - false - - - ..\Release_delaysign\ - true - ..\Release_delaysign\Microsoft.Z3.XML - true - pdbonly - AnyCPU - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - DELAYSIGN - - - bin\x64\Release_delaysign\ - true - bin\x64\Release_delaysign\Microsoft.Z3.XML - true - pdbonly - x64 - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - - - true - ..\x86\Debug\ - DEBUG;TRACE - true - full - x86 - ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - ..\x86\Debug\Microsoft.Z3.XML - - - bin\x86\Release\ - true - bin\x86\Release\Microsoft.Z3.xml - true - pdbonly - x86 - ..\external\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - - - bin\x86\external\ - true - bin\x86\external\Microsoft.Z3.XML - true - pdbonly - x86 - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - - - bin\x86\Release_delaysign\ - DELAYSIGN - true - bin\x86\Release_delaysign\Microsoft.Z3.XML - true - pdbonly - x86 - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in new file mode 100644 index 000000000..b2fda27e4 --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -0,0 +1,73 @@ + + + + + + Microsoft.Z3 + Microsoft.Z3 + + Z3 .NET Interface + Z3 .NET Interface + + Z3 + + .NET Interface to the Z3 Theorem Prover + .NET Interface to the Z3 Theorem Prover + + Copyright (C) 2006-2015 Microsoft Corporation + Copyright (C) 2006-2015 Microsoft Corporation + + Microsoft Corporation + Microsoft Corporation + + @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ + @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ + + @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ + @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ + + ${DOTNET_PACKAGE_VERSION} + + + + + + + netstandard2.0;net461;net45 + library + True + 1701,1702 + 4 + FRAMEWORK_LT_4 + + + + +${Z3_DOTNET_COMPILE_ITEMS} + + + + + + build + + + build + + + + + + + + runtimes\win-x64\native + + + + + + + + + + diff --git a/src/api/dotnet/Microsoft.Z3.props b/src/api/dotnet/Microsoft.Z3.props new file mode 100644 index 000000000..67bb471ba --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.props @@ -0,0 +1,22 @@ + + + + + + true + true + true + + + $(MSBuildThisFileDirectory)..\..\ + $(Z3_PACKAGE_PATH)runtimes\win-x64\native\libz3.dll + $(Z3_PACKAGE_PATH)runtimes\linux-x64\native\libz3.so + + + + + + false + + + diff --git a/src/api/dotnet/Microsoft.Z3.targets b/src/api/dotnet/Microsoft.Z3.targets new file mode 100644 index 000000000..80179ce4c --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.targets @@ -0,0 +1,11 @@ + + + + + + %(RecursiveDir)%(FileName)%(Extension) + PreserveNewest + + + + diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs.in b/src/api/dotnet/Properties/AssemblyInfo.cs.in deleted file mode 100644 index e5a85f16f..000000000 --- a/src/api/dotnet/Properties/AssemblyInfo.cs.in +++ /dev/null @@ -1,38 +0,0 @@ -using System; -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; -using System.Security.Permissions; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Z3 .NET Interface")] -[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("Microsoft Corporation")] -[assembly: AssemblyProduct("Z3")] -[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// The following GUID is for the ID of the typelib if this project is exposed to COM -[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -// [assembly: AssemblyVersion("4.2.0.0")] -[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] -[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] diff --git a/src/api/dotnet/core/DummyContracts.cs b/src/api/dotnet/core/DummyContracts.cs deleted file mode 100644 index 103cc1288..000000000 --- a/src/api/dotnet/core/DummyContracts.cs +++ /dev/null @@ -1,65 +0,0 @@ -/*++ -Copyright () 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 p) { return true; } - public static bool ForAll(int from, int to, Predicate p) { return true; } - [Conditional("false")] - public static void Invariant(bool b) { } - public static T[] Result() { return new T[1]; } - [Conditional("false")] - public static void EndContractBlock() { } - public static T ValueAtReturn(out T v) { T[] t = new T[1]; v = t[0]; return v; } - } -} diff --git a/src/api/dotnet/core/README.txt b/src/api/dotnet/core/README.txt deleted file mode 100644 index 72331d7f9..000000000 --- a/src/api/dotnet/core/README.txt +++ /dev/null @@ -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 diff --git a/src/api/dotnet/core/project.json b/src/api/dotnet/core/project.json deleted file mode 100644 index d54b6877b..000000000 --- a/src/api/dotnet/core/project.json +++ /dev/null @@ -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" - } - } -} diff --git a/src/api/dotnet/dotnet35/Example/App.config b/src/api/dotnet/dotnet35/Example/App.config deleted file mode 100644 index 737ed23f2..000000000 --- a/src/api/dotnet/dotnet35/Example/App.config +++ /dev/null @@ -1,6 +0,0 @@ - - - - - - diff --git a/src/api/dotnet/dotnet35/Example/Example.csproj b/src/api/dotnet/dotnet35/Example/Example.csproj deleted file mode 100644 index 842fbac41..000000000 --- a/src/api/dotnet/dotnet35/Example/Example.csproj +++ /dev/null @@ -1,78 +0,0 @@ - - - - - Debug - AnyCPU - {2A8E577B-7B6D-4CA9-832A-CA2EEC314812} - Exe - Properties - Example - Example - v4.5.2 - 512 - true - - - AnyCPU - true - full - false - bin\Debug\ - TRACE;DEBUG;FRAMEWORK_LT_4 - prompt - 4 - - - AnyCPU - pdbonly - true - bin\Release\ - TRACE;FRAMEWORK_LT_4 - prompt - 4 - - - true - bin\x64\Debug\ - TRACE;DEBUG;FRAMEWORK_LT_4 - full - x64 - prompt - MinimumRecommendedRules.ruleset - true - - - bin\x64\Release\ - TRACE;FRAMEWORK_LT_4 - true - pdbonly - x64 - prompt - MinimumRecommendedRules.ruleset - true - - - - Program.cs - - - - - - - - - {ec3db697-b734-42f7-9468-5b62821eeb5a} - Microsoft.Z3.NET35 - - - - - diff --git a/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs b/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs deleted file mode 100644 index ed0d8454f..000000000 --- a/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs +++ /dev/null @@ -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")] diff --git a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj deleted file mode 100644 index 15eaac445..000000000 --- a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj +++ /dev/null @@ -1,347 +0,0 @@ - - - - Debug - AnyCPU - 8.0.30703 - 2.0 - {EC3DB697-B734-42F7-9468-5B62821EEB5A} - Library - Properties - Microsoft.Z3 - Microsoft.Z3 - v3.5 - 512 - - - 0 - - - true - full - false - Debug\ - TRACE;DEBUG;FRAMEWORK_LT_4 - prompt - 4 - true - Debug\Microsoft.Z3.XML - False - False - True - False - False - True - False - True - True - False - False - False - True - False - False - False - True - False - False - True - True - True - False - False - - - - - - - True - Full - %28none%29 - 2 - - - pdbonly - true - Release\ - FRAMEWORK_LT_4 - prompt - 4 - true - Release\Microsoft.Z3.xml - x86 - - - true - - - - - - - false - - - true - bin\x64\Debug\ - TRACE;DEBUG;FRAMEWORK_LT_4 - true - Debug\Microsoft.Z3.XML - full - x64 - prompt - MinimumRecommendedRules.ruleset - - - bin\x64\Release\ - FRAMEWORK_LT_4 - true - Release\Microsoft.Z3.xml - true - pdbonly - x64 - prompt - MinimumRecommendedRules.ruleset - - - - packages\Code.Contract.1.0.0\lib\net35\Microsoft.Contracts.dll - True - - - - - - - AlgebraicNum.cs - - - ApplyResult.cs - - - ArithExpr.cs - - - ArithSort.cs - - - ArrayExpr.cs - - - ArraySort.cs - - - AST.cs - - - ASTMap.cs - - - ASTVector.cs - - - BitVecExpr.cs - - - BitVecNum.cs - - - BitVecSort.cs - - - BoolExpr.cs - - - BoolSort.cs - - - Constructor.cs - - - ConstructorList.cs - - - Context.cs - - - DatatypeExpr.cs - - - DatatypeSort.cs - - - Deprecated.cs - - - Enumerations.cs - - - EnumSort.cs - - - Expr.cs - - - FiniteDomainExpr.cs - - - FiniteDomainNum.cs - - - FiniteDomainSort.cs - - - Fixedpoint.cs - - - FPExpr.cs - - - FPNum.cs - - - FPRMExpr.cs - - - FPRMNum.cs - - - FPRMSort.cs - - - FPSort.cs - - - FuncDecl.cs - - - FuncInterp.cs - - - Global.cs - - - Goal.cs - - - IDecRefQueue.cs - - - InterpolationContext.cs - - - IntExpr.cs - - - IntNum.cs - - - IntSort.cs - - - IntSymbol.cs - - - ListSort.cs - - - Log.cs - - - Model.cs - - - Native.cs - - - Optimize.cs - - - ParamDescrs.cs - - - Params.cs - - - Pattern.cs - - - Probe.cs - - - Quantifier.cs - - - RatNum.cs - - - RealExpr.cs - - - RealSort.cs - - - ReExpr.cs - - - RelationSort.cs - - - ReSort.cs - - - SeqExpr.cs - - - SeqSort.cs - - - SetSort.cs - - - Solver.cs - - - Sort.cs - - - Statistics.cs - - - Status.cs - - - StringSymbol.cs - - - Symbol.cs - - - Tactic.cs - - - TupleSort.cs - - - UninterpretedSort.cs - - - Version.cs - - - Z3Exception.cs - - - Z3Object.cs - - - - - - - - - - - diff --git a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln deleted file mode 100644 index 1e33f136e..000000000 --- a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln +++ /dev/null @@ -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 diff --git a/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs b/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs deleted file mode 100644 index fb4319002..000000000 --- a/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs +++ /dev/null @@ -1,38 +0,0 @@ -using System; -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; -using System.Security.Permissions; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Z3 .NET Interface")] -[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("Microsoft Corporation")] -[assembly: AssemblyProduct("Z3")] -[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// The following GUID is for the ID of the typelib if this project is exposed to COM -[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -// [assembly: AssemblyVersion("4.2.0.0")] -[assembly: AssemblyVersion("4.5.1.6031")] -[assembly: AssemblyFileVersion("4.5.1.6031")] diff --git a/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in b/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in deleted file mode 100644 index e5a85f16f..000000000 --- a/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in +++ /dev/null @@ -1,38 +0,0 @@ -using System; -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; -using System.Security.Permissions; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Z3 .NET Interface")] -[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("Microsoft Corporation")] -[assembly: AssemblyProduct("Z3")] -[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// The following GUID is for the ID of the typelib if this project is exposed to COM -[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -// [assembly: AssemblyVersion("4.2.0.0")] -[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] -[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] diff --git a/src/api/dotnet/dotnet35/Readme.NET35 b/src/api/dotnet/dotnet35/Readme.NET35 deleted file mode 100644 index f8c2958ee..000000000 --- a/src/api/dotnet/dotnet35/Readme.NET35 +++ /dev/null @@ -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 diff --git a/src/api/dotnet/dotnet35/packages.config b/src/api/dotnet/dotnet35/packages.config deleted file mode 100644 index bc9f365bc..000000000 --- a/src/api/dotnet/dotnet35/packages.config +++ /dev/null @@ -1,4 +0,0 @@ - - - -