mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Merge branch 'working' of //z3-1/z3 into working

Browse source
This commit is contained in:
Leonardo de Moura 2012-10-12 07:48:45 -07:00
parent b0a2d8488d c11e134aae
commit 4d70722769
8 changed files with 102 additions and 82 deletions
Show stats 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;
}
}
}
}

8
Microsoft.Z3/Microsoft.Z3.csproj
View file

@ -208,10 +208,11 @@
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
</PropertyGroup>
<PropertyGroup>
<SignAssembly>true</SignAssembly>
<SignAssembly>false</SignAssembly>
</PropertyGroup>
<PropertyGroup>
<AssemblyOriginatorKeyFile>z3.snk</AssemblyOriginatorKeyFile>
<AssemblyOriginatorKeyFile>
</AssemblyOriginatorKeyFile>
</PropertyGroup>
<PropertyGroup>
<DelaySign>false</DelaySign>
@ -293,9 +294,6 @@
<ItemGroup>
<WCFMetadata Include="Service References\" />
</ItemGroup>
<ItemGroup>
<None Include="z3.snk" />
</ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<PropertyGroup>
<PostBuildEvent>

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)
{

BIN
Microsoft.Z3/z3.snk
View file

Binary file not shown.

14
Microsoft.Z3V3/AssemblyInfo.cpp
View file

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

36
Microsoft.Z3V3/Microsoft.Z3V3.vcxproj
View file

@ -259,7 +259,8 @@
<TargetMachine>MachineX86</TargetMachine>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Debug|x64'">
@ -282,7 +283,8 @@
<TargetMachine>MachineX64</TargetMachine>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">
@ -306,7 +308,8 @@
<TargetMachine>MachineX86</TargetMachine>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Release|x64'">
@ -330,7 +333,8 @@
<TargetMachine>MachineX64</TargetMachine>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Trace|Win32'">
@ -354,7 +358,8 @@
<TargetMachine>MachineX86</TargetMachine>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Trace|x64'">
@ -377,7 +382,8 @@
<TargetMachine>MachineX64</TargetMachine>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='release_mt|Win32'">
@ -401,7 +407,8 @@
<TargetMachine>MachineX86</TargetMachine>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='external|Win32'">
@ -426,7 +433,8 @@
<Profile>true</Profile>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='commercial|Win32'">
@ -450,7 +458,8 @@
<TargetMachine>MachineX86</TargetMachine>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)35MSSharedLib1024.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='external|x64'">
@ -475,7 +484,8 @@
<Profile>true</Profile>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='commercial|x64'">
@ -499,14 +509,16 @@
<TargetMachine>MachineX64</TargetMachine>
</Link>
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)35MSSharedLib1024.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'">
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='release_mt|x64'">
<PostBuildEvent>
<Command>sn.exe -Ra "$(TargetPath)" "$(ProjectDir)z3.snk"</Command>
<Command>
</Command>
</PostBuildEvent>
</ItemDefinitionGroup>
<ItemGroup>

BIN
Microsoft.Z3V3/z3.snk
View file

Binary file not shown.

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