added some more apis to Z3api

also added a reference from BoogieDriver to z3api

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)