new option for reversing the topological order - this could potential…

…ly help to speedup houdini refutation of candidates

Source/Core/CommandLineOptions.cs

@@ -399,6 +399,7 @@ public enum InstrumentationPlaces {
  public bool ExplainHoudini = false;
  public bool HoudiniOutputRefutedCandidates = false;
  public bool DisableLoopInvMaintainedAssert = false;
+ public bool ReverseTopologicalSorting = false;
  public bool DebugParallelHoudini = false;
  public bool HoudiniUseCrossDependencies = false;
  public string StagedHoudini = null;
@@ -1180,6 +1181,12 @@ public class AiFlags {
  }
  return true;
 
+ case "reverseTopologicalSorting":
+ if (ps.ConfirmArgumentCount(0)) {
+ ReverseTopologicalSorting = true;
+ }
+ return true;
+
  case "debugParallelHoudini":
  if (ps.ConfirmArgumentCount(0)) {
  DebugParallelHoudini = true;
@@ -1677,7 +1684,10 @@ loop headers (default)
  Outputs the refuted candidates
  /disableLoopInvMaintainedAssert
  Disables the loop invariant check to maintain the invariant after iteration.
- This is an under-approximation feature.
+ This is an under-approximation feature
+ /reverseTopologicalSorting
+ Reverses the order that roots are found in the Topological Sorting algorithm.
+ Can be used to potentially change the order that Houdini refutes candidates
 
  ---- Debugging and general tracing options ---------------------------------
 

Source/Core/DeadVarElim.cs

@@ -372,7 +372,12 @@ public class LiveVariableAnalysis {
  }
  }
 
- IEnumerable<Block> sortedNodes = dag.TopologicalSort();
+ IEnumerable<Block> sortedNodes;
+ if (CommandLineOptions.Clo.ReverseTopologicalSorting) {
+ sortedNodes = dag.TopologicalSort(true);
+ } else {
+ sortedNodes = dag.TopologicalSort();
+ }
  foreach (Block/*!*/ block in sortedNodes) {
  Contract.Assert(block != null);
  HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();

Source/Graph/Graph.cs

@@ -522,14 +522,14 @@ private class PreHeader {
  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 @@ private class PreHeader {
  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) {

Source/Houdini/Houdini.cs

@@ -822,7 +822,11 @@ private HashSet<RefutedAnnotation> ExchangeRefutedAnnotations(HashSet<RefutedAnn
  }
  }
 
+ int start = Environment.TickCount;
  refutedAnnotations = ExchangeRefutedAnnotations(refutedAnnotations);
+ int duration = Environment.TickCount - start;
+ if (CommandLineOptions.Clo.DebugParallelHoudini)
+ Console.WriteLine("*** Exchange of Refuted Candidates: " + duration + " ms ***");
 
  foreach (RefutedAnnotation refAnnot in refutedAnnotations) {
  AddRelatedToWorkList(refAnnot);

Source/VCGeneration/ConditionGeneration.cs

@@ -1342,7 +1342,14 @@ public class CounterexampleCollector : VerifierCallback {
  }
  }
  }
- IEnumerable sortedNodes = dag.TopologicalSort();
+
+ IEnumerable sortedNodes;
+ if (CommandLineOptions.Clo.ReverseTopologicalSorting) {
+ sortedNodes = dag.TopologicalSort(true);
+ } else {
+ sortedNodes = dag.TopologicalSort();
+ }
+
  Contract.Assert(sortedNodes != null);
  #endregion
 

Util/PortfolioSolver.py

@@ -64,7 +64,7 @@ class VerificationTask(multiprocessing.Process):
 
  isTrusted = True
 
- def __init__(self, taskID, queue, solver, errorLimit, checkForLMI, loopUnwind, timeout=0, timeoutErrorCode=None):
+ def __init__(self, taskID, queue, solver, errorLimit, checkForLMI, reverseTopSort, loopUnwind, timeout=0, timeoutErrorCode=None):
  super(VerificationTask, self).__init__()
  self.taskID = taskID
  self.queue = queue
@@ -84,6 +84,8 @@ def __init__(self, taskID, queue, solver, errorLimit, checkForLMI, loopUnwind, t
  if not checkForLMI:
  self.options += [ "/disableLoopInvMaintainedAssert" ]
  self.isTrusted = False
+ if reverseTopSort:
+ self.options += [ "/reverseTopologicalSorting" ]
  if (loopUnwind > 0):
  self.options += ["/loopUnroll:" + str(loopUnwind) ]
 
@@ -323,13 +325,13 @@ def main(argv=None):
 
  for taskID in range(CommandLineOptions.workers):
  if (taskID == 0):
- task = VerificationTask(taskID + 1, taskQueue, "Z3", 1, True, 0, **timeoutArguments)
+ task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, True, False, 0, **timeoutArguments)
  elif (taskID == 1):
- task = VerificationTask(taskID + 1, taskQueue, "Z3", 2, True, 0, **timeoutArguments)
+ task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, False, False, 0, **timeoutArguments)
  elif (taskID == 2):
- task = VerificationTask(taskID + 1, taskQueue, "Z3", 3, True, 0, **timeoutArguments)
+ task = VerificationTask(taskID + 1, taskQueue, "Z3", 3, True, False, 0, **timeoutArguments)
  elif (taskID == 3):
- task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, True, 0, **timeoutArguments)
+ task = VerificationTask(taskID + 1, taskQueue, "Z3", 4, True, False, 0, **timeoutArguments)
  task.start()
  toolTasks.append(task)