Node traversal iterator (#3845)

Implement an iterator for pre- and post-order traversals.

I believe that this will be useful in pre-processing passes, many of
which do postorder traversals that they implement by hand.

Right now this iterator does not support modification of the traversal
pattern, but we could add this later on, if we want it.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>

2 files changed, 282 insertions, 0 deletions

diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index d487bf560..438b7f7b6 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -13,6 +13,7 @@ cvc4_add_unit_test_black(node_builder_black expr)
 cvc4_add_unit_test_black(node_manager_black expr)
 cvc4_add_unit_test_white(node_manager_white expr)
 cvc4_add_unit_test_black(node_self_iterator_black expr)
+cvc4_add_unit_test_black(node_traversal_black expr)
 cvc4_add_unit_test_white(node_white expr)
 cvc4_add_unit_test_black(symbol_table_black expr)
 cvc4_add_unit_test_black(type_cardinality_public expr)
diff --git a/test/unit/expr/node_traversal_black.h b/test/unit/expr/node_traversal_black.h
new file mode 100644
index 000000000..b4a7c449c
--- /dev/null
+++ b/test/unit/expr/node_traversal_black.h
@@ -0,0 +1,281 @@
+/*********************                                                        */
+/*! \file node_traversal_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** 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).inPostorder();
+    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).inPostorder();
+    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).inPostorder())
+    {
+      ++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).inPostorder())
+    {
+      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).inPostorder();
+
+    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).inPostorder();
+
+    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).inPreorder();
+    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).inPreorder();
+    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).inPreorder())
+    {
+      ++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).inPreorder())
+    {
+      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).inPreorder();
+
+    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).inPreorder();
+
+    std::vector<TNode> actual;
+    std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+    TS_ASSERT_EQUALS(actual, expected);
+  }
+};