diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 12 |
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 {
|