1 /********************* */ 2 /*! \file node_visitor.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Dejan Jovanovic, Morgan Deters, Liana Hadarean 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief A simple visitor for nodes 13 ** 14 ** A simple visitor for nodes. 15 **/ 16 17 #pragma once 18 19 #include "cvc4_private.h" 20 21 #include <vector> 22 23 #include "expr/node.h" 24 25 namespace CVC4 { 26 27 /** 28 * Traverses the nodes reverse-topologically (children before parents), 29 * calling the visitor in order. 30 */ 31 template<typename Visitor> 32 class NodeVisitor { 33 34 /** For re-entry checking */ 35 static thread_local bool s_inRun; 36 37 /** 38 * Guard against NodeVisitor<> being re-entrant. 39 */ 40 template <class T> 41 class GuardReentry { 42 T& d_guard; 43 public: GuardReentry(T & guard)44 GuardReentry(T& guard) 45 : d_guard(guard) { 46 Assert(!d_guard); 47 d_guard = true; 48 } ~GuardReentry()49 ~GuardReentry() { 50 Assert(d_guard); 51 d_guard = false; 52 } 53 };/* class NodeVisitor<>::GuardReentry */ 54 55 public: 56 57 /** 58 * Element of the stack. 59 */ 60 struct stack_element { 61 /** The node to be visited */ 62 TNode node; 63 /** The parent of the node */ 64 TNode parent; 65 /** Have the children been queued up for visitation */ 66 bool children_added; stack_elementstack_element67 stack_element(TNode node, TNode parent) 68 : node(node), parent(parent), children_added(false) {} 69 };/* struct preprocess_stack_element */ 70 71 /** 72 * Performs the traversal. 73 */ run(Visitor & visitor,TNode node)74 static typename Visitor::return_type run(Visitor& visitor, TNode node) { 75 76 GuardReentry<bool> guard(s_inRun); 77 78 // Notify of a start 79 visitor.start(node); 80 81 // Do a reverse-topological sort of the subexpressions 82 std::vector<stack_element> toVisit; 83 toVisit.push_back(stack_element(node, node)); 84 while (!toVisit.empty()) { 85 stack_element& stackHead = toVisit.back(); 86 // The current node we are processing 87 TNode current = stackHead.node; 88 TNode parent = stackHead.parent; 89 90 if (visitor.alreadyVisited(current, parent)) { 91 // If already visited, we're done 92 toVisit.pop_back(); 93 } else if (stackHead.children_added) { 94 // Call the visitor 95 visitor.visit(current, parent); 96 // Done with this node, remove from the stack 97 toVisit.pop_back(); 98 } else { 99 // Mark that we have added the children 100 stackHead.children_added = true; 101 // We need to add the children 102 for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { 103 TNode childNode = *child_it; 104 if (!visitor.alreadyVisited(childNode, current)) { 105 toVisit.push_back(stack_element(childNode, current)); 106 } 107 } 108 } 109 } 110 111 // Notify that we're done 112 return visitor.done(node); 113 } 114 115 };/* class NodeVisitor<> */ 116 117 template <typename Visitor> 118 thread_local bool NodeVisitor<Visitor>::s_inRun = false; 119 120 }/* CVC4 namespace */ 121