1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
/********************* */
/*! \file node_visitor.h
** \verbatim
** Top contributors (to current version):
** Dejan Jovanovic, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. 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 CVC5 {
/**
* Traverses the nodes reverse-topologically (children before parents),
* calling the visitor in order.
*/
template<typename Visitor>
class NodeVisitor {
/** For re-entry checking */
static thread_local 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 d_node;
/** The parent of the node */
TNode d_parent;
/** Have the children been queued up for visitation */
bool d_childrenAdded;
stack_element(TNode node, TNode parent)
: d_node(node), d_parent(parent), d_childrenAdded(false)
{
}
};/* struct preprocess_stack_element */
/**
* Performs the traversal.
*/
static typename Visitor::return_type run(Visitor& visitor, TNode node) {
GuardReentry<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.d_node;
TNode parent = stackHead.d_parent;
if (visitor.alreadyVisited(current, parent)) {
// If already visited, we're done
toVisit.pop_back();
}
else if (stackHead.d_childrenAdded)
{
// 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.d_childrenAdded = 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>
thread_local bool NodeVisitor<Visitor>::s_inRun = false;
} // namespace CVC5
|
