GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/node_manager_black.cpp Lines: 210 210 100.0 %
Date: 2021-03-22 Branches: 651 2120 30.7 %

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