Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/node/node_builder_black.cpp	Lines:	223	223	100.0 %
Date:	2021-09-18	Branches:	909	3115	29.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Andres Noetzli, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * Black box testing of cvc5::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 cvc5 {

using namespace kind;

namespace test {

class TestNodeBlackNodeBuilder : public TestNode
{
 protected:
  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(TestNodeBlackNodeBuilder, ctors)
{
  /* Default size tests. */
  NodeBuilder def;
  ASSERT_EQ(def.getKind(), UNDEFINED_KIND);
#ifdef CVC5_ASSERTIONS
  ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
#endif

  NodeBuilder spec(d_specKind);
  ASSERT_EQ(spec.getKind(), d_specKind);
  ASSERT_EQ(spec.getNumChildren(), 0u);

  NodeBuilder from_nm(d_nodeManager);
  ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND);
#ifdef CVC5_ASSERTIONS
  ASSERT_DEATH(from_nm.getNumChildren(),
               "getKind\\(\\) != kind::UNDEFINED_KIND");
#endif

  NodeBuilder from_nm_kind(d_nodeManager, d_specKind);
  ASSERT_EQ(from_nm_kind.getKind(), d_specKind);
  ASSERT_EQ(from_nm_kind.getNumChildren(), 0u);

  /* Copy constructors */
  NodeBuilder copy(def);
  ASSERT_EQ(copy.getKind(), UNDEFINED_KIND);
#ifdef CVC5_ASSERTIONS
  ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
#endif
}

TEST_F(TestNodeBlackNodeBuilder, dtor)
{
  std::unique_ptr<NodeBuilder> nb(new NodeBuilder());
}

TEST_F(TestNodeBlackNodeBuilder, getKind)
{
  NodeBuilder noKind;
  ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);

  Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));
  noKind << x << x;
  ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);

  noKind << PLUS;
  ASSERT_EQ(noKind.getKind(), PLUS);

  Node n = noKind;
#ifdef CVC5_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(TestNodeBlackNodeBuilder, getNumChildren)
{
  Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));

  NodeBuilder nb;
#ifdef CVC5_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 CVC5_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 CVC5_ASSERTIONS
  ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND");
  Node n = nb;
  ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)");
#endif
}

TEST_F(TestNodeBlackNodeBuilder, 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 CVC5_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 CVC5_ASSERTIONS
  Node n = arr;
  ASSERT_DEATH(arr[0], "!isUsed\\(\\)");
#endif
}

TEST_F(TestNodeBlackNodeBuilder, clear)
{
  NodeBuilder nb;
  ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
#ifdef CVC5_ASSERTIONS
  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
#endif

  nb << d_specKind;
  push_back(nb, K);
  ASSERT_EQ(nb.getKind(), d_specKind);
  ASSERT_EQ(nb.getNumChildren(), K);

  nb.clear();
  ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
#ifdef CVC5_ASSERTIONS
  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
#endif

  nb << d_specKind;
  push_back(nb, K);
  ASSERT_EQ(nb.getKind(), d_specKind);
  ASSERT_EQ(nb.getNumChildren(), K);

  nb.clear(d_specKind);
  ASSERT_EQ(nb.getKind(), d_specKind);
  ASSERT_EQ(nb.getNumChildren(), 0u);

  push_back(nb, K);
  nb.clear();
  ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
#ifdef CVC5_ASSERTIONS
  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
#endif
}

TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
{
#ifdef CVC5_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 CVC5_ASSERTIONS
  Node n;
  ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children");
  nb.clear(PLUS);
#endif

#ifdef CVC5_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 CVC5_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(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
{
  NodeBuilder nb(d_specKind);
  ASSERT_EQ(nb.getKind(), d_specKind);
  ASSERT_EQ(nb.getNumChildren(), 0u);
  push_back(nb, K);
  ASSERT_EQ(nb.getKind(), d_specKind);
  ASSERT_EQ(nb.getNumChildren(), K);

#ifdef CVC5_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);

  push_back(overflow, 5 * K + 1);
  ASSERT_EQ(overflow.getKind(), d_specKind);
  ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1);
}

