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