9ca086d062b2b68fcc2fe46e526fb27e1aa0d018
1 /********************* */
2 /*! \file node_manager_black.h
4 ** Original author: Christopher L. Conway
5 ** Major contributors: Morgan Deters, Dejan Jovanovic
6 ** Minor contributors (to current version): Tim King
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::NodeManager.
14 ** White box testing of CVC4::NodeManager.
17 #include <cxxtest/TestSuite.h>
22 #include "expr/node_manager.h"
23 #include "expr/node_manager_attributes.h"
24 #include "context/context.h"
26 #include "util/rational.h"
27 #include "util/integer.h"
30 using namespace CVC4::expr
;
31 using namespace CVC4::kind
;
32 using namespace CVC4::context
;
34 class NodeManagerBlack
: public CxxTest::TestSuite
{
37 NodeManager
* d_nodeManager
;
38 NodeManagerScope
* d_scope
;
43 d_context
= new Context
;
44 d_nodeManager
= new NodeManager(d_context
, NULL
);
45 d_scope
= new NodeManagerScope(d_nodeManager
);
54 void testMkNodeNot() {
55 Node x
= d_nodeManager
->mkSkolem("x",d_nodeManager
->booleanType());
56 Node n
= d_nodeManager
->mkNode(NOT
, x
);
57 TS_ASSERT_EQUALS( n
.getNumChildren(), 1u );
58 TS_ASSERT_EQUALS( n
.getKind(), NOT
);
59 TS_ASSERT_EQUALS( n
[0], x
);
62 void testMkNodeBinary() {
63 Node x
= d_nodeManager
->mkSkolem("x",d_nodeManager
->booleanType());
64 Node y
= d_nodeManager
->mkSkolem("y",d_nodeManager
->booleanType());
65 Node n
= d_nodeManager
->mkNode(IMPLIES
, x
, y
);
66 TS_ASSERT_EQUALS( n
.getNumChildren(), 2u );
67 TS_ASSERT_EQUALS( n
.getKind(), IMPLIES
);
68 TS_ASSERT_EQUALS( n
[0], x
);
69 TS_ASSERT_EQUALS( n
[1], y
);
72 void testMkNodeThreeChildren() {
73 Node x
= d_nodeManager
->mkSkolem("x",d_nodeManager
->booleanType());
74 Node y
= d_nodeManager
->mkSkolem("y",d_nodeManager
->booleanType());
75 Node z
= d_nodeManager
->mkSkolem("z",d_nodeManager
->booleanType());
76 Node n
= d_nodeManager
->mkNode(AND
, x
, y
, z
);
77 TS_ASSERT_EQUALS( n
.getNumChildren(), 3u );
78 TS_ASSERT_EQUALS( n
.getKind(), AND
);
79 TS_ASSERT_EQUALS( n
[0], x
);
80 TS_ASSERT_EQUALS( n
[1], y
);
81 TS_ASSERT_EQUALS( n
[2], z
);
84 void testMkNodeFourChildren() {
85 Node x1
= d_nodeManager
->mkSkolem("x1",d_nodeManager
->booleanType());
86 Node x2
= d_nodeManager
->mkSkolem("x2",d_nodeManager
->booleanType());
87 Node x3
= d_nodeManager
->mkSkolem("x3",d_nodeManager
->booleanType());
88 Node x4
= d_nodeManager
->mkSkolem("x4",d_nodeManager
->booleanType());
89 Node n
= d_nodeManager
->mkNode(AND
, x1
, x2
, x3
, x4
);
90 TS_ASSERT_EQUALS( n
.getNumChildren(), 4u );
91 TS_ASSERT_EQUALS( n
.getKind(), AND
);
92 TS_ASSERT_EQUALS( n
[0], x1
);
93 TS_ASSERT_EQUALS( n
[1], x2
);
94 TS_ASSERT_EQUALS( n
[2], x3
);
95 TS_ASSERT_EQUALS( n
[3], x4
);
98 void testMkNodeFiveChildren() {
99 Node x1
= d_nodeManager
->mkSkolem("x1",d_nodeManager
->booleanType());
100 Node x2
= d_nodeManager
->mkSkolem("x2",d_nodeManager
->booleanType());
101 Node x3
= d_nodeManager
->mkSkolem("x3",d_nodeManager
->booleanType());
102 Node x4
= d_nodeManager
->mkSkolem("x4",d_nodeManager
->booleanType());
103 Node x5
= d_nodeManager
->mkSkolem("x5",d_nodeManager
->booleanType());
104 Node n
= d_nodeManager
->mkNode(AND
, x1
, x2
, x3
, x4
, x5
);
105 TS_ASSERT_EQUALS( n
.getNumChildren(), 5u );
106 TS_ASSERT_EQUALS( n
.getKind(), AND
);
107 TS_ASSERT_EQUALS( n
[0], x1
);
108 TS_ASSERT_EQUALS( n
[1], x2
);
109 TS_ASSERT_EQUALS( n
[2], x3
);
110 TS_ASSERT_EQUALS( n
[3], x4
);
111 TS_ASSERT_EQUALS( n
[4], x5
);
114 void testMkNodeVectorOfNodeChildren() {
115 Node x1
= d_nodeManager
->mkSkolem("x1",d_nodeManager
->booleanType());
116 Node x2
= d_nodeManager
->mkSkolem("x2",d_nodeManager
->booleanType());
117 Node x3
= d_nodeManager
->mkSkolem("x3",d_nodeManager
->booleanType());
118 std::vector
<Node
> args
;
122 Node n
= d_nodeManager
->mkNode(AND
, args
);
123 TS_ASSERT_EQUALS( n
.getNumChildren(), args
.size() );
124 TS_ASSERT_EQUALS( n
.getKind(), AND
);
125 for( unsigned i
= 0; i
< args
.size(); ++i
) {
126 TS_ASSERT_EQUALS( n
[i
], args
[i
]);
130 void testMkNodeVectorOfTNodeChildren() {
131 Node x1
= d_nodeManager
->mkSkolem("x1",d_nodeManager
->booleanType());
132 Node x2
= d_nodeManager
->mkSkolem("x2",d_nodeManager
->booleanType());
133 Node x3
= d_nodeManager
->mkSkolem("x3",d_nodeManager
->booleanType());
134 std::vector
<TNode
> args
;
138 Node n
= d_nodeManager
->mkNode(AND
, args
);
139 TS_ASSERT_EQUALS( n
.getNumChildren(), args
.size() );
140 TS_ASSERT_EQUALS( n
.getKind(), AND
);
141 for( unsigned i
= 0; i
< args
.size(); ++i
) {
142 TS_ASSERT_EQUALS( n
[i
], args
[i
]);
146 void testMkVarWithName() {
147 TypeNode booleanType
= d_nodeManager
->booleanType();
148 Node x
= d_nodeManager
->mkSkolem("x", booleanType
, "", NodeManager::SKOLEM_EXACT_NAME
);
149 TS_ASSERT_EQUALS(x
.getKind(),SKOLEM
);
150 TS_ASSERT_EQUALS(x
.getNumChildren(),0u);
151 TS_ASSERT_EQUALS(x
.getAttribute(VarNameAttr()),"x");
152 TS_ASSERT_EQUALS(x
.getType(),booleanType
);
155 void testMkConstBool() {
156 Node tt
= d_nodeManager
->mkConst(true);
157 TS_ASSERT_EQUALS(tt
.getConst
<bool>(),true);
158 Node ff
= d_nodeManager
->mkConst(false);
159 TS_ASSERT_EQUALS(ff
.getConst
<bool>(),false);
162 void testMkConstRat() {
164 Node n
= d_nodeManager
->mkConst(r
);
165 TS_ASSERT_EQUALS(n
.getConst
<Rational
>(),r
);
168 void testHasOperator() {
169 TS_ASSERT( NodeManager::hasOperator(AND
) );
170 TS_ASSERT( NodeManager::hasOperator(OR
) );
171 TS_ASSERT( NodeManager::hasOperator(NOT
) );
172 TS_ASSERT( NodeManager::hasOperator(APPLY_UF
) );
173 TS_ASSERT( !NodeManager::hasOperator(VARIABLE
) );
176 void testBooleanType() {
177 TypeNode t
= d_nodeManager
->booleanType();
178 TypeNode t2
= d_nodeManager
->booleanType();
179 TypeNode t3
= d_nodeManager
->mkSort("T");
180 TS_ASSERT( t
.isBoolean() );
181 TS_ASSERT( !t
.isFunction() );
182 TS_ASSERT( !t
.isNull() );
183 TS_ASSERT( !t
.isPredicate() );
184 TS_ASSERT( !t
.isSort() );
185 TS_ASSERT_EQUALS(t
, t2
);
186 TS_ASSERT( t
!= t3
);
189 TS_ASSERT_EQUALS( bt
, t
);
192 void testMkFunctionTypeBoolToBool() {
193 TypeNode booleanType
= d_nodeManager
->booleanType();
194 TypeNode t
= d_nodeManager
->mkFunctionType(booleanType
,booleanType
);
195 TypeNode t2
= d_nodeManager
->mkFunctionType(booleanType
,booleanType
);
197 TS_ASSERT( !t
.isBoolean() );
198 TS_ASSERT( t
.isFunction() );
199 TS_ASSERT( !t
.isNull() );
200 TS_ASSERT( t
.isPredicate() );
201 TS_ASSERT( !t
.isSort() );
203 TS_ASSERT_EQUALS( t
, t2
);
206 TS_ASSERT_EQUALS( ft
, t
);
207 TS_ASSERT_EQUALS(ft
.getArgTypes().size(), 1u);
208 TS_ASSERT_EQUALS(ft
.getArgTypes()[0], booleanType
);
209 TS_ASSERT_EQUALS(ft
.getRangeType(), booleanType
);
213 void testMkFunctionTypeVectorOfArgsWithReturnType() {
214 TypeNode a
= d_nodeManager
->mkSort();
215 TypeNode b
= d_nodeManager
->mkSort();
216 TypeNode c
= d_nodeManager
->mkSort();
218 std::vector
<TypeNode
> argTypes
;
219 argTypes
.push_back(a
);
220 argTypes
.push_back(b
);
222 TypeNode t
= d_nodeManager
->mkFunctionType(argTypes
,c
);
223 TypeNode t2
= d_nodeManager
->mkFunctionType(argTypes
,c
);
225 TS_ASSERT( !t
.isBoolean() );
226 TS_ASSERT( t
.isFunction() );
227 TS_ASSERT( !t
.isNull() );
228 TS_ASSERT( !t
.isPredicate() );
229 TS_ASSERT( !t
.isSort() );
231 TS_ASSERT_EQUALS( t
, t2
);
234 TS_ASSERT_EQUALS( ft
, t
);
235 TS_ASSERT_EQUALS(ft
.getArgTypes().size(), argTypes
.size());
236 TS_ASSERT_EQUALS(ft
.getArgTypes()[0], a
);
237 TS_ASSERT_EQUALS(ft
.getArgTypes()[1], b
);
238 TS_ASSERT_EQUALS(ft
.getRangeType(), c
);
242 void testMkFunctionTypeVectorOfArguments() {
243 TypeNode a
= d_nodeManager
->mkSort();
244 TypeNode b
= d_nodeManager
->mkSort();
245 TypeNode c
= d_nodeManager
->mkSort();
247 std::vector
<TypeNode
> types
;
252 TypeNode t
= d_nodeManager
->mkFunctionType(types
);
253 TypeNode t2
= d_nodeManager
->mkFunctionType(types
);
255 TS_ASSERT( !t
.isBoolean() );
256 TS_ASSERT( t
.isFunction() );
257 TS_ASSERT( !t
.isNull() );
258 TS_ASSERT( !t
.isPredicate() );
259 TS_ASSERT( !t
.isSort() );
261 TS_ASSERT_EQUALS( t
, t2
);
264 TS_ASSERT_EQUALS( ft
, t
);
265 TS_ASSERT_EQUALS(ft
.getArgTypes().size(), types
.size()-1);
266 TS_ASSERT_EQUALS(ft
.getArgTypes()[0], a
);
267 TS_ASSERT_EQUALS(ft
.getArgTypes()[1], b
);
268 TS_ASSERT_EQUALS(ft
.getRangeType(), c
);
271 void testMkPredicateType() {
272 TypeNode a
= d_nodeManager
->mkSort("a");
273 TypeNode b
= d_nodeManager
->mkSort("b");
274 TypeNode c
= d_nodeManager
->mkSort("c");
275 TypeNode booleanType
= d_nodeManager
->booleanType();
277 std::vector
<TypeNode
> argTypes
;
278 argTypes
.push_back(a
);
279 argTypes
.push_back(b
);
280 argTypes
.push_back(c
);
282 TypeNode t
= d_nodeManager
->mkPredicateType(argTypes
);
283 TypeNode t2
= d_nodeManager
->mkPredicateType(argTypes
);
285 TS_ASSERT( !t
.isBoolean() );
286 TS_ASSERT( t
.isFunction() );
287 TS_ASSERT( !t
.isNull() );
288 TS_ASSERT( t
.isPredicate() );
289 TS_ASSERT( !t
.isSort() );
291 TS_ASSERT_EQUALS( t
, t2
);
294 TS_ASSERT_EQUALS( ft
, t
);
295 TS_ASSERT_EQUALS(ft
.getArgTypes().size(), argTypes
.size());
296 TS_ASSERT_EQUALS(ft
.getArgTypes()[0], a
);
297 TS_ASSERT_EQUALS(ft
.getArgTypes()[1], b
);
298 TS_ASSERT_EQUALS(ft
.getArgTypes()[2], c
);
299 TS_ASSERT_EQUALS(ft
.getRangeType(), booleanType
);
303 /* This test is only valid if assertions are enabled. */
304 void testMkNodeTooFew() {
305 #ifdef CVC4_ASSERTIONS
306 Node x
= d_nodeManager
->mkSkolem( "x", d_nodeManager
->booleanType() );
307 TS_ASSERT_THROWS( d_nodeManager
->mkNode(AND
, x
), AssertionException
);
311 /* This test is only valid if assertions are enabled. */
312 void testMkNodeTooMany() {
313 #ifdef CVC4_ASSERTIONS
314 std::vector
<Node
> vars
;
315 const unsigned int max
= metakind::getUpperBoundForKind(AND
);
316 TypeNode boolType
= d_nodeManager
->booleanType();
317 Node skolem
= d_nodeManager
->mkSkolem("i", boolType
);
318 for( unsigned int i
= 0; i
<= max
; ++i
) {
319 vars
.push_back( skolem
);
321 TS_ASSERT_THROWS( d_nodeManager
->mkNode(AND
, vars
), AssertionException
);