Option for reversing Houdini worklist (for top-down analysis)

2 files changed, 12 insertions, 2 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 09549e55..a4374623 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -397,6 +397,7 @@ namespace Microsoft.Boogie {
     public bool IntraproceduralInfer = true;

     public bool ContractInfer = false;

     public bool ExplainHoudini = false;

+    public bool ReverseHoudiniWorklist = false;

     public bool ConcurrentHoudini = false;

     public bool ModifyTopologicalSorting = false;

     public bool DebugConcurrentHoudini = false;

@@ -1362,6 +1363,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||

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

               ps.CheckBooleanFlag("explainHoudini", ref ExplainHoudini) ||

+              ps.CheckBooleanFlag("reverseHoudiniWorklist", ref ReverseHoudiniWorklist) ||

               ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) ||

               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||

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

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index c3575800..e883d0bd 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -512,8 +512,9 @@ namespace Microsoft.Boogie.Houdini {
           queue.Enqueue(impl);

         }

       }

-      return queue;

-      

+      if (CommandLineOptions.Clo.ReverseHoudiniWorklist)

+          queue = queue.Reverse();

+      return queue;      

       /*

       Queue<Implementation> queue = new Queue<Implementation>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

@@ -815,6 +816,13 @@ namespace Microsoft.Boogie.Houdini {
       public bool Contains(Implementation impl) {

         return set.Contains(impl);

       }

+      public WorkQueue Reverse()

+      {

+          var ret = new WorkQueue();

+          foreach (var impl in queue.Reverse())

+              ret.Enqueue(impl);

+          return ret;

+      }

     }

 

     public class HoudiniState {