TEST_F(TestNodeBlackNodeBuilder, append)
{
  Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode);
  Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode);
  Node z = d_skolemManager->mkDummySkolem("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_skolemManager->mkDummySkolem("r", *d_realTypeNode);
  Node s = d_skolemManager->mkDummySkolem("s", *d_realTypeNode);
  Node t = d_skolemManager->mkDummySkolem("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 CVC5_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(TestNodeBlackNodeBuilder, 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 CVC5_ASSERTIONS
  ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)");
#endif
}

TEST_F(TestNodeBlackNodeBuilder, leftist_building)
{
  NodeBuilder nb;

  Node a = d_skolemManager->mkDummySkolem("a", *d_boolTypeNode);

  Node b = d_skolemManager->mkDummySkolem("b", *d_boolTypeNode);
  Node c = d_skolemManager->mkDummySkolem("c", *d_boolTypeNode);

  Node d = d_skolemManager->mkDummySkolem("d", *d_realTypeNode);
  Node e = d_skolemManager->mkDummySkolem("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 cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Andres Noetzli, Andrew Reynolds
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Black box testing of cvc5::NodeBuilder.
14		*/
15
16		#include <limits.h>
17
18		#include <sstream>
19		#include <vector>
20
21		#include "base/check.h"
22		#include "expr/kind.h"
23		#include "expr/node.h"
24		#include "expr/node_builder.h"
25		#include "expr/node_manager.h"
26		#include "test_node.h"
27		#include "util/rational.h"
28
29		#define K 30u
30		#define LARGE_K UINT_MAX / 40
31
32		namespace cvc5 {
33
34		using namespace kind;
35
36		namespace test {
37
38	44	class TestNodeBlackNodeBuilder : public TestNode
39		{
40		protected:
41	20	void push_back(NodeBuilder& nb, uint32_t n)
42		{
43	798	for (uint32_t i = 0; i < n; ++i)
44		{
45	778	nb << d_nodeManager->mkConst(true);
46		}
47	20	}
48		Kind d_specKind = AND;
49		};
50
51		/** Tests just constructors. No modification is done to the node. */
52	20	TEST_F(TestNodeBlackNodeBuilder, ctors)
53		{
54		/* Default size tests. */
55	4	NodeBuilder def;
56	2	ASSERT_EQ(def.getKind(), UNDEFINED_KIND);
57		#ifdef CVC5_ASSERTIONS
58	2	ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
59		#endif
60
61	4	NodeBuilder spec(d_specKind);
62	2	ASSERT_EQ(spec.getKind(), d_specKind);
63	2	ASSERT_EQ(spec.getNumChildren(), 0u);
64
65	4	NodeBuilder from_nm(d_nodeManager);
66	2	ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND);
67		#ifdef CVC5_ASSERTIONS
68	2	ASSERT_DEATH(from_nm.getNumChildren(),
69		"getKind\\(\\) != kind::UNDEFINED_KIND");
70		#endif
71
72	4	NodeBuilder from_nm_kind(d_nodeManager, d_specKind);
73	2	ASSERT_EQ(from_nm_kind.getKind(), d_specKind);
74	2	ASSERT_EQ(from_nm_kind.getNumChildren(), 0u);
75
76		/* Copy constructors */
77	4	NodeBuilder copy(def);
78	2	ASSERT_EQ(copy.getKind(), UNDEFINED_KIND);
79		#ifdef CVC5_ASSERTIONS
80	2	ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
81		#endif
82		}
83
84	20	TEST_F(TestNodeBlackNodeBuilder, dtor)
85		{
86	2	std::unique_ptr<NodeBuilder> nb(new NodeBuilder());
87	2	}
88
89	20	TEST_F(TestNodeBlackNodeBuilder, getKind)
90		{
91	4	NodeBuilder noKind;
92	2	ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
93
94	4	Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));
95	2	noKind << x << x;
96	2	ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
97
98	2	noKind << PLUS;
99	2	ASSERT_EQ(noKind.getKind(), PLUS);
100
101	4	Node n = noKind;
102		#ifdef CVC5_ASSERTIONS
103	2	ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)");
104		#endif
105
106	4	NodeBuilder spec(PLUS);
107	2	ASSERT_EQ(spec.getKind(), PLUS);
108	2	spec << x << x;
109	2	ASSERT_EQ(spec.getKind(), PLUS);
110		}
111
112	20	TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
113		{
114	4	Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));
115
116	4	NodeBuilder nb;
117		#ifdef CVC5_ASSERTIONS
118	2	ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
119		#endif
120
121	2	nb << PLUS << x << x;
122	2	ASSERT_EQ(nb.getNumChildren(), 2u);
123
124	2	nb << x << x;
125	2	ASSERT_EQ(nb.getNumChildren(), 4u);
126
127	2	nb.clear();
128		#ifdef CVC5_ASSERTIONS
129	2	ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
130		#endif
131
132	2	nb.clear(PLUS);
133	2	ASSERT_EQ(nb.getNumChildren(), 0u);
134
135	2	nb << x << x << x;
136	2	ASSERT_EQ(nb.getNumChildren(), 3u);
137
138	2	nb << x << x << x;
139	2	ASSERT_EQ(nb.getNumChildren(), 6u);
140
141		#ifdef CVC5_ASSERTIONS
142	2	ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND");
143	4	Node n = nb;
144	2	ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)");
145		#endif
146		}
147
148	20	TEST_F(TestNodeBlackNodeBuilder, operator_square)
149		{
150	4	NodeBuilder arr(d_specKind);
151
152	4	Node i_0 = d_nodeManager->mkConst(false);
153	4	Node i_2 = d_nodeManager->mkConst(true);
154	4	Node i_K = d_nodeManager->mkNode(NOT, i_0);
155
156		#ifdef CVC5_ASSERTIONS
157	2	ASSERT_DEATH(arr[-1], "index out of range");
158	2	ASSERT_DEATH(arr[0], "index out of range");
159		#endif
160
161	2	arr << i_0;
162	2	ASSERT_EQ(arr[0], i_0);
163
164	2	push_back(arr, 1);
165	2	arr << i_2;
166	2	ASSERT_EQ(arr[0], i_0);
167	2	ASSERT_EQ(arr[2], i_2);
168
169	2	push_back(arr, K - 3);
170	2	ASSERT_EQ(arr[0], i_0);
171	2	ASSERT_EQ(arr[2], i_2);
172	56	for (unsigned i = 3; i < K; ++i)
173		{
174	54	ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
175		}
176
177	2	arr << i_K;
178	2	ASSERT_EQ(arr[0], i_0);
179	2	ASSERT_EQ(arr[2], i_2);
180	56	for (unsigned i = 3; i < K; ++i)
181		{
182	54	ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
183		}
184	2	ASSERT_EQ(arr[K], i_K);
185
186		#ifdef CVC5_ASSERTIONS
187	4	Node n = arr;
188	2	ASSERT_DEATH(arr[0], "!isUsed\\(\\)");
189		#endif
190		}
191
192	20	TEST_F(TestNodeBlackNodeBuilder, clear)
193		{
194	4	NodeBuilder nb;
195	2	ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
196		#ifdef CVC5_ASSERTIONS
197	2	ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
198		#endif
199
200	2	nb << d_specKind;
201	2	push_back(nb, K);
202	2	ASSERT_EQ(nb.getKind(), d_specKind);
203	2	ASSERT_EQ(nb.getNumChildren(), K);
204
205	2	nb.clear();
206	2	ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
207		#ifdef CVC5_ASSERTIONS
208	2	ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
209		#endif
210
211	2	nb << d_specKind;
212	2	push_back(nb, K);
213	2	ASSERT_EQ(nb.getKind(), d_specKind);
214	2	ASSERT_EQ(nb.getNumChildren(), K);
215
216	2	nb.clear(d_specKind);
217	2	ASSERT_EQ(nb.getKind(), d_specKind);
218	2	ASSERT_EQ(nb.getNumChildren(), 0u);
219
220	2	push_back(nb, K);
221	2	nb.clear();
222	2	ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
223		#ifdef CVC5_ASSERTIONS
224	2	ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
225		#endif
226		}
227
228	20	TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
229		{
230		#ifdef CVC5_ASSERTIONS
231	4	NodeBuilder spec(d_specKind);
232	2	ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder");
233		#endif
234
235	4	NodeBuilder noSpec;
236	2	noSpec << d_specKind;
237	2	ASSERT_EQ(noSpec.getKind(), d_specKind);
238
239	4	NodeBuilder modified;
240	2	push_back(modified, K);
241	2	modified << d_specKind;
242	2	ASSERT_EQ(modified.getKind(), d_specKind);
243
244	4	NodeBuilder nb(d_specKind);
245	2	nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false);
246	2	nb.clear(PLUS);
247
248		#ifdef CVC5_ASSERTIONS
249	4	Node n;
250	2	ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children");
251	2	nb.clear(PLUS);
252		#endif
253
254		#ifdef CVC5_ASSERTIONS
255	2	ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder");
256		#endif
257
258	4	NodeBuilder testRef;
259	2	ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind);
260
261		#ifdef CVC5_ASSERTIONS
262	4	NodeBuilder testTwo;
263	2	ASSERT_DEATH(testTwo << d_specKind << PLUS,
264		"can't redefine the Kind of a NodeBuilder");
265		#endif
266
267	4	NodeBuilder testMixOrder1;
268	2	ASSERT_EQ(
269		(testMixOrder1 << d_specKind << d_nodeManager->mkConst(true)).getKind(),
270	2	d_specKind);
271	4	NodeBuilder testMixOrder2;
272	2	ASSERT_EQ(
273		(testMixOrder2 << d_nodeManager->mkConst(true) << d_specKind).getKind(),
274	2	d_specKind);
275		}
276
277	20	TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
278		{
279	4	NodeBuilder nb(d_specKind);
280	2	ASSERT_EQ(nb.getKind(), d_specKind);
281	2	ASSERT_EQ(nb.getNumChildren(), 0u);
282	2	push_back(nb, K);
283	2	ASSERT_EQ(nb.getKind(), d_specKind);
284	2	ASSERT_EQ(nb.getNumChildren(), K);
285
286		#ifdef CVC5_ASSERTIONS
287	4	Node n = nb;
288	2	ASSERT_DEATH(nb << n, "!isUsed\\(\\)");
289		#endif
290
291	4	NodeBuilder overflow(d_specKind);
292	2	ASSERT_EQ(overflow.getKind(), d_specKind);
293	2	ASSERT_EQ(overflow.getNumChildren(), 0u);
294
295	2	push_back(overflow, 5 * K + 1);
296	2	ASSERT_EQ(overflow.getKind(), d_specKind);
297	2	ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1);
298		}
299
300	20	TEST_F(TestNodeBlackNodeBuilder, append)
301		{
302	4	Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode);
303	4	Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode);
304	4	Node z = d_skolemManager->mkDummySkolem("z", *d_boolTypeNode);
305	4	Node m = d_nodeManager->mkNode(AND, y, z, x);
306	4	Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z);
307	4	Node o = d_nodeManager->mkNode(XOR, y, x);
308
309	4	Node r = d_skolemManager->mkDummySkolem("r", *d_realTypeNode);
310	4	Node s = d_skolemManager->mkDummySkolem("s", *d_realTypeNode);
311	4	Node t = d_skolemManager->mkDummySkolem("t", *d_realTypeNode);
312
313	2	Node p = d_nodeManager->mkNode(
314		EQUAL,
315	4	d_nodeManager->mkConst<Rational>(0),
316	8	d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t));
317	4	Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
318
319		#ifdef CVC5_ASSERTIONS
320	2	ASSERT_DEATH(d_nodeManager->mkNode(XOR, y, x, x),
321		"Nodes with kind XOR must have at most 2 children");
322		#endif
323
324	4	NodeBuilder b(d_specKind);
325
326		/* test append(TNode) */
327	2	b.append(n).append(o).append(q);
328
329	2	ASSERT_EQ(b.getNumChildren(), 3);
330	2	ASSERT_EQ(b[0], n);
331	2	ASSERT_EQ(b[1], o);
332	2	ASSERT_EQ(b[2], q);
333
334	4	std::vector<Node> v;
335	2	v.push_back(m);
336	2	v.push_back(p);
337	2	v.push_back(q);
338
339		/* test append(vector<Node>) */
340	2	b.append(v);
341
342	2	ASSERT_EQ(b.getNumChildren(), 6);
343	2	ASSERT_EQ(b[0], n);
344	2	ASSERT_EQ(b[1], o);
345	2	ASSERT_EQ(b[2], q);
346	2	ASSERT_EQ(b[3], m);
347	2	ASSERT_EQ(b[4], p);
348	2	ASSERT_EQ(b[5], q);
349
350		/* test append(iterator, iterator) */
351	2	b.append(v.rbegin(), v.rend());
352
353	2	ASSERT_EQ(b.getNumChildren(), 9);
354	2	ASSERT_EQ(b[0], n);
355	2	ASSERT_EQ(b[1], o);
356	2	ASSERT_EQ(b[2], q);
357	2	ASSERT_EQ(b[3], m);
358	2	ASSERT_EQ(b[4], p);
359	2	ASSERT_EQ(b[5], q);
360	2	ASSERT_EQ(b[6], q);
361	2	ASSERT_EQ(b[7], p);
362	2	ASSERT_EQ(b[8], m);
363		}
364
365	20	TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
366		{
367	4	NodeBuilder implicit(d_specKind);
368	4	NodeBuilder explic(d_specKind);
369
370	2	push_back(implicit, K);
371	2	push_back(explic, K);
372
373	4	Node nimpl = implicit;
374	4	Node nexplicit = (Node)explic;
375
376	2	ASSERT_EQ(nimpl.getKind(), d_specKind);
377	2	ASSERT_EQ(nimpl.getNumChildren(), K);
378
379	2	ASSERT_EQ(nexplicit.getKind(), d_specKind);
380	2	ASSERT_EQ(nexplicit.getNumChildren(), K);
381
382		#ifdef CVC5_ASSERTIONS
383	2	ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)");
384		#endif
385		}
386
387	20	TEST_F(TestNodeBlackNodeBuilder, leftist_building)
388		{
389	4	NodeBuilder nb;
390
391	4	Node a = d_skolemManager->mkDummySkolem("a", *d_boolTypeNode);
392
393	4	Node b = d_skolemManager->mkDummySkolem("b", *d_boolTypeNode);
394	4	Node c = d_skolemManager->mkDummySkolem("c", *d_boolTypeNode);
395
396	4	Node d = d_skolemManager->mkDummySkolem("d", *d_realTypeNode);
397	4	Node e = d_skolemManager->mkDummySkolem("e", *d_realTypeNode);
398
399	2	nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE;
400
401	4	Node n = nb;
402	2	ASSERT_EQ(n.getNumChildren(), 3u);
403	2	ASSERT_EQ(n.getType(), *d_realTypeNode);
404	2	ASSERT_EQ(n[0].getType(), *d_boolTypeNode);
405	2	ASSERT_EQ(n[1].getType(), *d_realTypeNode);
406	2	ASSERT_EQ(n[2].getType(), *d_realTypeNode);
407
408	4	Node nota = d_nodeManager->mkNode(NOT, a);
409	4	Node nota_or_b_or_c = d_nodeManager->mkNode(OR, nota, b, c);
410	4	Node n0 = d_nodeManager->mkNode(AND, nota_or_b_or_c, c, a);
411	4	Node nexpected = d_nodeManager->mkNode(ITE, n0, d, e);
412
413	2	ASSERT_EQ(nexpected, n);
414		}
415		} // namespace test
416	36	} // namespace cvc5