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