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)
--- /dev/null
+/********************* */
+/*! \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 <limits.h>
+
+#include <sstream>
+#include <vector>
+
+#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 <unsigned N>
+ void push_back(NodeBuilder<N>& 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<K> 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<K> 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<K> 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<K> 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<LARGE_K>* ws_size_large = new NodeBuilder<LARGE_K>;
+ 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<K> 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<K - 10> 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<K + 10> 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<K>* nb = new NodeBuilder<K>();
+ delete nb;
+}
+
+TEST_F(TestNodeBuilderBlackNode, begin_end)
+{
+ /* Test begin() and end() without resizing. */
+ NodeBuilder<K> ws(d_specKind);
+ ASSERT_EQ(ws.begin(), ws.end());
+
+ push_back(ws, K);
+ ASSERT_NE(ws.begin(), ws.end());
+
+ NodeBuilder<K>::iterator iter = ws.begin();
+ for (uint32_t i = 0; i < K; ++i)
+ {
+ ASSERT_NE(iter, ws.end());
+ ++iter;
+ }
+ ASSERT_EQ(iter, ws.end());
+
+ NodeBuilder<K>::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<K> 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<Rational>(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<Node> v;
+ v.push_back(m);
+ v.push_back(p);
+ v.push_back(q);
+
+ /* test append(vector<Node>) */
+ 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<K> implicit(d_specKind);
+ NodeBuilder<K> 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
+++ /dev/null
-/********************* */
-/*! \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 <cxxtest/TestSuite.h>
-
-#include <vector>
-#include <limits.h>
-#include <sstream>
-
-#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 <unsigned N>
- void push_back(NodeBuilder<N>& 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<nchild_thresh>& nb);
- //template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& 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<K> 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<K> 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<K> 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<K> 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<LARGE_K>* ws_size_large =
- new NodeBuilder<LARGE_K>;
- 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<K> 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<K-10> 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<K+10> 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<K>* nb = new NodeBuilder<K>();
- delete nb;
- //Not sure what to test other than survival
- }
-
- void testBeginEnd() {
- /* Test begin and ends without resizing */
- NodeBuilder<K> ws(specKind);
- TS_ASSERT_EQUALS(ws.begin(), ws.end());
-
- push_back(ws, K);
- TS_ASSERT_DIFFERS(ws.begin(), ws.end());
-
- NodeBuilder<K>::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<K>::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<K> 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<Rational>(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<Node> v;
- v.push_back(m);
- v.push_back(p);
- v.push_back(q);
- // test append(vector<Node>)
- 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<K> implicit(specKind);
- NodeBuilder<K> 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);
- }
-};
{
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<NodeManagerScope> d_scope;
std::unique_ptr<NodeManager> d_nodeManager;
- std::unique_ptr<TypeNode> d_intTypeNode;
std::unique_ptr<TypeNode> d_boolTypeNode;
std::unique_ptr<TypeNode> d_bvTypeNode;
+ std::unique_ptr<TypeNode> d_intTypeNode;
+ std::unique_ptr<TypeNode> d_realTypeNode;
};
} // namespace test
projects / cvc5.git / commitdiff