google test: expr: Migrate node_traversal_black. (#5868)

3 files changed, 298 insertions, 330 deletions

diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index 9f39a3b47..d07945d79 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -21,7 +21,7 @@ cvc4_add_unit_test_black(node_builder_black expr)
 cvc4_add_cxx_unit_test_black(node_manager_black expr)
 cvc4_add_unit_test_white(node_manager_white expr)
 cvc4_add_cxx_unit_test_black(node_self_iterator_black expr)
-cvc4_add_cxx_unit_test_black(node_traversal_black expr)
+cvc4_add_unit_test_black(node_traversal_black expr)
 cvc4_add_cxx_unit_test_white(node_white expr)
 cvc4_add_unit_test_black(symbol_table_black expr)
 cvc4_add_cxx_unit_test_black(type_cardinality_public expr)
diff --git a/test/unit/expr/node_traversal_black.cpp b/test/unit/expr/node_traversal_black.cpp
new file mode 100644
index 000000000..d2921a929
--- /dev/null
+++ b/test/unit/expr/node_traversal_black.cpp
@@ -0,0 +1,297 @@
+/*********************                                                        */
+/*! \file node_traversal_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Alex Ozdemir, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of node traversal iterators.
+ **/
+
+#include <algorithm>
+#include <cstddef>
+#include <iterator>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "expr/expr_manager.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/node_traversal.h"
+#include "expr/node_value.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackNodeTraversalPostorder : public TestNodeBlack
+{
+};
+
+class TestNodeBlackNodeTraversalPreorder : public TestNodeBlack
+{
+};
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, preincrement_iteration)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
+  NodeDfsIterator i = traversal.begin();
+  NodeDfsIterator end = traversal.end();
+  ASSERT_EQ(*i, tb);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_EQ(*i, eb);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_EQ(*i, cnd);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, postincrement_iteration)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
+  NodeDfsIterator i = traversal.begin();
+  NodeDfsIterator end = traversal.end();
+  ASSERT_EQ(*(i++), tb);
+  ASSERT_EQ(*(i++), eb);
+  ASSERT_EQ(*(i++), cnd);
+  ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, postorder_is_default)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  auto traversal = NodeDfsIterable(cnd);
+  NodeDfsIterator i = traversal.begin();
+  NodeDfsIterator end = traversal.end();
+  ASSERT_EQ(*i, tb);
+  ASSERT_FALSE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, range_for_loop)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  size_t count = 0;
+  for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
+  {
+    ++count;
+  }
+  ASSERT_EQ(count, 3);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, count_if_with_loop)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  size_t count = 0;
+  for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
+  {
+    if (i.isConst())
+    {
+      ++count;
+    }
+  }
+  ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, stl_count_if)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+
+  auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
+
+  size_t count = std::count_if(
+      traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
+  ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, stl_copy)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+  std::vector<TNode> expected = {tb, eb, cnd, top};
+
+  auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
+
+  std::vector<TNode> actual;
+  std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+  ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, skip_if)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+  std::vector<TNode> expected = {top};
+
+  auto traversal = NodeDfsIterable(
+      top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; });
+
+  std::vector<TNode> actual;
+  std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+  ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, skip_all)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+  std::vector<TNode> expected = {};
+
+  auto traversal =
+      NodeDfsIterable(top, VisitOrder::POSTORDER, [](TNode n) { return true; });
+
+  std::vector<TNode> actual;
+  std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+  ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, preincrement_iteration)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
+  NodeDfsIterator i = traversal.begin();
+  NodeDfsIterator end = traversal.end();
+  ASSERT_EQ(*i, cnd);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_EQ(*i, tb);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_EQ(*i, eb);
+  ASSERT_FALSE(i == end);
+  ++i;
+  ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, postincrement_iteration)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
+  NodeDfsIterator i = traversal.begin();
+  NodeDfsIterator end = traversal.end();
+  ASSERT_EQ(*(i++), cnd);
+  ASSERT_EQ(*(i++), tb);
+  ASSERT_EQ(*(i++), eb);
+  ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, range_for_loop)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  size_t count = 0;
+  for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
+  {
+    ++count;
+  }
+  ASSERT_EQ(count, 3);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, count_if_with_loop)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+  size_t count = 0;
+  for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
+  {
+    if (i.isConst())
+    {
+      ++count;
+    }
+  }
+  ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, stl_count_if)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+
+  auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
+
+  size_t count = std::count_if(
+      traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
+  ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, stl_copy)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+  std::vector<TNode> expected = {top, cnd, tb, eb};
+
+  auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
+
+  std::vector<TNode> actual;
+  std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+  ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, skip_if)
+{
+  const Node tb = d_nodeManager->mkConst(true);
+  const Node eb = d_nodeManager->mkConst(false);
+  const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+  std::vector<TNode> expected = {top, cnd, eb};
+
+  auto traversal = NodeDfsIterable(
+      top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; });
+
+  std::vector<TNode> actual;
+  std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+  ASSERT_EQ(actual, expected);
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/expr/node_traversal_black.h b/test/unit/expr/node_traversal_black.h
deleted file mode 100644
index d14255573..000000000
--- a/test/unit/expr/node_traversal_black.h
+++ /dev/null
@@ -1,329 +0,0 @@
-/*********************                                                        */
-/*! \file node_traversal_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Alex Ozdemir, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of node traversal iterators.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-// Used in some of the tests
-#include <algorithm>
-#include <cstddef>
-#include <iterator>
-#include <sstream>
-#include <string>
-#include <vector>
-
-#include "expr/expr_manager.h"
-#include "expr/node.h"
-#include "expr/node_builder.h"
-#include "expr/node_manager.h"
-#include "expr/node_traversal.h"
-#include "expr/node_value.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace std;
-
-class NodePostorderTraversalBlack : public CxxTest::TestSuite
-{
- private:
-  NodeManager* d_nodeManager;
-  NodeManagerScope* d_scope;
-
- public:
-  void setUp() override
-  {
-    d_nodeManager = new NodeManager(NULL);
-    d_scope = new NodeManagerScope(d_nodeManager);
-  }
-
-  void tearDown() override
-  {
-    delete d_scope;
-    delete d_nodeManager;
-  }
-
-  void testPreincrementIteration()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
-    auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
-    NodeDfsIterator i = traversal.begin();
-    NodeDfsIterator end = traversal.end();
-    TS_ASSERT_EQUALS(*i, tb);
-    TS_ASSERT_DIFFERS(i, end);
-    ++i;
-    TS_ASSERT_EQUALS(*i, eb);
-    TS_ASSERT_DIFFERS(i, end);
-    ++i;
-    TS_ASSERT_EQUALS(*i, cnd);
-    TS_ASSERT_DIFFERS(i, end);
-    ++i;
-    TS_ASSERT_EQUALS(i, end);
-  }
-
-  void testPostincrementIteration()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
-    auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
-    NodeDfsIterator i = traversal.begin();
-    NodeDfsIterator end = traversal.end();
-    TS_ASSERT_EQUALS(*(i++), tb);
-    TS_ASSERT_EQUALS(*(i++), eb);
-    TS_ASSERT_EQUALS(*(i++), cnd);
-    TS_ASSERT_EQUALS(i, end);
-  }
-
-  void testPostorderIsDefault()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
-    auto traversal = NodeDfsIterable(cnd);
-    NodeDfsIterator i = traversal.begin();
-    NodeDfsIterator end = traversal.end();
-    TS_ASSERT_EQUALS(*i, tb);
-    TS_ASSERT_DIFFERS(i, end);
-  }
-
-  void testRangeForLoop()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
-    size_t count = 0;
-    for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
-    {
-      ++count;
-    }
-    TS_ASSERT_EQUALS(count, 3);
-  }
-
-  void testCountIfWithLoop()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
-    size_t count = 0;
-    for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
-    {
-      if (i.isConst())
-      {
-        ++count;
-      }
-    }
-    TS_ASSERT_EQUALS(count, 2);
-  }
-
-  void testStlCountIf()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-    Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
-
-    auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
-
-    size_t count = std::count_if(traversal.begin(),
-                                 traversal.end(),
-                                 [](TNode n) { return n.isConst(); });
-    TS_ASSERT_EQUALS(count, 2);
-  }
-
-  void testStlCopy()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-    Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
-    std::vector<TNode> expected = {tb, eb, cnd, top};
-
-    auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
-
-    std::vector<TNode> actual;
-    std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
-    TS_ASSERT_EQUALS(actual, expected);
-  }
-
-  void testSkipIf()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-    Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
-    std::vector<TNode> expected = {top};
-
-    auto traversal = NodeDfsIterable(
-        top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; });
-
-    std::vector<TNode> actual;
-    std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
-    TS_ASSERT_EQUALS(actual, expected);
-  }
-
-  void testSkipAll()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-    Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
-    std::vector<TNode> expected = {};
-
-    auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER,
-        [](TNode n) { return true; });
-
-    std::vector<TNode> actual;
-    std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
-    TS_ASSERT_EQUALS(actual, expected);
-  }
-};
-
-class NodePreorderTraversalBlack : public CxxTest::TestSuite
-{
- private:
-  NodeManager* d_nodeManager;
-  NodeManagerScope* d_scope;
-
- public:
-  void setUp() override
-  {
-    d_nodeManager = new NodeManager(NULL);
-    d_scope = new NodeManagerScope(d_nodeManager);
-  }
-
-  void tearDown() override
-  {
-    delete d_scope;
-    delete d_nodeManager;
-  }
-
-  void testPreincrementIteration()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
-    auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
-    NodeDfsIterator i = traversal.begin();
-    NodeDfsIterator end = traversal.end();
-    TS_ASSERT_EQUALS(*i, cnd);
-    TS_ASSERT_DIFFERS(i, end);
-    ++i;
-    TS_ASSERT_EQUALS(*i, tb);
-    TS_ASSERT_DIFFERS(i, end);
-    ++i;
-    TS_ASSERT_EQUALS(*i, eb);
-    TS_ASSERT_DIFFERS(i, end);
-    ++i;
-    TS_ASSERT_EQUALS(i, end);
-  }
-
-  void testPostincrementIteration()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
-    auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
-    NodeDfsIterator i = traversal.begin();
-    NodeDfsIterator end = traversal.end();
-    TS_ASSERT_EQUALS(*(i++), cnd);
-    TS_ASSERT_EQUALS(*(i++), tb);
-    TS_ASSERT_EQUALS(*(i++), eb);
-    TS_ASSERT_EQUALS(i, end);
-  }
-
-  void testRangeForLoop()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
-    size_t count = 0;
-    for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
-    {
-      ++count;
-    }
-    TS_ASSERT_EQUALS(count, 3);
-  }
-
-  void testCountIfWithLoop()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
-    size_t count = 0;
-    for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
-    {
-      if (i.isConst())
-      {
-        ++count;
-      }
-    }
-    TS_ASSERT_EQUALS(count, 2);
-  }
-
-  void testStlCountIf()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-    Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
-
-    auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
-
-    size_t count = std::count_if(traversal.begin(),
-                                 traversal.end(),
-                                 [](TNode n) { return n.isConst(); });
-    TS_ASSERT_EQUALS(count, 2);
-  }
-
-  void testStlCopy()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-    Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
-    std::vector<TNode> expected = {top, cnd, tb, eb};
-
-    auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
-
-    std::vector<TNode> actual;
-    std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
-    TS_ASSERT_EQUALS(actual, expected);
-  }
-
-  void testSkipIf()
-  {
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-    Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
-    std::vector<TNode> expected = {top, cnd, eb};
-
-    auto traversal = NodeDfsIterable(
-        top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; });
-
-    std::vector<TNode> actual;
-    std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
-    TS_ASSERT_EQUALS(actual, expected);
-  }
-};