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

1 files changed, 19 insertions, 18 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();

     }