From 6834b4a129b932a18edb384cb78e6b573e54325a Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 9 Feb 2021 08:01:29 -0800 Subject: [PATCH] google test: expr: Migrate node_self_iterator_black. (#5865) --- test/unit/expr/CMakeLists.txt | 2 +- test/unit/expr/node_self_iterator_black.cpp | 57 ++++++++++++++++ test/unit/expr/node_self_iterator_black.h | 75 --------------------- 3 files changed, 58 insertions(+), 76 deletions(-) create mode 100644 test/unit/expr/node_self_iterator_black.cpp delete mode 100644 test/unit/expr/node_self_iterator_black.h diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 39545d056..f4af29bdc 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -20,7 +20,7 @@ cvc4_add_unit_test_black(node_algorithm_black expr) 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_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) diff --git a/test/unit/expr/node_self_iterator_black.cpp b/test/unit/expr/node_self_iterator_black.cpp new file mode 100644 index 000000000..20d04b52b --- /dev/null +++ b/test/unit/expr/node_self_iterator_black.cpp @@ -0,0 +1,57 @@ +/********************* */ +/*! \file node_self_iterator_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, Tim King + ** 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 CVC4::expr::NodeSelfIterator + ** + ** Black box testing of CVC4::expr::NodeSelfIterator + **/ + +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_self_iterator.h" +#include "test_node.h" + +namespace CVC4 { + +using namespace kind; +using namespace expr; + +namespace test { + +class TestNodeBlackNodeSelfIterator : public TestNodeBlack +{ +}; + +TEST_F(TestNodeBlackNodeSelfIterator, iteration) +{ + Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); + Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode); + Node x_and_y = x.andNode(y); + NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y); + ASSERT_NE(i, x_and_y.end()); + ASSERT_NE(j, x_and_y.end()); + ASSERT_EQ(*i, x_and_y); + ASSERT_EQ(*j, x_and_y); + ASSERT_EQ(*i++, x_and_y); + ASSERT_EQ(*j++, x_and_y); + ASSERT_EQ(i, NodeSelfIterator::selfEnd(x_and_y)); + ASSERT_EQ(j, NodeSelfIterator::selfEnd(x_and_y)); + ASSERT_EQ(i, x_and_y.end()); + ASSERT_EQ(j, x_and_y.end()); + + i = x_and_y.begin(); + ASSERT_NE(i, x_and_y.end()); + ASSERT_EQ(*i, x); + ASSERT_EQ(*++i, y); + ASSERT_EQ(++i, x_and_y.end()); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h deleted file mode 100644 index 5fbdcc612..000000000 --- a/test/unit/expr/node_self_iterator_black.h +++ /dev/null @@ -1,75 +0,0 @@ -/********************* */ -/*! \file node_self_iterator_black.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway, Tim King - ** 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 CVC4::expr::NodeSelfIterator - ** - ** Black box testing of CVC4::expr::NodeSelfIterator - **/ - -#include - -#include "expr/node.h" -#include "expr/node_self_iterator.h" -#include "expr/node_builder.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::expr; -using namespace std; - -class NodeSelfIteratorBlack : public CxxTest::TestSuite { -private: - - NodeManager* d_nodeManager; - NodeManagerScope* d_scope; - TypeNode* d_booleanType; - TypeNode* d_realType; - - public: - void setUp() override - { - d_nodeManager = new NodeManager(NULL); - d_scope = new NodeManagerScope(d_nodeManager); - d_booleanType = new TypeNode(d_nodeManager->booleanType()); - d_realType = new TypeNode(d_nodeManager->realType()); - } - - void tearDown() override - { - delete d_booleanType; - delete d_scope; - delete d_nodeManager; - } - - void testSelfIteration() { - Node x = d_nodeManager->mkSkolem("x", *d_booleanType); - Node y = d_nodeManager->mkSkolem("y", *d_booleanType); - Node x_and_y = x.andNode(y); - NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y); - TS_ASSERT(i != x_and_y.end()); - TS_ASSERT(j != x_and_y.end()); - TS_ASSERT(*i == x_and_y); - TS_ASSERT(*j == x_and_y); - TS_ASSERT(*i++ == x_and_y); - TS_ASSERT(*j++ == x_and_y); - TS_ASSERT(i == NodeSelfIterator::selfEnd(x_and_y)); - TS_ASSERT(j == NodeSelfIterator::selfEnd(x_and_y)); - TS_ASSERT(i == x_and_y.end()); - TS_ASSERT(j == x_and_y.end()); - - i = x_and_y.begin(); - TS_ASSERT(i != x_and_y.end()); - TS_ASSERT(*i == x); - TS_ASSERT(*++i == y); - TS_ASSERT(++i == x_and_y.end()); - } - -}; -- 2.30.2