Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/node/node_manager_black.cpp	Lines:	197	197	100.0 %
Date:	2021-09-16	Branches:	594	1950	30.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Dejan Jovanovic, 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::NodeManager.
 */

#include <string>
#include <vector>

#include "base/output.h"
#include "expr/node_manager.h"
#include "expr/node_manager_attributes.h"
#include "test_node.h"
#include "util/integer.h"
#include "util/rational.h"

namespace cvc5 {

using namespace kind;
using namespace expr;

namespace test {

class TestNodeBlackNodeManager : public TestNode
{
};

TEST_F(TestNodeBlackNodeManager, mkNode_not)
{
  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
  Node n = d_nodeManager->mkNode(NOT, x);
  ASSERT_EQ(n.getNumChildren(), 1u);
  ASSERT_EQ(n.getKind(), NOT);
  ASSERT_EQ(n[0], x);
}

TEST_F(TestNodeBlackNodeManager, mkNode_binary)
{
  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
  Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
  Node n = d_nodeManager->mkNode(IMPLIES, x, y);
  ASSERT_EQ(n.getNumChildren(), 2u);
  ASSERT_EQ(n.getKind(), IMPLIES);
  ASSERT_EQ(n[0], x);
  ASSERT_EQ(n[1], y);
}

TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
{
  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
  Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
  Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType());
  Node n = d_nodeManager->mkNode(AND, x, y, z);
  ASSERT_EQ(n.getNumChildren(), 3u);
  ASSERT_EQ(n.getKind(), AND);
  ASSERT_EQ(n[0], x);
  ASSERT_EQ(n[1], y);
  ASSERT_EQ(n[2], z);
}

TEST_F(TestNodeBlackNodeManager, mkNode_init_list)
{
  Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
  Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
  Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
  Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType());
  // Negate second argument to test the use of temporary nodes
  Node n = d_nodeManager->mkNode(AND, {x1, x2.negate(), x3, x4});
  ASSERT_EQ(n.getNumChildren(), 4u);
  ASSERT_EQ(n.getKind(), AND);
  ASSERT_EQ(n[0], x1);
  ASSERT_EQ(n[1], x2.negate());
  ASSERT_EQ(n[2], x3);
  ASSERT_EQ(n[3], x4);
}

TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
{
  Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
  Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
  Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
  std::vector<Node> args;
  args.push_back(x1);
  args.push_back(x2);
  args.push_back(x3);
  Node n = d_nodeManager->mkNode(AND, args);
  ASSERT_EQ(n.getNumChildren(), args.size());
  ASSERT_EQ(n.getKind(), AND);
  for (unsigned i = 0; i < args.size(); ++i)
  {
    ASSERT_EQ(n[i], args[i]);
  }
}

TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
{
  Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
  Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
  Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
  std::vector<TNode> args;
  args.push_back(x1);
  args.push_back(x2);
  args.push_back(x3);
  Node n = d_nodeManager->mkNode(AND, args);
  ASSERT_EQ(n.getNumChildren(), args.size());
  ASSERT_EQ(n.getKind(), AND);
  for (unsigned i = 0; i < args.size(); ++i)
  {
    ASSERT_EQ(n[i], args[i]);
  }
}

TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
{
  Node x = d_skolemManager->mkDummySkolem(
      "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
  ASSERT_EQ(x.getKind(), SKOLEM);
  ASSERT_EQ(x.getNumChildren(), 0u);
  ASSERT_EQ(x.getAttribute(VarNameAttr()), "x");
  ASSERT_EQ(x.getType(), *d_boolTypeNode);
}

TEST_F(TestNodeBlackNodeManager, mkConst_bool)
{
  Node tt = d_nodeManager->mkConst(true);
  ASSERT_EQ(tt.getConst<bool>(), true);
  Node ff = d_nodeManager->mkConst(false);
  ASSERT_EQ(ff.getConst<bool>(), false);
}

TEST_F(TestNodeBlackNodeManager, mkConst_rational)
{
  Rational r("3/2");
  Node n = d_nodeManager->mkConst(r);
  ASSERT_EQ(n.getConst<Rational>(), r);
}

TEST_F(TestNodeBlackNodeManager, hasOperator)
{
  ASSERT_TRUE(NodeManager::hasOperator(AND));
  ASSERT_TRUE(NodeManager::hasOperator(OR));
  ASSERT_TRUE(NodeManager::hasOperator(NOT));
  ASSERT_TRUE(NodeManager::hasOperator(APPLY_UF));
  ASSERT_TRUE(!NodeManager::hasOperator(VARIABLE));
}

TEST_F(TestNodeBlackNodeManager, booleanType)
{
  TypeNode t = d_nodeManager->booleanType();
  TypeNode t2 = d_nodeManager->booleanType();
  TypeNode t3 = d_nodeManager->mkSort("T");
  ASSERT_TRUE(t.isBoolean());
  ASSERT_FALSE(t.isFunction());
  ASSERT_FALSE(t.isNull());
  ASSERT_FALSE(t.isPredicate());
  ASSERT_FALSE(t.isSort());
  ASSERT_EQ(t, t2);
  ASSERT_NE(t, t3);

  TypeNode bt = t;
  ASSERT_EQ(bt, t);
}

TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool)
{
  TypeNode booleanType = d_nodeManager->booleanType();
  TypeNode t = d_nodeManager->mkFunctionType(booleanType, booleanType);
  TypeNode t2 = d_nodeManager->mkFunctionType(booleanType, booleanType);

  ASSERT_FALSE(t.isBoolean());
  ASSERT_TRUE(t.isFunction());
  ASSERT_FALSE(t.isNull());
  ASSERT_TRUE(t.isPredicate());
  ASSERT_FALSE(t.isSort());

  ASSERT_EQ(t, t2);

  TypeNode ft = t;
  ASSERT_EQ(ft, t);
  ASSERT_EQ(ft.getArgTypes().size(), 1u);
  ASSERT_EQ(ft.getArgTypes()[0], booleanType);
  ASSERT_EQ(ft.getRangeType(), booleanType);
}

TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type)
{
  TypeNode a = d_nodeManager->mkSort();
  TypeNode b = d_nodeManager->mkSort();
  TypeNode c = d_nodeManager->mkSort();

  std::vector<TypeNode> argTypes;
  argTypes.push_back(a);
  argTypes.push_back(b);

  TypeNode t = d_nodeManager->mkFunctionType(argTypes, c);
  TypeNode t2 = d_nodeManager->mkFunctionType(argTypes, c);

  ASSERT_FALSE(t.isBoolean());
  ASSERT_TRUE(t.isFunction());
  ASSERT_FALSE(t.isNull());
  ASSERT_FALSE(t.isPredicate());
  ASSERT_FALSE(t.isSort());

  ASSERT_EQ(t, t2);

  TypeNode ft = t;
  ASSERT_EQ(ft, t);
  ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
  ASSERT_EQ(ft.getArgTypes()[0], a);
  ASSERT_EQ(ft.getArgTypes()[1], b);
  ASSERT_EQ(ft.getRangeType(), c);
}

TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments)
{
  TypeNode a = d_nodeManager->mkSort();
  TypeNode b = d_nodeManager->mkSort();
  TypeNode c = d_nodeManager->mkSort();

  std::vector<TypeNode> types;
  types.push_back(a);
  types.push_back(b);
  types.push_back(c);

  TypeNode t = d_nodeManager->mkFunctionType(types);
  TypeNode t2 = d_nodeManager->mkFunctionType(types);

  ASSERT_FALSE(t.isBoolean());
  ASSERT_TRUE(t.isFunction());
  ASSERT_FALSE(t.isNull());
  ASSERT_FALSE(t.isPredicate());
  ASSERT_FALSE(t.isSort());

  ASSERT_EQ(t, t2);

  TypeNode ft = t;
  ASSERT_EQ(ft, t);
  ASSERT_EQ(ft.getArgTypes().size(), types.size() - 1);
  ASSERT_EQ(ft.getArgTypes()[0], a);
  ASSERT_EQ(ft.getArgTypes()[1], b);
  ASSERT_EQ(ft.getRangeType(), c);
}

TEST_F(TestNodeBlackNodeManager, mkPredicateType)
{
  TypeNode a = d_nodeManager->mkSort("a");
  TypeNode b = d_nodeManager->mkSort("b");
  TypeNode c = d_nodeManager->mkSort("c");
  TypeNode booleanType = d_nodeManager->booleanType();

  std::vector<TypeNode> argTypes;
  argTypes.push_back(a);
  argTypes.push_back(b);
  argTypes.push_back(c);

  TypeNode t = d_nodeManager->mkPredicateType(argTypes);
  TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);

  ASSERT_FALSE(t.isBoolean());
  ASSERT_TRUE(t.isFunction());
  ASSERT_FALSE(t.isNull());
  ASSERT_TRUE(t.isPredicate());
  ASSERT_FALSE(t.isSort());

  ASSERT_EQ(t, t2);

  TypeNode ft = t;
  ASSERT_EQ(ft, t);
  ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
  ASSERT_EQ(ft.getArgTypes()[0], a);
  ASSERT_EQ(ft.getArgTypes()[1], b);
  ASSERT_EQ(ft.getArgTypes()[2], c);
  ASSERT_EQ(ft.getRangeType(), booleanType);
}

