diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 6c50320ed..17c8e7c3f 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -112,3 +112,10 @@ set_target_properties(z3_tptp5 PROPERTIES EXCLUDE_FROM_ALL TRUE) if (BUILD_PYTHON_BINDINGS) add_subdirectory(python) endif() + +################################################################################ +# Build dotnet examples +################################################################################ +#if (BUILD_DOTNET_BINDINGS) +# add_subdirectory(dotnet) +#endif() \ No newline at end of file diff --git a/examples/dotnet/dotnet.csproj b/examples/dotnet/dotnet.csproj new file mode 100644 index 000000000..7776259ea --- /dev/null +++ b/examples/dotnet/dotnet.csproj @@ -0,0 +1,12 @@ + + + + Exe + netcoreapp2.0 + + + + + + + diff --git a/src/api/dotnet/Microsoft.Z3.Sharp.pc.in b/src/api/dotnet/Microsoft.Z3.Sharp.pc.in deleted file mode 100644 index 8ca4e788b..000000000 --- a/src/api/dotnet/Microsoft.Z3.Sharp.pc.in +++ /dev/null @@ -1,7 +0,0 @@ -prefix=@PREFIX@ -assemblies_dir=${prefix}/lib/mono/@GAC_PKG_NAME@ - -Name: @GAC_PKG_NAME@ -Description: .NET bindings for The Microsoft Z3 SMT solver -Version: @VERSION@ -Libs: -r:${assemblies_dir}/Microsoft.Z3.dll diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj deleted file mode 100644 index 045c610dd..000000000 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ /dev/null @@ -1,418 +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..fc6d6a978 --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -0,0 +1,95 @@ + + + + + + Microsoft.Z3 + Microsoft.Z3 + Microsoft.Z3 + + Z3 .NET Interface + Z3 .NET Interface + + Z3 + + Z3 is a satisfiability modulo theories solver from Microsoft Research. + .NET Interface to the Z3 Theorem Prover + + Copyright (C) 2006-2019 Microsoft Corporation + Copyright (C) 2006-2019 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} + smt constraint solver theorem prover + + Microsoft + Microsoft + + + + + false + false + + + + DELAYSIGN + true + true + + + + + + netstandard2.0;net45 + library + True + 1701,1702 + 4 + true + $(OutputPath)\Microsoft.Z3.xml + + + + +${Z3_DOTNET_COMPILE_ITEMS} + + + + + + build + + + build + + + + + + + + + runtimes\win-x64\native + + + runtimes\linux-x64\native + + + + + + + runtimes\win-x86\native + + + + diff --git a/src/api/dotnet/Microsoft.Z3.props b/src/api/dotnet/Microsoft.Z3.props new file mode 100644 index 000000000..a5db71359 --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.props @@ -0,0 +1,23 @@ + + + + + + true + true + true + + + $(MSBuildThisFileDirectory)..\ + $(Z3_PACKAGE_PATH)runtimes\win-x64\native\libz3.dll + $(Z3_PACKAGE_PATH)runtimes\win-x86\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..38e56b350 --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.targets @@ -0,0 +1,11 @@ + + + + + + %(RecursiveDir)%(FileName)%(Extension) + PreserveNewest + + + + 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 - - - - - - -