diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-08-19 11:20:18 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-08-19 11:20:18 +0100 |
| commit | 133dac43b2d0daa022bfe26ab15bcdfaf75eae0e (patch) | |
| tree | 82705cc27b6d5d0c06212d7a006a9a30bcfe9ff0 /Source/Graph | |
| parent | 819c1f07fe1e0244e14306ad1dee213a9a034f1e (diff) | |
new option for reversing the topological order - this could potentially help to speedup houdini refutation of candidates
Diffstat (limited to 'Source/Graph')
| -rw-r--r-- | Source/Graph/Graph.cs | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index b6fe8cfc..4a78c27f 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -522,14 +522,14 @@ namespace Microsoft.Boogie.GraphUtil { return dominees == null ? new List<Node>() : dominees;
}
- public IEnumerable<Node/*?*/> TopologicalSort() {
+ public IEnumerable<Node/*?*/> TopologicalSort(bool reversed = false) {
bool acyclic;
List<Node> sortedList;
- this.TarjanTopSort(out acyclic, out sortedList);
+ this.TarjanTopSort(out acyclic, out sortedList, reversed);
return acyclic ? sortedList : new List<Node>();
}
// From Tarjan 1972
- public void TarjanTopSort(out bool acyclic, out List<Node> sortedNodes) {
+ public void TarjanTopSort(out bool acyclic, out List<Node> sortedNodes, bool reversed = false) {
int n = this.Nodes.Count;
if (n == 0) {
acyclic = true;
@@ -558,10 +558,19 @@ namespace Microsoft.Boogie.GraphUtil { while (sortedIndex < n) {
// find a root (i.e., its index)
int rootIndex = -1;
- for (int i = 0; i < n; i++) {
- if (incomingEdges[i] == 0) {
- rootIndex = i;
- break;
+ if (reversed) {
+ for (int i = n-1; i >= 0; i--) {
+ if (incomingEdges[i] == 0) {
+ rootIndex = i;
+ break;
+ }
+ }
+ } else {
+ for (int i = 0; i < n; i++) {
+ if (incomingEdges[i] == 0) {
+ rootIndex = i;
+ break;
+ }
}
}
if (rootIndex == -1) {
|