added a new api to Z3apiProcessTheoremProver for asserting axioms

2 files changed, 17 insertions, 14 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index e5c52add..96d68bec 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -136,10 +136,6 @@
       <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 940f4ce6..c5e53cea 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -48,7 +48,7 @@ namespace Microsoft.Boogie.Z3
         public override void Close()

         {

             base.Close();

-            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

+            Z3SafeContext cm = context.cm;

             cm.z3.Dispose();

             cm.config.Config.Dispose();

             cm.CloseLog();

@@ -56,7 +56,7 @@ namespace Microsoft.Boogie.Z3
 

         public void PushAxiom(VCExpr axiom)

         {

-            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

+            Z3SafeContext cm = context.cm;

             cm.CreateBacktrackPoint();

             LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

             cm.AddAxiom(axiom, linOptions);

@@ -65,7 +65,7 @@ namespace Microsoft.Boogie.Z3
 

         private void PushConjecture(VCExpr conjecture)

         {

-            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

+            Z3SafeContext cm = context.cm;

             cm.CreateBacktrackPoint();

             LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

             cm.AddConjecture(conjecture, linOptions);

@@ -79,16 +79,16 @@ namespace Microsoft.Boogie.Z3
 

         public void CreateBacktrackPoint()

         {

-            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

+            Z3SafeContext cm = 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>());

-            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

+            Z3SafeContext cm = context.cm;

             Push();

-            cm.AddAxiom(((Z3apiProverContext)context).Axioms, linOptions);

+            cm.AddAxiom(context.Axioms, linOptions);

             cm.AddConjecture(vc, linOptions);

             outcome = cm.Check(out z3LabelModels);

             Pop();

@@ -96,32 +96,39 @@ namespace Microsoft.Boogie.Z3
   

         public void Check()

         {

-            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

+            Z3SafeContext cm = context.cm;

             outcome = cm.Check(out z3LabelModels);

         }

 

         public void Push()

         {

-            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

+            Z3SafeContext cm = context.cm;

             cm.CreateBacktrackPoint();

         }

 

         public override void Pop()

         {

-            Z3SafeContext cm = ((Z3apiProverContext)context).cm;

+            Z3SafeContext cm = 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;

+            Z3SafeContext cm = context.cm;

             if (polarity)

                 cm.AddAxiom(vc, linOptions);

             else

                 cm.AddConjecture(vc, linOptions);

         }

 

+        public void AssertAxioms()

+        {

+            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

+            Z3SafeContext cm = context.cm;

+            cm.AddAxiom(context.Axioms, linOptions);

+        }

+

         // Number of axioms pushed since the last call to FlushAxioms

         public override int NumAxiomsPushed()

         {