From 6753de3481faf192825a3f01c6004b2712e0aab2 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Fri, 27 Aug 2010 07:12:52 +0000
Subject: added some more apis to Z3api also added a reference from
 BoogieDriver to z3api

---
 Source/Provers/Z3api/ProverLayer.cs | 27 ++++++++++++++++++++++++---
 Source/Provers/Z3api/SafeContext.cs |  7 ++++++-
 2 files changed, 30 insertions(+), 4 deletions(-)

(limited to 'Source/Provers')

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)
-- 
cgit v1.2.3