Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Black box testing of node traversal iterators.
11 : : */
12 : :
13 : : #include <algorithm>
14 : : #include <cstddef>
15 : : #include <iterator>
16 : : #include <sstream>
17 : : #include <string>
18 : : #include <vector>
19 : :
20 : : #include "expr/node.h"
21 : : #include "expr/node_builder.h"
22 : : #include "expr/node_manager.h"
23 : : #include "expr/node_traversal.h"
24 : : #include "expr/node_value.h"
25 : : #include "test_node.h"
26 : :
27 : : namespace cvc5::internal {
28 : :
29 : : namespace test {
30 : :
31 : : class TestNodeBlackNodeTraversalPostorder : public TestNode
32 : : {
33 : : };
34 : :
35 : : class TestNodeBlackNodeTraversalPreorder : public TestNode
36 : : {
37 : : };
38 : :
39 : 4 : TEST_F(TestNodeBlackNodeTraversalPostorder, preincrement_iteration)
40 : : {
41 : 1 : const Node tb = d_nodeManager->mkConst(true);
42 : 1 : const Node eb = d_nodeManager->mkConst(false);
43 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
44 : :
45 : 2 : auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
46 : 1 : NodeDfsIterator i = traversal.begin();
47 : 1 : NodeDfsIterator end = traversal.end();
48 [ - + ][ + - ]: 1 : ASSERT_EQ(*i, tb);
49 [ - + ][ + - ]: 1 : ASSERT_FALSE(i == end);
50 : 1 : ++i;
51 [ - + ][ + - ]: 1 : ASSERT_EQ(*i, eb);
52 [ - + ][ + - ]: 1 : ASSERT_FALSE(i == end);
53 : 1 : ++i;
54 [ - + ][ + - ]: 1 : ASSERT_EQ(*i, cnd);
55 [ - + ][ + - ]: 1 : ASSERT_FALSE(i == end);
56 : 1 : ++i;
57 [ - + ][ + - ]: 1 : ASSERT_TRUE(i == end);
58 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
59 : :
60 : 4 : TEST_F(TestNodeBlackNodeTraversalPostorder, postincrement_iteration)
61 : : {
62 : 1 : const Node tb = d_nodeManager->mkConst(true);
63 : 1 : const Node eb = d_nodeManager->mkConst(false);
64 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
65 : :
66 : 2 : auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
67 : 1 : NodeDfsIterator i = traversal.begin();
68 : 1 : NodeDfsIterator end = traversal.end();
69 [ - + ][ + - ]: 2 : ASSERT_EQ(*(i++), tb);
70 [ - + ][ + - ]: 2 : ASSERT_EQ(*(i++), eb);
71 [ - + ][ + - ]: 2 : ASSERT_EQ(*(i++), cnd);
72 [ - + ][ + - ]: 1 : ASSERT_TRUE(i == end);
73 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
74 : :
75 : 4 : TEST_F(TestNodeBlackNodeTraversalPostorder, postorder_is_default)
76 : : {
77 : 1 : const Node tb = d_nodeManager->mkConst(true);
78 : 1 : const Node eb = d_nodeManager->mkConst(false);
79 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
80 : :
81 : 2 : auto traversal = NodeDfsIterable(cnd);
82 : 1 : NodeDfsIterator i = traversal.begin();
83 : 1 : NodeDfsIterator end = traversal.end();
84 [ - + ][ + - ]: 1 : ASSERT_EQ(*i, tb);
85 [ - + ][ + - ]: 1 : ASSERT_FALSE(i == end);
86 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
87 : :
88 : 4 : TEST_F(TestNodeBlackNodeTraversalPostorder, range_for_loop)
89 : : {
90 : 1 : const Node tb = d_nodeManager->mkConst(true);
91 : 1 : const Node eb = d_nodeManager->mkConst(false);
92 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
93 : :
94 : 1 : size_t count = 0;
95 [ + + ]: 4 : for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
96 : : {
97 : 3 : ++count;
98 : 4 : }
99 [ - + ][ + - ]: 1 : ASSERT_EQ(count, 3);
100 [ + - ][ + - ]: 1 : }
[ + - ]
101 : :
102 : 4 : TEST_F(TestNodeBlackNodeTraversalPostorder, count_if_with_loop)
103 : : {
104 : 1 : const Node tb = d_nodeManager->mkConst(true);
105 : 1 : const Node eb = d_nodeManager->mkConst(false);
106 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
107 : :
108 : 1 : size_t count = 0;
109 [ + + ]: 4 : for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
110 : : {
111 [ + + ]: 3 : if (i.isConst())
112 : : {
113 : 2 : ++count;
114 : : }
115 : 4 : }
116 [ - + ][ + - ]: 1 : ASSERT_EQ(count, 2);
117 [ + - ][ + - ]: 1 : }
[ + - ]
118 : :
119 : 4 : TEST_F(TestNodeBlackNodeTraversalPostorder, stl_count_if)
120 : : {
121 : 1 : const Node tb = d_nodeManager->mkConst(true);
122 : 1 : const Node eb = d_nodeManager->mkConst(false);
123 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
124 : 2 : const Node top = d_nodeManager->mkNode(Kind::XOR, cnd, cnd);
125 : :
126 : 2 : auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
127 : :
128 : 1 : size_t count = std::count_if(
129 : 6 : traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
130 [ - + ][ + - ]: 1 : ASSERT_EQ(count, 2);
131 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
132 : :
133 : 4 : TEST_F(TestNodeBlackNodeTraversalPostorder, stl_copy)
134 : : {
135 : 1 : const Node tb = d_nodeManager->mkConst(true);
136 : 1 : const Node eb = d_nodeManager->mkConst(false);
137 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
138 : 2 : const Node top = d_nodeManager->mkNode(Kind::XOR, cnd, cnd);
139 : 6 : std::vector<TNode> expected = {tb, eb, cnd, top};
140 : :
141 : 2 : auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
142 : :
143 : 1 : std::vector<TNode> actual;
144 : 1 : std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
145 [ - + ][ + - ]: 1 : ASSERT_EQ(actual, expected);
146 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
147 : :
148 : 4 : TEST_F(TestNodeBlackNodeTraversalPostorder, skip_if)
149 : : {
150 : 1 : const Node tb = d_nodeManager->mkConst(true);
151 : 1 : const Node eb = d_nodeManager->mkConst(false);
152 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
153 : 2 : const Node top = d_nodeManager->mkNode(Kind::XOR, cnd, cnd);
154 : 3 : std::vector<TNode> expected = {top};
155 : :
156 : : auto traversal = NodeDfsIterable(
157 : 5 : top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; });
158 : :
159 : 1 : std::vector<TNode> actual;
160 : 1 : std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
161 [ - + ][ + - ]: 1 : ASSERT_EQ(actual, expected);
162 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
163 : :
164 : 4 : TEST_F(TestNodeBlackNodeTraversalPostorder, skip_all)
165 : : {
166 : 1 : const Node tb = d_nodeManager->mkConst(true);
167 : 1 : const Node eb = d_nodeManager->mkConst(false);
168 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
169 : 2 : const Node top = d_nodeManager->mkNode(Kind::XOR, cnd, cnd);
170 : 1 : std::vector<TNode> expected = {};
171 : :
172 : : auto traversal =
173 : 3 : NodeDfsIterable(top, VisitOrder::POSTORDER, [](TNode) { return true; });
174 : :
175 : 1 : std::vector<TNode> actual;
176 : 1 : std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
177 [ - + ][ + - ]: 1 : ASSERT_EQ(actual, expected);
178 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
179 : :
180 : 4 : TEST_F(TestNodeBlackNodeTraversalPreorder, preincrement_iteration)
181 : : {
182 : 1 : const Node tb = d_nodeManager->mkConst(true);
183 : 1 : const Node eb = d_nodeManager->mkConst(false);
184 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
185 : :
186 : 2 : auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
187 : 1 : NodeDfsIterator i = traversal.begin();
188 : 1 : NodeDfsIterator end = traversal.end();
189 [ - + ][ + - ]: 1 : ASSERT_EQ(*i, cnd);
190 [ - + ][ + - ]: 1 : ASSERT_FALSE(i == end);
191 : 1 : ++i;
192 [ - + ][ + - ]: 1 : ASSERT_EQ(*i, tb);
193 [ - + ][ + - ]: 1 : ASSERT_FALSE(i == end);
194 : 1 : ++i;
195 [ - + ][ + - ]: 1 : ASSERT_EQ(*i, eb);
196 [ - + ][ + - ]: 1 : ASSERT_FALSE(i == end);
197 : 1 : ++i;
198 [ - + ][ + - ]: 1 : ASSERT_TRUE(i == end);
199 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
200 : :
201 : 4 : TEST_F(TestNodeBlackNodeTraversalPreorder, postincrement_iteration)
202 : : {
203 : 1 : const Node tb = d_nodeManager->mkConst(true);
204 : 1 : const Node eb = d_nodeManager->mkConst(false);
205 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
206 : :
207 : 2 : auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
208 : 1 : NodeDfsIterator i = traversal.begin();
209 : 1 : NodeDfsIterator end = traversal.end();
210 [ - + ][ + - ]: 2 : ASSERT_EQ(*(i++), cnd);
211 [ - + ][ + - ]: 2 : ASSERT_EQ(*(i++), tb);
212 [ - + ][ + - ]: 2 : ASSERT_EQ(*(i++), eb);
213 [ - + ][ + - ]: 1 : ASSERT_TRUE(i == end);
214 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
215 : :
216 : 4 : TEST_F(TestNodeBlackNodeTraversalPreorder, range_for_loop)
217 : : {
218 : 1 : const Node tb = d_nodeManager->mkConst(true);
219 : 1 : const Node eb = d_nodeManager->mkConst(false);
220 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
221 : :
222 : 1 : size_t count = 0;
223 [ + + ]: 4 : for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
224 : : {
225 : 3 : ++count;
226 : 4 : }
227 [ - + ][ + - ]: 1 : ASSERT_EQ(count, 3);
228 [ + - ][ + - ]: 1 : }
[ + - ]
229 : :
230 : 4 : TEST_F(TestNodeBlackNodeTraversalPreorder, count_if_with_loop)
231 : : {
232 : 1 : const Node tb = d_nodeManager->mkConst(true);
233 : 1 : const Node eb = d_nodeManager->mkConst(false);
234 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
235 : :
236 : 1 : size_t count = 0;
237 [ + + ]: 4 : for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
238 : : {
239 [ + + ]: 3 : if (i.isConst())
240 : : {
241 : 2 : ++count;
242 : : }
243 : 4 : }
244 [ - + ][ + - ]: 1 : ASSERT_EQ(count, 2);
245 [ + - ][ + - ]: 1 : }
[ + - ]
246 : :
247 : 4 : TEST_F(TestNodeBlackNodeTraversalPreorder, stl_count_if)
248 : : {
249 : 1 : const Node tb = d_nodeManager->mkConst(true);
250 : 1 : const Node eb = d_nodeManager->mkConst(false);
251 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
252 : 2 : const Node top = d_nodeManager->mkNode(Kind::XOR, cnd, cnd);
253 : :
254 : 2 : auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
255 : :
256 : 1 : size_t count = std::count_if(
257 : 6 : traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
258 [ - + ][ + - ]: 1 : ASSERT_EQ(count, 2);
259 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
260 : :
261 : 4 : TEST_F(TestNodeBlackNodeTraversalPreorder, stl_copy)
262 : : {
263 : 1 : const Node tb = d_nodeManager->mkConst(true);
264 : 1 : const Node eb = d_nodeManager->mkConst(false);
265 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
266 : 2 : const Node top = d_nodeManager->mkNode(Kind::XOR, cnd, cnd);
267 : 6 : std::vector<TNode> expected = {top, cnd, tb, eb};
268 : :
269 : 2 : auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
270 : :
271 : 1 : std::vector<TNode> actual;
272 : 1 : std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
273 [ - + ][ + - ]: 1 : ASSERT_EQ(actual, expected);
274 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
275 : :
276 : 4 : TEST_F(TestNodeBlackNodeTraversalPreorder, skip_if)
277 : : {
278 : 1 : const Node tb = d_nodeManager->mkConst(true);
279 : 1 : const Node eb = d_nodeManager->mkConst(false);
280 : 2 : const Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
281 : 2 : const Node top = d_nodeManager->mkNode(Kind::XOR, cnd, cnd);
282 : 5 : std::vector<TNode> expected = {top, cnd, eb};
283 : :
284 : : auto traversal = NodeDfsIterable(
285 : 6 : top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; });
286 : :
287 : 1 : std::vector<TNode> actual;
288 : 1 : std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
289 [ - + ][ + - ]: 1 : ASSERT_EQ(actual, expected);
290 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
291 : : } // namespace test
292 : : } // namespace cvc5::internal
|
