GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/node_builder_black.cpp Lines: 326 326 100.0 %
Date: 2021-03-23 Branches: 1532 5508 27.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_builder_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Tim King, Morgan Deters
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::NodeBuilder.
13
 **
14
 ** Black box testing of CVC4::NodeBuilder.
15
 **/
16
17
#include <limits.h>
18
19
#include <sstream>
20
#include <vector>
21
22
#include "base/check.h"
23
#include "expr/kind.h"
24
#include "expr/node.h"
25
#include "expr/node_builder.h"
26
#include "expr/node_manager.h"
27
#include "test_node.h"
28
#include "util/rational.h"
29
30
#define K 30u
31
#define LARGE_K UINT_MAX / 40
32
33
namespace CVC4 {
34
35
using namespace kind;
36
37
namespace test {
38
39
52
class TestNodeBlackNodeBuilder : public TestNode
40
{
41
 protected:
42
  template <unsigned N>
43
24
  void push_back(NodeBuilder<N>& nb, uint32_t n)
44
  {
45
922
    for (uint32_t i = 0; i < n; ++i)
46
    {
47
898
      nb << d_nodeManager->mkConst(true);
48
    }
49
24
  }
50
  Kind d_specKind = AND;
51
};
52
53
/** Tests just constructors. No modification is done to the node. */
54
22
TEST_F(TestNodeBlackNodeBuilder, ctors)
55
{
56
  /* Default size tests. */
57
4
  NodeBuilder<> def;
58
2
  ASSERT_EQ(def.getKind(), UNDEFINED_KIND);
59
#ifdef CVC4_ASSERTIONS
60
2
  ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
61
2
  ASSERT_DEATH(def.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
62
2
  ASSERT_DEATH(def.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
63
#endif
64
65
4
  NodeBuilder<> spec(d_specKind);
66
2
  ASSERT_EQ(spec.getKind(), d_specKind);
67
2
  ASSERT_EQ(spec.getNumChildren(), 0u);
68
2
  ASSERT_EQ(spec.begin(), spec.end());
69
70
4
  NodeBuilder<> from_nm(d_nodeManager.get());
71
2
  ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND);
72
#ifdef CVC4_ASSERTIONS
73
2
  ASSERT_DEATH(from_nm.getNumChildren(),
74
               "getKind\\(\\) != kind::UNDEFINED_KIND");
75
2
  ASSERT_DEATH(from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
76
2
  ASSERT_DEATH(from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
77
#endif
78
79
4
  NodeBuilder<> from_nm_kind(d_nodeManager.get(), d_specKind);
80
2
  ASSERT_EQ(from_nm_kind.getKind(), d_specKind);
81
2
  ASSERT_EQ(from_nm_kind.getNumChildren(), 0u);
82
2
  ASSERT_EQ(from_nm_kind.begin(), from_nm_kind.end());
83
84
  /* Non-default size tests */
85
4
  NodeBuilder<K> ws;
86
2
  ASSERT_EQ(ws.getKind(), UNDEFINED_KIND);
87
#ifdef CVC4_ASSERTIONS
88
2
  ASSERT_DEATH(ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
89
2
  ASSERT_DEATH(ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
90
2
  ASSERT_DEATH(ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
91
#endif
92
93
4
  NodeBuilder<K> ws_kind(d_specKind);
94
2
  ASSERT_EQ(ws_kind.getKind(), d_specKind);
95
2
  ASSERT_EQ(ws_kind.getNumChildren(), 0u);
96
2
  ASSERT_EQ(ws_kind.begin(), ws_kind.end());
97
98
4
  NodeBuilder<K> ws_from_nm(d_nodeManager.get());
99
2
  ASSERT_EQ(ws_from_nm.getKind(), UNDEFINED_KIND);
100
#ifdef CVC4_ASSERTIONS
101
2
  ASSERT_DEATH(ws_from_nm.getNumChildren(),
102
               "getKind\\(\\) != kind::UNDEFINED_KIND");
103
2
  ASSERT_DEATH(ws_from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
104
2
  ASSERT_DEATH(ws_from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
105
#endif
106
107
4
  NodeBuilder<K> ws_from_nm_kind(d_nodeManager.get(), d_specKind);
108
2
  ASSERT_EQ(ws_from_nm_kind.getKind(), d_specKind);
109
2
  ASSERT_EQ(ws_from_nm_kind.getNumChildren(), 0u);
110
2
  ASSERT_EQ(ws_from_nm_kind.begin(), ws_from_nm_kind.end());
111
112
  /* Extreme size tests */
113
4
  NodeBuilder<0> ws_size_0;
114
115
  /* Allocating on the heap instead of the stack. */
116
2
  NodeBuilder<LARGE_K>* ws_size_large = new NodeBuilder<LARGE_K>;
117
2
  delete ws_size_large;
118
119
  /* Copy constructors */
120
4
  NodeBuilder<> copy(def);
121
2
  ASSERT_EQ(copy.getKind(), UNDEFINED_KIND);
122
#ifdef CVC4_ASSERTIONS
123
2
  ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
124
2
  ASSERT_DEATH(copy.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
125
2
  ASSERT_DEATH(copy.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
126
#endif
127
128
4
  NodeBuilder<K> cp_ws(ws);
129
2
  ASSERT_EQ(cp_ws.getKind(), UNDEFINED_KIND);
130
#ifdef CVC4_ASSERTIONS
131
2
  ASSERT_DEATH(cp_ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
132
2
  ASSERT_DEATH(cp_ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
133
2
  ASSERT_DEATH(cp_ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
134
#endif
135
136
4
  NodeBuilder<K - 10> cp_from_larger(ws);
137
2
  ASSERT_EQ(cp_from_larger.getKind(), UNDEFINED_KIND);
138
#ifdef CVC4_ASSERTIONS
139
2
  ASSERT_DEATH(cp_from_larger.getNumChildren(),
140
               "getKind\\(\\) != kind::UNDEFINED_KIND");
141
2
  ASSERT_DEATH(cp_from_larger.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
142
2
  ASSERT_DEATH(cp_from_larger.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
143
#endif
144
145
4
  NodeBuilder<K + 10> cp_from_smaller(ws);
146
2
  ASSERT_EQ(cp_from_smaller.getKind(), UNDEFINED_KIND);
147
#ifdef CVC4_ASSERTIONS
148
2
  ASSERT_DEATH(cp_from_smaller.getNumChildren(),
149
               "getKind\\(\\) != kind::UNDEFINED_KIND");
150
2
  ASSERT_DEATH(cp_from_smaller.begin(),
151
               "getKind\\(\\) != kind::UNDEFINED_KIND");
152
2
  ASSERT_DEATH(cp_from_smaller.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
153
#endif
154
}
155
156
22
TEST_F(TestNodeBlackNodeBuilder, dtor)
157
{
158
2
  NodeBuilder<K>* nb = new NodeBuilder<K>();
159
2
  delete nb;
160
2
}
161
162
22
TEST_F(TestNodeBlackNodeBuilder, begin_end)
163
{
164
  /* Test begin() and end() without resizing. */
165
4
  NodeBuilder<K> ws(d_specKind);
166
2
  ASSERT_EQ(ws.begin(), ws.end());
167
168
2
  push_back(ws, K);
169
2
  ASSERT_NE(ws.begin(), ws.end());
170
171
2
  NodeBuilder<K>::iterator iter = ws.begin();
172
62
  for (uint32_t i = 0; i < K; ++i)
173
  {
174
60
    ASSERT_NE(iter, ws.end());
175
60
    ++iter;
176
  }
177
2
  ASSERT_EQ(iter, ws.end());
178
179
2
  NodeBuilder<K>::const_iterator citer = ws.begin();
180
62
  for (uint32_t i = 0; i < K; ++i)
181
  {
182
60
    ASSERT_NE(citer, ws.end());
183
60
    ++citer;
184
  }
185
2
  ASSERT_EQ(citer, ws.end());
186
187
  /* Repeat same tests and make sure that resizing occurs. */
188
4
  NodeBuilder<> smaller(d_specKind);
189
2
  ASSERT_EQ(smaller.begin(), smaller.end());
190
191
2
  push_back(smaller, K);
192
2
  ASSERT_NE(smaller.begin(), smaller.end());
193
194
2
  NodeBuilder<>::iterator smaller_iter = smaller.begin();
195
62
  for (uint32_t i = 0; i < K; ++i)
196
  {
197
60
    ASSERT_NE(smaller_iter, smaller.end());
198
60
    ++smaller_iter;
199
  }
200
2
  ASSERT_EQ(iter, ws.end());
201
202
2
  NodeBuilder<>::const_iterator smaller_citer = smaller.begin();
203
62
  for (uint32_t i = 0; i < K; ++i)
204
  {
205
60
    ASSERT_NE(smaller_citer, smaller.end());
206
60
    ++smaller_citer;
207
  }
208
2
  ASSERT_EQ(smaller_citer, smaller.end());
209
}
210
211
22
TEST_F(TestNodeBlackNodeBuilder, iterator)
212
{
213
4
  NodeBuilder<> b;
214
4
  Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
215
4
  Node y = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
216
4
  Node z = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
217
2
  b << x << y << z << AND;
218
219
  {
220
2
    NodeBuilder<>::iterator i = b.begin();
221
2
    ASSERT_EQ(*i++, x);
222
2
    ASSERT_EQ(*i++, y);
223
2
    ASSERT_EQ(*i++, z);
224
2
    ASSERT_EQ(i, b.end());
225
  }
226
227
  {
228
2
    const NodeBuilder<>& c = b;
229
2
    NodeBuilder<>::const_iterator i = c.begin();
230
2
    ASSERT_EQ(*i++, x);
231
2
    ASSERT_EQ(*i++, y);
232
2
    ASSERT_EQ(*i++, z);
233
2
    ASSERT_EQ(i, b.end());
234
  }
235
}
236
237
22
TEST_F(TestNodeBlackNodeBuilder, getKind)
238
{
239
4
  NodeBuilder<> noKind;
240
2
  ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
241
242
4
  Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
243
2
  noKind << x << x;
244
2
  ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
245
246
2
  noKind << PLUS;
247
248
2
  ASSERT_EQ(noKind.getKind(), PLUS);
249
250
4
  Node n = noKind;
251
252
#ifdef CVC4_ASSERTIONS
253
2
  ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)");
254
#endif
255
256
4
  NodeBuilder<> spec(PLUS);
257
2
  ASSERT_EQ(spec.getKind(), PLUS);
258
2
  spec << x << x;
259
2
  ASSERT_EQ(spec.getKind(), PLUS);
260
}
261
262
22
TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
263
{
264
4
  Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
265
266
4
  NodeBuilder<> nb;
267
#ifdef CVC4_ASSERTIONS
268
2
  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
269
#endif
270
2
  nb << PLUS << x << x;
271
272
2
  ASSERT_EQ(nb.getNumChildren(), 2u);
273
274
2
  nb << x << x;
275
2
  ASSERT_EQ(nb.getNumChildren(), 4u);
276
277
2
  nb.clear();
278
#ifdef CVC4_ASSERTIONS
279
2
  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
280
#endif
281
2
  nb.clear(PLUS);
282
2
  ASSERT_EQ(nb.getNumChildren(), 0u);
283
2
  nb << x << x << x;
284
285
2
  ASSERT_EQ(nb.getNumChildren(), 3u);
286
287
2
  nb << x << x << x;
288
2
  ASSERT_EQ(nb.getNumChildren(), 6u);
289
290
#ifdef CVC4_ASSERTIONS
291
2
  ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND");
292
4
  Node n = nb;
293
2
  ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)");
294
#endif
295
}
296
297
22
TEST_F(TestNodeBlackNodeBuilder, operator_square)
298
{
299
4
  NodeBuilder<> arr(d_specKind);
300
301
4
  Node i_0 = d_nodeManager->mkConst(false);
302
4
  Node i_2 = d_nodeManager->mkConst(true);
303
4
  Node i_K = d_nodeManager->mkNode(NOT, i_0);
304
305
#ifdef CVC4_ASSERTIONS
306
2
  ASSERT_DEATH(arr[-1], "index out of range");
307
2
  ASSERT_DEATH(arr[0], "index out of range");
308
#endif
309
310
2
  arr << i_0;
311
312
2
  ASSERT_EQ(arr[0], i_0);
313
314
2
  push_back(arr, 1);
315
316
2
  arr << i_2;
317
318
2
  ASSERT_EQ(arr[0], i_0);
319
2
  ASSERT_EQ(arr[2], i_2);
320
321
2
  push_back(arr, K - 3);
322
323
2
  ASSERT_EQ(arr[0], i_0);
324
2
  ASSERT_EQ(arr[2], i_2);
325
56
  for (unsigned i = 3; i < K; ++i)
326
  {
327
54
    ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
328
  }
329
330
2
  arr << i_K;
331
332
2
  ASSERT_EQ(arr[0], i_0);
333
2
  ASSERT_EQ(arr[2], i_2);
334
56
  for (unsigned i = 3; i < K; ++i)
335
  {
336
54
    ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
337
  }
338
2
  ASSERT_EQ(arr[K], i_K);
339
340
#ifdef CVC4_ASSERTIONS
341
4
  Node n = arr;
342
2
  ASSERT_DEATH(arr[0], "!isUsed\\(\\)");
343
#endif
344
}
345
346
22
TEST_F(TestNodeBlackNodeBuilder, clear)
347
{
348
4
  NodeBuilder<> nb;
349
350
2
  ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
351
#ifdef CVC4_ASSERTIONS
352
2
  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
353
2
  ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
354
2
  ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
355
#endif
356
357
2
  nb << d_specKind;
358
2
  push_back(nb, K);
359
360
2
  ASSERT_EQ(nb.getKind(), d_specKind);
361
2
  ASSERT_EQ(nb.getNumChildren(), K);
362
2
  ASSERT_NE(nb.begin(), nb.end());
363
364
2
  nb.clear();
365
366
2
  ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
367
#ifdef CVC4_ASSERTIONS
368
2
  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
369
2
  ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
370
2
  ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
371
#endif
372
373
2
  nb << d_specKind;
374
2
  push_back(nb, K);
375
376
2
  ASSERT_EQ(nb.getKind(), d_specKind);
377
2
  ASSERT_EQ(nb.getNumChildren(), K);
378
2
  ASSERT_NE(nb.begin(), nb.end());
379
380
2
  nb.clear(d_specKind);
381
382
2
  ASSERT_EQ(nb.getKind(), d_specKind);
383
2
  ASSERT_EQ(nb.getNumChildren(), 0u);
384
2
  ASSERT_EQ(nb.begin(), nb.end());
385
386
2
  push_back(nb, K);
387
2
  nb.clear();
388
389
2
  ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
390
#ifdef CVC4_ASSERTIONS
391
2
  ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
392
2
  ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
393
2
  ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
394
#endif
395
}
396
397
22
TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
398
{
399
#ifdef CVC4_ASSERTIONS
400
4
  NodeBuilder<> spec(d_specKind);
401
2
  ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder");
402
#endif
403
404
4
  NodeBuilder<> noSpec;
405
2
  noSpec << d_specKind;
406
2
  ASSERT_EQ(noSpec.getKind(), d_specKind);
407
408
4
  NodeBuilder<> modified;
409
2
  push_back(modified, K);
410
2
  modified << d_specKind;
411
2
  ASSERT_EQ(modified.getKind(), d_specKind);
412
413
4
  NodeBuilder<> nb(d_specKind);
414
2
  nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false);
415
2
  nb.clear(PLUS);
416
417
#ifdef CVC4_ASSERTIONS
418
4
  Node n;
419
2
  ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children");
420
2
  nb.clear(PLUS);
421
#endif
422
423
#ifdef CVC4_ASSERTIONS
424
2
  ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder");
425
#endif
426
427
4
  NodeBuilder<> testRef;
428
2
  ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind);
429
430
#ifdef CVC4_ASSERTIONS
431
4
  NodeBuilder<> testTwo;
432
2
  ASSERT_DEATH(testTwo << d_specKind << PLUS,
433
               "can't redefine the Kind of a NodeBuilder");
434
#endif
435
436
4
  NodeBuilder<> testMixOrder1;
437
2
  ASSERT_EQ(
438
      (testMixOrder1 << d_specKind << d_nodeManager->mkConst(true)).getKind(),
439
2
      d_specKind);
440
4
  NodeBuilder<> testMixOrder2;
441
2
  ASSERT_EQ(
442
      (testMixOrder2 << d_nodeManager->mkConst(true) << d_specKind).getKind(),
443
2
      d_specKind);
444
}
445
446
22
TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
447
{
448
4
  NodeBuilder<K> nb(d_specKind);
449
2
  ASSERT_EQ(nb.getKind(), d_specKind);
450
2
  ASSERT_EQ(nb.getNumChildren(), 0u);
451
2
  ASSERT_EQ(nb.begin(), nb.end());
452
2
  push_back(nb, K);
453
2
  ASSERT_EQ(nb.getKind(), d_specKind);
454
2
  ASSERT_EQ(nb.getNumChildren(), K);
455
2
  ASSERT_NE(nb.begin(), nb.end());
456
457
#ifdef CVC4_ASSERTIONS
458
4
  Node n = nb;
459
2
  ASSERT_DEATH(nb << n, "!isUsed\\(\\)");
460
#endif
461
462
4
  NodeBuilder<> overflow(d_specKind);
463
2
  ASSERT_EQ(overflow.getKind(), d_specKind);
464
2
  ASSERT_EQ(overflow.getNumChildren(), 0u);
465
2
  ASSERT_EQ(overflow.begin(), overflow.end());
466
467
2
  push_back(overflow, 5 * K + 1);
468
469
2
  ASSERT_EQ(overflow.getKind(), d_specKind);
470
2
  ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1);
471
2
  ASSERT_NE(overflow.begin(), overflow.end());
472
}
473
474
22
TEST_F(TestNodeBlackNodeBuilder, append)
475
{
476
4
  Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
477
4
  Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
478
4
  Node z = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
479
4
  Node m = d_nodeManager->mkNode(AND, y, z, x);
480
4
  Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z);
481
4
  Node o = d_nodeManager->mkNode(XOR, y, x);
482
483
4
  Node r = d_nodeManager->mkSkolem("r", *d_realTypeNode);
484
4
  Node s = d_nodeManager->mkSkolem("s", *d_realTypeNode);
485
4
  Node t = d_nodeManager->mkSkolem("t", *d_realTypeNode);
486
487
  Node p = d_nodeManager->mkNode(
488
      EQUAL,
489
4
      d_nodeManager->mkConst<Rational>(0),
490
8
      d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t));
491
4
  Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
492
493
#ifdef CVC4_ASSERTIONS
494
2
  ASSERT_DEATH(d_nodeManager->mkNode(XOR, y, x, x),
495
               "Nodes with kind XOR must have at most 2 children");
496
#endif
497
498
4
  NodeBuilder<> b(d_specKind);
499
500
  /* test append(TNode) */
501
2
  b.append(n).append(o).append(q);
502
503
2
  ASSERT_EQ(b.getNumChildren(), 3);
504
2
  ASSERT_EQ(b[0], n);
505
2
  ASSERT_EQ(b[1], o);
506
2
  ASSERT_EQ(b[2], q);
507
508
4
  std::vector<Node> v;
509
2
  v.push_back(m);
510
2
  v.push_back(p);
511
2
  v.push_back(q);
512
513
  /* test append(vector<Node>) */
514
2
  b.append(v);
515
516
2
  ASSERT_EQ(b.getNumChildren(), 6);
517
2
  ASSERT_EQ(b[0], n);
518
2
  ASSERT_EQ(b[1], o);
519
2
  ASSERT_EQ(b[2], q);
520
2
  ASSERT_EQ(b[3], m);
521
2
  ASSERT_EQ(b[4], p);
522
2
  ASSERT_EQ(b[5], q);
523
524
  /* test append(iterator, iterator) */
525
2
  b.append(v.rbegin(), v.rend());
526
527
2
  ASSERT_EQ(b.getNumChildren(), 9);
528
2
  ASSERT_EQ(b[0], n);
529
2
  ASSERT_EQ(b[1], o);
530
2
  ASSERT_EQ(b[2], q);
531
2
  ASSERT_EQ(b[3], m);
532
2
  ASSERT_EQ(b[4], p);
533
2
  ASSERT_EQ(b[5], q);
534
2
  ASSERT_EQ(b[6], q);
535
2
  ASSERT_EQ(b[7], p);
536
2
  ASSERT_EQ(b[8], m);
537
}
538
539
22
TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
540
{
541
4
  NodeBuilder<K> implicit(d_specKind);
542
4
  NodeBuilder<K> explic(d_specKind);
543
544
2
  push_back(implicit, K);
545
2
  push_back(explic, K);
546
547
4
  Node nimpl = implicit;
548
4
  Node nexplicit = (Node)explic;
549
550
2
  ASSERT_EQ(nimpl.getKind(), d_specKind);
551
2
  ASSERT_EQ(nimpl.getNumChildren(), K);
552
553
2
  ASSERT_EQ(nexplicit.getKind(), d_specKind);
554
2
  ASSERT_EQ(nexplicit.getNumChildren(), K);
555
556
#ifdef CVC4_ASSERTIONS
557
2
  ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)");
558
#endif
559
}
560
561
22
TEST_F(TestNodeBlackNodeBuilder, leftist_building)
562
{
563
4
  NodeBuilder<> nb;
564
565
4
  Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode);
566
567
4
  Node b = d_nodeManager->mkSkolem("b", *d_boolTypeNode);
568
4
  Node c = d_nodeManager->mkSkolem("c", *d_boolTypeNode);
569
570
4
  Node d = d_nodeManager->mkSkolem("d", *d_realTypeNode);
571
4
  Node e = d_nodeManager->mkSkolem("e", *d_realTypeNode);
572
573
2
  nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE;
574
575
4
  Node n = nb;
576
2
  ASSERT_EQ(n.getNumChildren(), 3u);
577
2
  ASSERT_EQ(n.getType(), *d_realTypeNode);
578
2
  ASSERT_EQ(n[0].getType(), *d_boolTypeNode);
579
2
  ASSERT_EQ(n[1].getType(), *d_realTypeNode);
580
2
  ASSERT_EQ(n[2].getType(), *d_realTypeNode);
581
582
4
  Node nota = d_nodeManager->mkNode(NOT, a);
583
4
  Node nota_or_b_or_c = d_nodeManager->mkNode(OR, nota, b, c);
584
4
  Node n0 = d_nodeManager->mkNode(AND, nota_or_b_or_c, c, a);
585
4
  Node nexpected = d_nodeManager->mkNode(ITE, n0, d, e);
586
587
2
  ASSERT_EQ(nexpected, n);
588
}
589
}  // namespace test
590
122578
}  // namespace CVC4