Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/node/node_manager_black.cpp	Lines:	211	211	100.0 %
Date:	2021-05-21	Branches:	651	2120	30.7 %


/******************************************************************************
 * 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_four_children)
{
  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());
  Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
  ASSERT_EQ(n.getNumChildren(), 4u);
  ASSERT_EQ(n.getKind(), AND);
  ASSERT_EQ(n[0], x1);
  ASSERT_EQ(n[1], x2);
  ASSERT_EQ(n[2], x3);
  ASSERT_EQ(n[3], x4);
}

TEST_F(TestNodeBlackNodeManager, mkNode_five_children)
{
  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());
  Node x5 = d_skolemManager->mkDummySkolem("x5", d_nodeManager->booleanType());
  Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
  ASSERT_EQ(n.getNumChildren(), 5u);
  ASSERT_EQ(n.getKind(), AND);
  ASSERT_EQ(n[0], x1);
  ASSERT_EQ(n[1], x2);
  ASSERT_EQ(n[2], x3);
  ASSERT_EQ(n[3], x4);
  ASSERT_EQ(n[4], x5);
}

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	72	class TestNodeBlackNodeManager : public TestNode
34		{
35		};
36
37	27	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	27	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	27	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	27	TEST_F(TestNodeBlackNodeManager, mkNode_four_children)
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	4	Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
77	2	ASSERT_EQ(n.getNumChildren(), 4u);
78	2	ASSERT_EQ(n.getKind(), AND);
79	2	ASSERT_EQ(n[0], x1);
80	2	ASSERT_EQ(n[1], x2);
81	2	ASSERT_EQ(n[2], x3);
82	2	ASSERT_EQ(n[3], x4);
83		}
84
85	27	TEST_F(TestNodeBlackNodeManager, mkNode_five_children)
86		{
87	4	Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
88	4	Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
89	4	Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
90	4	Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType());
91	4	Node x5 = d_skolemManager->mkDummySkolem("x5", d_nodeManager->booleanType());
92	4	Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
93	2	ASSERT_EQ(n.getNumChildren(), 5u);
94	2	ASSERT_EQ(n.getKind(), AND);
95	2	ASSERT_EQ(n[0], x1);
96	2	ASSERT_EQ(n[1], x2);
97	2	ASSERT_EQ(n[2], x3);
98	2	ASSERT_EQ(n[3], x4);
99	2	ASSERT_EQ(n[4], x5);
100		}
101
102	27	TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
103		{
104	4	Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
105	4	Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
106	4	Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
107	4	std::vector<Node> args;
108	2	args.push_back(x1);
109	2	args.push_back(x2);
110	2	args.push_back(x3);
111	4	Node n = d_nodeManager->mkNode(AND, args);
112	2	ASSERT_EQ(n.getNumChildren(), args.size());
113	2	ASSERT_EQ(n.getKind(), AND);
114	8	for (unsigned i = 0; i < args.size(); ++i)
115		{
116	6	ASSERT_EQ(n[i], args[i]);
117		}
118		}
119
120	27	TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
121		{
122	4	Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
123	4	Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
124	4	Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
125	4	std::vector<TNode> args;
126	2	args.push_back(x1);
127	2	args.push_back(x2);
128	2	args.push_back(x3);
129	4	Node n = d_nodeManager->mkNode(AND, args);
130	2	ASSERT_EQ(n.getNumChildren(), args.size());
131	2	ASSERT_EQ(n.getKind(), AND);
132	8	for (unsigned i = 0; i < args.size(); ++i)
133		{
134	6	ASSERT_EQ(n[i], args[i]);
135		}
136		}
137
138	27	TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
139		{
140	2	Node x = d_skolemManager->mkDummySkolem(
141	4	"x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
142	2	ASSERT_EQ(x.getKind(), SKOLEM);
143	2	ASSERT_EQ(x.getNumChildren(), 0u);
144	2	ASSERT_EQ(x.getAttribute(VarNameAttr()), "x");
145	2	ASSERT_EQ(x.getType(), *d_boolTypeNode);
146		}
147
148	27	TEST_F(TestNodeBlackNodeManager, mkConst_bool)
149		{
150	4	Node tt = d_nodeManager->mkConst(true);
151	2	ASSERT_EQ(tt.getConst<bool>(), true);
152	4	Node ff = d_nodeManager->mkConst(false);
153	2	ASSERT_EQ(ff.getConst<bool>(), false);
154		}
155
156	27	TEST_F(TestNodeBlackNodeManager, mkConst_rational)
157		{
158	4	Rational r("3/2");
159	4	Node n = d_nodeManager->mkConst(r);
160	2	ASSERT_EQ(n.getConst<Rational>(), r);
161		}
162
163	27	TEST_F(TestNodeBlackNodeManager, hasOperator)
164		{
165	2	ASSERT_TRUE(NodeManager::hasOperator(AND));
166	2	ASSERT_TRUE(NodeManager::hasOperator(OR));
167	2	ASSERT_TRUE(NodeManager::hasOperator(NOT));
168	2	ASSERT_TRUE(NodeManager::hasOperator(APPLY_UF));
169	2	ASSERT_TRUE(!NodeManager::hasOperator(VARIABLE));
170		}
171
172	27	TEST_F(TestNodeBlackNodeManager, booleanType)
173		{
174	4	TypeNode t = d_nodeManager->booleanType();
175	4	TypeNode t2 = d_nodeManager->booleanType();
176	4	TypeNode t3 = d_nodeManager->mkSort("T");
177	2	ASSERT_TRUE(t.isBoolean());
178	2	ASSERT_FALSE(t.isFunction());
179	2	ASSERT_FALSE(t.isNull());
180	2	ASSERT_FALSE(t.isPredicate());
181	2	ASSERT_FALSE(t.isSort());
182	2	ASSERT_EQ(t, t2);
183	2	ASSERT_NE(t, t3);
184
185	4	TypeNode bt = t;
186	2	ASSERT_EQ(bt, t);
187		}
188
189	27	TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool)
190		{
191	4	TypeNode booleanType = d_nodeManager->booleanType();
192	4	TypeNode t = d_nodeManager->mkFunctionType(booleanType, booleanType);
193	4	TypeNode t2 = d_nodeManager->mkFunctionType(booleanType, booleanType);
194
195	2	ASSERT_FALSE(t.isBoolean());
196	2	ASSERT_TRUE(t.isFunction());
197	2	ASSERT_FALSE(t.isNull());
198	2	ASSERT_TRUE(t.isPredicate());
199	2	ASSERT_FALSE(t.isSort());
200
201	2	ASSERT_EQ(t, t2);
202
203	4	TypeNode ft = t;
204	2	ASSERT_EQ(ft, t);
205	2	ASSERT_EQ(ft.getArgTypes().size(), 1u);
206	2	ASSERT_EQ(ft.getArgTypes()[0], booleanType);
207	2	ASSERT_EQ(ft.getRangeType(), booleanType);
208		}
209
210	27	TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type)
211		{
212	4	TypeNode a = d_nodeManager->mkSort();
213	4	TypeNode b = d_nodeManager->mkSort();
214	4	TypeNode c = d_nodeManager->mkSort();
215
216	4	std::vector<TypeNode> argTypes;
217	2	argTypes.push_back(a);
218	2	argTypes.push_back(b);
219
220	4	TypeNode t = d_nodeManager->mkFunctionType(argTypes, c);
221	4	TypeNode t2 = d_nodeManager->mkFunctionType(argTypes, c);
222
223	2	ASSERT_FALSE(t.isBoolean());
224	2	ASSERT_TRUE(t.isFunction());
225	2	ASSERT_FALSE(t.isNull());
226	2	ASSERT_FALSE(t.isPredicate());
227	2	ASSERT_FALSE(t.isSort());
228
229	2	ASSERT_EQ(t, t2);
230
231	4	TypeNode ft = t;
232	2	ASSERT_EQ(ft, t);
233	2	ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
234	2	ASSERT_EQ(ft.getArgTypes()[0], a);
235	2	ASSERT_EQ(ft.getArgTypes()[1], b);
236	2	ASSERT_EQ(ft.getRangeType(), c);
237		}
238
239	27	TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments)
240		{
241	4	TypeNode a = d_nodeManager->mkSort();
242	4	TypeNode b = d_nodeManager->mkSort();
243	4	TypeNode c = d_nodeManager->mkSort();
244
245	4	std::vector<TypeNode> types;
246	2	types.push_back(a);
247	2	types.push_back(b);
248	2	types.push_back(c);
249
250	4	TypeNode t = d_nodeManager->mkFunctionType(types);
251	4	TypeNode t2 = d_nodeManager->mkFunctionType(types);
252
253	2	ASSERT_FALSE(t.isBoolean());
254	2	ASSERT_TRUE(t.isFunction());
255	2	ASSERT_FALSE(t.isNull());
256	2	ASSERT_FALSE(t.isPredicate());
257	2	ASSERT_FALSE(t.isSort());
258
259	2	ASSERT_EQ(t, t2);
260
261	4	TypeNode ft = t;
262	2	ASSERT_EQ(ft, t);
263	2	ASSERT_EQ(ft.getArgTypes().size(), types.size() - 1);
264	2	ASSERT_EQ(ft.getArgTypes()[0], a);
265	2	ASSERT_EQ(ft.getArgTypes()[1], b);
266	2	ASSERT_EQ(ft.getRangeType(), c);
267		}
268
269	27	TEST_F(TestNodeBlackNodeManager, mkPredicateType)
270		{
271	4	TypeNode a = d_nodeManager->mkSort("a");
272	4	TypeNode b = d_nodeManager->mkSort("b");
273	4	TypeNode c = d_nodeManager->mkSort("c");
274	4	TypeNode booleanType = d_nodeManager->booleanType();
275
276	4	std::vector<TypeNode> argTypes;
277	2	argTypes.push_back(a);
278	2	argTypes.push_back(b);
279	2	argTypes.push_back(c);
280
281	4	TypeNode t = d_nodeManager->mkPredicateType(argTypes);
282	4	TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
283
284	2	ASSERT_FALSE(t.isBoolean());
285	2	ASSERT_TRUE(t.isFunction());
286	2	ASSERT_FALSE(t.isNull());
287	2	ASSERT_TRUE(t.isPredicate());
288	2	ASSERT_FALSE(t.isSort());
289
290	2	ASSERT_EQ(t, t2);
291
292	4	TypeNode ft = t;
293	2	ASSERT_EQ(ft, t);
294	2	ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
295	2	ASSERT_EQ(ft.getArgTypes()[0], a);
296	2	ASSERT_EQ(ft.getArgTypes()[1], b);
297	2	ASSERT_EQ(ft.getArgTypes()[2], c);
298	2	ASSERT_EQ(ft.getRangeType(), booleanType);
299		}
300
301		/* This test is only valid if assertions are enabled. */
302	27	TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
303		{
304		#ifdef CVC5_ASSERTIONS
305	4	Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
306	2	ASSERT_DEATH(d_nodeManager->mkNode(AND, x),
307		"Nodes with kind AND must have at least 2 children");
308		#endif
309		}
310
311		/* This test is only valid if assertions are enabled. */
312	27	TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
313		{
314		#ifdef CVC5_ASSERTIONS
315	4	std::vector<Node> vars;
316	2	const uint32_t max = metakind::getMaxArityForKind(AND);
317	4	TypeNode boolType = d_nodeManager->booleanType();
318	4	Node skolem_i = d_skolemManager->mkDummySkolem("i", boolType);
319	4	Node skolem_j = d_skolemManager->mkDummySkolem("j", boolType);
320	4	Node andNode = skolem_i.andNode(skolem_j);
321	4	Node orNode = skolem_i.orNode(skolem_j);
322	89478490	while (vars.size() <= max)
323		{
324	44739244	vars.push_back(andNode);
325	44739244	vars.push_back(skolem_j);
326	44739244	vars.push_back(orNode);
327		}
328	2	ASSERT_DEATH(d_nodeManager->mkNode(AND, vars), "toSize > d_nvMaxChildren");
329		#endif
330		}
331		} // namespace test
332	805460993	} // namespace cvc5