summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit')
-rw-r--r--test/unit/expr/CMakeLists.txt1
-rw-r--r--test/unit/expr/node_traversal_black.h281
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);
+ }
+};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback