Introduce ApiProverInterface.CheckOutcomeCore() for stratified inlining; simplify push/pop handling

3 files changed, 24 insertions, 22 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 92b00fe1..9bb605b7 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -93,7 +93,6 @@ namespace Microsoft.Boogie.SMTLib
           PrepareCommon();

       }

       prevOutcomeAvailable = false;

-      pendingPop = false;

     }

 

     void SetupProcess()

@@ -382,6 +381,23 @@ namespace Microsoft.Boogie.SMTLib
 

     [NoDefaultContract]

     public override Outcome CheckOutcome(ErrorHandler handler)

+    {

+      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+

+      var result = Outcome.Undetermined;

+

+      if (Process == null)

+        return result;

+

+      result = CheckOutcomeCore(handler);

+      SendThisVC("(pop 1)");

+      FlushLogFile();

+

+      return result;

+    }

+

+    [NoDefaultContract]

+    public override Outcome CheckOutcomeCore(ErrorHandler handler)

     {  

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       

@@ -443,16 +459,6 @@ namespace Microsoft.Boogie.SMTLib
           }

         }

 

-        if (CommandLineOptions.Clo.StratifiedInlining == 0)

-        {

-            SendThisVC("(pop 1)");

-        }

-        else if (CommandLineOptions.Clo.StratifiedInlining > 0 && pendingPop)

-        {

-            pendingPop = false;

-            SendThisVC("(pop 1)");

-        }

-

         FlushLogFile();

 

         if (CommandLineOptions.Clo.RestartProverPerVC && Process != null)

@@ -785,7 +791,7 @@ namespace Microsoft.Boogie.SMTLib
 

     public override void Check()

     {

-        Contract.Assert(pendingPop == false && prevOutcomeAvailable == false);

+        Contract.Assert(prevOutcomeAvailable == false);

 

         PrepareCommon();

         SendThisVC("(check-sat)");

@@ -801,15 +807,13 @@ namespace Microsoft.Boogie.SMTLib
     /// Extra state for ApiChecker (used by stratifiedInlining)

     /// </summary>

     bool prevOutcomeAvailable;

-    bool pendingPop;

     Outcome prevOutcome;

     static int nameCounter = 0;

 

     public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)

     {

-        Contract.Assert(pendingPop == false && prevOutcomeAvailable == false);

+        Contract.Assert(prevOutcomeAvailable == false);

 

-        Push();

         unsatCore = new List<int>();

 

         // Name the assumptions

@@ -830,7 +834,6 @@ namespace Microsoft.Boogie.SMTLib
         prevOutcomeAvailable = true;

         if (prevOutcome != Outcome.Valid)

         {

-            pendingPop = true;

             return;

         }

         Contract.Assert(usingUnsatCore, "SMTLib prover not setup for computing unsat cores");

@@ -840,8 +843,6 @@ namespace Microsoft.Boogie.SMTLib
         if(resp.Name != "") unsatCore.Add(nameToAssumption[resp.Name]);

         foreach (var s in resp.Arguments) unsatCore.Add(nameToAssumption[s.Name]);

 

-        Pop();

-

         FlushLogFile();

     }

 

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 5176d494..f0e6b384 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -848,6 +848,7 @@ namespace Microsoft.Boogie {
       public abstract void AssertAxioms();

       public abstract void Check();

       public abstract void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore);

+      public abstract Outcome CheckOutcomeCore(ErrorHandler handler);

       public abstract void Push();

       public virtual void SetTimeOut(int ms) { }

   }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index ad11152a..1ba5a26d 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1209,7 +1209,7 @@ namespace VC
 

             TheoremProver.AssertAxioms();

             TheoremProver.Check();

-            ProverInterface.Outcome outcome = TheoremProver.CheckOutcome(reporter);

+            ProverInterface.Outcome outcome = TheoremProver.CheckOutcomeCore(reporter);

             numQueries++;

 

             switch (outcome) {

@@ -1256,11 +1256,11 @@ namespace VC
               return CheckVC();

             }

 

-            //TheoremProver.Push();

+            TheoremProver.Push();

             TheoremProver.AssertAxioms();

             TheoremProver.CheckAssumptions(assumptions, out unsatCore);

-            ProverInterface.Outcome outcome = TheoremProver.CheckOutcome(reporter);

-            //TheoremProver.Pop();

+            ProverInterface.Outcome outcome = TheoremProver.CheckOutcomeCore(reporter);

+            TheoremProver.Pop();

             numQueries++;

 

             switch (outcome) {