GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/node_black.cpp Lines: 446 447 99.8 %
Date: 2021-03-23 Branches: 1522 4513 33.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Morgan Deters, Andrew Reynolds
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::Node.
13
 **
14
 ** Black box testing of CVC4::Node.
15
 **/
16
17
#include <algorithm>
18
#include <sstream>
19
#include <string>
20
#include <vector>
21
22
#include "api/cvc4cpp.h"
23
#include "expr/dtype.h"
24
#include "expr/dtype_cons.h"
25
#include "expr/node.h"
26
#include "expr/node_builder.h"
27
#include "expr/node_manager.h"
28
#include "expr/node_value.h"
29
#include "smt/smt_engine.h"
30
#include "test_node.h"
31
#include "theory/rewriter.h"
32
33
namespace CVC4 {
34
35
using namespace kind;
36
37
namespace test {
38
39
namespace {
40
/** Returns N skolem nodes from 'nodeManager' with the same `type`. */
41
8
std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager,
42
                                   uint32_t n,
43
                                   TypeNode type)
44
{
45
8
  std::vector<Node> skolems;
46
32
  for (uint32_t i = 0; i < n; i++)
47
  {
48
24
    skolems.push_back(nodeManager->mkSkolem(
49
        "skolem_", type, "Created by makeNSkolemNodes()"));
50
  }
51
8
  return skolems;
52
}
53
}  // namespace
54
55
124
class TestNodeBlackNode : public TestNode
56
{
57
 protected:
58
62
  void SetUp() override
59
  {
60
62
    TestNode::SetUp();
61
    // setup an SMT engine so that options are in scope
62
124
    Options opts;
63
    char* argv[2];
64
62
    argv[0] = strdup("");
65
62
    argv[1] = strdup("--output-lang=ast");
66
62
    Options::parseOptions(&opts, 2, argv);
67
62
    free(argv[0]);
68
62
    free(argv[1]);
69
62
    d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
70
62
  }
71
72
  std::unique_ptr<SmtEngine> d_smt;
73
74
  bool imp(bool a, bool b) const { return (!a) || (b); }
75
18
  bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); }
76
77
1000
  void testNaryExpForSize(Kind k, uint32_t n)
78
  {
79
2000
    NodeBuilder<> nbz(k);
80
2000
    Node trueNode = d_nodeManager->mkConst(true);
81
514452
    for (uint32_t i = 0; i < n; ++i)
82
    {
83
513452
      nbz << trueNode;
84
    }
85
2000
    Node result = nbz;
86
1000
    ASSERT_EQ(n, result.getNumChildren());
87
  }
