diff options
Diffstat (limited to 'src/smt_util/node_visitor.h')
-rw-r--r-- | src/smt_util/node_visitor.h | 120 |
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 */ |