1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Alex Ozdemir, Andres Noetzli |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Iterators for traversing nodes. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "node_traversal.h" |
17 |
|
|
18 |
|
#include <functional> |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
|
22 |
1312 |
NodeDfsIterator::NodeDfsIterator(TNode n, |
23 |
|
VisitOrder order, |
24 |
1312 |
std::function<bool(TNode)> skipIf) |
25 |
|
: d_stack{n}, |
26 |
|
d_visited(), |
27 |
|
d_order(order), |
28 |
|
d_current(TNode()), |
29 |
1312 |
d_skipIf(skipIf) |
30 |
|
{ |
31 |
1312 |
} |
32 |
|
|
33 |
1312 |
NodeDfsIterator::NodeDfsIterator(VisitOrder order) |
34 |
|
: d_stack(), |
35 |
|
d_visited(), |
36 |
|
d_order(order), |
37 |
|
d_current(TNode()), |
38 |
1312 |
d_skipIf([](TNode) { return false; }) |
39 |
|
{ |
40 |
1312 |
} |
41 |
|
|
42 |
2731 |
NodeDfsIterator& NodeDfsIterator::operator++() |
43 |
|
{ |
44 |
|
// If we were just constructed, advance to first visit, **before** |
45 |
|
// advancing past it to the next visit (below). |
46 |
2731 |
initializeIfUninitialized(); |
47 |
|
|
48 |
|
// Advance to the next visit |
49 |
2731 |
advanceToNextVisit(); |
50 |
2731 |
return *this; |
51 |
|
} |
52 |
|
|
53 |
12 |
NodeDfsIterator NodeDfsIterator::operator++(int) |
54 |
|
{ |
55 |
12 |
NodeDfsIterator copyOfOld(*this); |
56 |
12 |
++*this; |
57 |
12 |
return copyOfOld; |
58 |
|
} |
59 |
|
|
60 |
2734 |
TNode& NodeDfsIterator::operator*() |
61 |
|
{ |
62 |
|
// If we were just constructed, advance to first visit |
63 |
2734 |
initializeIfUninitialized(); |
64 |
2734 |
Assert(!d_current.isNull()); |
65 |
|
|
66 |
2734 |
return d_current; |
67 |
|
} |
68 |
|
|
69 |
4031 |
bool NodeDfsIterator::operator==(NodeDfsIterator& other) |
70 |
|
{ |
71 |
|
// Unitialize this node, and the other, before comparing. |
72 |
4031 |
initializeIfUninitialized(); |
73 |
4031 |
other.initializeIfUninitialized(); |
74 |
|
// The stack and current node uniquely represent traversal state. We need not |
75 |
|
// use the scheduled node set. |
76 |
|
// |
77 |
|
// Users should not compare iterators for traversals of different nodes, or |
78 |
|
// traversals with different skipIfs. |
79 |
4031 |
Assert(d_order == other.d_order); |
80 |
4031 |
return d_stack == other.d_stack && d_current == other.d_current; |
81 |
|
} |
82 |
|
|
83 |
4009 |
bool NodeDfsIterator::operator!=(NodeDfsIterator& other) |
84 |
|
{ |
85 |
4009 |
return !(*this == other); |
86 |
|
} |
87 |
|
|
88 |
12927 |
void NodeDfsIterator::advanceToNextVisit() |
89 |
|
{ |
90 |
|
// While a node is enqueued and we're not at the right visit type |
91 |
17096 |
while (!d_stack.empty()) |
92 |
|
{ |
93 |
9927 |
TNode back = d_stack.back(); |
94 |
6907 |
auto visitEntry = d_visited.find(back); |
95 |
6907 |
if (visitEntry == d_visited.end()) |
96 |
|
{ |
97 |
|
// if we haven't pre-visited this node, pre-visit it |
98 |
5041 |
if (d_skipIf(back)) |
99 |
|
{ |
100 |
|
// actually, skip it if the skip predicate says so... |
101 |
1149 |
d_stack.pop_back(); |
102 |
1149 |
continue; |
103 |
|
} |
104 |
2743 |
d_visited[back] = false; |
105 |
2743 |
d_current = back; |
106 |
|
// Use integer underflow to reverse-iterate |
107 |
5606 |
for (size_t n = back.getNumChildren(), i = n - 1; i < n; --i) |
108 |
|
{ |
109 |
2863 |
d_stack.push_back(back[i]); |
110 |
|
} |
111 |
2743 |
if (d_order == VisitOrder::PREORDER) |
112 |
|
{ |
113 |
48 |
return; |
114 |
|
} |
115 |
|
} |
116 |
3015 |
else if (d_order == VisitOrder::PREORDER || visitEntry->second) |
117 |
|
{ |
118 |
|
// if we're previsiting or we've already post-visited this node: skip it |
119 |
325 |
d_stack.pop_back(); |
120 |
|
} |
121 |
|
else |
122 |
|
{ |
123 |
|
// otherwise, this is a post-visit |
124 |
2690 |
visitEntry->second = true; |
125 |
2690 |
d_current = back; |
126 |
2690 |
d_stack.pop_back(); |
127 |
2690 |
return; |
128 |
|
} |
129 |
|
} |
130 |
|
// We're at the end of the traversal: nullify the current node to agree |
131 |
|
// with the "end" iterator. |
132 |
6020 |
d_current = TNode(); |
133 |
|
} |
134 |
|
|
135 |
13527 |
void NodeDfsIterator::initializeIfUninitialized() |
136 |
|
{ |
137 |
13527 |
if (d_current.isNull()) |
138 |
|
{ |
139 |
6027 |
advanceToNextVisit(); |
140 |
|
} |
141 |
13527 |
} |
142 |
|
|
143 |
1312 |
NodeDfsIterable::NodeDfsIterable(TNode n, |
144 |
|
VisitOrder order, |
145 |
1312 |
std::function<bool(TNode)> skipIf) |
146 |
1312 |
: d_node(n), d_order(order), d_skipIf(skipIf) |
147 |
|
{ |
148 |
1312 |
} |
149 |
|
|
150 |
1312 |
NodeDfsIterator NodeDfsIterable::begin() const |
151 |
|
{ |
152 |
1312 |
return NodeDfsIterator(d_node, d_order, d_skipIf); |
153 |
|
} |
154 |
|
|
155 |
1312 |
NodeDfsIterator NodeDfsIterable::end() const |
156 |
|
{ |
157 |
1312 |
return NodeDfsIterator(d_order); |
158 |
|
} |
159 |
|
|
160 |
31125 |
} // namespace cvc5 |