1 /********************* */
2 /*! \file node_self_iterator_black.h
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
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 Black box testing of CVC4::expr::NodeSelfIterator
14 ** Black box testing of CVC4::expr::NodeSelfIterator
17 #include <cxxtest/TestSuite.h>
19 #include "expr/node.h"
20 #include "expr/node_self_iterator.h"
21 #include "expr/node_builder.h"
22 #include "expr/convenience_node_builders.h"
25 using namespace CVC4::kind
;
26 using namespace CVC4::expr
;
29 class NodeSelfIteratorBlack
: public CxxTest::TestSuite
{
32 NodeManager
* d_nodeManager
;
33 NodeManagerScope
* d_scope
;
34 TypeNode
* d_booleanType
;
40 d_nodeManager
= new NodeManager(NULL
);
41 d_scope
= new NodeManagerScope(d_nodeManager
);
42 d_booleanType
= new TypeNode(d_nodeManager
->booleanType());
43 d_realType
= new TypeNode(d_nodeManager
->realType());
52 void testSelfIteration() {
53 Node x
= d_nodeManager
->mkSkolem("x", *d_booleanType
);
54 Node y
= d_nodeManager
->mkSkolem("y", *d_booleanType
);
55 Node x_and_y
= x
&& y
;
56 NodeSelfIterator i
= x_and_y
, j
= NodeSelfIterator::self(x_and_y
);
57 TS_ASSERT(i
!= x_and_y
.end());
58 TS_ASSERT(j
!= x_and_y
.end());
59 TS_ASSERT(*i
== x_and_y
);
60 TS_ASSERT(*j
== x_and_y
);
61 TS_ASSERT(*i
++ == x_and_y
);
62 TS_ASSERT(*j
++ == x_and_y
);
63 TS_ASSERT(i
== NodeSelfIterator::selfEnd(x_and_y
));
64 TS_ASSERT(j
== NodeSelfIterator::selfEnd(x_and_y
));
65 TS_ASSERT(i
== x_and_y
.end());
66 TS_ASSERT(j
== x_and_y
.end());
69 TS_ASSERT(i
!= x_and_y
.end());
72 TS_ASSERT(++i
== x_and_y
.end());