/stratifiedInline:n eagerly inlines n times before calling the stratified inlining algorithm.

3 files changed, 15 insertions, 7 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc
index e95b439e..74ad7b8e 100644
--- a/Source/BoogieDriver/BoogieDriver.ssc
+++ b/Source/BoogieDriver/BoogieDriver.ssc
@@ -440,7 +440,8 @@ namespace Microsoft.Boogie
             inline = true;

           }

         }

-        if (inline && CommandLineOptions.Clo.LazyInlining == 0) {

+        if (inline && CommandLineOptions.Clo.LazyInlining == 0 &&

+            CommandLineOptions.Clo.StratifiedInlining == 0) {

           foreach (Declaration d in TopLevelDeclarations) {

             Implementation impl = d as Implementation;

             if (impl != null) {

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index ff901532..6a0c274a 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -987,7 +987,8 @@ namespace Microsoft.Boogie
                   StratifiedInlining = 1;  

                   break;

                 default:

-                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                  StratifiedInlining = Int32.Parse((!)args[ps.i]);

+                  //ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

                   break;

               }

             }

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index 967d02c4..b80fc88f 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -1680,9 +1680,8 @@ namespace VC
        int expansionCount = 0;

        int total_axioms_pushed = 0;

        

-       /*

        // Do eager inlining

-       while(calls.currCandidates.Count != 0) 

+       for(int i = 1; i < CommandLineOptions.Clo.StratifiedInlining && calls.currCandidates.Count > 0; i ++) 

        {

           List<int>! toExpand = new List<int>();

           foreach(int id in calls.currCandidates) {

@@ -1692,7 +1691,6 @@ namespace VC
           total_axioms_pushed +=

             DoExpansion(toExpand, calls, checker);

        }

-       */

        

        int cnt = 0;

        while(cnt < 500) {

@@ -1792,6 +1790,7 @@ namespace VC
       throws UnexpectedProverOutputException;

     {       

        int old_axioms_pushed = checker.TheoremProver.NumAxiomsPushed();

+       VCExpr! exprToPush = VCExpressionGenerator.True;

 	   foreach(int id in candidates) {

 	      VCExprNAry! expr = calls.id2Candidate[id];

 		  string procName = ((!)(expr.Op as VCExprBoogieFunctionOp)).Func.Name;

@@ -1839,9 +1838,12 @@ namespace VC
 		  expansion = calls.Mutate(expansion, true);

 		  

 		  expansion = checker.VCExprGen.Eq(expr, expansion);

-		  checker.TheoremProver.PushVCExpression(expansion);

+		  exprToPush = checker.VCExprGen.And(exprToPush, expansion);

+		  //checker.TheoremProver.PushVCExpression(expansion);

 		  

 	    }

+	    checker.TheoremProver.PushVCExpression(exprToPush);

+	    

 	    int axioms_pushed = checker.TheoremProver.NumAxiomsPushed() - old_axioms_pushed;

 	    checker.TheoremProver.FlushAxiomsToTheoremProver();

 	    return axioms_pushed;

@@ -1878,9 +1880,13 @@ namespace VC
        checker.TheoremProver.FlushAxiomsToTheoremProver();

        checker.BeginCheck(implName, vc, reporter);

        checker.ProverDone.WaitOne();

-

+       

        ProverInterface.Outcome outcome = (checker).ReadOutcome();

        

+       //checker.BeginCheck(implName, vc, reporter);

+       //checker.ProverDone.WaitOne();

+       //outcome = (checker).ReadOutcome();

+       

        switch (outcome) {

          case ProverInterface.Outcome.Valid:

             return Outcome.Correct;