88
};
89
90
40
TEST_F(TestNodeBlackNode, null) { Node::null(); }
91
92
40
TEST_F(TestNodeBlackNode, is_null)
93
{
94
4
  Node a = Node::null();
95
2
  ASSERT_TRUE(a.isNull());
96
97
4
  Node b = Node();
98
2
  ASSERT_TRUE(b.isNull());
99
100
4
  Node c = b;
101
2
  ASSERT_TRUE(c.isNull());
102
}
103
104
40
TEST_F(TestNodeBlackNode, copy_ctor) { Node e(Node::null()); }
105
106
40
TEST_F(TestNodeBlackNode, dtor)
107
{
108
  /* No access to internals? Only test that this is crash free. */
109
2
  Node* n = nullptr;
110
2
  ASSERT_NO_FATAL_FAILURE(n = new Node());
111
2
  if (n)
112
  {
113
2
    delete n;
114
  }
115
}
116
117
/* operator== */
118
40
TEST_F(TestNodeBlackNode, operator_equals)
119
{
120
4
  Node a, b, c;
121
122
2
  b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
123
124
2
  a = b;
125
2
  c = a;
126
127
4
  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
128
129
2
  ASSERT_TRUE(a == a);
130
2
  ASSERT_TRUE(a == b);
131
2
  ASSERT_TRUE(a == c);
132
133
2
  ASSERT_TRUE(b == a);
134
2
  ASSERT_TRUE(b == b);
135
2
  ASSERT_TRUE(b == c);
136
137
2
  ASSERT_TRUE(c == a);
138
2
  ASSERT_TRUE(c == b);
139
2
  ASSERT_TRUE(c == c);
140
141
2
  ASSERT_TRUE(d == d);
142
143
2
  ASSERT_FALSE(d == a);
144
2
  ASSERT_FALSE(d == b);
145
2
  ASSERT_FALSE(d == c);
146
147
2
  ASSERT_FALSE(a == d);
148
2
  ASSERT_FALSE(b == d);
149
2
  ASSERT_FALSE(c == d);
150
}
151
152
/* operator!= */
153
40
TEST_F(TestNodeBlackNode, operator_not_equals)
154
{
155
4
  Node a, b, c;
156
157
2
  b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
158
159
2
  a = b;
160
2
  c = a;
161
162
4
  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
163
164
  /*structed assuming operator == works */
165
2
  ASSERT_TRUE(iff(a != a, !(a == a)));
166
2
  ASSERT_TRUE(iff(a != b, !(a == b)));
167
2
  ASSERT_TRUE(iff(a != c, !(a == c)));
168
169
2
  ASSERT_TRUE(iff(b != a, !(b == a)));
170
2
  ASSERT_TRUE(iff(b != b, !(b == b)));
171
2
  ASSERT_TRUE(iff(b != c, !(b == c)));
172
173
2
  ASSERT_TRUE(iff(c != a, !(c == a)));
174
2
  ASSERT_TRUE(iff(c != b, !(c == b)));
175
2
  ASSERT_TRUE(iff(c != c, !(c == c)));
176
177
2
  ASSERT_TRUE(!(d != d));
178
179
2
  ASSERT_TRUE(d != a);
180
2
  ASSERT_TRUE(d != b);
181
2
  ASSERT_TRUE(d != c);
182
}
183
184
/* operator[] */
185
40
TEST_F(TestNodeBlackNode, operator_square)
186
{
187
#ifdef CVC4_ASSERTIONS
188
  // Basic bounds check on a node w/out children
189
2
  ASSERT_DEATH(Node::null()[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
190
2
  ASSERT_DEATH(Node::null()[0], "i >= 0 && unsigned\\(i\\) < d_nchildren");
191
#endif
192
193
  // Basic access check
194
4
  Node tb = d_nodeManager->mkConst(true);
195
4
  Node eb = d_nodeManager->mkConst(false);
196
4
  Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
197
4
  Node ite = cnd.iteNode(tb, eb);
198
199
2
  ASSERT_EQ(tb, cnd[0]);
200
2
  ASSERT_EQ(eb, cnd[1]);
201
202
2
  ASSERT_EQ(cnd, ite[0]);
203
2
  ASSERT_EQ(tb, ite[1]);
204
2
  ASSERT_EQ(eb, ite[2]);
205
206
#ifdef CVC4_ASSERTIONS
207
  // Bounds check on a node with children
208
2
  ASSERT_DEATH(ite == ite[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
209
2
  ASSERT_DEATH(ite == ite[4], "i >= 0 && unsigned\\(i\\) < d_nchildren");
210
#endif
211
}
212
213
/* operator= */
214
40
TEST_F(TestNodeBlackNode, operator_assign)
215
{
216
4
  Node a, b;
217
  Node c = d_nodeManager->mkNode(
218
4
      NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
219
220
2
  b = c;
221
2
  ASSERT_EQ(b, c);
222
223
2
  a = b = c;
224
225
2
  ASSERT_EQ(a, b);
226
2
  ASSERT_EQ(a, c);
227
}
228
229
/* operator< */
230
40
TEST_F(TestNodeBlackNode, operator_less_than)
231
{
232
  // We don't have access to the ids so we can't test the implementation
233
  // in the black box tests.
234
235
4
  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
236
4
  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
237
238
2
  ASSERT_TRUE(a < b || b < a);
239
2
  ASSERT_TRUE(!(a < b && b < a));
240
241
4
  Node c = d_nodeManager->mkNode(AND, a, b);
242
4
  Node d = d_nodeManager->mkNode(AND, a, b);
243
244
2
  ASSERT_FALSE(c < d);
245
2
  ASSERT_FALSE(d < c);
246
247
  // simple test of descending descendant property
248
4
  Node child = d_nodeManager->mkConst(true);
249
4
  Node parent = d_nodeManager->mkNode(NOT, child);
250
251
2
  ASSERT_TRUE(child < parent);
252
253
  // slightly less simple test of DD property
254
4
  std::vector<Node> chain;
255
2
  const int N = 500;
256
4
  Node curr = d_nodeManager->mkNode(OR, a, b);
257
2
  chain.push_back(curr);
258
1002
  for (int i = 0; i < N; ++i)
259
  {
260
1000
    curr = d_nodeManager->mkNode(AND, curr, curr);
261
1000
    chain.push_back(curr);
262
  }
263
264
1002
  for (int i = 0; i < N; ++i)
265
  {
266
250500
    for (int j = i + 1; j < N; ++j)
267
    {
268
499000
      Node chain_i = chain[i];
269
499000
      Node chain_j = chain[j];
270
249500
      ASSERT_TRUE(chain_i < chain_j);
271
    }
272
  }
273
}
274
275
40
TEST_F(TestNodeBlackNode, eqNode)
276
{
277
4
  TypeNode t = d_nodeManager->mkSort();
278
4
  Node left = d_nodeManager->mkSkolem("left", t);
279
4
  Node right = d_nodeManager->mkSkolem("right", t);
280
4
  Node eq = left.eqNode(right);
281
282
2
  ASSERT_EQ(EQUAL, eq.getKind());
283
2
  ASSERT_EQ(2, eq.getNumChildren());
284
285
2
  ASSERT_EQ(eq[0], left);
286
2
  ASSERT_EQ(eq[1], right);
287
}
288
289
40
TEST_F(TestNodeBlackNode, notNode)
290
{
291
4
  Node child = d_nodeManager->mkConst(true);
292
4
  Node parent = child.notNode();
293
294
2
  ASSERT_EQ(NOT, parent.getKind());
295
2
  ASSERT_EQ(1, parent.getNumChildren());
296
297
2
  ASSERT_EQ(parent[0], child);
298
}
299
300
40
TEST_F(TestNodeBlackNode, andNode)
301
{
302
4
  Node left = d_nodeManager->mkConst(true);
303
4
  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
304
4
  Node eq = left.andNode(right);
305
306
2
  ASSERT_EQ(AND, eq.getKind());
307
2
  ASSERT_EQ(2, eq.getNumChildren());
308
309
2
  ASSERT_EQ(*(eq.begin()), left);
310
2
  ASSERT_EQ(*(++eq.begin()), right);
311
}
312
313
40
TEST_F(TestNodeBlackNode, orNode)
314
{
315
4
  Node left = d_nodeManager->mkConst(true);
316
4
  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
317
4
  Node eq = left.orNode(right);
318
319
2
  ASSERT_EQ(OR, eq.getKind());
320
2
  ASSERT_EQ(2, eq.getNumChildren());
321
322
2
  ASSERT_EQ(*(eq.begin()), left);
323
2
  ASSERT_EQ(*(++eq.begin()), right);
324
}
325
326
40
TEST_F(TestNodeBlackNode, iteNode)
327
{
328
4
  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
329
4
  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
330
331
4
  Node cnd = d_nodeManager->mkNode(OR, a, b);
332
4
  Node thenBranch = d_nodeManager->mkConst(true);
333
4
  Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
334
4
  Node ite = cnd.iteNode(thenBranch, elseBranch);
335
336
2
  ASSERT_EQ(ITE, ite.getKind());
337
2
  ASSERT_EQ(3, ite.getNumChildren());
338
339
2
  ASSERT_EQ(*(ite.begin()), cnd);
340
2
  ASSERT_EQ(*(++ite.begin()), thenBranch);
341
2
  ASSERT_EQ(*(++(++ite.begin())), elseBranch);
342
}
343
344
40
TEST_F(TestNodeBlackNode, iffNode)
345
{
346
4
  Node left = d_nodeManager->mkConst(true);
347
4
  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
348
4
  Node eq = left.eqNode(right);
349
350
2
  ASSERT_EQ(EQUAL, eq.getKind());
351
2
  ASSERT_EQ(2, eq.getNumChildren());
352
353
2
  ASSERT_EQ(*(eq.begin()), left);
354
2
  ASSERT_EQ(*(++eq.begin()), right);
355
}
356
357
40
TEST_F(TestNodeBlackNode, impNode)
358
{
359
4
  Node left = d_nodeManager->mkConst(true);
360
4
  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
361
4
  Node eq = left.impNode(right);
362
363
2
  ASSERT_EQ(IMPLIES, eq.getKind());
364
2
  ASSERT_EQ(2, eq.getNumChildren());
365
366
2
  ASSERT_EQ(*(eq.begin()), left);
367
2
  ASSERT_EQ(*(++eq.begin()), right);
368
}
369
370
40
TEST_F(TestNodeBlackNode, xorNode)
371
{
372
4
  Node left = d_nodeManager->mkConst(true);
373
4
  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
374
4
  Node eq = left.xorNode(right);
375
376
2
  ASSERT_EQ(XOR, eq.getKind());
377
2
  ASSERT_EQ(2, eq.getNumChildren());
378
379
2
  ASSERT_EQ(*(eq.begin()), left);
380
2
  ASSERT_EQ(*(++eq.begin()), right);
381
}
382
383
40
TEST_F(TestNodeBlackNode, getKind)
384
{
385
4
  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
386
4
  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
387
388
4
  Node n = d_nodeManager->mkNode(NOT, a);
389
2
  ASSERT_EQ(NOT, n.getKind());
390
391
2
  n = d_nodeManager->mkNode(EQUAL, a, b);
392
2
  ASSERT_EQ(EQUAL, n.getKind());
393
394
4
  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
395
4
  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
396
397
2
  n = d_nodeManager->mkNode(PLUS, x, y);
398
2
  ASSERT_EQ(PLUS, n.getKind());
399
400
2
  n = d_nodeManager->mkNode(UMINUS, x);
401
2
  ASSERT_EQ(UMINUS, n.getKind());
402
}
403
404
40
TEST_F(TestNodeBlackNode, getOperator)
405
{
406
4
  TypeNode sort = d_nodeManager->mkSort("T");
407
4
  TypeNode booleanType = d_nodeManager->booleanType();
408
4
  TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
409
410
4
  Node f = d_nodeManager->mkSkolem("f", predType);
411
4
  Node a = d_nodeManager->mkSkolem("a", sort);
412
4
  Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
413
414
2
  ASSERT_TRUE(fa.hasOperator());
415
2
  ASSERT_FALSE(f.hasOperator());
416
2
  ASSERT_FALSE(a.hasOperator());
417
418
2
  ASSERT_EQ(fa.getNumChildren(), 1);
419
2
  ASSERT_EQ(f.getNumChildren(), 0);
420
2
  ASSERT_EQ(a.getNumChildren(), 0);
421
422
2
  ASSERT_EQ(f, fa.getOperator());
423
#ifdef CVC4_ASSERTIONS
424
2
  ASSERT_DEATH(f.getOperator(), "mk == kind::metakind::PARAMETERIZED");
425
2
  ASSERT_DEATH(a.getOperator(), "mk == kind::metakind::PARAMETERIZED");
426
#endif
427
}
428
429
40
TEST_F(TestNodeBlackNode, getNumChildren)
430
{
431
4
  Node trueNode = d_nodeManager->mkConst(true);
432
433
2
  ASSERT_EQ(0, (Node::null()).getNumChildren());
434
2
  ASSERT_EQ(1, trueNode.notNode().getNumChildren());
435
2
  ASSERT_EQ(2, trueNode.andNode(trueNode).getNumChildren());
436
437
2
  srand(0);
438
1002
  for (uint32_t i = 0; i < 500; ++i)
439
  {
440
1000
    uint32_t n = rand() % 1000 + 2;
441
1000
    testNaryExpForSize(AND, n);
442
  }
443
444
#ifdef CVC4_ASSERTIONS
445
2
  ASSERT_DEATH(testNaryExpForSize(AND, 0),
446
               "getNumChildren\\(\\) >= "
447
               "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
448
2
  ASSERT_DEATH(testNaryExpForSize(AND, 1),
449
               "getNumChildren\\(\\) >= "
450
               "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
451
2
  ASSERT_DEATH(testNaryExpForSize(NOT, 0),
452
               "getNumChildren\\(\\) >= "
453
               "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
454
2
  ASSERT_DEATH(testNaryExpForSize(NOT, 2),
455
               "getNumChildren\\(\\) <= "
456
               "kind::metakind::getMaxArityForKind\\(getKind\\(\\)\\)");
457
#endif /* CVC4_ASSERTIONS */
458
}
459
460
40
TEST_F(TestNodeBlackNode, iterator)
461
{
462
4
  NodeBuilder<> b;
463
4
  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
464
4
  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
465
4
  Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
466
4
  Node n = b << x << y << z << kind::AND;
467
468
  {  // iterator
469
2
    Node::iterator i = n.begin();
470
2
    ASSERT_EQ(*i++, x);
471
2
    ASSERT_EQ(*i++, y);
472
2
    ASSERT_EQ(*i++, z);
473
2
    ASSERT_EQ(i, n.end());
474
  }
475
476
  {  // same for const iterator
477
2
    const Node& c = n;
478
2
    Node::const_iterator i = c.begin();
479
2
    ASSERT_EQ(*i++, x);
480
2
    ASSERT_EQ(*i++, y);
481
2
    ASSERT_EQ(*i++, z);
482
2
    ASSERT_EQ(i, n.end());
483
  }
484
}
485
486
40
TEST_F(TestNodeBlackNode, kinded_iterator)
487
{
488
4
  TypeNode integerType = d_nodeManager->integerType();
489
490
4
  Node x = d_nodeManager->mkSkolem("x", integerType);
491
4
  Node y = d_nodeManager->mkSkolem("y", integerType);
492
4
  Node z = d_nodeManager->mkSkolem("z", integerType);
493
4
  Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
494
4
  Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
495
496
  {  // iterator
497
4
    Node::kinded_iterator i = plus_x_y_z.begin(PLUS);
498
2
    ASSERT_EQ(*i++, x);
499
2
    ASSERT_EQ(*i++, y);
500
2
    ASSERT_EQ(*i++, z);
501
2
    ASSERT_TRUE(i == plus_x_y_z.end(PLUS));
502
503
2
    i = x.begin(PLUS);
504
2
    ASSERT_EQ(*i++, x);
505
2
    ASSERT_TRUE(i == x.end(PLUS));
506
  }
507
}
508
509
40
TEST_F(TestNodeBlackNode, toString)
510
{
511
4
  TypeNode booleanType = d_nodeManager->booleanType();
512
513
  Node w = d_nodeManager->mkSkolem(
514
4
      "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
515
  Node x = d_nodeManager->mkSkolem(
516
4
      "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
517
  Node y = d_nodeManager->mkSkolem(
518
4
      "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
519
  Node z = d_nodeManager->mkSkolem(
520
4
      "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
521
4
  Node m = NodeBuilder<>() << w << x << kind::OR;
522
4
  Node n = NodeBuilder<>() << m << y << z << kind::AND;
523
524
2
  ASSERT_EQ(n.toString(), "(AND (OR w x) y z)");
525
}
526
527
40
TEST_F(TestNodeBlackNode, toStream)
528
{
529
4
  TypeNode booleanType = d_nodeManager->booleanType();
530
531
  Node w = d_nodeManager->mkSkolem(
532
4
      "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
533
  Node x = d_nodeManager->mkSkolem(
534
4
      "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
535
  Node y = d_nodeManager->mkSkolem(
536
4
      "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
537
  Node z = d_nodeManager->mkSkolem(
538
4
      "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
539
4
  Node m = NodeBuilder<>() << x << y << kind::OR;
540
4
  Node n = NodeBuilder<>() << w << m << z << kind::AND;
541
4
  Node o = NodeBuilder<>() << n << n << kind::XOR;
542
543
4
  std::stringstream sstr;
544
2
  sstr << Node::dag(false);
545
2
  n.toStream(sstr);
546
2
  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
547
548
2
  sstr.str(std::string());
549
2
  o.toStream(sstr, -1, 0);
550
2
  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
551
552
2
  sstr.str(std::string());
553
2
  sstr << n;
554
2
  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
555
556
2
  sstr.str(std::string());
557
2
  sstr << o;
558
2
  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
559
560
2
  sstr.str(std::string());
561
2
  sstr << Node::setdepth(0) << n;
562
2
  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
563
564
2
  sstr.str(std::string());
565
2
  sstr << Node::setdepth(0) << o;
566
2
  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
567
568
2
  sstr.str(std::string());
569
2
  sstr << Node::setdepth(1) << n;
570
2
  ASSERT_EQ(sstr.str(), "(AND w (OR (...) (...)) z)");
571
572
2
  sstr.str(std::string());
573
2
  sstr << Node::setdepth(1) << o;
574
2
  ASSERT_EQ(sstr.str(),
575
2
            "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))");
576
577
2
  sstr.str(std::string());
578
2
  sstr << Node::setdepth(2) << n;
579
2
  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
580
581
2
  sstr.str(std::string());
582
2
  sstr << Node::setdepth(2) << o;
583
2
  ASSERT_EQ(sstr.str(),
584
2
            "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))");
585
586
2
  sstr.str(std::string());
587
2
  sstr << Node::setdepth(3) << n;
588
2
  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
589
590
2
  sstr.str(std::string());
591
2
  sstr << Node::setdepth(3) << o;
592
2
  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
593
}
594
595
40
TEST_F(TestNodeBlackNode, dagifier)
596
{
597
4
  TypeNode intType = d_nodeManager->integerType();
598
4
  TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
599
600
  Node x =
601
4
      d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
602
  Node y =
603
4
      d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
604
  Node f =
605
4
      d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
606
  Node g =
607
4
      d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
608
4
  Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
609
4
  Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
610
4
  Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
611
4
  Node gy = d_nodeManager->mkNode(APPLY_UF, g, y);
612
4
  Node fgx = d_nodeManager->mkNode(APPLY_UF, f, gx);
613
4
  Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx);
614
4
  Node fffx = d_nodeManager->mkNode(APPLY_UF, f, ffx);
615
4
  Node fffx_eq_x = d_nodeManager->mkNode(EQUAL, fffx, x);
616
4
  Node fffx_eq_y = d_nodeManager->mkNode(EQUAL, fffx, y);
617
4
  Node fx_eq_gx = d_nodeManager->mkNode(EQUAL, fx, gx);
618
4
  Node x_eq_y = d_nodeManager->mkNode(EQUAL, x, y);
619
4
  Node fgx_eq_gy = d_nodeManager->mkNode(EQUAL, fgx, gy);
620
621
  Node n = d_nodeManager->mkNode(
622
4
      OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy);
623
624
4
  std::stringstream sstr;
625
2
  sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4);
626
2
  sstr << Node::dag(false) << n;  // never dagify
627
2
  ASSERT_EQ(sstr.str(),
628
            "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = "
629
2
            "y) OR (f(g(x)) = g(y))");
630
}
631
632
40
TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node)
633
{
634
  const std::vector<Node> skolems =
635
4
      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
636
4
  Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
637
4
  std::vector<Node> children;
638
8
  for (Node child : add)
639
  {
640
6
    children.push_back(child);
641
  }
642
2
  ASSERT_TRUE(children.size() == skolems.size()
643
2
              && std::equal(children.begin(), children.end(), skolems.begin()));
644
}
645
646
40
TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode)
647
{
648
  const std::vector<Node> skolems =
649
4
      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
650
4
  Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
651
4
  std::vector<TNode> children;
652
8
  for (TNode child : add)
653
  {
654
6
    children.push_back(child);
655
  }
656
2
  ASSERT_TRUE(children.size() == skolems.size()
657
2
              && std::equal(children.begin(), children.end(), skolems.begin()));
658
}
659
660
40
TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node)
661
{
662
  const std::vector<Node> skolems =
663
4
      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
664
4
  Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
665
4
  TNode add_tnode = add_node;
666
4
  std::vector<Node> children;
667
8
  for (Node child : add_tnode)
668
  {
669
6
    children.push_back(child);
670
  }
671
2
  ASSERT_TRUE(children.size() == skolems.size()
672
2
              && std::equal(children.begin(), children.end(), skolems.begin()));
673
}
674
675
40
TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode)
676
{
677
  const std::vector<Node> skolems =
678
4
      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
679
4
  Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
680
4
  TNode add_tnode = add_node;
681
4
  std::vector<TNode> children;
682
8
  for (TNode child : add_tnode)
683
  {
684
6
    children.push_back(child);
685
  }
686
2
  ASSERT_TRUE(children.size() == skolems.size()
687
2
              && std::equal(children.begin(), children.end(), skolems.begin()));
688
}
689
690
40
TEST_F(TestNodeBlackNode, isConst)
691
{
692
  // more complicated "constants" exist in datatypes and arrays theories
693
4
  DType list("list");
694
  std::shared_ptr<DTypeConstructor> consC =
695
4
      std::make_shared<DTypeConstructor>("cons");
696
2
  consC->addArg("car", d_nodeManager->integerType());
697
2
  consC->addArgSelf("cdr");
698
2
  list.addConstructor(consC);
699
2
  list.addConstructor(std::make_shared<DTypeConstructor>("nil"));
700
4
  TypeNode listType = d_nodeManager->mkDatatypeType(list);
701
  const std::vector<std::shared_ptr<DTypeConstructor> >& lcons =
702
2
      listType.getDType().getConstructors();
703
4
  Node cons = lcons[0]->getConstructor();
704
4
  Node nil = lcons[1]->getConstructor();
705
4
  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
706
  Node cons_x_nil =
707
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
708
                            cons,
709
                            x,
710
4
                            d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
711
  Node cons_1_nil =
712
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
713
                            cons,
714
4
                            d_nodeManager->mkConst(Rational(1)),
715
8
                            d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
716
  Node cons_1_cons_2_nil = d_nodeManager->mkNode(
717
      APPLY_CONSTRUCTOR,
718
      cons,
719
4
      d_nodeManager->mkConst(Rational(1)),
720
10
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
721
                            cons,
722
4
                            d_nodeManager->mkConst(Rational(2)),
723
14
                            d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)));
724
2
  ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst());
725
2
  ASSERT_FALSE(cons_x_nil.isConst());
726
2
  ASSERT_TRUE(cons_1_nil.isConst());
727
2
  ASSERT_TRUE(cons_1_cons_2_nil.isConst());
728
729
4
  TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
730
8
                                                d_nodeManager->integerType());
731
4
  Node zero = d_nodeManager->mkConst(Rational(0));
732
4
  Node one = d_nodeManager->mkConst(Rational(1));
733
4
  Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
734
2
  ASSERT_TRUE(storeAll.isConst());
735
736
4
  Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
737
2
  ASSERT_FALSE(arr.isConst());
738
2
  arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
739
2
  ASSERT_TRUE(arr.isConst());
740
4
  Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
741
2
  ASSERT_FALSE(arr2.isConst());
742
2
  arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
743
2
  ASSERT_FALSE(arr2.isConst());
744
745
4
  arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
746
4
                                       d_nodeManager->mkBitVectorType(1));
747
2
  zero = d_nodeManager->mkConst(BitVector(1, unsigned(0)));
748
2
  one = d_nodeManager->mkConst(BitVector(1, unsigned(1)));
749
2
  storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
750
2
  ASSERT_TRUE(storeAll.isConst());
751
752
2
  arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
753
2
  ASSERT_FALSE(arr.isConst());
754
2
  arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
755
2
  ASSERT_TRUE(arr.isConst());
756
2
  arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
757
2
  ASSERT_FALSE(arr2.isConst());
758
2
  arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
759
2
  ASSERT_FALSE(arr2.isConst());
760
2
  arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
761
2
  ASSERT_FALSE(arr2.isConst());
762
}
763
764
namespace {
765
2
Node level0(NodeManager* nm)
766
{
767
4
  NodeBuilder<> nb(kind::AND);
768
4
  Node x = nm->mkSkolem("x", nm->booleanType());
769
2
  nb << x;
770
2
  nb << x;
771
4
  return Node(nb.constructNode());
772
}
773
TNode level1(NodeManager* nm) { return level0(nm); }
774
}  // namespace
775
776
/**
777
 * This is for demonstrating what a certain type of user error looks like.
778
 */
779
40
TEST_F(TestNodeBlackNode, node_tnode_usage)
780
{
781
4
  Node n;
782
2
  ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get()));
783
2
  ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0");
784
}
785
786
}  // namespace test
787
6889852
}  // namespace CVC4