From 01210f43ba6f343784a76be5a1a16da55e4e25d6 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 5 Feb 2021 09:20:46 -0800 Subject: [PATCH] google test: expr: Migrate node_builder_black. (#5855) --- test/unit/expr/CMakeLists.txt | 2 +- test/unit/expr/node_builder_black.cpp | 590 ++++++++++++++++++++++++ test/unit/expr/node_builder_black.h | 626 -------------------------- test/unit/test_node.h | 6 +- 4 files changed, 595 insertions(+), 629 deletions(-) create mode 100644 test/unit/expr/node_builder_black.cpp delete mode 100644 test/unit/expr/node_builder_black.h diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index aa7e06ef0..442b2c7d3 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -17,7 +17,7 @@ cvc4_add_unit_test_black(kind_black expr) cvc4_add_unit_test_black(kind_map_black expr) cvc4_add_unit_test_black(node_black expr) cvc4_add_unit_test_black(node_algorithm_black expr) -cvc4_add_cxx_unit_test_black(node_builder_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_cxx_unit_test_black(node_self_iterator_black expr) diff --git a/test/unit/expr/node_builder_black.cpp b/test/unit/expr/node_builder_black.cpp new file mode 100644 index 000000000..3ba78950b --- /dev/null +++ b/test/unit/expr/node_builder_black.cpp @@ -0,0 +1,590 @@ +/********************* */ +/*! \file node_builder_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Tim King, 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 Black box testing of CVC4::NodeBuilder. + ** + ** Black box testing of CVC4::NodeBuilder. + **/ + +#include + +#include +#include + +#include "base/check.h" +#include "expr/kind.h" +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "test_node.h" +#include "util/rational.h" + +#define K 30u +#define LARGE_K UINT_MAX / 40 + +namespace CVC4 { + +using namespace CVC4::kind; + +namespace test { + +class TestNodeBuilderBlackNode : public TestNodeBlack +{ + protected: + template + void push_back(NodeBuilder& nb, uint32_t n) + { + for (uint32_t i = 0; i < n; ++i) + { + nb << d_nodeManager->mkConst(true); + } + } + Kind d_specKind = AND; +}; + +/** Tests just constructors. No modification is done to the node. */ +TEST_F(TestNodeBuilderBlackNode, ctors) +{ + /* Default size tests. */ + NodeBuilder<> def; + ASSERT_EQ(def.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(def.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(def.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder<> spec(d_specKind); + ASSERT_EQ(spec.getKind(), d_specKind); + ASSERT_EQ(spec.getNumChildren(), 0u); + ASSERT_EQ(spec.begin(), spec.end()); + + NodeBuilder<> from_nm(d_nodeManager.get()); + ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(from_nm.getNumChildren(), + "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder<> from_nm_kind(d_nodeManager.get(), d_specKind); + ASSERT_EQ(from_nm_kind.getKind(), d_specKind); + ASSERT_EQ(from_nm_kind.getNumChildren(), 0u); + ASSERT_EQ(from_nm_kind.begin(), from_nm_kind.end()); + + /* Non-default size tests */ + NodeBuilder ws; + ASSERT_EQ(ws.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder ws_kind(d_specKind); + ASSERT_EQ(ws_kind.getKind(), d_specKind); + ASSERT_EQ(ws_kind.getNumChildren(), 0u); + ASSERT_EQ(ws_kind.begin(), ws_kind.end()); + + NodeBuilder ws_from_nm(d_nodeManager.get()); + ASSERT_EQ(ws_from_nm.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(ws_from_nm.getNumChildren(), + "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(ws_from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(ws_from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder ws_from_nm_kind(d_nodeManager.get(), d_specKind); + ASSERT_EQ(ws_from_nm_kind.getKind(), d_specKind); + ASSERT_EQ(ws_from_nm_kind.getNumChildren(), 0u); + ASSERT_EQ(ws_from_nm_kind.begin(), ws_from_nm_kind.end()); + + /* Extreme size tests */ + NodeBuilder<0> ws_size_0; + + /* Allocating on the heap instead of the stack. */ + NodeBuilder* ws_size_large = new NodeBuilder; + delete ws_size_large; + + /* Copy constructors */ + NodeBuilder<> copy(def); + ASSERT_EQ(copy.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(copy.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(copy.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder cp_ws(ws); + ASSERT_EQ(cp_ws.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(cp_ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder cp_from_larger(ws); + ASSERT_EQ(cp_from_larger.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(cp_from_larger.getNumChildren(), + "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_from_larger.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_from_larger.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder cp_from_smaller(ws); + ASSERT_EQ(cp_from_smaller.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(cp_from_smaller.getNumChildren(), + "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_from_smaller.begin(), + "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_from_smaller.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif +} + +TEST_F(TestNodeBuilderBlackNode, dtor) +{ + NodeBuilder* nb = new NodeBuilder(); + delete nb; +} + +TEST_F(TestNodeBuilderBlackNode, begin_end) +{ + /* Test begin() and end() without resizing. */ + NodeBuilder ws(d_specKind); + ASSERT_EQ(ws.begin(), ws.end()); + + push_back(ws, K); + ASSERT_NE(ws.begin(), ws.end()); + + NodeBuilder::iterator iter = ws.begin(); + for (uint32_t i = 0; i < K; ++i) + { + ASSERT_NE(iter, ws.end()); + ++iter; + } + ASSERT_EQ(iter, ws.end()); + + NodeBuilder::const_iterator citer = ws.begin(); + for (uint32_t i = 0; i < K; ++i) + { + ASSERT_NE(citer, ws.end()); + ++citer; + } + ASSERT_EQ(citer, ws.end()); + + /* Repeat same tests and make sure that resizing occurs. */ + NodeBuilder<> smaller(d_specKind); + ASSERT_EQ(smaller.begin(), smaller.end()); + + push_back(smaller, K); + ASSERT_NE(smaller.begin(), smaller.end()); + + NodeBuilder<>::iterator smaller_iter = smaller.begin(); + for (uint32_t i = 0; i < K; ++i) + { + ASSERT_NE(smaller_iter, smaller.end()); + ++smaller_iter; + } + ASSERT_EQ(iter, ws.end()); + + NodeBuilder<>::const_iterator smaller_citer = smaller.begin(); + for (uint32_t i = 0; i < K; ++i) + { + ASSERT_NE(smaller_citer, smaller.end()); + ++smaller_citer; + } + ASSERT_EQ(smaller_citer, smaller.end()); +} + +TEST_F(TestNodeBuilderBlackNode, iterator) +{ + NodeBuilder<> b; + Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); + Node y = d_nodeManager->mkSkolem("z", *d_boolTypeNode); + Node z = d_nodeManager->mkSkolem("y", *d_boolTypeNode); + b << x << y << z << AND; + + { + NodeBuilder<>::iterator i = b.begin(); + ASSERT_EQ(*i++, x); + ASSERT_EQ(*i++, y); + ASSERT_EQ(*i++, z); + ASSERT_EQ(i, b.end()); + } + + { + const NodeBuilder<>& c = b; + NodeBuilder<>::const_iterator i = c.begin(); + ASSERT_EQ(*i++, x); + ASSERT_EQ(*i++, y); + ASSERT_EQ(*i++, z); + ASSERT_EQ(i, b.end()); + } +} + +TEST_F(TestNodeBuilderBlackNode, getKind) +{ + NodeBuilder<> noKind; + ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); + + Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode)); + noKind << x << x; + ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); + + noKind << PLUS; + + ASSERT_EQ(noKind.getKind(), PLUS); + + Node n = noKind; + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)"); +#endif + + NodeBuilder<> spec(PLUS); + ASSERT_EQ(spec.getKind(), PLUS); + spec << x << x; + ASSERT_EQ(spec.getKind(), PLUS); +} + +TEST_F(TestNodeBuilderBlackNode, getNumChildren) +{ + Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode)); + + NodeBuilder<> nb; +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + nb << PLUS << x << x; + + ASSERT_EQ(nb.getNumChildren(), 2u); + + nb << x << x; + ASSERT_EQ(nb.getNumChildren(), 4u); + + nb.clear(); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + nb.clear(PLUS); + ASSERT_EQ(nb.getNumChildren(), 0u); + nb << x << x << x; + + ASSERT_EQ(nb.getNumChildren(), 3u); + + nb << x << x << x; + ASSERT_EQ(nb.getNumChildren(), 6u); + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND"); + Node n = nb; + ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)"); +#endif +} + +TEST_F(TestNodeBuilderBlackNode, operator_square) +{ + NodeBuilder<> arr(d_specKind); + + Node i_0 = d_nodeManager->mkConst(false); + Node i_2 = d_nodeManager->mkConst(true); + Node i_K = d_nodeManager->mkNode(NOT, i_0); + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(arr[-1], "index out of range"); + ASSERT_DEATH(arr[0], "index out of range"); +#endif + + arr << i_0; + + ASSERT_EQ(arr[0], i_0); + + push_back(arr, 1); + + arr << i_2; + + ASSERT_EQ(arr[0], i_0); + ASSERT_EQ(arr[2], i_2); + + push_back(arr, K - 3); + + ASSERT_EQ(arr[0], i_0); + ASSERT_EQ(arr[2], i_2); + for (unsigned i = 3; i < K; ++i) + { + ASSERT_EQ(arr[i], d_nodeManager->mkConst(true)); + } + + arr << i_K; + + ASSERT_EQ(arr[0], i_0); + ASSERT_EQ(arr[2], i_2); + for (unsigned i = 3; i < K; ++i) + { + ASSERT_EQ(arr[i], d_nodeManager->mkConst(true)); + } + ASSERT_EQ(arr[K], i_K); + +#ifdef CVC4_ASSERTIONS + Node n = arr; + ASSERT_DEATH(arr[0], "!isUsed\\(\\)"); +#endif +} + +TEST_F(TestNodeBuilderBlackNode, clear) +{ + NodeBuilder<> nb; + + ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + nb << d_specKind; + push_back(nb, K); + + ASSERT_EQ(nb.getKind(), d_specKind); + ASSERT_EQ(nb.getNumChildren(), K); + ASSERT_NE(nb.begin(), nb.end()); + + nb.clear(); + + ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + nb << d_specKind; + push_back(nb, K); + + ASSERT_EQ(nb.getKind(), d_specKind); + ASSERT_EQ(nb.getNumChildren(), K); + ASSERT_NE(nb.begin(), nb.end()); + + nb.clear(d_specKind); + + ASSERT_EQ(nb.getKind(), d_specKind); + ASSERT_EQ(nb.getNumChildren(), 0u); + ASSERT_EQ(nb.begin(), nb.end()); + + push_back(nb, K); + nb.clear(); + + ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif +} + +TEST_F(TestNodeBuilderBlackNode, operator_stream_insertion_kind) +{ +#ifdef CVC4_ASSERTIONS + NodeBuilder<> spec(d_specKind); + ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder"); +#endif + + NodeBuilder<> noSpec; + noSpec << d_specKind; + ASSERT_EQ(noSpec.getKind(), d_specKind); + + NodeBuilder<> modified; + push_back(modified, K); + modified << d_specKind; + ASSERT_EQ(modified.getKind(), d_specKind); + + NodeBuilder<> nb(d_specKind); + nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false); + nb.clear(PLUS); + +#ifdef CVC4_ASSERTIONS + Node n; + ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children"); + nb.clear(PLUS); +#endif + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder"); +#endif + + NodeBuilder<> testRef; + ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind); + +#ifdef CVC4_ASSERTIONS + NodeBuilder<> testTwo; + ASSERT_DEATH(testTwo << d_specKind << PLUS, + "can't redefine the Kind of a NodeBuilder"); +#endif + + NodeBuilder<> testMixOrder1; + ASSERT_EQ( + (testMixOrder1 << d_specKind << d_nodeManager->mkConst(true)).getKind(), + d_specKind); + NodeBuilder<> testMixOrder2; + ASSERT_EQ( + (testMixOrder2 << d_nodeManager->mkConst(true) << d_specKind).getKind(), + d_specKind); +} + +TEST_F(TestNodeBuilderBlackNode, operator_stream_insertion_node) +{ + NodeBuilder nb(d_specKind); + ASSERT_EQ(nb.getKind(), d_specKind); + ASSERT_EQ(nb.getNumChildren(), 0u); + ASSERT_EQ(nb.begin(), nb.end()); + push_back(nb, K); + ASSERT_EQ(nb.getKind(), d_specKind); + ASSERT_EQ(nb.getNumChildren(), K); + ASSERT_NE(nb.begin(), nb.end()); + +#ifdef CVC4_ASSERTIONS + Node n = nb; + ASSERT_DEATH(nb << n, "!isUsed\\(\\)"); +#endif + + NodeBuilder<> overflow(d_specKind); + ASSERT_EQ(overflow.getKind(), d_specKind); + ASSERT_EQ(overflow.getNumChildren(), 0u); + ASSERT_EQ(overflow.begin(), overflow.end()); + + push_back(overflow, 5 * K + 1); + + ASSERT_EQ(overflow.getKind(), d_specKind); + ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1); + ASSERT_NE(overflow.begin(), overflow.end()); +} + +TEST_F(TestNodeBuilderBlackNode, append) +{ + Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); + Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode); + Node z = d_nodeManager->mkSkolem("z", *d_boolTypeNode); + Node m = d_nodeManager->mkNode(AND, y, z, x); + Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z); + Node o = d_nodeManager->mkNode(XOR, y, x); + + Node r = d_nodeManager->mkSkolem("r", *d_realTypeNode); + Node s = d_nodeManager->mkSkolem("s", *d_realTypeNode); + Node t = d_nodeManager->mkSkolem("t", *d_realTypeNode); + + Node p = d_nodeManager->mkNode( + EQUAL, + d_nodeManager->mkConst(0), + d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t)); + Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y)); + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(d_nodeManager->mkNode(XOR, y, x, x), + "Nodes with kind XOR must have at most 2 children"); +#endif + + NodeBuilder<> b(d_specKind); + + /* test append(TNode) */ + b.append(n).append(o).append(q); + + ASSERT_EQ(b.getNumChildren(), 3); + ASSERT_EQ(b[0], n); + ASSERT_EQ(b[1], o); + ASSERT_EQ(b[2], q); + + std::vector v; + v.push_back(m); + v.push_back(p); + v.push_back(q); + + /* test append(vector) */ + b.append(v); + + ASSERT_EQ(b.getNumChildren(), 6); + ASSERT_EQ(b[0], n); + ASSERT_EQ(b[1], o); + ASSERT_EQ(b[2], q); + ASSERT_EQ(b[3], m); + ASSERT_EQ(b[4], p); + ASSERT_EQ(b[5], q); + + /* test append(iterator, iterator) */ + b.append(v.rbegin(), v.rend()); + + ASSERT_EQ(b.getNumChildren(), 9); + ASSERT_EQ(b[0], n); + ASSERT_EQ(b[1], o); + ASSERT_EQ(b[2], q); + ASSERT_EQ(b[3], m); + ASSERT_EQ(b[4], p); + ASSERT_EQ(b[5], q); + ASSERT_EQ(b[6], q); + ASSERT_EQ(b[7], p); + ASSERT_EQ(b[8], m); +} + +TEST_F(TestNodeBuilderBlackNode, operator_node_cast) +{ + NodeBuilder implicit(d_specKind); + NodeBuilder explic(d_specKind); + + push_back(implicit, K); + push_back(explic, K); + + Node nimpl = implicit; + Node nexplicit = (Node)explic; + + ASSERT_EQ(nimpl.getKind(), d_specKind); + ASSERT_EQ(nimpl.getNumChildren(), K); + + ASSERT_EQ(nexplicit.getKind(), d_specKind); + ASSERT_EQ(nexplicit.getNumChildren(), K); + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)"); +#endif +} + +TEST_F(TestNodeBuilderBlackNode, leftist_building) +{ + NodeBuilder<> nb; + + Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode); + + Node b = d_nodeManager->mkSkolem("b", *d_boolTypeNode); + Node c = d_nodeManager->mkSkolem("c", *d_boolTypeNode); + + Node d = d_nodeManager->mkSkolem("d", *d_realTypeNode); + Node e = d_nodeManager->mkSkolem("e", *d_realTypeNode); + + nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE; + + Node n = nb; + ASSERT_EQ(n.getNumChildren(), 3u); + ASSERT_EQ(n.getType(), *d_realTypeNode); + ASSERT_EQ(n[0].getType(), *d_boolTypeNode); + ASSERT_EQ(n[1].getType(), *d_realTypeNode); + ASSERT_EQ(n[2].getType(), *d_realTypeNode); + + Node nota = d_nodeManager->mkNode(NOT, a); + Node nota_or_b_or_c = d_nodeManager->mkNode(OR, nota, b, c); + Node n0 = d_nodeManager->mkNode(AND, nota_or_b_or_c, c, a); + Node nexpected = d_nodeManager->mkNode(ITE, n0, d, e); + + ASSERT_EQ(nexpected, n); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h deleted file mode 100644 index 6c8fec461..000000000 --- a/test/unit/expr/node_builder_black.h +++ /dev/null @@ -1,626 +0,0 @@ -/********************* */ -/*! \file node_builder_black.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Mathias Preiner - ** 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::NodeBuilder. - ** - ** Black box testing of CVC4::NodeBuilder. - **/ - -#include - -#include -#include -#include - -#include "base/check.h" -#include "expr/kind.h" -#include "expr/node.h" -#include "expr/node_builder.h" -#include "expr/node_manager.h" -#include "test_utils.h" -#include "util/rational.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace std; - -class NodeBuilderBlack : public CxxTest::TestSuite { -private: - - NodeManager* d_nm; - NodeManagerScope* d_scope; - TypeNode* d_booleanType; - TypeNode* d_integerType; - TypeNode* d_realType; - - public: - void setUp() override - { - d_nm = new NodeManager(NULL); - d_scope = new NodeManagerScope(d_nm); - - specKind = AND; - d_integerType = new TypeNode(d_nm->integerType()); - d_booleanType = new TypeNode(d_nm->booleanType()); - d_realType = new TypeNode(d_nm->realType()); - } - - void tearDown() override - { - delete d_integerType; - delete d_booleanType; - delete d_realType; - delete d_scope; - delete d_nm; - } - - - template - void push_back(NodeBuilder& nb, int n){ - for(int i = 0; i < n; ++i){ - nb << d_nm->mkConst(true); - } - } - -#define K 30u -#define LARGE_K UINT_MAX / 40 - - Kind specKind; - - /** - * Tests just constructors. No modification is done to the node. - */ - void testNodeConstructors() { - - //inline NodeBuilder(); - //inline NodeBuilder(Kind k); - //inline NodeBuilder(const NodeBuilder& nb); - //template inline NodeBuilder(const NodeBuilder& nb); - //inline NodeBuilder(NodeManager* nm); - //inline NodeBuilder(NodeManager* nm, Kind k); - - /* default size tests */ - NodeBuilder<> def; - TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(def.getNumChildren()); - TS_UTILS_EXPECT_ABORT(def.begin()); - TS_UTILS_EXPECT_ABORT(def.end()); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder<> spec(specKind); - TS_ASSERT_EQUALS(spec.getKind(), specKind); - TS_ASSERT_EQUALS(spec.getNumChildren(), 0u); - TS_ASSERT_EQUALS(spec.begin(), spec.end()); - - - NodeBuilder<> from_nm(d_nm); - TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(from_nm.getNumChildren()); - TS_UTILS_EXPECT_ABORT(from_nm.begin()); - TS_UTILS_EXPECT_ABORT(from_nm.end()); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder<> from_nm_kind(d_nm, specKind); - TS_ASSERT_EQUALS(from_nm_kind.getKind(), specKind); - TS_ASSERT_EQUALS(from_nm_kind.getNumChildren(), 0u); - TS_ASSERT_EQUALS(from_nm_kind.begin(), from_nm_kind.end()); - - - /* Non-default size tests */ - - NodeBuilder ws; - TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(ws.getNumChildren()); - TS_UTILS_EXPECT_ABORT(ws.begin()); - TS_UTILS_EXPECT_ABORT(ws.end()); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder ws_kind(specKind); - TS_ASSERT_EQUALS(ws_kind.getKind(), specKind); - TS_ASSERT_EQUALS(ws_kind.getNumChildren(), 0u); - TS_ASSERT_EQUALS(ws_kind.begin(), ws_kind.end()); - - - NodeBuilder ws_from_nm(d_nm); - TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(ws_from_nm.getNumChildren()); - TS_UTILS_EXPECT_ABORT(ws_from_nm.begin()); - TS_UTILS_EXPECT_ABORT(ws_from_nm.end()); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder ws_from_nm_kind(d_nm, specKind); - TS_ASSERT_EQUALS(ws_from_nm_kind.getKind(), specKind); - TS_ASSERT_EQUALS(ws_from_nm_kind.getNumChildren(), 0u); - TS_ASSERT_EQUALS(ws_from_nm_kind.begin(), ws_from_nm_kind.end()); - - - /* Extreme size tests */ - NodeBuilder<0> ws_size_0; - - // Allocating on the heap instead of the stack. - NodeBuilder* ws_size_large = - new NodeBuilder; - delete ws_size_large; - - /* CopyConstructors */ - - NodeBuilder<> copy(def); - TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(copy.getNumChildren()); - TS_UTILS_EXPECT_ABORT(copy.begin()); - TS_UTILS_EXPECT_ABORT(copy.end()); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder cp_ws(ws); - TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(cp_ws.getNumChildren()); - TS_UTILS_EXPECT_ABORT(cp_ws.begin()); - TS_UTILS_EXPECT_ABORT(cp_ws.end()); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder cp_from_larger(ws); - TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(cp_from_larger.getNumChildren()); - TS_UTILS_EXPECT_ABORT(cp_from_larger.begin()); - TS_UTILS_EXPECT_ABORT(cp_from_larger.end()); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder cp_from_smaller(ws); - TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(cp_from_smaller.getNumChildren()); - TS_UTILS_EXPECT_ABORT(cp_from_smaller.begin()); - TS_UTILS_EXPECT_ABORT(cp_from_smaller.end()); -#endif /* CVC4_ASSERTIONS */ - } - - void testDestructor() { - //inline ~NodeBuilder(); - NodeBuilder* nb = new NodeBuilder(); - delete nb; - //Not sure what to test other than survival - } - - void testBeginEnd() { - /* Test begin and ends without resizing */ - NodeBuilder ws(specKind); - TS_ASSERT_EQUALS(ws.begin(), ws.end()); - - push_back(ws, K); - TS_ASSERT_DIFFERS(ws.begin(), ws.end()); - - NodeBuilder::iterator iter = ws.begin(); - for(unsigned i = 0; i < K; ++i){ - TS_ASSERT_DIFFERS(iter, ws.end()); - ++iter; - } - TS_ASSERT_EQUALS(iter, ws.end()); - - NodeBuilder::const_iterator citer = ws.begin(); - for(unsigned i = 0; i < K; ++i){ - TS_ASSERT_DIFFERS(citer, ws.end()); - ++citer; - } - TS_ASSERT_EQUALS(citer, ws.end()); - - /* Do the same tests and make sure that resizing occurs */ - - NodeBuilder<> smaller(specKind); - TS_ASSERT_EQUALS(smaller.begin(), smaller.end()); - - push_back(smaller, K); - TS_ASSERT_DIFFERS(smaller.begin(), smaller.end()); - - NodeBuilder<>::iterator smaller_iter = smaller.begin(); - for(unsigned i = 0; i < K; ++i){ - TS_ASSERT_DIFFERS(smaller_iter, smaller.end()); - ++smaller_iter; - } - TS_ASSERT_EQUALS(iter, ws.end()); - - NodeBuilder<>::const_iterator smaller_citer = smaller.begin(); - for(unsigned i = 0; i < K; ++i){ - TS_ASSERT_DIFFERS(smaller_citer, smaller.end()); - ++smaller_citer; - } - TS_ASSERT_EQUALS(smaller_citer, smaller.end()); - } - - void testIterator() { - NodeBuilder<> b; - Node x = d_nm->mkSkolem("x", *d_booleanType); - Node y = d_nm->mkSkolem("z", *d_booleanType); - Node z = d_nm->mkSkolem("y", *d_booleanType); - b << x << y << z << AND; - - { - NodeBuilder<>::iterator i = b.begin(); - TS_ASSERT(*i++ == x); - TS_ASSERT(*i++ == y); - TS_ASSERT(*i++ == z); - TS_ASSERT(i == b.end()); - } - - { - const NodeBuilder<>& c = b; - NodeBuilder<>::const_iterator i = c.begin(); - TS_ASSERT(*i++ == x); - TS_ASSERT(*i++ == y); - TS_ASSERT(*i++ == z); - TS_ASSERT(i == b.end()); - } - } - - void testGetKind() { - /* Kind getKind() const; */ - NodeBuilder<> noKind; - TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); - - Node x( d_nm->mkSkolem( "x", *d_integerType ) ); - noKind << x << x; - // push_back(noKind, K); - TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); - - noKind << PLUS; - - TS_ASSERT_EQUALS(noKind.getKind(), PLUS); - - Node n = noKind; - -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(noKind.getKind()); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder<> spec(PLUS); - TS_ASSERT_EQUALS(spec.getKind(), PLUS); - spec << x << x ; - TS_ASSERT_EQUALS(spec.getKind(), PLUS); - } - - void testGetNumChildren() { - /* unsigned getNumChildren() const; */ - Node x( d_nm->mkSkolem( "x", *d_integerType ) ); - - NodeBuilder<> nb; -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); -#endif /* CVC4_ASSERTIONS */ - nb << PLUS << x << x; - - TS_ASSERT_EQUALS(nb.getNumChildren(), 2u); - - nb << x << x; - TS_ASSERT_EQUALS(nb.getNumChildren(), 4u); - - Node n = nb;// avoid warning on clear() - nb.clear(); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); -#endif /* CVC4_ASSERTIONS */ - nb.clear(PLUS); - TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); - nb << x << x << x; - - TS_ASSERT_EQUALS(nb.getNumChildren(), 3u); - - nb << x << x << x; - TS_ASSERT_EQUALS(nb.getNumChildren(), 6u); - -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(nb << PLUS); - n = nb; - TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); -#endif /* CVC4_ASSERTIONS */ - } - - void testOperatorSquare() { - /* - Node operator[](int i) const { - TS_ASSERT(i >= 0 && i < d_ev->getNumChildren()); - return Node(d_ev->d_children[i]); - } - */ - NodeBuilder<> arr(specKind); - - Node i_0 = d_nm->mkConst(false); - Node i_2 = d_nm->mkConst(true); - Node i_K = d_nm->mkNode(NOT, i_0); - -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(arr[-1]); - TS_UTILS_EXPECT_ABORT(arr[0]); -#endif /* CVC4_ASSERTIONS */ - - arr << i_0; - - TS_ASSERT_EQUALS(arr[0], i_0); - - push_back(arr,1); - - arr << i_2; - - TS_ASSERT_EQUALS(arr[0], i_0); - TS_ASSERT_EQUALS(arr[2], i_2); - - push_back(arr, K - 3); - - TS_ASSERT_EQUALS(arr[0], i_0); - TS_ASSERT_EQUALS(arr[2], i_2); - for(unsigned i = 3; i < K; ++i) { - TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true)); - } - - arr << i_K; - - TS_ASSERT_EQUALS(arr[0], i_0); - TS_ASSERT_EQUALS(arr[2], i_2); - for(unsigned i = 3; i < K; ++i) { - TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true)); - } - TS_ASSERT_EQUALS(arr[K], i_K); - -#ifdef CVC4_ASSERTIONS - Node n = arr; - TS_UTILS_EXPECT_ABORT(arr[0]); -#endif /* CVC4_ASSERTIONS */ - } - - void testClear() { - /* void clear(Kind k = UNDEFINED_KIND); */ - NodeBuilder<> nb; - - TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); - TS_UTILS_EXPECT_ABORT(nb.begin()); - TS_UTILS_EXPECT_ABORT(nb.end()); -#endif /* CVC4_ASSERTIONS */ - - nb << specKind; - push_back(nb, K); - - TS_ASSERT_EQUALS(nb.getKind(), specKind); - TS_ASSERT_EQUALS(nb.getNumChildren(), K); - TS_ASSERT_DIFFERS(nb.begin(), nb.end()); - - Node n = nb;// avoid warning on clear() - nb.clear(); - - TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); - TS_UTILS_EXPECT_ABORT(nb.begin()); - TS_UTILS_EXPECT_ABORT(nb.end()); -#endif /* CVC4_ASSERTIONS */ - - nb << specKind; - push_back(nb, K); - - TS_ASSERT_EQUALS(nb.getKind(), specKind); - TS_ASSERT_EQUALS(nb.getNumChildren(), K); - TS_ASSERT_DIFFERS(nb.begin(), nb.end()); - - n = nb;// avoid warning on clear() - nb.clear(specKind); - - TS_ASSERT_EQUALS(nb.getKind(), specKind); - TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); - TS_ASSERT_EQUALS(nb.begin(), nb.end()); - - push_back(nb, K); - n = nb;// avoid warning on clear() - nb.clear(); - - TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); - TS_UTILS_EXPECT_ABORT(nb.begin()); - TS_UTILS_EXPECT_ABORT(nb.end()); -#endif /* CVC4_ASSERTIONS */ - } - - void testStreamInsertionKind() { - /* NodeBuilder& operator<<(const Kind& k); */ - -#ifdef CVC4_ASSERTIONS - NodeBuilder<> spec(specKind); - TS_UTILS_EXPECT_ABORT(spec << PLUS); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder<> noSpec; - noSpec << specKind; - TS_ASSERT_EQUALS(noSpec.getKind(), specKind); - - - NodeBuilder<> modified; - push_back(modified, K); - modified << specKind; - TS_ASSERT_EQUALS(modified.getKind(), specKind); - - NodeBuilder<> nb(specKind); - nb << d_nm->mkConst(true) << d_nm->mkConst(false); - Node n = nb;// avoid warning on clear() - nb.clear(PLUS); - -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(n = nb); - nb.clear(PLUS); -#endif /* CVC4_ASSERTIONS */ - -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(nb << PLUS); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder<> testRef; - TS_ASSERT_EQUALS((testRef << specKind).getKind(), specKind); - -#ifdef CVC4_ASSERTIONS - NodeBuilder<> testTwo; - TS_UTILS_EXPECT_ABORT(testTwo << specKind << PLUS); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder<> testMixOrder1; - TS_ASSERT_EQUALS((testMixOrder1 << specKind << d_nm->mkConst(true)).getKind(), - specKind); - NodeBuilder<> testMixOrder2; - TS_ASSERT_EQUALS((testMixOrder2 << d_nm->mkConst(true) << specKind).getKind(), - specKind); - } - - void testStreamInsertionNode() { - /* NodeBuilder& operator<<(const Node& n); */ - NodeBuilder nb(specKind); - TS_ASSERT_EQUALS(nb.getKind(), specKind); - TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); - TS_ASSERT_EQUALS(nb.begin(), nb.end()); - push_back(nb,K); - TS_ASSERT_EQUALS(nb.getKind(), specKind); - TS_ASSERT_EQUALS(nb.getNumChildren(), K); - TS_ASSERT_DIFFERS(nb.begin(), nb.end()); - -#ifdef CVC4_ASSERTIONS - Node n = nb; - TS_UTILS_EXPECT_ABORT(nb << n); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder<> overflow(specKind); - TS_ASSERT_EQUALS(overflow.getKind(), specKind); - TS_ASSERT_EQUALS(overflow.getNumChildren(), 0u); - TS_ASSERT_EQUALS(overflow.begin(), overflow.end()); - - push_back(overflow,5*K+1); - - TS_ASSERT_EQUALS(overflow.getKind(), specKind); - TS_ASSERT_EQUALS(overflow.getNumChildren(), 5 * K + 1); - TS_ASSERT_DIFFERS(overflow.begin(), overflow.end()); - - } - - void testAppend() { - Node x = d_nm->mkSkolem("x", *d_booleanType); - Node y = d_nm->mkSkolem("y", *d_booleanType); - Node z = d_nm->mkSkolem("z", *d_booleanType); - Node m = d_nm->mkNode(AND, y, z, x); - Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z); - Node o = d_nm->mkNode(XOR, y, x); - - Node r = d_nm->mkSkolem("r", *d_realType); - Node s = d_nm->mkSkolem("s", *d_realType); - Node t = d_nm->mkSkolem("t", *d_realType); - - Node p = d_nm->mkNode(EQUAL, d_nm->mkConst(0), - d_nm->mkNode(PLUS, r, d_nm->mkNode(UMINUS, s), t)); - Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y)); - -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(d_nm->mkNode(XOR, y, x, x)); -#endif /* CVC4_ASSERTIONS */ - - NodeBuilder<> b(specKind); - - // test append(TNode) - b.append(n).append(o).append(q); - - TS_ASSERT(b.getNumChildren() == 3); - TS_ASSERT(b[0] == n); - TS_ASSERT(b[1] == o); - TS_ASSERT(b[2] == q); - - vector v; - v.push_back(m); - v.push_back(p); - v.push_back(q); - // test append(vector) - b.append(v); - - TS_ASSERT(b.getNumChildren() == 6); - TS_ASSERT(b[0] == n); - TS_ASSERT(b[1] == o); - TS_ASSERT(b[2] == q); - TS_ASSERT(b[3] == m); - TS_ASSERT(b[4] == p); - TS_ASSERT(b[5] == q); - - // test append(iterator, iterator) - b.append(v.rbegin(), v.rend()); - - TS_ASSERT(b.getNumChildren() == 9); - TS_ASSERT(b[0] == n); - TS_ASSERT(b[1] == o); - TS_ASSERT(b[2] == q); - TS_ASSERT(b[3] == m); - TS_ASSERT(b[4] == p); - TS_ASSERT(b[5] == q); - TS_ASSERT(b[6] == q); - TS_ASSERT(b[7] == p); - TS_ASSERT(b[8] == m); - } - - void testOperatorNodeCast() { - /* operator Node();*/ - NodeBuilder implicit(specKind); - NodeBuilder explic(specKind); - - push_back(implicit, K); - push_back(explic, K); - - Node nimpl = implicit; - Node nexplicit = (Node) explic; - - TS_ASSERT_EQUALS(nimpl.getKind(), specKind); - TS_ASSERT_EQUALS(nimpl.getNumChildren(), K); - - TS_ASSERT_EQUALS(nexplicit.getKind(), specKind); - TS_ASSERT_EQUALS(nexplicit.getNumChildren(), K); - -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(Node blah = implicit); -#endif /* CVC4_ASSERTIONS */ - } - - void testLeftistBuilding() { - NodeBuilder<> nb; - - Node a = d_nm->mkSkolem("a", *d_booleanType); - - Node b = d_nm->mkSkolem("b", *d_booleanType); - Node c = d_nm->mkSkolem("c", *d_booleanType); - - Node d = d_nm->mkSkolem("d", *d_realType); - Node e = d_nm->mkSkolem("e", *d_realType); - - nb << a << NOT - << b << c << OR - << c << a << AND - << d << e << ITE; - - Node n = nb; - TS_ASSERT_EQUALS(n.getNumChildren(), 3u); - TS_ASSERT_EQUALS(n.getType(), *d_realType); - TS_ASSERT_EQUALS(n[0].getType(), *d_booleanType); - TS_ASSERT_EQUALS(n[1].getType(), *d_realType); - TS_ASSERT_EQUALS(n[2].getType(), *d_realType); - - Node nota = d_nm->mkNode(NOT, a); - Node nota_or_b_or_c = d_nm->mkNode(OR, nota, b, c); - Node n0 = d_nm->mkNode(AND, nota_or_b_or_c, c, a); - Node nexpected = d_nm->mkNode(ITE, n0, d, e); - - TS_ASSERT_EQUALS(nexpected, n); - } -}; diff --git a/test/unit/test_node.h b/test/unit/test_node.h index 774c9e4d0..3f2bfcc32 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -31,16 +31,18 @@ class TestNodeBlack : public TestInternal { d_nodeManager.reset(new NodeManager(nullptr)); d_scope.reset(new NodeManagerScope(d_nodeManager.get())); - d_intTypeNode.reset(new TypeNode(d_nodeManager->integerType())); d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType())); d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2))); + d_intTypeNode.reset(new TypeNode(d_nodeManager->integerType())); + d_realTypeNode.reset(new TypeNode(d_nodeManager->realType())); } std::unique_ptr d_scope; std::unique_ptr d_nodeManager; - std::unique_ptr d_intTypeNode; std::unique_ptr d_boolTypeNode; std::unique_ptr d_bvTypeNode; + std::unique_ptr d_intTypeNode; + std::unique_ptr d_realTypeNode; }; } // namespace test -- 2.30.2