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/Z3api/ProverLayer.cs | |
| parent | 472add0311262812bcae6902b8d5d25316f91f77 (diff) | |
added some more apis to Z3api
also added a reference from BoogieDriver to z3api
Diffstat (limited to 'Source/Provers/Z3api/ProverLayer.cs')
| -rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 27 |
1 files changed, 24 insertions, 3 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()
{
|