bcb3155e1d6f26ed659c25bff388bf8048451c28
1 /********************* */
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): Tim King, Dejan Jovanovic
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief White box testing of CVC4::Node.
14 ** White box testing of CVC4::Node.
17 #include <cxxtest/TestSuite.h>
21 #include "expr/node_value.h"
22 #include "expr/node_builder.h"
23 #include "expr/node_manager.h"
24 #include "expr/node.h"
25 #include "context/context.h"
26 #include "util/cvc4_assert.h"
29 using namespace CVC4::kind
;
30 using namespace CVC4::context
;
31 using namespace CVC4::expr
;
34 class NodeWhite
: public CxxTest::TestSuite
{
38 NodeManagerScope
* d_scope
;
43 d_ctxt
= new Context();
44 d_nm
= new NodeManager(d_ctxt
, NULL
);
45 d_scope
= new NodeManagerScope(d_nm
);
55 TS_ASSERT_EQUALS(Node::null(), Node::s_null
);
64 TS_ASSERT(b
.d_nv
->getId() == 0);
65 TS_ASSERT(b
.d_nv
->getKind() == UNDEFINED_KIND
);
66 TS_ASSERT_EQUALS(b
.d_nv
->d_nchildren
, 0u);
70 void testIterators() {
71 Node x
= d_nm
->mkVar("x", d_nm
->integerType());
72 Node y
= d_nm
->mkVar("y", d_nm
->integerType());
73 Node x_plus_y
= d_nm
->mkNode(PLUS
, x
, y
);
74 Node two
= d_nm
->mkConst(Rational(2));
75 Node x_times_2
= d_nm
->mkNode(MULT
, x
, two
);
77 Node n
= d_nm
->mkNode(PLUS
, x_times_2
, x_plus_y
, y
);
81 i
= find(n
.begin(), n
.end(), x_plus_y
);
82 TS_ASSERT(i
!= n
.end());
83 TS_ASSERT(*i
== x_plus_y
);
85 i
= find(n
.begin(), n
.end(), x
);
86 TS_ASSERT(i
== n
.end());
88 i
= find(x_times_2
.begin(), x_times_2
.end(), two
);
89 TS_ASSERT(i
!= x_times_2
.end());
92 i
= find(n
.begin(), n
.end(), y
);
93 TS_ASSERT(i
!= n
.end());
97 copy(n
.begin(), n
.end(), back_inserter(v
));
98 TS_ASSERT(n
.getNumChildren() == v
.size());
99 TS_ASSERT(3 == v
.size());
100 TS_ASSERT(v
[0] == x_times_2
);
101 TS_ASSERT(v
[1] == x_plus_y
);
102 TS_ASSERT(v
[2] == y
);