diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/expr/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/expr/node_traversal_black.h | 281 |
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); + } +}; |