From: Aina Niemetz Date: Fri, 5 Feb 2021 20:11:54 +0000 (-0800) Subject: google test: expr: Migrate node_manager_white. (#5864) X-Git-Tag: cvc5-1.0.0~2316 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2bfc07aa99484fde9d86d27efd0bee48a26a8362;p=cvc5.git google test: expr: Migrate node_manager_white. (#5864) --- diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 442b2c7d3..89de279e0 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -19,7 +19,7 @@ cvc4_add_unit_test_black(node_black expr) 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_cxx_unit_test_white(node_manager_white expr) +cvc4_add_unit_test_white(node_manager_white expr) cvc4_add_cxx_unit_test_black(node_self_iterator_black expr) cvc4_add_cxx_unit_test_black(node_traversal_black expr) cvc4_add_cxx_unit_test_white(node_white expr) diff --git a/test/unit/expr/node_manager_white.cpp b/test/unit/expr/node_manager_white.cpp new file mode 100644 index 000000000..e7c9cf69d --- /dev/null +++ b/test/unit/expr/node_manager_white.cpp @@ -0,0 +1,84 @@ +/********************* */ +/*! \file node_manager_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Andres Noetzli + ** 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::NodeManager. + ** + ** White box testing of CVC4::NodeManager. + **/ + +#include + +#include "expr/node_manager.h" +#include "test_node.h" +#include "util/integer.h" +#include "util/rational.h" + +namespace CVC4 { + +using namespace CVC4::expr; + +namespace test { + +class TestNodeWhiteNodeManager : public TestNodeWhite +{ +}; + +TEST_F(TestNodeWhiteNodeManager, mkConst_rational) +{ + Rational i("3"); + Node n = d_nodeManager->mkConst(i); + Node m = d_nodeManager->mkConst(i); + ASSERT_EQ(n.getId(), m.getId()); +} + +TEST_F(TestNodeWhiteNodeManager, oversized_node_builder) +{ + NodeBuilder<> nb; + + ASSERT_NO_THROW(nb.realloc(15)); + ASSERT_NO_THROW(nb.realloc(25)); + ASSERT_NO_THROW(nb.realloc(256)); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.realloc(100), "toSize > d_nvMaxChildren"); +#endif /* CVC4_ASSERTIONS */ + ASSERT_NO_THROW(nb.realloc(257)); + ASSERT_NO_THROW(nb.realloc(4000)); + ASSERT_NO_THROW(nb.realloc(20000)); + ASSERT_NO_THROW(nb.realloc(60000)); + ASSERT_NO_THROW(nb.realloc(65535)); + ASSERT_NO_THROW(nb.realloc(65536)); + ASSERT_NO_THROW(nb.realloc(67108863)); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.realloc(67108863), "toSize > d_nvMaxChildren"); +#endif /* CVC4_ASSERTIONS */ +} + +TEST_F(TestNodeWhiteNodeManager, topological_sort) +{ + TypeNode boolType = d_nodeManager->booleanType(); + Node i = d_nodeManager->mkSkolem("i", boolType); + Node j = d_nodeManager->mkSkolem("j", boolType); + Node n1 = d_nodeManager->mkNode(kind::AND, j, j); + Node n2 = d_nodeManager->mkNode(kind::AND, i, n1); + + { + std::vector roots = {n1.d_nv}; + ASSERT_EQ(NodeManager::TopologicalSort(roots), roots); + } + + { + std::vector roots = {n2.d_nv, n1.d_nv}; + std::vector result = {n1.d_nv, n2.d_nv}; + ASSERT_EQ(NodeManager::TopologicalSort(roots), result); + } +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h deleted file mode 100644 index 3b2d451b0..000000000 --- a/test/unit/expr/node_manager_white.h +++ /dev/null @@ -1,94 +0,0 @@ -/********************* */ -/*! \file node_manager_white.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, 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 White box testing of CVC4::NodeManager. - ** - ** White box testing of CVC4::NodeManager. - **/ - -#include - -#include - -#include "expr/node_manager.h" -#include "test_utils.h" -#include "util/integer.h" -#include "util/rational.h" - -using namespace CVC4; -using namespace CVC4::expr; - -class NodeManagerWhite : 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 testMkConstRational() { - Rational i("3"); - Node n = d_nm->mkConst(i); - Node m = d_nm->mkConst(i); - TS_ASSERT_EQUALS(n.getId(), m.getId()); - } - - void testOversizedNodeBuilder() { - NodeBuilder<> nb; - - TS_ASSERT_THROWS_NOTHING(nb.realloc(15)); - TS_ASSERT_THROWS_NOTHING(nb.realloc(25)); - TS_ASSERT_THROWS_NOTHING(nb.realloc(256)); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(nb.realloc(100)); -#endif /* CVC4_ASSERTIONS */ - TS_ASSERT_THROWS_NOTHING(nb.realloc(257)); - TS_ASSERT_THROWS_NOTHING(nb.realloc(4000)); - TS_ASSERT_THROWS_NOTHING(nb.realloc(20000)); - TS_ASSERT_THROWS_NOTHING(nb.realloc(60000)); - TS_ASSERT_THROWS_NOTHING(nb.realloc(65535)); - TS_ASSERT_THROWS_NOTHING(nb.realloc(65536)); - TS_ASSERT_THROWS_NOTHING(nb.realloc(67108863)); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(nb.realloc(67108863)); -#endif /* CVC4_ASSERTIONS */ - } - - void testTopologicalSort() - { - TypeNode boolType = d_nm->booleanType(); - Node i = d_nm->mkSkolem("i", boolType); - Node j = d_nm->mkSkolem("j", boolType); - Node n1 = d_nm->mkNode(kind::AND, j, j); - Node n2 = d_nm->mkNode(kind::AND, i, n1); - - { - std::vector roots = {n1.d_nv}; - TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), roots); - } - - { - std::vector roots = {n2.d_nv, n1.d_nv}; - std::vector result = {n1.d_nv, n2.d_nv}; - TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), result); - } - } -}; diff --git a/test/unit/test_node.h b/test/unit/test_node.h index 3f2bfcc32..6a68bcd00 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -45,6 +45,19 @@ class TestNodeBlack : public TestInternal std::unique_ptr d_realTypeNode; }; +class TestNodeWhite : public TestInternal +{ + protected: + void SetUp() override + { + d_nodeManager.reset(new NodeManager(nullptr)); + d_scope.reset(new NodeManagerScope(d_nodeManager.get())); + } + + std::unique_ptr d_scope; + std::unique_ptr d_nodeManager; +}; + } // namespace test } // namespace CVC4 #endif