--- /dev/null
+/********************* */
+/*! \file node_traversal.cpp
+ ** \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 Iterators for traversing nodes.
+ **/
+
+#include "node_traversal.h"
+
+namespace CVC4 {
+
+NodeDfsIterator::NodeDfsIterator(TNode n, bool postorder)
+ : d_stack{n},
+ d_visited(),
+ d_postorder(postorder),
+ d_current(TNode())
+{
+}
+
+NodeDfsIterator::NodeDfsIterator(bool postorder)
+ : d_stack(),
+ d_visited(),
+ d_postorder(postorder),
+ d_current(TNode())
+{
+}
+
+NodeDfsIterator& NodeDfsIterator::operator++()
+{
+ // If we were just constructed, advance to first visit, **before**
+ // advancing past it to the next visit (below).
+ initializeIfUninitialized();
+
+ // Advance to the next visit
+ advanceToNextVisit();
+ return *this;
+}
+
+NodeDfsIterator NodeDfsIterator::operator++(int)
+{
+ NodeDfsIterator copyOfOld(*this);
+ ++*this;
+ return copyOfOld;
+}
+
+TNode& NodeDfsIterator::operator*()
+{
+ // If we were just constructed, advance to first visit
+ initializeIfUninitialized();
+ Assert(!d_current.isNull());
+
+ return d_current;
+}
+
+bool NodeDfsIterator::operator==(const NodeDfsIterator& other) const
+{
+ // The stack and current node uniquely represent traversal state. We need not
+ // use the scheduled node set.
+ //
+ // Users should not compare iterators for traversals of different nodes.
+ Assert(d_postorder == other.d_postorder);
+ return d_stack == other.d_stack && d_current == other.d_current;
+}
+
+bool NodeDfsIterator::operator!=(const NodeDfsIterator& other) const
+{
+ return !(*this == other);
+}
+
+void NodeDfsIterator::advanceToNextVisit()
+{
+ // While a node is enqueued and we're not at the right visit type
+ while (!d_stack.empty())
+ {
+ TNode back = d_stack.back();
+ auto visitEntry = d_visited.find(back);
+ if (visitEntry == d_visited.end())
+ {
+ // if we haven't pre-visited this node, pre-visit it
+ d_visited[back] = false;
+ d_current = back;
+ // Use integer underflow to reverse-iterate
+ for (size_t n = back.getNumChildren(), i = n - 1; i < n; --i)
+ {
+ d_stack.push_back(back[i]);
+ }
+ if (!d_postorder)
+ {
+ return;
+ }
+ }
+ else if (!d_postorder || visitEntry->second)
+ {
+ // if we're previsiting or we've already post-visited this node: skip it
+ d_stack.pop_back();
+ }
+ else
+ {
+ // otherwise, this is a post-visit
+ visitEntry->second = true;
+ d_current = back;
+ d_stack.pop_back();
+ return;
+ }
+ }
+ // We're at the end of the traversal: nullify the current node to agree
+ // with the "end" iterator.
+ d_current = TNode();
+}
+
+void NodeDfsIterator::initializeIfUninitialized()
+{
+ if (d_current.isNull())
+ {
+ advanceToNextVisit();
+ }
+}
+
+NodeDfsIterable::NodeDfsIterable(TNode n) : d_node(n), d_postorder(true) {}
+
+NodeDfsIterable& NodeDfsIterable::inPostorder()
+{
+ d_postorder = true;
+ return *this;
+}
+
+NodeDfsIterable& NodeDfsIterable::inPreorder()
+{
+ d_postorder = false;
+ return *this;
+}
+
+NodeDfsIterator NodeDfsIterable::begin() const
+{
+ return NodeDfsIterator(d_node, d_postorder);
+}
+
+NodeDfsIterator NodeDfsIterable::end() const
+{
+ return NodeDfsIterator(d_postorder);
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file node_traversal.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 Iterators for traversing nodes.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__NODE_TRAVERSAL_H
+#define CVC4__EXPR__NODE_TRAVERSAL_H
+
+#include <cstddef>
+#include <iterator>
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+// Iterator for traversing a node in post-order
+// It does DAG-traversal, so indentical sub-nodes will be visited once only.
+class NodeDfsIterator
+{
+ public:
+ // STL type definitions for an iterator
+ using value_type = TNode;
+ using pointer = TNode*;
+ using reference = TNode&;
+ using iterator_category = std::forward_iterator_tag;
+ using difference_type = std::ptrdiff_t;
+
+ // Construct a traversal iterator beginning at `n`
+ NodeDfsIterator(TNode n, bool postorder);
+ // Construct an end-of-traversal iterator
+ NodeDfsIterator(bool postorder);
+
+ // Move/copy construction and assignment. Destructor.
+ NodeDfsIterator(NodeDfsIterator&&) = default;
+ NodeDfsIterator& operator=(NodeDfsIterator&&) = default;
+ NodeDfsIterator(NodeDfsIterator&) = default;
+ NodeDfsIterator& operator=(NodeDfsIterator&) = default;
+ ~NodeDfsIterator() = default;
+
+ // Preincrement
+ NodeDfsIterator& operator++();
+ // Postincrement
+ NodeDfsIterator operator++(int);
+ // Dereference
+ reference operator*();
+ // Equals
+ bool operator==(const NodeDfsIterator&) const;
+ // Not equals
+ bool operator!=(const NodeDfsIterator&) const;
+
+ private:
+ // While we're not at an appropriate visit (see d_postorder), advance.
+ // In each step:
+ // * enqueue children of a not-yet-pre-visited node (and mark it
+ // previsited)
+ // * pop a not-yet-post-visited node (and mark it post-visited)
+ // * pop an already post-visited node.
+ // After calling this, `d_current` will be changed to the next node, if there
+ // is another node in the traversal.
+ void advanceToNextVisit();
+
+ // If this iterator hasn't been dereferenced or incremented yet, advance to
+ // first visit.
+ // Necessary because we are lazy and don't find our first visit node at
+ // construction time.
+ void initializeIfUninitialized();
+
+ // Stack of nodes to visit.
+ std::vector<TNode> d_stack;
+
+ // Whether (and how) we've visited a node.
+ // Absent if we haven't visited it.
+ // Set to `false` if we've already pre-visited it (enqueued its children).
+ // Set to `true` if we've also already post-visited it.
+ std::unordered_map<TNode, bool, TNodeHashFunction> d_visited;
+
+ // Whether this is a post-order iterator (the alternative is pre-order)
+ bool d_postorder;
+
+ // Whether this iterator has been initialized (advanced to its first
+ // visit)
+ bool d_initialized;
+
+ // Current referent node. A valid node to visit if non-null.
+ // Null after construction (but before first access) and at the end.
+ TNode d_current;
+};
+
+// Node wrapper that is iterable in DAG post-order
+class NodeDfsIterable
+{
+ public:
+ NodeDfsIterable(TNode n);
+
+ // Modifying the traversal order
+ // Modify this iterable to be in post-order (default)
+ NodeDfsIterable& inPostorder();
+ // Modify this iterable to be in pre-order
+ NodeDfsIterable& inPreorder();
+
+ // Move/copy construction and assignment. Destructor.
+ NodeDfsIterable(NodeDfsIterable&&) = default;
+ NodeDfsIterable& operator=(NodeDfsIterable&&) = default;
+ NodeDfsIterable(NodeDfsIterable&) = default;
+ NodeDfsIterable& operator=(NodeDfsIterable&) = default;
+ ~NodeDfsIterable() = default;
+
+ NodeDfsIterator begin() const;
+ NodeDfsIterator end() const;
+
+ private:
+ TNode d_node;
+ bool d_postorder;
+};
+
+} // namespace CVC4
+
+#endif // CVC4__EXPR__NODE_TRAVERSAL_H
--- /dev/null
+/********************* */
+/*! \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);
+ }
+};
projects / cvc5.git / commitdiff