diff options
| author |  qadeer <unknown> | 2010-08-27 07:12:52 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-08-27 07:12:52 +0000 |
| commit | 6753de3481faf192825a3f01c6004b2712e0aab2 (patch) | |
| tree | c5559e7023d2586b993f00f375c376c879fc5740 /Source/Provers | |
| parent | 472add0311262812bcae6902b8d5d25316f91f77 (diff) | |
added some more apis to Z3api
also added a reference from BoogieDriver to z3api
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 27 | ||||
| -rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 7 |
2 files changed, 30 insertions, 4 deletions
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)
|