From 6c475660d8fb6fafa40510b0703c3aafbcf79072 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 12 Oct 2012 15:12:21 +0100 Subject: [PATCH 1/2] Removed support for signed assemblies. Users are advised to build their own assemblies from the source code, which they can sign using their own private keys. Signed-off-by: Christoph M. Wintersteiger --- Microsoft.Z3/Microsoft.Z3.csproj | 8 +++--- Microsoft.Z3/z3.snk | Bin 596 -> 0 bytes Microsoft.Z3V3/AssemblyInfo.cpp | 14 +++++----- Microsoft.Z3V3/Microsoft.Z3V3.vcxproj | 36 +++++++++++++++++--------- Microsoft.Z3V3/z3.snk | Bin 596 -> 0 bytes 5 files changed, 34 insertions(+), 24 deletions(-) delete mode 100644 Microsoft.Z3/z3.snk delete mode 100644 Microsoft.Z3V3/z3.snk 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/z3.snk b/Microsoft.Z3/z3.snk deleted file mode 100644 index 1c1ac87139db582e9021fd69893f32c23450bc67..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 596 zcmV-a0;~N80ssI2Bme+XQ$aES1ONa50097ZdN^E`fV9($I`dn<1f}a+1i;_!$y;J4 zee;lDbzQFm79@J~Ur^w}{$f#z2?xqAj>XryfQ*x%kO4Cl)u^c0HB!a{bvPi?)i8iv zfIOQ{?t#eU5G(LC{DMJ7?Yfb}*D0r<0RC%R3_qZ=Dz~^8!WLVA67o=R^5!ctR?E5r zTZTnWM3seP-F7UD=c-9e^wfVQrSDO_|F(yHd1Bi}9*{u0P5bXD-4|d?GB!uf5dL6D zA@1Iy352^5cF^X1u9ob7yioyvp%rI31-q*Z{P_7~oJ*&An4NRDD-@o-``1PLAWHZ< z<@D<3OD2z@fg*XSeCl2cQN{4XIW5m=ajoGS;Zfb6lN_Ff@*0vkeA}cfGrqL%0IlIw z`)!pN!Wc?1${pgpA0^pS(kzGn1#`S=5RamF3XZsCQ0+AJ+JS&{RP$uvs?*qkWrUxo+PV zgx9qdq7iY6(QhyrK;^KOslOqAWXw=mb`m(|xeT+xFTyojbY+%->2=77E*~oQtZN>S zq9xdu!RmBGMdK0RfJ6YMBHDi%@3`wydNE*iYSuEg@V?E=f0CG iozI4Z`K&(xgd3HMachineX86 - 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 1c1ac87139db582e9021fd69893f32c23450bc67..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 596 zcmV-a0;~N80ssI2Bme+XQ$aES1ONa50097ZdN^E`fV9($I`dn<1f}a+1i;_!$y;J4 zee;lDbzQFm79@J~Ur^w}{$f#z2?xqAj>XryfQ*x%kO4Cl)u^c0HB!a{bvPi?)i8iv zfIOQ{?t#eU5G(LC{DMJ7?Yfb}*D0r<0RC%R3_qZ=Dz~^8!WLVA67o=R^5!ctR?E5r zTZTnWM3seP-F7UD=c-9e^wfVQrSDO_|F(yHd1Bi}9*{u0P5bXD-4|d?GB!uf5dL6D zA@1Iy352^5cF^X1u9ob7yioyvp%rI31-q*Z{P_7~oJ*&An4NRDD-@o-``1PLAWHZ< z<@D<3OD2z@fg*XSeCl2cQN{4XIW5m=ajoGS;Zfb6lN_Ff@*0vkeA}cfGrqL%0IlIw z`)!pN!Wc?1${pgpA0^pS(kzGn1#`S=5RamF3XZsCQ0+AJ+JS&{RP$uvs?*qkWrUxo+PV zgx9qdq7iY6(QhyrK;^KOslOqAWXw=mb`m(|xeT+xFTyojbY+%->2=77E*~oQtZN>S zq9xdu!RmBGMdK0RfJ6YMBHDi%@3`wydNE*iYSuEg@V?E=f0CG iozI4Z`K&(xgd3H Date: Fri, 12 Oct 2012 15:13:38 +0100 Subject: [PATCH 2/2] Formatting and build configuration fixes. Signed-off-by: Christoph M. Wintersteiger --- Microsoft.Z3/Log.cs | 88 +++++++++++++++++++++--------------------- Microsoft.Z3/Solver.cs | 28 ++++++++------ z3-prover.sln | 10 ++++- 3 files changed, 68 insertions(+), 58 deletions(-) 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/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/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