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

1 files changed, 10 insertions, 2 deletions

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 {