Avoid restarting the theorem prover for stratified inlining because it

can lose context.
Added a cache for FindLeastToVerify

4 files changed, 69 insertions, 2 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index dcc007fe..88d8bdaa 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -512,6 +512,12 @@ namespace Microsoft.Boogie {
                   }

                   outcome = svcgen.FindLeastToVerify(impl, program, ref ss);

                   errors = new List<Counterexample>();

+                  Console.Write("Result: ");

+                  foreach (var s in ss)

+                  {

+                      Console.Write("{0} ", s);

+                  }

+                  Console.WriteLine();

               }

               else

               {

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index d2a7de58..8f2d0c68 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1530,6 +1530,7 @@ namespace Microsoft.Boogie {
         TypeEncodingMethod = TypeEncoding.Monomorphic;

         UseArrayTheory = true;

         UseAbstractInterpretation = false;

+        MaxProverMemory = 0; // no max: avoids restarts

         if (ProverName == "Z3API")

         {

             ProverCCLimit = 1;

diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 68c02c5d..95d8950a 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -511,7 +511,13 @@ namespace Microsoft.Boogie.Simplify {
           thmProver = null;

           currentProverHasBeenABadBoy = false;

           restarts++;

+

+          if (CommandLineOptions.Clo.StratifiedInlining > 0)

+          {

+              Console.WriteLine("Warning: restarting theorem prover. Context could be lost");

+          }

         }

+          

         FireUpNewProver();

       }

       cce.EndExpose();

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 0b76387d..4b22b1cc 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -897,6 +897,13 @@ namespace VC
             // Record current time

             var startTime = DateTime.Now;

 

+            // No Max: avoids theorem prover restarts

+            CommandLineOptions.Clo.MaxProverMemory = 0;

+

+            // Initialize cache

+            satQueryCache = new Dictionary<int, List<HashSet<string>>>();

+            unsatQueryCache = new Dictionary<int, List<HashSet<string>>>();

+

             // Get the checker

             Checker checker = FindCheckerFor(impl, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null);

 

@@ -930,7 +937,8 @@ namespace VC
                 var constant = decl as Constant;

                 if (constant == null) continue;

                 if (!allBoolVars.Contains(constant.Name)) continue;

-                allConsts.Add(checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(constant));

+                var v = checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(constant);

+                allConsts.Add(v);

             }

 

             // Now, lets start the algo

@@ -985,11 +993,31 @@ namespace VC
             return refinementLoop(apiChecker, a, c, allVars);

         }

 

+        Dictionary<int, List<HashSet<string>>> satQueryCache;

+        Dictionary<int, List<HashSet<string>>> unsatQueryCache;

+

         private bool refinementLoopCheckPath(StratifiedCheckerInterface apiChecker, HashSet<VCExprVar> varsToSet, HashSet<VCExprVar> allVars)

         {

             var assumptions = new List<VCExpr>();

             List<int> temp = null;

 

+            var query = new HashSet<string>();

+            varsToSet.Iter(v => query.Add(v.Name));

+

+            if (checkCache(query, unsatQueryCache))

+            {

+                apiChecker.LogComment("FindLeast: Query Cache Hit");

+                return true;

+            }

+            if (checkCache(query, satQueryCache))

+            {

+                apiChecker.LogComment("FindLeast: Query Cache Hit");

+                return false;

+            }

+

+

+            apiChecker.LogComment("FindLeast: Query Begin");

+

             //Console.Write("Query: ");

             foreach (var c in allVars)

             {

@@ -1008,11 +1036,37 @@ namespace VC
             var o = apiChecker.CheckAssumptions(assumptions, out temp);

             Debug.Assert(o == Outcome.Correct || o == Outcome.Errors);

             //Console.WriteLine("Result = " + o.ToString());

+            apiChecker.LogComment("FindLeast: Query End");

+

+            if (o == Outcome.Correct)

+            {

+                insertCache(query, unsatQueryCache);

+                return true;

+            }

 

-            if (o == Outcome.Correct) return true;

+            insertCache(query, satQueryCache);

             return false;

         }

 

+        private bool checkCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache)

+        {

+            if (!cache.ContainsKey(q.Count)) return false;

+            foreach (var s in cache[q.Count])

+            {

+                if (q.SetEquals(s)) return true;

+            }

+            return false;

+        }

+

+        private void insertCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache)

+        {

+            if (!cache.ContainsKey(q.Count))

+            {

+                cache.Add(q.Count, new List<HashSet<string>>());

+            }

+            cache[q.Count].Add(q);

+        }

+

         public static void Partition<T>(HashSet<T> values, out HashSet<T> part1, out HashSet<T> part2)

         {

             part1 = new HashSet<T>();