GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/node_traversal_black.cpp Lines: 170 170 100.0 %
Date: 2021-09-17 Branches: 477 1222 39.0 %

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