d88d72b854efb31633df0495fdd2c64ad5a5e326
1 /********************* */
2 /*! \file datatype_black.h
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): Andrew Reynolds
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 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::Datatype
14 ** Black box testing of CVC4::Datatype.
17 #include <cxxtest/TestSuite.h>
20 #include "util/datatype.h"
22 #include "expr/expr.h"
23 #include "expr/expr_manager.h"
28 class DatatypeBlack
: public CxxTest::TestSuite
{
35 d_em
= new ExprManager();
36 Debug
.on("datatypes");
37 Debug
.on("groundterms");
44 void testEnumeration() {
45 Datatype
colors("colors");
47 DatatypeConstructor
yellow("yellow", "is_yellow");
48 DatatypeConstructor
blue("blue", "is_blue");
49 DatatypeConstructor
green("green", "is_green");
50 DatatypeConstructor
red("red", "is_red");
52 colors
.addConstructor(yellow
);
53 colors
.addConstructor(blue
);
54 colors
.addConstructor(green
);
55 colors
.addConstructor(red
);
57 Debug("datatypes") << colors
<< std::endl
;
58 DatatypeType colorsType
= d_em
->mkDatatypeType(colors
);
59 Debug("datatypes") << colorsType
<< std::endl
;
61 Expr ctor
= colorsType
.getDatatype()[1].getConstructor();
62 Expr apply
= d_em
->mkExpr(kind::APPLY_CONSTRUCTOR
, ctor
);
63 Debug("datatypes") << apply
<< std::endl
;
65 const Datatype
& colorsDT
= colorsType
.getDatatype();
66 TS_ASSERT(colorsDT
.getConstructor("blue") == ctor
);
67 TS_ASSERT(colorsDT
["blue"].getConstructor() == ctor
);
68 TS_ASSERT_THROWS(colorsDT
["blue"].getSelector("foo"), IllegalArgumentException
);
69 TS_ASSERT_THROWS(colorsDT
["blue"]["foo"], IllegalArgumentException
);
71 TS_ASSERT(colorsType
.getDatatype().isFinite());
72 TS_ASSERT(colorsType
.getDatatype().getCardinality().compare(4) == Cardinality::EQUAL
);
73 TS_ASSERT(ctor
.getType().getCardinality().compare(1) == Cardinality::EQUAL
);
74 TS_ASSERT(colorsType
.getDatatype().isWellFounded());
75 Debug("groundterms") << "ground term of " << colorsType
.getDatatype().getName() << endl
76 << " is " << colorsType
.mkGroundTerm() << endl
;
77 TS_ASSERT(colorsType
.mkGroundTerm().getType() == colorsType
);
78 // all ctors should be well-founded too
79 for(Datatype::const_iterator i
= colorsType
.getDatatype().begin(),
80 i_end
= colorsType
.getDatatype().end();
83 TS_ASSERT((*i
).isWellFounded());
84 Debug("groundterms") << "ground term of " << *i
<< endl
85 << " is " << (*i
).mkGroundTerm( colorsType
) << endl
;
86 TS_ASSERT((*i
).mkGroundTerm( colorsType
).getType() == colorsType
);
93 DatatypeConstructor
succ("succ", "is_succ");
94 succ
.addArg("pred", DatatypeSelfType());
95 nat
.addConstructor(succ
);
97 DatatypeConstructor
zero("zero", "is_zero");
98 nat
.addConstructor(zero
);
100 Debug("datatypes") << nat
<< std::endl
;
101 DatatypeType natType
= d_em
->mkDatatypeType(nat
);
102 Debug("datatypes") << natType
<< std::endl
;
104 Expr ctor
= natType
.getDatatype()[1].getConstructor();
105 Expr apply
= d_em
->mkExpr(kind::APPLY_CONSTRUCTOR
, ctor
);
106 Debug("datatypes") << apply
<< std::endl
;
108 TS_ASSERT(! natType
.getDatatype().isFinite());
109 TS_ASSERT(natType
.getDatatype().getCardinality().compare(Cardinality::INTEGERS
) == Cardinality::EQUAL
);
110 TS_ASSERT(natType
.getDatatype().isWellFounded());
111 Debug("groundterms") << "ground term of " << natType
.getDatatype().getName() << endl
112 << " is " << natType
.mkGroundTerm() << endl
;
113 TS_ASSERT(natType
.mkGroundTerm().getType() == natType
);
114 // all ctors should be well-founded too
115 for(Datatype::const_iterator i
= natType
.getDatatype().begin(),
116 i_end
= natType
.getDatatype().end();
119 Debug("datatypes") << "checking " << (*i
).getName() << endl
;
120 TS_ASSERT((*i
).isWellFounded());
121 Debug("groundterms") << "ground term of " << *i
<< endl
122 << " is " << (*i
).mkGroundTerm( natType
) << endl
;
123 TS_ASSERT((*i
).mkGroundTerm( natType
).getType() == natType
);
128 Datatype
tree("tree");
129 Type integerType
= d_em
->integerType();
131 DatatypeConstructor
node("node", "is_node");
132 node
.addArg("left", DatatypeSelfType());
133 node
.addArg("right", DatatypeSelfType());
134 tree
.addConstructor(node
);
136 DatatypeConstructor
leaf("leaf", "is_leaf");
137 leaf
.addArg("leaf", integerType
);
138 tree
.addConstructor(leaf
);
140 Debug("datatypes") << tree
<< std::endl
;
141 DatatypeType treeType
= d_em
->mkDatatypeType(tree
);
142 Debug("datatypes") << treeType
<< std::endl
;
144 Expr ctor
= treeType
.getDatatype()[1].getConstructor();
145 TS_ASSERT(treeType
.getConstructor("leaf") == ctor
);
146 TS_ASSERT(treeType
.getConstructor("leaf") == ctor
);
147 TS_ASSERT_THROWS(treeType
.getConstructor("leff"), IllegalArgumentException
);
149 TS_ASSERT(! treeType
.getDatatype().isFinite());
150 TS_ASSERT(treeType
.getDatatype().getCardinality().compare(Cardinality::INTEGERS
) == Cardinality::EQUAL
);
151 TS_ASSERT(treeType
.getDatatype().isWellFounded());
152 Debug("groundterms") << "ground term of " << treeType
.getDatatype().getName() << endl
153 << " is " << treeType
.mkGroundTerm() << endl
;
154 TS_ASSERT(treeType
.mkGroundTerm().getType() == treeType
);
155 // all ctors should be well-founded too
156 for(Datatype::const_iterator i
= treeType
.getDatatype().begin(),
157 i_end
= treeType
.getDatatype().end();
160 TS_ASSERT((*i
).isWellFounded());
161 Debug("groundterms") << "ground term of " << *i
<< endl
162 << " is " << (*i
).mkGroundTerm( treeType
) << endl
;
163 TS_ASSERT((*i
).mkGroundTerm( treeType
).getType() == treeType
);
168 Datatype
list("list");
169 Type integerType
= d_em
->integerType();
171 DatatypeConstructor
cons("cons", "is_cons");
172 cons
.addArg("car", integerType
);
173 cons
.addArg("cdr", DatatypeSelfType());
174 list
.addConstructor(cons
);
176 DatatypeConstructor
nil("nil", "is_nil");
177 list
.addConstructor(nil
);
179 Debug("datatypes") << list
<< std::endl
;
180 DatatypeType listType
= d_em
->mkDatatypeType(list
);
181 Debug("datatypes") << listType
<< std::endl
;
183 TS_ASSERT(! listType
.getDatatype().isFinite());
184 TS_ASSERT(listType
.getDatatype().getCardinality().compare(Cardinality::INTEGERS
) == Cardinality::EQUAL
);
185 TS_ASSERT(listType
.getDatatype().isWellFounded());
186 Debug("groundterms") << "ground term of " << listType
.getDatatype().getName() << endl
187 << " is " << listType
.mkGroundTerm() << endl
;
188 TS_ASSERT(listType
.mkGroundTerm().getType() == listType
);
189 // all ctors should be well-founded too
190 for(Datatype::const_iterator i
= listType
.getDatatype().begin(),
191 i_end
= listType
.getDatatype().end();
194 TS_ASSERT((*i
).isWellFounded());
195 Debug("groundterms") << "ground term of " << *i
<< endl
196 << " is " << (*i
).mkGroundTerm( listType
) << endl
;
197 TS_ASSERT((*i
).mkGroundTerm( listType
).getType() == listType
);
201 void testListReal() {
202 Datatype
list("list");
203 Type realType
= d_em
->realType();
205 DatatypeConstructor
cons("cons", "is_cons");
206 cons
.addArg("car", realType
);
207 cons
.addArg("cdr", DatatypeSelfType());
208 list
.addConstructor(cons
);
210 DatatypeConstructor
nil("nil", "is_nil");
211 list
.addConstructor(nil
);
213 Debug("datatypes") << list
<< std::endl
;
214 DatatypeType listType
= d_em
->mkDatatypeType(list
);
215 Debug("datatypes") << listType
<< std::endl
;
217 TS_ASSERT(! listType
.getDatatype().isFinite());
218 TS_ASSERT(listType
.getDatatype().getCardinality().compare(Cardinality::REALS
) == Cardinality::EQUAL
);
219 TS_ASSERT(listType
.getDatatype().isWellFounded());
220 Debug("groundterms") << "ground term of " << listType
.getDatatype().getName() << endl
221 << " is " << listType
.mkGroundTerm() << endl
;
222 TS_ASSERT(listType
.mkGroundTerm().getType() == listType
);
223 // all ctors should be well-founded too
224 for(Datatype::const_iterator i
= listType
.getDatatype().begin(),
225 i_end
= listType
.getDatatype().end();
228 TS_ASSERT((*i
).isWellFounded());
229 Debug("groundterms") << "ground term of " << *i
<< endl
230 << " is " << (*i
).mkGroundTerm( listType
) << endl
;
231 TS_ASSERT((*i
).mkGroundTerm( listType
).getType() == listType
);
235 void testListBoolean() {
236 Datatype
list("list");
237 Type booleanType
= d_em
->booleanType();
239 DatatypeConstructor
cons("cons", "is_cons");
240 cons
.addArg("car", booleanType
);
241 cons
.addArg("cdr", DatatypeSelfType());
242 list
.addConstructor(cons
);
244 DatatypeConstructor
nil("nil", "is_nil");
245 list
.addConstructor(nil
);
247 Debug("datatypes") << list
<< std::endl
;
248 DatatypeType listType
= d_em
->mkDatatypeType(list
);
249 Debug("datatypes") << listType
<< std::endl
;
251 TS_ASSERT(! listType
.getDatatype().isFinite());
252 TS_ASSERT(listType
.getDatatype().getCardinality().compare(Cardinality::INTEGERS
) == Cardinality::EQUAL
);
253 TS_ASSERT(listType
.getDatatype().isWellFounded());
254 Debug("groundterms") << "ground term of " << listType
.getDatatype().getName() << endl
255 << " is " << listType
.mkGroundTerm() << endl
;
256 TS_ASSERT(listType
.mkGroundTerm().getType() == listType
);
257 // all ctors should be well-founded too
258 for(Datatype::const_iterator i
= listType
.getDatatype().begin(),
259 i_end
= listType
.getDatatype().end();
262 TS_ASSERT((*i
).isWellFounded());
263 Debug("groundterms") << "ground term of " << *i
<< endl
264 << " is " << (*i
).mkGroundTerm( listType
) << endl
;
265 TS_ASSERT((*i
).mkGroundTerm( listType
).getType() == listType
);
269 void testMutualListTrees() {
270 /* Create two mutual datatypes corresponding to this definition
274 * tree = node(left: tree, right: tree) | leaf(list),
275 * list = cons(car: tree, cdr: list) | nil
278 Datatype
tree("tree");
279 DatatypeConstructor
node("node", "is_node");
280 node
.addArg("left", DatatypeSelfType());
281 node
.addArg("right", DatatypeSelfType());
282 tree
.addConstructor(node
);
284 DatatypeConstructor
leaf("leaf", "is_leaf");
285 leaf
.addArg("leaf", DatatypeUnresolvedType("list"));
286 tree
.addConstructor(leaf
);
288 Debug("datatypes") << tree
<< std::endl
;
290 Datatype
list("list");
291 DatatypeConstructor
cons("cons", "is_cons");
292 cons
.addArg("car", DatatypeUnresolvedType("tree"));
293 cons
.addArg("cdr", DatatypeSelfType());
294 list
.addConstructor(cons
);
296 DatatypeConstructor
nil("nil", "is_nil");
297 list
.addConstructor(nil
);
299 Debug("datatypes") << list
<< std::endl
;
301 TS_ASSERT(! tree
.isResolved());
302 TS_ASSERT(! node
.isResolved());
303 TS_ASSERT(! leaf
.isResolved());
304 TS_ASSERT(! list
.isResolved());
305 TS_ASSERT(! cons
.isResolved());
306 TS_ASSERT(! nil
.isResolved());
308 vector
<Datatype
> dts
;
311 vector
<DatatypeType
> dtts
= d_em
->mkMutualDatatypeTypes(dts
);
313 TS_ASSERT(dtts
[0].getDatatype().isResolved());
314 TS_ASSERT(dtts
[1].getDatatype().isResolved());
316 TS_ASSERT(! dtts
[0].getDatatype().isFinite());
317 TS_ASSERT(dtts
[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS
) == Cardinality::EQUAL
);
318 TS_ASSERT(dtts
[0].getDatatype().isWellFounded());
319 Debug("groundterms") << "ground term of " << dtts
[0].getDatatype().getName() << endl
320 << " is " << dtts
[0].mkGroundTerm() << endl
;
321 TS_ASSERT(dtts
[0].mkGroundTerm().getType() == dtts
[0]);
322 // all ctors should be well-founded too
323 for(Datatype::const_iterator i
= dtts
[0].getDatatype().begin(),
324 i_end
= dtts
[0].getDatatype().end();
327 TS_ASSERT((*i
).isWellFounded());
328 Debug("groundterms") << "ground term of " << *i
<< endl
329 << " is " << (*i
).mkGroundTerm( dtts
[0] ) << endl
;
330 TS_ASSERT((*i
).mkGroundTerm( dtts
[0] ).getType() == dtts
[0]);
333 TS_ASSERT(! dtts
[1].getDatatype().isFinite());
334 TS_ASSERT(dtts
[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS
) == Cardinality::EQUAL
);
335 TS_ASSERT(dtts
[1].getDatatype().isWellFounded());
336 Debug("groundterms") << "ground term of " << dtts
[1].getDatatype().getName() << endl
337 << " is " << dtts
[1].mkGroundTerm() << endl
;
338 TS_ASSERT(dtts
[1].mkGroundTerm().getType() == dtts
[1]);
339 // all ctors should be well-founded too
340 for(Datatype::const_iterator i
= dtts
[1].getDatatype().begin(),
341 i_end
= dtts
[1].getDatatype().end();
344 TS_ASSERT((*i
).isWellFounded());
345 Debug("groundterms") << "ground term of " << *i
<< endl
346 << " is " << (*i
).mkGroundTerm( dtts
[1] ) << endl
;
347 TS_ASSERT((*i
).mkGroundTerm( dtts
[1] ).getType() == dtts
[1]);
350 // add another constructor to list datatype resulting in an
352 DatatypeConstructor
otherNil("otherNil", "is_otherNil");
353 dts
[1].addConstructor(otherNil
);
356 vector
<DatatypeType
> dtts2
= d_em
->mkMutualDatatypeTypes(dts
);
358 TS_ASSERT_DIFFERS(dtts
, dtts2
);
359 TS_ASSERT_DIFFERS(dtts
[1], dtts2
[1]);
361 // tree is also different because it's a tree of otherNil-lists
362 TS_ASSERT_DIFFERS(dtts
[0], dtts2
[0]);
364 TS_ASSERT(! dtts2
[0].getDatatype().isFinite());
365 TS_ASSERT(dtts2
[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS
) == Cardinality::EQUAL
);
366 TS_ASSERT(dtts2
[0].getDatatype().isWellFounded());
367 Debug("groundterms") << "ground term of " << dtts2
[0].getDatatype().getName() << endl
368 << " is " << dtts2
[0].mkGroundTerm() << endl
;
369 TS_ASSERT(dtts2
[0].mkGroundTerm().getType() == dtts2
[0]);
370 // all ctors should be well-founded too
371 for(Datatype::const_iterator i
= dtts2
[0].getDatatype().begin(),
372 i_end
= dtts2
[0].getDatatype().end();
375 TS_ASSERT((*i
).isWellFounded());
376 Debug("groundterms") << "ground term of " << *i
<< endl
377 << " is " << (*i
).mkGroundTerm( dtts2
[0] ) << endl
;
378 TS_ASSERT((*i
).mkGroundTerm( dtts2
[0] ).getType() == dtts2
[0]);
381 TS_ASSERT(! dtts2
[1].getDatatype().isFinite());
382 TS_ASSERT(dtts2
[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS
) == Cardinality::EQUAL
);
383 TS_ASSERT(dtts2
[1].getDatatype().isWellFounded());
384 Debug("groundterms") << "ground term of " << dtts2
[1].getDatatype().getName() << endl
385 << " is " << dtts2
[1].mkGroundTerm() << endl
;
386 TS_ASSERT(dtts2
[1].mkGroundTerm().getType() == dtts2
[1]);
387 // all ctors should be well-founded too
388 for(Datatype::const_iterator i
= dtts2
[1].getDatatype().begin(),
389 i_end
= dtts2
[1].getDatatype().end();
392 TS_ASSERT((*i
).isWellFounded());
393 Debug("groundterms") << "ground term of " << *i
<< endl
394 << " is " << (*i
).mkGroundTerm( dtts2
[1] ) << endl
;
395 TS_ASSERT((*i
).mkGroundTerm( dtts2
[1] ).getType() == dtts2
[1]);
399 void testNotSoWellFounded() {
400 Datatype
tree("tree");
402 DatatypeConstructor
node("node", "is_node");
403 node
.addArg("left", DatatypeSelfType());
404 node
.addArg("right", DatatypeSelfType());
405 tree
.addConstructor(node
);
407 Debug("datatypes") << tree
<< std::endl
;
408 DatatypeType treeType
= d_em
->mkDatatypeType(tree
);
409 Debug("datatypes") << treeType
<< std::endl
;
411 TS_ASSERT(! treeType
.getDatatype().isFinite());
412 TS_ASSERT(treeType
.getDatatype().getCardinality().compare(Cardinality::INTEGERS
) == Cardinality::EQUAL
);
413 TS_ASSERT(! treeType
.getDatatype().isWellFounded());
414 TS_ASSERT_THROWS_ANYTHING( treeType
.mkGroundTerm() );
415 TS_ASSERT_THROWS_ANYTHING( treeType
.getDatatype().mkGroundTerm( treeType
) );
416 // all ctors should be not-well-founded either
417 for(Datatype::const_iterator i
= treeType
.getDatatype().begin(),
418 i_end
= treeType
.getDatatype().end();
421 TS_ASSERT(! (*i
).isWellFounded());
422 TS_ASSERT_THROWS_ANYTHING( (*i
).mkGroundTerm( treeType
) );
426 };/* class DatatypeBlack */