diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 5b10dadd0..20bb012b1 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -818,6 +818,7 @@ namespace test_mapi BigIntCheck(ctx, ctx.MkReal("234234333/2")); +#if !FRAMEWORK_LT_4 string bn = "1234567890987654321"; if (ctx.MkInt(bn).BigInteger.ToString() != bn) @@ -828,6 +829,7 @@ namespace test_mapi if (ctx.MkBV(bn, 32).BigInteger.ToString() == bn) throw new TestFailedException(); +#endif // Error handling test. try @@ -1094,8 +1096,10 @@ namespace test_mapi static void BigIntCheck(Context ctx, RatNum r) { +#if !FRAMEWORK_LT_4 Console.WriteLine("Num: " + r.BigIntNumerator); Console.WriteLine("Den: " + r.BigIntDenominator); +#endif } /// diff --git a/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs b/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs new file mode 100644 index 000000000..ef95285e0 --- /dev/null +++ b/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +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("7a55be70-b47a-42c0-bb06-a6c3c3102947")] + +// 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 new file mode 100644 index 000000000..7eaf16fd4 --- /dev/null +++ b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj @@ -0,0 +1,325 @@ + + + + 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 + + + + 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 + + + + + + + + + + + \ No newline at end of file diff --git a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln new file mode 100644 index 000000000..c71a920a2 --- /dev/null +++ b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln @@ -0,0 +1,48 @@ + +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", "{7A55BE70-B47A-42C0-BB06-A6C3C3102947}" +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|Any CPU + {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.Build.0 = Release|Any CPU + {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.ActiveCfg = Release|Any CPU + {EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.Build.0 = Release|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Debug|Any CPU.Build.0 = Debug|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Debug|x64.ActiveCfg = Debug|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Debug|x64.Build.0 = Debug|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Debug|x86.ActiveCfg = Debug|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Debug|x86.Build.0 = Debug|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Release|Any CPU.ActiveCfg = Release|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Release|Any CPU.Build.0 = Release|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Release|x64.ActiveCfg = Release|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Release|x64.Build.0 = Release|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.Release|x86.ActiveCfg = Release|Any CPU + {7A55BE70-B47A-42C0-BB06-A6C3C3102947}.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 new file mode 100644 index 000000000..fb4319002 --- /dev/null +++ b/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs @@ -0,0 +1,38 @@ +using System; +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; +using System.Security.Permissions; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("Z3 .NET Interface")] +[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("Microsoft Corporation")] +[assembly: AssemblyProduct("Z3")] +[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("4.2.0.0")] +[assembly: AssemblyVersion("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 new file mode 100644 index 000000000..e5a85f16f --- /dev/null +++ b/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in @@ -0,0 +1,38 @@ +using System; +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; +using System.Security.Permissions; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("Z3 .NET Interface")] +[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("Microsoft Corporation")] +[assembly: AssemblyProduct("Z3")] +[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("4.2.0.0")] +[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] +[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] diff --git a/src/api/dotnet/Readme.NET35 b/src/api/dotnet/dotnet35/Readme.NET35 similarity index 87% rename from src/api/dotnet/Readme.NET35 rename to src/api/dotnet/dotnet35/Readme.NET35 index 73743fd15..f8c2958ee 100644 --- a/src/api/dotnet/Readme.NET35 +++ b/src/api/dotnet/dotnet35/Readme.NET35 @@ -6,4 +6,5 @@ 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" +- 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 new file mode 100644 index 000000000..daa06aed7 --- /dev/null +++ b/src/api/dotnet/dotnet35/packages.config @@ -0,0 +1,4 @@ + + + + \ No newline at end of file