1 files changed, 120 insertions, 0 deletions
diff --git a/src/smt_util/node_visitor.h b/src/smt_util/node_visitor.h
new file mode 100644
index 000000000..c8958b7b5
--- /dev/null
+++ b/src/smt_util/node_visitor.h
@@ -0,0 +1,120 @@
+/*********************                                                        */
+/*! \file node_visitor.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: Liana Hadarean, Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A simple visitor for nodes
+ **
+ ** A simple visitor for nodes.
+ **/
+
+#pragma once
+
+#include "cvc4_private.h"
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+/**
+ * Traverses the nodes reverse-topologically (children before parents),
+ * calling the visitor in order.
+ */
+template<typename Visitor>
+class NodeVisitor {
+
+  /** For re-entry checking */
+  static CVC4_THREADLOCAL(bool) s_inRun;
+
+  /**
+   * Guard against NodeVisitor<> being re-entrant.
+   */
+  template <class T>
+  class GuardReentry {
+    T& d_guard;
+  public:
+    GuardReentry(T& guard)
+    : d_guard(guard) {
+      Assert(!d_guard);
+      d_guard = true;
+    }
+    ~GuardReentry() {
+      Assert(d_guard);
+      d_guard = false;
+    }
+  };/* class NodeVisitor<>::GuardReentry */
+
+public:
+
+  /**
+   * Element of the stack.
+   */
+  struct stack_element {
+    /** The node to be visited */
+    TNode node;
+    /** The parent of the node */
+    TNode parent;
+    /** Have the children been queued up for visitation */
+    bool children_added;
+    stack_element(TNode node, TNode parent)
+    : node(node), parent(parent), children_added(false) {}
+  };/* struct preprocess_stack_element */
+
+  /**
+   * Performs the traversal.
+   */
+  static typename Visitor::return_type run(Visitor& visitor, TNode node) {
+
+    GuardReentry<CVC4_THREADLOCAL_TYPE(bool)> guard(s_inRun);
+
+    // Notify of a start
+    visitor.start(node);
+
+    // Do a reverse-topological sort of the subexpressions
+    std::vector<stack_element> toVisit;
+    toVisit.push_back(stack_element(node, node));
+    while (!toVisit.empty()) {
+      stack_element& stackHead = toVisit.back();
+      // The current node we are processing
+      TNode current = stackHead.node;
+      TNode parent = stackHead.parent;
+
+      if (visitor.alreadyVisited(current, parent)) {
+        // If already visited, we're done
+        toVisit.pop_back();
+      } else if (stackHead.children_added) {
+        // Call the visitor
+        visitor.visit(current, parent);
+        // Done with this node, remove from the stack
+        toVisit.pop_back();
+      } else {
+        // Mark that we have added the children
+        stackHead.children_added = true;
+        // We need to add the children
+        for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
+          TNode childNode = *child_it;
+          if (!visitor.alreadyVisited(childNode, current)) {
+            toVisit.push_back(stack_element(childNode, current));
+          }
+        }
+      }
+    }
+
+    // Notify that we're done
+    return visitor.done(node);
+  }
+
+};/* class NodeVisitor<> */
+
+template <typename Visitor>
+CVC4_THREADLOCAL(bool) NodeVisitor<Visitor>::s_inRun = false;
+
+}/* CVC4 namespace */