1 /********************* */
4 ** Top contributors (to current version):
5 ** Morgan Deters, Tim King, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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
12 ** \brief White box testing of CVC4::Node.
14 ** White box testing of CVC4::Node.
17 #include <cxxtest/TestSuite.h>
21 #include "base/cvc4_assert.h"
22 #include "expr/node.h"
23 #include "expr/node_builder.h"
24 #include "expr/node_manager.h"
25 #include "expr/node_value.h"
28 using namespace CVC4::kind
;
29 using namespace CVC4::expr
;
32 class NodeWhite
: public CxxTest::TestSuite
{
35 NodeManagerScope
* d_scope
;
40 d_nm
= new NodeManager(NULL
);
41 d_scope
= new NodeManagerScope(d_nm
);
44 void tearDown() override
51 TS_ASSERT_EQUALS(Node::null(), Node::s_null
);
60 TS_ASSERT(b
.d_nv
->getId() == 0);
61 TS_ASSERT(b
.d_nv
->getKind() == UNDEFINED_KIND
);
62 TS_ASSERT_EQUALS(b
.d_nv
->d_nchildren
, 0u);
66 void testIterators() {
67 Node x
= d_nm
->mkVar("x", d_nm
->integerType());
68 Node y
= d_nm
->mkVar("y", d_nm
->integerType());
69 Node x_plus_y
= d_nm
->mkNode(PLUS
, x
, y
);
70 Node two
= d_nm
->mkConst(Rational(2));
71 Node x_times_2
= d_nm
->mkNode(MULT
, x
, two
);
73 Node n
= d_nm
->mkNode(PLUS
, x_times_2
, x_plus_y
, y
);
77 i
= find(n
.begin(), n
.end(), x_plus_y
);
78 TS_ASSERT(i
!= n
.end());
79 TS_ASSERT(*i
== x_plus_y
);
81 i
= find(n
.begin(), n
.end(), x
);
82 TS_ASSERT(i
== n
.end());
84 i
= find(x_times_2
.begin(), x_times_2
.end(), two
);
85 TS_ASSERT(i
!= x_times_2
.end());
88 i
= find(n
.begin(), n
.end(), y
);
89 TS_ASSERT(i
!= n
.end());
93 copy(n
.begin(), n
.end(), back_inserter(v
));
94 TS_ASSERT(n
.getNumChildren() == v
.size());
95 TS_ASSERT(3 == v
.size());
96 TS_ASSERT(v
[0] == x_times_2
);
97 TS_ASSERT(v
[1] == x_plus_y
);