GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/node_traversal_black.cpp Lines: 170 170 100.0 %
Date: 2021-03-23 Branches: 478 1224 39.1 %

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