From 2ba8c852864ecb2eea3be2253fb80af1328de158 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 8 Feb 2021 12:03:05 -0800 Subject: [PATCH] google test: expr: Migrate node_white. (#5869) --- test/unit/expr/CMakeLists.txt | 2 +- test/unit/expr/node_white.cpp | 82 ++++++++++++++++++++++++++++ test/unit/expr/node_white.h | 100 ---------------------------------- test/unit/test_node.h | 1 - 4 files changed, 83 insertions(+), 102 deletions(-) create mode 100644 test/unit/expr/node_white.cpp delete mode 100644 test/unit/expr/node_white.h diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index d07945d79..18201b8a8 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -22,7 +22,7 @@ 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_traversal_black expr) -cvc4_add_cxx_unit_test_white(node_white expr) +cvc4_add_unit_test_white(node_white expr) cvc4_add_unit_test_black(symbol_table_black expr) cvc4_add_cxx_unit_test_black(type_cardinality_public expr) cvc4_add_cxx_unit_test_white(type_node_white expr) diff --git a/test/unit/expr/node_white.cpp b/test/unit/expr/node_white.cpp new file mode 100644 index 000000000..2581cb546 --- /dev/null +++ b/test/unit/expr/node_white.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file node_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters + ** 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 White box testing of CVC4::Node. + ** + ** White box testing of CVC4::Node. + **/ + +#include + +#include "base/check.h" +#include "test_node.h" + +namespace CVC4 { + +using namespace kind; +using namespace expr; + +namespace test { + +class TestNodeWhiteNode : public TestNodeWhite +{ +}; + +TEST_F(TestNodeWhiteNode, null) { ASSERT_EQ(Node::null(), Node::s_null); } + +TEST_F(TestNodeWhiteNode, copy_ctor) { Node e(Node::s_null); } + +TEST_F(TestNodeWhiteNode, builder) +{ + NodeBuilder<> b; + ASSERT_TRUE(b.d_nv->getId() == 0); + ASSERT_TRUE(b.d_nv->getKind() == UNDEFINED_KIND); + ASSERT_EQ(b.d_nv->d_nchildren, 0u); + /* etc. */ +} + +TEST_F(TestNodeWhiteNode, iterators) +{ + Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType()); + Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType()); + Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y); + Node two = d_nodeManager->mkConst(Rational(2)); + Node x_times_2 = d_nodeManager->mkNode(MULT, x, two); + + Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y); + + Node::iterator i; + + i = std::find(n.begin(), n.end(), x_plus_y); + ASSERT_TRUE(i != n.end()); + ASSERT_TRUE(*i == x_plus_y); + + i = std::find(n.begin(), n.end(), x); + ASSERT_TRUE(i == n.end()); + + i = std::find(x_times_2.begin(), x_times_2.end(), two); + ASSERT_TRUE(i != x_times_2.end()); + ASSERT_TRUE(*i == two); + + i = std::find(n.begin(), n.end(), y); + ASSERT_TRUE(i != n.end()); + ASSERT_TRUE(*i == y); + + std::vector v; + copy(n.begin(), n.end(), back_inserter(v)); + ASSERT_EQ(n.getNumChildren(), v.size()); + ASSERT_EQ(3, v.size()); + ASSERT_EQ(v[0], x_times_2); + ASSERT_EQ(v[1], x_plus_y); + ASSERT_EQ(v[2], y); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h deleted file mode 100644 index b435e1ce0..000000000 --- a/test/unit/expr/node_white.h +++ /dev/null @@ -1,100 +0,0 @@ -/********************* */ -/*! \file node_white.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Dejan Jovanovic - ** 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 White box testing of CVC4::Node. - ** - ** White box testing of CVC4::Node. - **/ - -#include - -#include - -#include "base/check.h" -#include "expr/node.h" -#include "expr/node_builder.h" -#include "expr/node_manager.h" -#include "expr/node_value.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::expr; -using namespace std; - -class NodeWhite : public CxxTest::TestSuite { - - NodeManager* d_nm; - NodeManagerScope* d_scope; - - public: - void setUp() override - { - d_nm = new NodeManager(NULL); - d_scope = new NodeManagerScope(d_nm); - } - - void tearDown() override - { - delete d_scope; - delete d_nm; - } - - void testNull() { - TS_ASSERT_EQUALS(Node::null(), Node::s_null); - } - - void testCopyCtor() { - Node e(Node::s_null); - } - - void testBuilder() { - NodeBuilder<> b; - TS_ASSERT(b.d_nv->getId() == 0); - TS_ASSERT(b.d_nv->getKind() == UNDEFINED_KIND); - TS_ASSERT_EQUALS(b.d_nv->d_nchildren, 0u); - /* etc. */ - } - - void testIterators() { - Node x = d_nm->mkVar("x", d_nm->integerType()); - Node y = d_nm->mkVar("y", d_nm->integerType()); - Node x_plus_y = d_nm->mkNode(PLUS, x, y); - Node two = d_nm->mkConst(Rational(2)); - Node x_times_2 = d_nm->mkNode(MULT, x, two); - - Node n = d_nm->mkNode(PLUS, x_times_2, x_plus_y, y); - - Node::iterator i; - - i = find(n.begin(), n.end(), x_plus_y); - TS_ASSERT(i != n.end()); - TS_ASSERT(*i == x_plus_y); - - i = find(n.begin(), n.end(), x); - TS_ASSERT(i == n.end()); - - i = find(x_times_2.begin(), x_times_2.end(), two); - TS_ASSERT(i != x_times_2.end()); - TS_ASSERT(*i == two); - - i = find(n.begin(), n.end(), y); - TS_ASSERT(i != n.end()); - TS_ASSERT(*i == y); - - vector v; - copy(n.begin(), n.end(), back_inserter(v)); - TS_ASSERT(n.getNumChildren() == v.size()); - TS_ASSERT(3 == v.size()); - TS_ASSERT(v[0] == x_times_2); - TS_ASSERT(v[1] == x_plus_y); - TS_ASSERT(v[2] == y); - } -}; diff --git a/test/unit/test_node.h b/test/unit/test_node.h index 6a68bcd00..82064c67a 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -57,7 +57,6 @@ class TestNodeWhite : public TestInternal std::unique_ptr d_scope; std::unique_ptr d_nodeManager; }; - } // namespace test } // namespace CVC4 #endif -- 2.30.2