summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2014-01-28 21:48:33 +0530
committerGravatar akashlal <unknown>2014-01-28 21:48:33 +0530
commit37ddd0bd2f8118948a95bffedbbc8d976adaa7ce (patch)
treeb6b622d40f1d80237446b123ad47cbf0a7bb5f4a /Source
parentcd500f3653905b029cf019a8709433c90df03fe1 (diff)
Option for reversing Houdini worklist (for top-down analysis)
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/CommandLineOptions.cs2
-rw-r--r--Source/Houdini/Houdini.cs12
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 {