mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Formatting and build configuration fixes.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-10-12 15:13:38 +01:00
parent 6c475660d8
commit c11e134aae
3 changed files with 68 additions and 58 deletions
Download patch file Download diff file Expand all files Collapse all files

88
Microsoft.Z3/Log.cs
View file

@ -22,58 +22,58 @@ using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Interaction logging for Z3.
/// </summary>
/// <remarks>
/// Note that this is a global, static log and if multiple Context
/// objects are created, it logs the interaction with all of them.
/// </remarks>
/// <summary>
/// Interaction logging for Z3.
/// </summary>
/// <remarks>
/// Note that this is a global, static log and if multiple Context
/// objects are created, it logs the interaction with all of them.
/// </remarks>
[ContractVerification(true)]
public static class Log
{
private static bool m_is_open = false;
/// <summary>
/// Open an interaction log file.
/// </summary>
/// <param name="filename">the name of the file to open</param>
/// <returns>True if opening the log file succeeds, false otherwise.</returns>
public static bool Open(string filename)
{
m_is_open = true;
return Native.Z3_open_log(filename) == 1;
}
private static bool m_is_open = false;
/// <summary>
/// Closes the interaction log.
/// </summary>
public static void Close()
{
m_is_open = false;
Native.Z3_close_log();
}
/// <summary>
/// Open an interaction log file.
/// </summary>
/// <param name="filename">the name of the file to open</param>
/// <returns>True if opening the log file succeeds, false otherwise.</returns>
public static bool Open(string filename)
{
m_is_open = true;
return Native.Z3_open_log(filename) == 1;
}
/// <summary>
/// Appends the user-provided string <paramref name="s"/> to the interaction log.
/// </summary>
public static void Append(string s)
{
Contract.Requires(isOpen());
/// <summary>
/// Closes the interaction log.
/// </summary>
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);
}
/// <summary>
/// Appends the user-provided string <paramref name="s"/> to the interaction log.
/// </summary>
public static void Append(string s)
{
Contract.Requires(isOpen());
/// <summary>
/// Checks whether the interaction log is opened.
/// </summary>
/// <returns>True if the interaction log is open, false otherwise.</returns>
if (!m_is_open)
throw new Z3Exception("Log cannot be closed.");
Native.Z3_append_log(s);
}
/// <summary>
/// Checks whether the interaction log is opened.
/// </summary>
/// <returns>True if the interaction log is open, false otherwise.</returns>
[Pure]
public static bool isOpen()
{
return m_is_open;
{
return m_is_open;
}
}
}
}

28
Microsoft.Z3/Solver.cs
View file

@ -33,10 +33,12 @@ namespace Microsoft.Z3
/// </summary>
public string Help
{
get {
get
{
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_solver_get_help(Context.nCtx, NativeObject); }
return Native.Z3_solver_get_help(Context.nCtx, NativeObject);
}
}
/// <summary>
@ -56,13 +58,13 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieves parameter descriptions for solver.
/// </summary>
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));
}
}
/// <summary>
@ -250,10 +252,12 @@ namespace Microsoft.Z3
/// </summary>
public Statistics Statistics
{
get {
get
{
Contract.Ensures(Contract.Result<Statistics>() != 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));
}
}
/// <summary>
@ -282,7 +286,7 @@ namespace Microsoft.Z3
{
Native.Z3_solver_dec_ref(ctx.nCtx, obj);
}
};
};
internal override void IncRef(IntPtr o)
{

10
z3-prover.sln
View file

@ -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