diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.csproj | 6 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 27 | ||||
| -rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 7 |
3 files changed, 35 insertions, 5 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index 5b08ba0d..a238ea24 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -3,7 +3,7 @@ <PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.30729</ProductVersion>
+ <ProductVersion>9.0.21022</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</ProjectGuid>
<OutputType>Exe</OutputType>
@@ -122,6 +122,10 @@ <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>
<Name>SMTLib</Name>
</ProjectReference>
+ <ProjectReference Include="..\Provers\Z3api\Z3api.csproj">
+ <Project>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</Project>
+ <Name>Z3api</Name>
+ </ProjectReference>
<ProjectReference Include="..\Provers\Z3\Z3.csproj">
<Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>
<Name>Z3</Name>
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index 0803098d..b270674d 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -72,12 +72,18 @@ namespace Microsoft.Boogie.Z3 cm.AddConjecture(conjecture, linOptions);
}
- public override void PushVCExpression(VCExpr vc)
+ public void PushVCExpression(VCExpr vc)
{
PushAxiom(vc);
numAxiomsPushed++;
}
+ public void CreateBacktrackPoint()
+ {
+ Z3SafeContext cm = ((Z3apiProverContext)context).cm;
+ cm.CreateBacktrackPoint();
+ }
+
public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
@@ -85,19 +91,34 @@ namespace Microsoft.Boogie.Z3 cm.AddConjecture(vc, linOptions);
outcome = cm.Check(out z3LabelModels);
}
+
+ public void Check()
+ {
+ outcome = cm.Check(out z3LabelModels);
+ }
- public void CreateBacktrackPoint()
+ public void Push()
{
Z3SafeContext cm = ((Z3apiProverContext)context).cm;
cm.CreateBacktrackPoint();
}
- override public void Pop()
+ public void Pop()
{
Z3SafeContext cm = ((Z3apiProverContext)context).cm;
cm.Backtrack();
}
+ public void Assert(VCExpr vc, bool polarity)
+ {
+ LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
+ Z3SafeContext cm = ((Z3apiProverContext)context).cm;
+ if (polarity)
+ cm.AddAxiom(vc, linOptions);
+ else
+ cm.AddConjecture(vc, linOptions);
+ }
+
// Number of axioms pushed since the last call to FlushAxioms
public override int NumAxiomsPushed()
{
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index 67cff382..d6dc404c 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -109,6 +109,10 @@ namespace Microsoft.Boogie.Z3 this.tm = new Z3TypeCachedBuilder(this);
this.gen = gen;
this.namer = new UniqueNamer();
+ if (CommandLineOptions.Clo.SimplifyLogFilePath != null)
+ {
+ z3.TraceToFile(CommandLineOptions.Clo.SimplifyLogFilePath);
+ }
}
public void CreateBacktrackPoint()
@@ -342,6 +346,7 @@ namespace Microsoft.Boogie.Z3 {
boogieErrors = new List<Z3ErrorModelAndLabels>();
LBool outcome = LBool.Undef;
+ z3.Push();
while (boogieErrors.Count < this.config.Counterexamples)
{
Model z3Model;
@@ -363,7 +368,7 @@ namespace Microsoft.Boogie.Z3 else
break;
}
-
+ z3.Pop();
if (boogieErrors.Count > 0)
return ProverInterface.Outcome.Invalid;
else if (outcome == LBool.False)
|