Boogie: Added stratified inlining. It is enabled using the flag /stratifiedInline:1.

1 files changed, 53 insertions, 3 deletions

diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc
index bd618c24..2a50adee 100644
--- a/Source/Provers/Simplify/ProverInterface.ssc
+++ b/Source/Provers/Simplify/ProverInterface.ssc
@@ -156,9 +156,11 @@ namespace Microsoft.Boogie.Simplify
 

     protected abstract AxiomVCExprTranslator! SpawnVCExprTranslator();

 

-    protected void FeedNewAxiomsDecls2Prover() throws UnexpectedProverOutputException; {

+    // Return the number of axioms pushed to the theorem prover

+    protected int FeedNewAxiomsDecls2Prover() throws UnexpectedProverOutputException; {

       if (thmProver == null)

-        return;

+        return 0;

+      int ret = 0;

       foreach (string! s in vcExprTranslator.NewTypeDecls) {

         LogCommon(s);

         thmProver.Feed(s, 0);

@@ -166,7 +168,9 @@ namespace Microsoft.Boogie.Simplify
       foreach (string! s in vcExprTranslator.NewAxioms) {

         LogBgPush(s);

         thmProver.AddAxioms(s);

+        ret ++;

       }

+      return ret;

     }

 

     protected static string! CodebaseString() {

@@ -278,6 +282,32 @@ namespace Microsoft.Boogie.Simplify
     {

       vcExprTranslator.AddAxiom( vcExprTranslator.translate(vc,1) ); 

     }

+    

+    public override string! VCExpressionToString(VCExpr! vc)

+    {

+      return vcExprTranslator.translate(vc, 1);

+    }

+    

+    // Number of axioms pushed since the last call to Check

+    public override int NumAxiomsPushed() 

+    {

+       return vcExprTranslator.NewAxiomsCount;

+    }

+    

+    // Feed the axioms pushed since the last call to Check to the theorem prover

+    public override int FlushAxiomsToTheoremProver() 

+      throws UnexpectedProverOutputException;

+    {

+       return FeedNewAxiomsDecls2Prover();

+    }

+

+    public override void Pop() 

+      throws UnexpectedProverOutputException;

+    {

+       assert thmProver != null;

+       LogCommon("(BG_POP)");

+       thmProver.PopAxioms();

+    }

 

     [NoDefaultContract]  // important, since we have no idea what state the object might be in when this handler is invoked

     void ControlCHandler(object o, ConsoleCancelEventArgs a)

@@ -316,13 +346,24 @@ namespace Microsoft.Boogie.Simplify
 

         Helpers.ExtraTraceInformation("Sending data to theorem prover");

 

-        FeedNewAxiomsDecls2Prover();

+        int num_axioms_pushed = 

+           FeedNewAxiomsDecls2Prover();

+        

         string! prelude = ctx.GetProverCommands(false);

         vcString = prelude + vcString;

         LogActivity(vcString);

 

         assert thmProver != null;

         thmProver.BeginCheck(descriptiveName, vcString);

+        

+        if(CommandLineOptions.Clo.StratifiedInlining > 0) {

+			// Pop all the axioms that were pushed by FeedNewAxiomsDecls2Prover

+			for(int i = 0; i < num_axioms_pushed; i++) 

+			{

+			   LogBgPop();

+			   thmProver.PopAxioms();

+			}

+        }

 

         if (CommandLineOptions.Clo.RestartProverPerVC) {

           LogComment("Will restart the prover due to /restartProver option");

@@ -418,6 +459,10 @@ namespace Microsoft.Boogie.Simplify
       LogCommon(")");

     }

 

+    public void LogBgPop() {

+      LogCommon("(BG_POP)");

+    }

+    

     [NoDefaultContract]

     private void FireUpNewProver()

       requires IsExposed;

@@ -525,6 +570,11 @@ namespace Microsoft.Boogie.Simplify
     public readonly List<string!>! AllAxioms;

     private List<string!>! NewAxiomsAttr;

 

+    // The length of the list NewAxiomsAttr

+    public int NewAxiomsCount { get {

+      return NewAxiomsAttr.Count;

+    } }

+

     public List<string!>! NewAxioms { get {

       List<string!>! res = NewAxiomsAttr;

       NewAxiomsAttr = new List<string!> ();