/* This test is only valid if assertions are enabled. */
TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
{
#ifdef CVC5_ASSERTIONS
  Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
  ASSERT_DEATH(d_nodeManager->mkNode(AND, x),
               "Nodes with kind AND must have at least 2 children");
#endif
}

/* This test is only valid if assertions are enabled. */
TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
{
#ifdef CVC5_ASSERTIONS
  std::vector<Node> vars;
  const uint32_t max = metakind::getMaxArityForKind(AND);
  TypeNode boolType = d_nodeManager->booleanType();
  Node skolem_i = d_skolemManager->mkDummySkolem("i", boolType);
  Node skolem_j = d_skolemManager->mkDummySkolem("j", boolType);
  Node andNode = skolem_i.andNode(skolem_j);
  Node orNode = skolem_i.orNode(skolem_j);
  while (vars.size() <= max)
  {
    vars.push_back(andNode);
    vars.push_back(skolem_j);
    vars.push_back(orNode);
  }
  ASSERT_DEATH(d_nodeManager->mkNode(AND, vars), "toSize > d_nvMaxChildren");
#endif
}
}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Dejan Jovanovic, 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::NodeManager.
14		*/
15
16		#include <string>
17		#include <vector>
18
19		#include "base/output.h"
20		#include "expr/node_manager.h"
21		#include "expr/node_manager_attributes.h"
22		#include "test_node.h"
23		#include "util/integer.h"
24		#include "util/rational.h"
25
26		namespace cvc5 {
27
28		using namespace kind;
29		using namespace expr;
30
31		namespace test {
32
33	68	class TestNodeBlackNodeManager : public TestNode
34		{
35		};
36
37	26	TEST_F(TestNodeBlackNodeManager, mkNode_not)
38		{
39	4	Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
40	4	Node n = d_nodeManager->mkNode(NOT, x);
41	2	ASSERT_EQ(n.getNumChildren(), 1u);
42	2	ASSERT_EQ(n.getKind(), NOT);
43	2	ASSERT_EQ(n[0], x);
44		}
45
46	26	TEST_F(TestNodeBlackNodeManager, mkNode_binary)
47		{
48	4	Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
49	4	Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
50	4	Node n = d_nodeManager->mkNode(IMPLIES, x, y);
51	2	ASSERT_EQ(n.getNumChildren(), 2u);
52	2	ASSERT_EQ(n.getKind(), IMPLIES);
53	2	ASSERT_EQ(n[0], x);
54	2	ASSERT_EQ(n[1], y);
55		}
56
57	26	TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
58		{
59	4	Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
60	4	Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
61	4	Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType());
62	4	Node n = d_nodeManager->mkNode(AND, x, y, z);
63	2	ASSERT_EQ(n.getNumChildren(), 3u);
64	2	ASSERT_EQ(n.getKind(), AND);
65	2	ASSERT_EQ(n[0], x);
66	2	ASSERT_EQ(n[1], y);
67	2	ASSERT_EQ(n[2], z);
68		}
69
70	26	TEST_F(TestNodeBlackNodeManager, mkNode_init_list)
71		{
72	4	Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
73	4	Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
74	4	Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
75	4	Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType());
76		// Negate second argument to test the use of temporary nodes
77	4	Node n = d_nodeManager->mkNode(AND, {x1, x2.negate(), x3, x4});
78	2	ASSERT_EQ(n.getNumChildren(), 4u);
79	2	ASSERT_EQ(n.getKind(), AND);
80	2	ASSERT_EQ(n[0], x1);
81	2	ASSERT_EQ(n[1], x2.negate());
82	2	ASSERT_EQ(n[2], x3);
83	2	ASSERT_EQ(n[3], x4);
84		}
85
86	26	TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
87		{
88	4	Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
89	4	Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
90	4	Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
91	4	std::vector<Node> args;
92	2	args.push_back(x1);
93	2	args.push_back(x2);
94	2	args.push_back(x3);
95	4	Node n = d_nodeManager->mkNode(AND, args);
96	2	ASSERT_EQ(n.getNumChildren(), args.size());
97	2	ASSERT_EQ(n.getKind(), AND);
98	8	for (unsigned i = 0; i < args.size(); ++i)
99		{
100	6	ASSERT_EQ(n[i], args[i]);
101		}
102		}
103
104	26	TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
105		{
106	4	Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
107	4	Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
108	4	Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
109	4	std::vector<TNode> args;
110	2	args.push_back(x1);
111	2	args.push_back(x2);
112	2	args.push_back(x3);
113	4	Node n = d_nodeManager->mkNode(AND, args);
114	2	ASSERT_EQ(n.getNumChildren(), args.size());
115	2	ASSERT_EQ(n.getKind(), AND);
116	8	for (unsigned i = 0; i < args.size(); ++i)
117		{
118	6	ASSERT_EQ(n[i], args[i]);
119		}
120		}
121
122	26	TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
123		{
124	2	Node x = d_skolemManager->mkDummySkolem(
125	4	"x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
126	2	ASSERT_EQ(x.getKind(), SKOLEM);
127	2	ASSERT_EQ(x.getNumChildren(), 0u);
128	2	ASSERT_EQ(x.getAttribute(VarNameAttr()), "x");
129	2	ASSERT_EQ(x.getType(), *d_boolTypeNode);
130		}
131
132	26	TEST_F(TestNodeBlackNodeManager, mkConst_bool)
133		{
134	4	Node tt = d_nodeManager->mkConst(true);
135	2	ASSERT_EQ(tt.getConst<bool>(), true);
136	4	Node ff = d_nodeManager->mkConst(false);
137	2	ASSERT_EQ(ff.getConst<bool>(), false);
138		}
139
140	26	TEST_F(TestNodeBlackNodeManager, mkConst_rational)
141		{
142	4	Rational r("3/2");
143	4	Node n = d_nodeManager->mkConst(r);
144	2	ASSERT_EQ(n.getConst<Rational>(), r);
145		}
146
147	26	TEST_F(TestNodeBlackNodeManager, hasOperator)
148		{
149	2	ASSERT_TRUE(NodeManager::hasOperator(AND));
150	2	ASSERT_TRUE(NodeManager::hasOperator(OR));
151	2	ASSERT_TRUE(NodeManager::hasOperator(NOT));
152	2	ASSERT_TRUE(NodeManager::hasOperator(APPLY_UF));
153	2	ASSERT_TRUE(!NodeManager::hasOperator(VARIABLE));
154		}
155
156	26	TEST_F(TestNodeBlackNodeManager, booleanType)
157		{
158	4	TypeNode t = d_nodeManager->booleanType();
159	4	TypeNode t2 = d_nodeManager->booleanType();
160	4	TypeNode t3 = d_nodeManager->mkSort("T");
161	2	ASSERT_TRUE(t.isBoolean());
162	2	ASSERT_FALSE(t.isFunction());
163	2	ASSERT_FALSE(t.isNull());
164	2	ASSERT_FALSE(t.isPredicate());
165	2	ASSERT_FALSE(t.isSort());
166	2	ASSERT_EQ(t, t2);
167	2	ASSERT_NE(t, t3);
168
169	4	TypeNode bt = t;
170	2	ASSERT_EQ(bt, t);
171		}
172
173	26	TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool)
174		{
175	4	TypeNode booleanType = d_nodeManager->booleanType();
176	4	TypeNode t = d_nodeManager->mkFunctionType(booleanType, booleanType);
177	4	TypeNode t2 = d_nodeManager->mkFunctionType(booleanType, booleanType);
178
179	2	ASSERT_FALSE(t.isBoolean());
180	2	ASSERT_TRUE(t.isFunction());
181	2	ASSERT_FALSE(t.isNull());
182	2	ASSERT_TRUE(t.isPredicate());
183	2	ASSERT_FALSE(t.isSort());
184
185	2	ASSERT_EQ(t, t2);
186
187	4	TypeNode ft = t;
188	2	ASSERT_EQ(ft, t);
189	2	ASSERT_EQ(ft.getArgTypes().size(), 1u);
190	2	ASSERT_EQ(ft.getArgTypes()[0], booleanType);
191	2	ASSERT_EQ(ft.getRangeType(), booleanType);
192		}
193
194	26	TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type)
195		{
196	4	TypeNode a = d_nodeManager->mkSort();
197	4	TypeNode b = d_nodeManager->mkSort();
198	4	TypeNode c = d_nodeManager->mkSort();
199
200	4	std::vector<TypeNode> argTypes;
201	2	argTypes.push_back(a);
202	2	argTypes.push_back(b);
203
204	4	TypeNode t = d_nodeManager->mkFunctionType(argTypes, c);
205	4	TypeNode t2 = d_nodeManager->mkFunctionType(argTypes, c);
206
207	2	ASSERT_FALSE(t.isBoolean());
208	2	ASSERT_TRUE(t.isFunction());
209	2	ASSERT_FALSE(t.isNull());
210	2	ASSERT_FALSE(t.isPredicate());
211	2	ASSERT_FALSE(t.isSort());
212
213	2	ASSERT_EQ(t, t2);
214
215	4	TypeNode ft = t;
216	2	ASSERT_EQ(ft, t);
217	2	ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
218	2	ASSERT_EQ(ft.getArgTypes()[0], a);
219	2	ASSERT_EQ(ft.getArgTypes()[1], b);
220	2	ASSERT_EQ(ft.getRangeType(), c);
221		}
222
223	26	TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments)
224		{
225	4	TypeNode a = d_nodeManager->mkSort();
226	4	TypeNode b = d_nodeManager->mkSort();
227	4	TypeNode c = d_nodeManager->mkSort();
228
229	4	std::vector<TypeNode> types;
230	2	types.push_back(a);
231	2	types.push_back(b);
232	2	types.push_back(c);
233
234	4	TypeNode t = d_nodeManager->mkFunctionType(types);
235	4	TypeNode t2 = d_nodeManager->mkFunctionType(types);
236
237	2	ASSERT_FALSE(t.isBoolean());
238	2	ASSERT_TRUE(t.isFunction());
239	2	ASSERT_FALSE(t.isNull());
240	2	ASSERT_FALSE(t.isPredicate());
241	2	ASSERT_FALSE(t.isSort());
242
243	2	ASSERT_EQ(t, t2);
244
245	4	TypeNode ft = t;
246	2	ASSERT_EQ(ft, t);
247	2	ASSERT_EQ(ft.getArgTypes().size(), types.size() - 1);
248	2	ASSERT_EQ(ft.getArgTypes()[0], a);
249	2	ASSERT_EQ(ft.getArgTypes()[1], b);
250	2	ASSERT_EQ(ft.getRangeType(), c);
251		}
252
253	26	TEST_F(TestNodeBlackNodeManager, mkPredicateType)
254		{
255	4	TypeNode a = d_nodeManager->mkSort("a");
256	4	TypeNode b = d_nodeManager->mkSort("b");
257	4	TypeNode c = d_nodeManager->mkSort("c");
258	4	TypeNode booleanType = d_nodeManager->booleanType();
259
260	4	std::vector<TypeNode> argTypes;
261	2	argTypes.push_back(a);
262	2	argTypes.push_back(b);
263	2	argTypes.push_back(c);
264
265	4	TypeNode t = d_nodeManager->mkPredicateType(argTypes);
266	4	TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
267
268	2	ASSERT_FALSE(t.isBoolean());
269	2	ASSERT_TRUE(t.isFunction());
270	2	ASSERT_FALSE(t.isNull());
271	2	ASSERT_TRUE(t.isPredicate());
272	2	ASSERT_FALSE(t.isSort());
273
274	2	ASSERT_EQ(t, t2);
275
276	4	TypeNode ft = t;
277	2	ASSERT_EQ(ft, t);
278	2	ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
279	2	ASSERT_EQ(ft.getArgTypes()[0], a);
280	2	ASSERT_EQ(ft.getArgTypes()[1], b);
281	2	ASSERT_EQ(ft.getArgTypes()[2], c);
282	2	ASSERT_EQ(ft.getRangeType(), booleanType);
283		}
284
285		/* This test is only valid if assertions are enabled. */
286	26	TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
287		{
288		#ifdef CVC5_ASSERTIONS
289	4	Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
290	2	ASSERT_DEATH(d_nodeManager->mkNode(AND, x),
291		"Nodes with kind AND must have at least 2 children");
292		#endif
293		}
294
295		/* This test is only valid if assertions are enabled. */
296	26	TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
297		{
298		#ifdef CVC5_ASSERTIONS
299	4	std::vector<Node> vars;
300	2	const uint32_t max = metakind::getMaxArityForKind(AND);
301	4	TypeNode boolType = d_nodeManager->booleanType();
302	4	Node skolem_i = d_skolemManager->mkDummySkolem("i", boolType);
303	4	Node skolem_j = d_skolemManager->mkDummySkolem("j", boolType);
304	4	Node andNode = skolem_i.andNode(skolem_j);
305	4	Node orNode = skolem_i.orNode(skolem_j);
306	89478490	while (vars.size() <= max)
307		{
308	44739244	vars.push_back(andNode);
309	44739244	vars.push_back(skolem_j);
310	44739244	vars.push_back(orNode);
311		}
312	2	ASSERT_DEATH(d_nodeManager->mkNode(AND, vars), "toSize > d_nvMaxChildren");
313		#endif
314		}
315		} // namespace test
316	805453846	} // namespace cvc5