added nonUniformUnfolding option

3 files changed, 14 insertions, 14 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 5e5a896a..ed80f6ac 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -565,6 +565,7 @@ namespace Microsoft.Boogie {
     public bool StratifiedInliningWithoutModels = false; // disable model generation for SI

     public int StratifiedInliningVerbose = 0; // verbosity level

     public int RecursionBound = 500;

+    public bool NonUniformUnfolding = false;

     public string inferLeastForUnsat = null;

     public string CoverageReporterPath = null;

     public Process coverageReporter = null; // used internally for debugging

@@ -1223,7 +1224,8 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||

               ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||

               ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||

-              ps.CheckBooleanFlag("printAssignment", ref PrintAssignment)

+              ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||

+              ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding)

               ) {

             // one of the boolean flags matched

             return true;

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 9987e6f4..5667429a 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -864,9 +864,9 @@ namespace Microsoft.Boogie.SMTLib
         }

         Check();

         outcome = CheckOutcomeCore(handler);

-        Pop();

         if (outcome != Outcome.Valid)

           break;

+        Pop();

         string relaxVar = "relax_" + k;

         relaxVars.Add(relaxVar);

         SendThisVC("(declare-fun " + relaxVar + " () Int)");

@@ -882,6 +882,7 @@ namespace Microsoft.Boogie.SMTLib
       if (outcome == Outcome.Invalid) {

         foreach (var relaxVar in relaxVars) {

           SendThisVC("(get-value (" + relaxVar + "))");

+          FlushLogFile();

           var resp = Process.GetProverResponse();

           if (resp == null) break;

           if (!(resp.Name == "" && resp.ArgCount == 1)) break;

@@ -896,6 +897,7 @@ namespace Microsoft.Boogie.SMTLib
           else

             break;

         }

+        Pop();

       }

 

       Pop();

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 12be00b2..98f20d21 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1106,7 +1106,8 @@ namespace VC
             checker.TheoremProver.LogComment(str);

           }

 

-          public Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions, out List<int> unsatisfiedSoftAssumptions) {

+          public Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions) {

+            List<int> unsatisfiedSoftAssumptions;

             ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, reporter);

             switch (outcome) {

               case ProverInterface.Outcome.Valid:

@@ -1613,7 +1614,7 @@ namespace VC
             // bool underApproxNeeded = true;

 

             // The recursion bound for stratified search

-            int bound = 1;

+            int bound = CommandLineOptions.Clo.NonUniformUnfolding ? CommandLineOptions.Clo.RecursionBound : 1;

 

             int done = 0;

 

@@ -1720,13 +1721,7 @@ namespace VC
                         if (block.Count == 0)

                         {

                             // Increment bound

-                            var minRecReached = CommandLineOptions.Clo.RecursionBound + 1;

-                            foreach (var id in calls.currCandidates)

-                            {

-                                var rb = calls.getRecursionBound(id);

-                                if (bound < rb && rb < minRecReached) minRecReached = rb;

-                            }

-                            bound = minRecReached;

+                            bound++;

                             if (useSummary) summaryComputation.boundChanged();

 

                             if (bound > CommandLineOptions.Clo.RecursionBound)

@@ -2210,7 +2205,6 @@ namespace VC
             bool allTrue = true;

             bool allFalse = true;

             List<VCExpr> softAssumptions = new List<VCExpr>();

-            List<int> unsatisfiedSoftAssumptions;

 

             assumptions = new List<VCExpr>();

             procsThatReachedRecBound.Clear();

@@ -2220,7 +2214,7 @@ namespace VC
                 int idBound = calls.getRecursionBound(id);

                 if (idBound <= bound)

                 {

-                    if (idBound > 0)

+                    if (idBound > 1)

                       softAssumptions.Add(calls.getFalseExpr(id));

                     if (block.Contains(id))

                     {

@@ -2249,7 +2243,9 @@ namespace VC
             }

             else

             {

-                ret = checker.CheckAssumptions(assumptions, softAssumptions, out unsatisfiedSoftAssumptions);

+              ret = CommandLineOptions.Clo.NonUniformUnfolding

+                    ? checker.CheckAssumptions(assumptions, softAssumptions)

+                    : checker.CheckAssumptions(assumptions);

             }

 

             if (ret != Outcome.Correct && ret != Outcome.Errors)