diff --git a/Microsoft.Z3/Log.cs b/Microsoft.Z3/Log.cs index 9058f73f5..f8b2ea88b 100644 --- a/Microsoft.Z3/Log.cs +++ b/Microsoft.Z3/Log.cs @@ -22,58 +22,58 @@ using System.Diagnostics.Contracts; namespace Microsoft.Z3 { - /// - /// Interaction logging for Z3. - /// - /// - /// Note that this is a global, static log and if multiple Context - /// objects are created, it logs the interaction with all of them. - /// + /// + /// Interaction logging for Z3. + /// + /// + /// Note that this is a global, static log and if multiple Context + /// objects are created, it logs the interaction with all of them. + /// [ContractVerification(true)] public static class Log - { - private static bool m_is_open = false; - - /// - /// Open an interaction log file. - /// - /// the name of the file to open - /// True if opening the log file succeeds, false otherwise. - public static bool Open(string filename) { - m_is_open = true; - return Native.Z3_open_log(filename) == 1; - } + private static bool m_is_open = false; - /// - /// Closes the interaction log. - /// - public static void Close() - { - m_is_open = false; - Native.Z3_close_log(); - } + /// + /// Open an interaction log file. + /// + /// the name of the file to open + /// True if opening the log file succeeds, false otherwise. + public static bool Open(string filename) + { + m_is_open = true; + return Native.Z3_open_log(filename) == 1; + } - /// - /// Appends the user-provided string to the interaction log. - /// - public static void Append(string s) - { - Contract.Requires(isOpen()); + /// + /// Closes the interaction log. + /// + public static void Close() + { + m_is_open = false; + Native.Z3_close_log(); + } - if (!m_is_open) - throw new Z3Exception("Log cannot be closed."); - Native.Z3_append_log(s); - } + /// + /// Appends the user-provided string to the interaction log. + /// + public static void Append(string s) + { + Contract.Requires(isOpen()); - /// - /// Checks whether the interaction log is opened. - /// - /// True if the interaction log is open, false otherwise. + if (!m_is_open) + throw new Z3Exception("Log cannot be closed."); + Native.Z3_append_log(s); + } + + /// + /// Checks whether the interaction log is opened. + /// + /// True if the interaction log is open, false otherwise. [Pure] public static bool isOpen() - { - return m_is_open; + { + return m_is_open; + } } - } } diff --git a/Microsoft.Z3/Microsoft.Z3.csproj b/Microsoft.Z3/Microsoft.Z3.csproj index 9ca28df75..62ec169b0 100644 --- a/Microsoft.Z3/Microsoft.Z3.csproj +++ b/Microsoft.Z3/Microsoft.Z3.csproj @@ -208,10 +208,11 @@ true - true + false - z3.snk + + false @@ -293,9 +294,6 @@ - - - diff --git a/Microsoft.Z3/Solver.cs b/Microsoft.Z3/Solver.cs index 2403108c1..6450a8cbc 100644 --- a/Microsoft.Z3/Solver.cs +++ b/Microsoft.Z3/Solver.cs @@ -33,10 +33,12 @@ namespace Microsoft.Z3 /// public string Help { - get { + get + { Contract.Ensures(Contract.Result() != null); - return Native.Z3_solver_get_help(Context.nCtx, NativeObject); } + return Native.Z3_solver_get_help(Context.nCtx, NativeObject); + } } /// @@ -56,13 +58,13 @@ namespace Microsoft.Z3 /// /// Retrieves parameter descriptions for solver. /// - ParamDescrs ParameterDescriptions - { - get - { - return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); - } - } + public ParamDescrs ParameterDescriptions + { + get + { + return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); + } + } /// @@ -250,10 +252,12 @@ namespace Microsoft.Z3 /// public Statistics Statistics { - get { + get + { Contract.Ensures(Contract.Result() != null); - return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject)); } + return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject)); + } } /// @@ -282,7 +286,7 @@ namespace Microsoft.Z3 { Native.Z3_solver_dec_ref(ctx.nCtx, obj); } - }; + }; internal override void IncRef(IntPtr o) { diff --git a/Microsoft.Z3/z3.snk b/Microsoft.Z3/z3.snk deleted file mode 100644 index 1c1ac8713..000000000 Binary files a/Microsoft.Z3/z3.snk and /dev/null differ diff --git a/Microsoft.Z3V3/AssemblyInfo.cpp b/Microsoft.Z3V3/AssemblyInfo.cpp index 54bea937e..86a8775e6 100644 --- a/Microsoft.Z3V3/AssemblyInfo.cpp +++ b/Microsoft.Z3V3/AssemblyInfo.cpp @@ -25,10 +25,10 @@ using namespace System::Security::Permissions; [assembly:AssemblyVersionAttribute("4.2.0.0")]; [assembly:AssemblyFileVersionAttribute("4.2.0.0")]; -#ifdef DELAYSIGN -[assembly:AssemblyKeyFile("35MSSharedLib1024.snk")]; -[assembly:AssemblyDelaySign(true)]; -#else -[assembly:AssemblyKeyFile("z3.snk")]; -[assembly:AssemblyDelaySign(true)]; -#endif +//#ifdef DELAYSIGN +//[assembly:AssemblyKeyFile("35MSSharedLib1024.snk")]; +//[assembly:AssemblyDelaySign(true)]; +//#else +//[assembly:AssemblyKeyFile("z3.snk")]; +//[assembly:AssemblyDelaySign(true)]; +//#endif diff --git a/Microsoft.Z3V3/Microsoft.Z3V3.vcxproj b/Microsoft.Z3V3/Microsoft.Z3V3.vcxproj index ac99eef86..506e0e17d 100644 --- a/Microsoft.Z3V3/Microsoft.Z3V3.vcxproj +++ b/Microsoft.Z3V3/Microsoft.Z3V3.vcxproj @@ -259,7 +259,8 @@ MachineX86 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -282,7 +283,8 @@ MachineX64 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -306,7 +308,8 @@ MachineX86 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -330,7 +333,8 @@ MachineX64 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -354,7 +358,8 @@ MachineX86 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -377,7 +382,8 @@ MachineX64 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -401,7 +407,8 @@ MachineX86 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -426,7 +433,8 @@ true - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -450,7 +458,8 @@ MachineX86 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)35MSSharedLib1024.snk" + + @@ -475,7 +484,8 @@ true - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + @@ -499,14 +509,16 @@ MachineX64 - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)35MSSharedLib1024.snk" + + - sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk" + + diff --git a/Microsoft.Z3V3/z3.snk b/Microsoft.Z3V3/z3.snk deleted file mode 100644 index 1c1ac8713..000000000 Binary files a/Microsoft.Z3V3/z3.snk and /dev/null differ diff --git a/z3-prover.sln b/z3-prover.sln index 7823930ae..1b016a5e9 100644 --- a/z3-prover.sln +++ b/z3-prover.sln @@ -276,6 +276,7 @@ Global {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|Mixed Platforms.ActiveCfg = external|Win32 {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|Mixed Platforms.Build.0 = external|Win32 {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|Win32.ActiveCfg = Release|Win32 + {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|Win32.Build.0 = Release|Win32 {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|x64.ActiveCfg = external|x64 {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|x64.Build.0 = external|x64 {9E76526D-EDA2-4B88-9616-A8FC08F31071}.external|x86.ActiveCfg = Release|Win32 @@ -326,6 +327,7 @@ Global {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|Mixed Platforms.ActiveCfg = external|Win32 {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|Mixed Platforms.Build.0 = external|Win32 {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|Win32.ActiveCfg = external|Win32 + {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|Win32.Build.0 = external|Win32 {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|x64.ActiveCfg = external|x64 {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|x64.Build.0 = external|x64 {0BF8CB94-61C7-4545-AE55-C58D858AA8B6}.external|x86.ActiveCfg = external|x64 @@ -374,6 +376,7 @@ Global {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|Mixed Platforms.ActiveCfg = external|Win32 {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|Mixed Platforms.Build.0 = external|Win32 {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|Win32.ActiveCfg = external|Win32 + {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|Win32.Build.0 = external|Win32 {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|x64.ActiveCfg = external|x64 {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|x64.Build.0 = external|x64 {F008F2C4-D652-4A58-8DEF-DB83E2355454}.external|x86.ActiveCfg = external|x64 @@ -422,6 +425,7 @@ Global {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|Mixed Platforms.ActiveCfg = external|Win32 {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|Mixed Platforms.Build.0 = external|Win32 {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|Win32.ActiveCfg = external|Win32 + {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|Win32.Build.0 = external|Win32 {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|x64.ActiveCfg = external|x64 {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|x64.Build.0 = external|x64 {7C154132-AAAB-4F60-B652-F8C51A63D244}.external|x86.ActiveCfg = external|x64 @@ -469,7 +473,8 @@ Global {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Any CPU.ActiveCfg = external|Any CPU {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Mixed Platforms.ActiveCfg = external|Any CPU {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Mixed Platforms.Build.0 = external|Any CPU - {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Win32.ActiveCfg = external|x64 + {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Win32.ActiveCfg = external|Any CPU + {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|Win32.Build.0 = external|Any CPU {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|x64.ActiveCfg = external|x64 {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|x64.Build.0 = external|x64 {EC3DB697-B734-42F7-9468-5B62821EEB5A}.external|x86.ActiveCfg = external|x64 @@ -517,7 +522,8 @@ Global {D350BC78-8455-45D3-9759-073394378BF2}.external|Any CPU.ActiveCfg = Release|x64 {D350BC78-8455-45D3-9759-073394378BF2}.external|Mixed Platforms.ActiveCfg = Release|x86 {D350BC78-8455-45D3-9759-073394378BF2}.external|Mixed Platforms.Build.0 = Release|x86 - {D350BC78-8455-45D3-9759-073394378BF2}.external|Win32.ActiveCfg = Release|x64 + {D350BC78-8455-45D3-9759-073394378BF2}.external|Win32.ActiveCfg = Release|Any CPU + {D350BC78-8455-45D3-9759-073394378BF2}.external|Win32.Build.0 = Release|Any CPU {D350BC78-8455-45D3-9759-073394378BF2}.external|x64.ActiveCfg = Release|x64 {D350BC78-8455-45D3-9759-073394378BF2}.external|x64.Build.0 = Release|x64 {D350BC78-8455-45D3-9759-073394378BF2}.external|x86.ActiveCfg = Release|x64