diff --git a/.gitignore b/.gitignore
index e189a9569..9b239a566 100644
--- a/.gitignore
+++ b/.gitignore
@@ -76,3 +76,5 @@ src/api/ml/z3.mllib
*.bak
doc/api
doc/code
+.vs
+examples/**/obj
diff --git a/CMakeSettings.json b/CMakeSettings.json
new file mode 100644
index 000000000..f8c4fa7c6
--- /dev/null
+++ b/CMakeSettings.json
@@ -0,0 +1,17 @@
+{
+ "configurations": [
+ {
+ "name": "x64-Release",
+ "generator": "Visual Studio 15 2017 Win64",
+ "configurationType": "RelWithDebInfo",
+ "inheritEnvironments": [
+ "msvc_x64_x64"
+ ],
+ "buildRoot": "F:\\b\\z3\\build\\${name}",
+ "installRoot": "F:\\b\\z3\\install\\${name}",
+ "cmakeCommandArgs": "",
+ "buildCommandArgs": "",
+ "ctestCommandArgs": ""
+ }
+ ]
+}
\ No newline at end of file
diff --git a/cmake/modules/DotnetImports.props.in b/cmake/modules/DotnetImports.props.in
index fba9ae301..090d46502 100644
--- a/cmake/modules/DotnetImports.props.in
+++ b/cmake/modules/DotnetImports.props.in
@@ -1,7 +1,8 @@
${_DN_OUTPUT_PATH}/
- ${XPLAT_LIB_DIR}/
+ ${_DN_XPLAT_LIB_DIR}/
${_DN_VERSION}
+ ${_DN_CUSTOM_BUILDPROPS}
diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake
index f424d3f23..4bcfe2215 100644
--- a/cmake/modules/FindDotnet.cmake
+++ b/cmake/modules/FindDotnet.cmake
@@ -32,9 +32,15 @@
# produced by running the .NET program, and can be consumed from other build steps.
#
# ```
-# RUN_DOTNET(
+# RUN_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP]
# [ARGUMENTS program_args...]
-# [OUTPUT outputs...])
+# [OUTPUT outputs...]
+# [CONFIG configuration]
+# [PLATFORM platform]
+# [DEPENDS depend_nuget_packages... ]
+# [OUTPUT_PATH output_path relative to cmake binary output dir]
+# [CUSTOM_BUILDPROPS value....]
+# [SOURCES additional_file_dependencies... ])
# ```
#
# ADD_MSBUILD -- add a project to be built by msbuild. Windows-only. When building in Unix systems, msbuild targets are skipped.
@@ -54,11 +60,11 @@
# Multiple smoke tests will be run one-by-one to avoid global resource conflicts.
#
# SMOKETEST_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP]
+# [ARGUMENTS program_args...]
# [CONFIG configuration]
# [PLATFORM platform]
-# [PACKAGE output_nuget_packages... ]
-# [VERSION nuget_package_version]
# [DEPENDS depend_nuget_packages... ]
+# [OUTPUT_PATH output_path relative to cmake binary output dir]
# [CUSTOM_BUILDPROPS value....]
# [SOURCES additional_file_dependencies... ])
#
@@ -81,7 +87,8 @@
#
# ```
# TEST_DOTNET(
-# [ARGUMENTS additional_dotnet_test_args...])
+# [ARGUMENTS additional_dotnet_test_args...]
+# [OUTPUT_PATH output_path relative to cmake binary output dir])
# ```
#
# GEN_DOTNET_PROPS -- Generates a Directory.Build.props file. The created file is populated with MSBuild properties:
@@ -153,7 +160,6 @@ FUNCTION(DOTNET_REGISTER_LOCAL_REPOSITORY repo_name repo_path)
ENDFUNCTION()
FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
- FILE(GLOB_RECURSE DOTNET_deps *.cs *.fs *.xaml *.csproj *.fsproj *.tsl)
CMAKE_PARSE_ARGUMENTS(
# prefix
_DN
@@ -166,18 +172,29 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
# the input arguments
${arguments})
+ GET_FILENAME_COMPONENT(_DN_abs_proj "${_DN_PROJECT}" ABSOLUTE)
+ GET_FILENAME_COMPONENT(_DN_proj_dir "${_DN_abs_proj}" DIRECTORY)
+ GET_FILENAME_COMPONENT(_DN_projname "${_DN_PROJECT}" NAME)
+ STRING(REGEX REPLACE "\\.[^.]*$" "" _DN_projname_noext ${_DN_projname})
+
+ FILE(GLOB_RECURSE DOTNET_deps
+ ${_DN_proj_dir}/*.cs
+ ${_DN_proj_dir}/*.fs
+ ${_DN_proj_dir}/*.vb
+ ${_DN_proj_dir}/*.xaml
+ ${_DN_proj_dir}/*.resx
+ ${_DN_proj_dir}/*.xml
+ ${_DN_proj_dir}/*.*proj
+ ${_DN_proj_dir}/*.cs
+ ${_DN_proj_dir}/*.config)
LIST(APPEND DOTNET_deps ${_DN_SOURCES})
SET(_DN_deps "")
FOREACH(dep ${DOTNET_deps})
- IF(NOT dep MATCHES /obj/)
+ IF(NOT dep MATCHES /obj/ AND NOT dep MATCHES /bin/)
LIST(APPEND _DN_deps ${dep})
ENDIF()
ENDFOREACH()
- 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)
@@ -186,10 +203,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
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()
+ SET(_DN_CONFIG Release)
ENDIF()
# If platform is not specified, do not pass the Platform property.
@@ -217,7 +231,7 @@ FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments)
# Later we then copy the outputs to the destination.
IF(NOT _DN_OUTPUT_PATH)
- SET(_DN_OUTPUT_PATH "bin")
+ SET(_DN_OUTPUT_PATH ${_DN_projname_noext})
ENDIF()
GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_CURRENT_BINARY_DIR}/${_DN_OUTPUT_PATH} ABSOLUTE)
@@ -295,14 +309,14 @@ 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} -PackagesDirectory packages
- COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean /p:Configuration="${DOTNET_CONFIG}"
+ COMMAND ${CMAKE_COMMAND} -E echo "======= Building msbuild project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]"
+ COMMAND ${NUGET_EXE} restore -Force ${DOTNET_PROJPATH}
+ COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}"
COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Build ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}")
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 ${CMAKE_COMMAND} -E echo "======= Building .NET project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]"
COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES}
COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES}
COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS})
@@ -310,21 +324,22 @@ MACRO(DOTNET_BUILD_COMMANDS)
ENDIF()
# DOTNET_OUTPUTS refer to artifacts produced, that the BUILD_proj_name target depends on.
- SET(DOTNET_OUTPUTS "")
+ SET(DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp)
+ LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${DOTNET_OUTPUTS})
IF(NOT "${DOTNET_PACKAGES}" STREQUAL "")
MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (version ${DOTNET_PACKAGE_VERSION})")
SET(_DN_OUTPUTS "")
FOREACH(pkg ${DOTNET_PACKAGES})
LIST(APPEND _DN_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg)
LIST(APPEND DOTNET_OUTPUTS ${CMAKE_BINARY_DIR}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg)
+
+ LIST(APPEND _DN_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg)
+ LIST(APPEND DOTNET_OUTPUTS ${CMAKE_BINARY_DIR}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg)
ENDFOREACH()
LIST(APPEND build_dotnet_cmds COMMAND ${DOTNET_EXE} pack --no-build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_PACK_OPTIONS})
LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E copy ${_DN_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(
@@ -358,17 +373,23 @@ FUNCTION(ADD_MSBUILD DOTNET_PROJECT)
ENDFUNCTION()
FUNCTION(RUN_DOTNET DOTNET_PROJECT)
- DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}")
+ DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN};NETCOREAPP")
+ MESSAGE("-- Adding dotnet run project ${DOTNET_PROJECT}")
+ FILE(MAKE_DIRECTORY ${DOTNET_OUTPUT_PATH})
ADD_CUSTOM_COMMAND(
OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT}
DEPENDS ${DOTNET_deps}
- COMMAND ${DOTNET_EXE} run ${DOTNET_RUN_ARGUMENTS}
+ COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES}
+ COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES}
+ COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS}
+ # XXX tfm
+ COMMAND ${DOTNET_EXE} ${DOTNET_OUTPUT_PATH}/netcoreapp2.0/${DOTNET_PROJNAME}.dll ${DOTNET_RUN_ARGUMENTS}
COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp
- WORKING_DIRECTORY ${DOTNET_PROJDIR})
+ WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH})
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})
+ ADD_DOTNET_DEPENDENCY_TARGETS(RUN)
ENDFUNCTION()
FUNCTION(TEST_DOTNET DOTNET_PROJECT)
@@ -382,20 +403,18 @@ FUNCTION(TEST_DOTNET DOTNET_PROJECT)
ADD_TEST(NAME ${DOTNET_PROJNAME}
COMMAND ${DOTNET_EXE} test ${test_framework_args} --results-directory "${CMAKE_BINARY_DIR}" --logger trx ${DOTNET_RUN_ARGUMENTS}
- WORKING_DIRECTORY ${DOTNET_PROJDIR})
+ WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH})
ENDFUNCTION()
-SET(DOTNET_LAST_SMOKETEST "")
+SET_PROPERTY(GLOBAL PROPERTY DOTNET_LAST_SMOKETEST "")
FUNCTION(SMOKETEST_DOTNET DOTNET_PROJECT)
+ MESSAGE("-- Adding dotnet smoke test project ${DOTNET_PROJECT}")
IF(WIN32)
- ADD_DOTNET(${DOTNET_PROJECT} "${ARGN}")
- # TODO should run on all targeted frameworks
- RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}" ARGUMENTS -f netcoreapp2.0)
+ RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}")
ELSE()
- ADD_DOTNET(${DOTNET_PROJECT} "${ARGN}" NETCOREAPP)
- RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}" ARGUMENTS -f netcoreapp2.0)
+ RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}")
ENDIF()
DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}")
@@ -404,11 +423,13 @@ FUNCTION(SMOKETEST_DOTNET DOTNET_PROJECT)
ALL
DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp)
ADD_DOTNET_DEPENDENCY_TARGETS(SMOKETEST)
- IF(DOTNET_LAST_SMOKETEST)
- ADD_DEPENDENCIES(SMOKETEST_${DOTNET_PROJNAME} ${DOTNET_LAST_SMOKETEST})
+ GET_PROPERTY(_dn_last_smoketest GLOBAL PROPERTY DOTNET_LAST_SMOKETEST)
+ IF(_dn_last_smoketest)
+ MESSAGE("${_dn_last_smoketest} -> SMOKETEST_${DOTNET_PROJNAME}")
+ ADD_DEPENDENCIES(SMOKETEST_${DOTNET_PROJNAME} ${_dn_last_smoketest})
ENDIF()
# Chain the smoke tests together so they are executed sequentially
- SET(DOTNET_LAST_SMOKETEST SMOKETEST_${DOTNET_PROJNAME})
+ SET_PROPERTY(GLOBAL PROPERTY DOTNET_LAST_SMOKETEST SMOKETEST_${DOTNET_PROJNAME})
ENDFUNCTION()
diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in
index ee7b9237d..34321e90b 100644
--- a/src/api/dotnet/Microsoft.Z3.csproj.in
+++ b/src/api/dotnet/Microsoft.Z3.csproj.in
@@ -15,8 +15,8 @@
.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
+ Copyright (C) 2006-2019 Microsoft Corporation
+ Copyright (C) 2006-2019 Microsoft Corporation
Microsoft Corporation
Microsoft Corporation
@@ -36,163 +36,19 @@
false
-
- 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
-
-
- true
- GlobalSuppressions.cs
- 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
-
-
- true
- GlobalSuppressions.cs
- 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
-
+
- true
- GlobalSuppressions.cs
- 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
-
- true
- GlobalSuppressions.cs
- 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
- GlobalSuppressions.cs
- 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
-
-
-
+
netstandard2.0;net461;net45
library
True
1701,1702
4
- FRAMEWORK_LT_4
true
$(OutputPath)\Microsoft.Z3.xml
@@ -224,20 +80,11 @@ ${Z3_DOTNET_COMPILE_ITEMS}
-
-
+
+
runtimes\win-x86\native
-
- runtimes\linux-x86\native
-
-
-
-
-
-
-
diff --git a/src/api/dotnet/core/README.txt b/src/api/dotnet/core/README.txt
deleted file mode 100644
index fa274f72b..000000000
--- a/src/api/dotnet/core/README.txt
+++ /dev/null
@@ -1,15 +0,0 @@
-Z3 API for .NET Core
-
-Z3's .NET API uses Code Contracts, which are not included in .NET Core. The
-enclosed file called DummyContracts.cs provides stubs for the Code Contracts
-functions, so that the API will compile, but not perform any contract
-checking. To build this using .NET core, run (in this directory):
-
-dotnet restore
-dotnet build core.csproj -c Release
-
-If you are building with the cmake system, you should first
-copy over files that are produced by the compiler into
-this directory. You need to copy over Native.cs and Enumeration.cs
-
--- good luck!
diff --git a/src/api/dotnet/core/core.csproj b/src/api/dotnet/core/core.csproj
deleted file mode 100644
index 5fa3275cf..000000000
--- a/src/api/dotnet/core/core.csproj
+++ /dev/null
@@ -1,18 +0,0 @@
-
-
-
- netcoreapp1.0
- $(DefineConstants);DOTNET_CORE
- portable
- Microsoft.Z3
- Library
- core
- $(PackageTargetFallback);dnxcore50
- 1.0.4
-
-
-
-
-
-
-
diff --git a/src/api/dotnet/dotnet35/Readme.NET35 b/src/api/dotnet/dotnet35/Readme.NET35
deleted file mode 100644
index 75210f8b6..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 conditional 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