1 /*********************                                                        */
2 /*! \file datatype_black.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Morgan Deters, Andrew Reynolds, Andres Noetzli
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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
11  **
12  ** \brief Black box testing of CVC4::Datatype
13  **
14  ** Black box testing of CVC4::Datatype.
15  **/
16 
17 #include <cxxtest/TestSuite.h>
18 #include <sstream>
19 
20 #include "expr/datatype.h"
21 #include "expr/expr.h"
22 #include "expr/expr_manager.h"
23 #include "expr/expr_manager_scope.h"
24 #include "expr/type_node.h"
25 
26 using namespace CVC4;
27 using namespace std;
28 
29 class DatatypeBlack : public CxxTest::TestSuite {
30 
31   ExprManager* d_em;
32   ExprManagerScope* d_scope;
33 
34  public:
setUp()35   void setUp() override
36   {
37     d_em = new ExprManager();
38     d_scope = new ExprManagerScope(*d_em);
39     Debug.on("datatypes");
40     Debug.on("groundterms");
41   }
42 
tearDown()43   void tearDown() override
44   {
45     delete d_scope;
46     delete d_em;
47   }
48 
testEnumeration()49   void testEnumeration() {
50     Datatype colors("colors");
51 
52     DatatypeConstructor yellow("yellow", "is_yellow");
53     DatatypeConstructor blue("blue", "is_blue");
54     DatatypeConstructor green("green", "is_green");
55     DatatypeConstructor red("red", "is_red");
56 
57     colors.addConstructor(yellow);
58     colors.addConstructor(blue);
59     colors.addConstructor(green);
60     colors.addConstructor(red);
61 
62     Debug("datatypes") << colors << std::endl;
63     DatatypeType colorsType = d_em->mkDatatypeType(colors);
64     Debug("datatypes") << colorsType << std::endl;
65 
66     Expr ctor = colorsType.getDatatype()[1].getConstructor();
67     Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor);
68     Debug("datatypes") << apply << std::endl;
69 
70     const Datatype& colorsDT = colorsType.getDatatype();
71     TS_ASSERT(colorsDT.getConstructor("blue") == ctor);
72     TS_ASSERT(colorsDT["blue"].getConstructor() == ctor);
73     TS_ASSERT_THROWS(colorsDT["blue"].getSelector("foo"),
74                      IllegalArgumentException&);
75     TS_ASSERT_THROWS(colorsDT["blue"]["foo"], IllegalArgumentException&);
76 
77     TS_ASSERT(! colorsType.getDatatype().isParametric());
78     TS_ASSERT(colorsType.getDatatype().isFinite());
79     TS_ASSERT(colorsType.getDatatype().getCardinality().compare(4) == Cardinality::EQUAL);
80     TS_ASSERT(ctor.getType().getCardinality().compare(1) == Cardinality::EQUAL);
81     TS_ASSERT(colorsType.getDatatype().isWellFounded());
82     Debug("groundterms") << "ground term of " << colorsType.getDatatype().getName() << endl
83                          << "  is " << colorsType.mkGroundTerm() << endl;
84     TS_ASSERT(colorsType.mkGroundTerm().getType() == colorsType);
85   }
86 
testNat()87   void testNat() {
88     Datatype nat("nat");
89 
90     DatatypeConstructor succ("succ", "is_succ");
91     succ.addArg("pred", DatatypeSelfType());
92     nat.addConstructor(succ);
93 
94     DatatypeConstructor zero("zero", "is_zero");
95     nat.addConstructor(zero);
96 
97     Debug("datatypes") << nat << std::endl;
98     DatatypeType natType = d_em->mkDatatypeType(nat);
99     Debug("datatypes") << natType << std::endl;
100 
101     Expr ctor = natType.getDatatype()[1].getConstructor();
102     Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor);
103     Debug("datatypes") << apply << std::endl;
104 
105     TS_ASSERT(! natType.getDatatype().isParametric());
106     TS_ASSERT(! natType.getDatatype().isFinite());
107     TS_ASSERT(natType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
108     TS_ASSERT(natType.getDatatype().isWellFounded());
109     Debug("groundterms") << "ground term of " << natType.getDatatype().getName() << endl
110                          << "  is " << natType.mkGroundTerm() << endl;
111     TS_ASSERT(natType.mkGroundTerm().getType() == natType);
112   }
113 
testTree()114   void testTree() {
115     Datatype tree("tree");
116     Type integerType = d_em->integerType();
117 
118     DatatypeConstructor node("node", "is_node");
119     node.addArg("left", DatatypeSelfType());
120     node.addArg("right", DatatypeSelfType());
121     tree.addConstructor(node);
122 
123     DatatypeConstructor leaf("leaf", "is_leaf");
124     leaf.addArg("leaf", integerType);
125     tree.addConstructor(leaf);
126 
127     Debug("datatypes") << tree << std::endl;
128     DatatypeType treeType = d_em->mkDatatypeType(tree);
129     Debug("datatypes") << treeType << std::endl;
130 
131     Expr ctor = treeType.getDatatype()[1].getConstructor();
132     TS_ASSERT(treeType.getConstructor("leaf") == ctor);
133     TS_ASSERT(treeType.getConstructor("leaf") == ctor);
134     TS_ASSERT_THROWS(treeType.getConstructor("leff"),
135                      IllegalArgumentException&);
136 
137     TS_ASSERT(! treeType.getDatatype().isParametric());
138     TS_ASSERT(! treeType.getDatatype().isFinite());
139     TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
140     TS_ASSERT(treeType.getDatatype().isWellFounded());
141     Debug("groundterms") << "ground term of " << treeType.getDatatype().getName() << endl
142                          << "  is " << treeType.mkGroundTerm() << endl;
143     TS_ASSERT(treeType.mkGroundTerm().getType() == treeType);
144   }
145 
testListInt()146   void testListInt() {
147     Datatype list("list");
148     Type integerType = d_em->integerType();
149 
150     DatatypeConstructor cons("cons", "is_cons");
151     cons.addArg("car", integerType);
152     cons.addArg("cdr", DatatypeSelfType());
153     list.addConstructor(cons);
154 
155     DatatypeConstructor nil("nil", "is_nil");
156     list.addConstructor(nil);
157 
158     Debug("datatypes") << list << std::endl;
159     DatatypeType listType = d_em->mkDatatypeType(list);
160     Debug("datatypes") << listType << std::endl;
161 
162     TS_ASSERT(! listType.getDatatype().isParametric());
163     TS_ASSERT(! listType.getDatatype().isFinite());
164     TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
165     TS_ASSERT(listType.getDatatype().isWellFounded());
166     Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
167                          << "  is " << listType.mkGroundTerm() << endl;
168     TS_ASSERT(listType.mkGroundTerm().getType() == listType);
169   }
170 
testListReal()171   void testListReal() {
172     Datatype list("list");
173     Type realType = d_em->realType();
174 
175     DatatypeConstructor cons("cons", "is_cons");
176     cons.addArg("car", realType);
177     cons.addArg("cdr", DatatypeSelfType());
178     list.addConstructor(cons);
179 
180     DatatypeConstructor nil("nil", "is_nil");
181     list.addConstructor(nil);
182 
183     Debug("datatypes") << list << std::endl;
184     DatatypeType listType = d_em->mkDatatypeType(list);
185     Debug("datatypes") << listType << std::endl;
186 
187     TS_ASSERT(! listType.getDatatype().isParametric());
188     TS_ASSERT(! listType.getDatatype().isFinite());
189     TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL);
190     TS_ASSERT(listType.getDatatype().isWellFounded());
191     Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
192                          << "  is " << listType.mkGroundTerm() << endl;
193     TS_ASSERT(listType.mkGroundTerm().getType() == listType);
194   }
195 
testListBoolean()196   void testListBoolean() {
197     Datatype list("list");
198     Type booleanType = d_em->booleanType();
199 
200     DatatypeConstructor cons("cons", "is_cons");
201     cons.addArg("car", booleanType);
202     cons.addArg("cdr", DatatypeSelfType());
203     list.addConstructor(cons);
204 
205     DatatypeConstructor nil("nil", "is_nil");
206     list.addConstructor(nil);
207 
208     Debug("datatypes") << list << std::endl;
209     DatatypeType listType = d_em->mkDatatypeType(list);
210     Debug("datatypes") << listType << std::endl;
211 
212     TS_ASSERT(! listType.getDatatype().isFinite());
213     TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
214     TS_ASSERT(listType.getDatatype().isWellFounded());
215     Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
216                          << "  is " << listType.mkGroundTerm() << endl;
217     TS_ASSERT(listType.mkGroundTerm().getType() == listType);
218   }
219 
testMutualListTrees()220   void testMutualListTrees() {
221     /* Create two mutual datatypes corresponding to this definition
222      * block:
223      *
224      *   DATATYPE
225      *     tree = node(left: tree, right: tree) | leaf(list),
226      *     list = cons(car: tree, cdr: list) | nil
227      *   END;
228      */
229     Datatype tree("tree");
230     DatatypeConstructor node("node", "is_node");
231     node.addArg("left", DatatypeSelfType());
232     node.addArg("right", DatatypeSelfType());
233     tree.addConstructor(node);
234 
235     DatatypeConstructor leaf("leaf", "is_leaf");
236     leaf.addArg("leaf", DatatypeUnresolvedType("list"));
237     tree.addConstructor(leaf);
238 
239     Debug("datatypes") << tree << std::endl;
240 
241     Datatype list("list");
242     DatatypeConstructor cons("cons", "is_cons");
243     cons.addArg("car", DatatypeUnresolvedType("tree"));
244     cons.addArg("cdr", DatatypeSelfType());
245     list.addConstructor(cons);
246 
247     DatatypeConstructor nil("nil", "is_nil");
248     list.addConstructor(nil);
249 
250     Debug("datatypes") << list << std::endl;
251 
252     TS_ASSERT(! tree.isResolved());
253     TS_ASSERT(! node.isResolved());
254     TS_ASSERT(! leaf.isResolved());
255     TS_ASSERT(! list.isResolved());
256     TS_ASSERT(! cons.isResolved());
257     TS_ASSERT(! nil.isResolved());
258 
259     vector<Datatype> dts;
260     dts.push_back(tree);
261     dts.push_back(list);
262     vector<DatatypeType> dtts = d_em->mkMutualDatatypeTypes(dts);
263 
264     TS_ASSERT(dtts[0].getDatatype().isResolved());
265     TS_ASSERT(dtts[1].getDatatype().isResolved());
266 
267     TS_ASSERT(! dtts[0].getDatatype().isFinite());
268     TS_ASSERT(dtts[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
269     TS_ASSERT(dtts[0].getDatatype().isWellFounded());
270     Debug("groundterms") << "ground term of " << dtts[0].getDatatype().getName() << endl
271                          << "  is " << dtts[0].mkGroundTerm() << endl;
272     TS_ASSERT(dtts[0].mkGroundTerm().getType() == dtts[0]);
273 
274     TS_ASSERT(! dtts[1].getDatatype().isFinite());
275     TS_ASSERT(dtts[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
276     TS_ASSERT(dtts[1].getDatatype().isWellFounded());
277     Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl
278                          << "  is " << dtts[1].mkGroundTerm() << endl;
279     TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]);
280 
281     // add another constructor to list datatype resulting in an
282     // "otherNil-list"
283     DatatypeConstructor otherNil("otherNil", "is_otherNil");
284     dts[1].addConstructor(otherNil);
285 
286     // remake the types
287     vector<DatatypeType> dtts2 = d_em->mkMutualDatatypeTypes(dts);
288 
289     TS_ASSERT_DIFFERS(dtts, dtts2);
290     TS_ASSERT_DIFFERS(dtts[1], dtts2[1]);
291 
292     // tree is also different because it's a tree of otherNil-lists
293     TS_ASSERT_DIFFERS(dtts[0], dtts2[0]);
294 
295     TS_ASSERT(! dtts2[0].getDatatype().isFinite());
296     TS_ASSERT(dtts2[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
297     TS_ASSERT(dtts2[0].getDatatype().isWellFounded());
298     Debug("groundterms") << "ground term of " << dtts2[0].getDatatype().getName() << endl
299                          << "  is " << dtts2[0].mkGroundTerm() << endl;
300     TS_ASSERT(dtts2[0].mkGroundTerm().getType() == dtts2[0]);
301 
302     TS_ASSERT(! dtts2[1].getDatatype().isParametric());
303     TS_ASSERT(! dtts2[1].getDatatype().isFinite());
304     TS_ASSERT(dtts2[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
305     TS_ASSERT(dtts2[1].getDatatype().isWellFounded());
306     Debug("groundterms") << "ground term of " << dtts2[1].getDatatype().getName() << endl
307                          << "  is " << dtts2[1].mkGroundTerm() << endl;
308     TS_ASSERT(dtts2[1].mkGroundTerm().getType() == dtts2[1]);
309   }
310 
testNotSoWellFounded()311   void testNotSoWellFounded() {
312     Datatype tree("tree");
313 
314     DatatypeConstructor node("node", "is_node");
315     node.addArg("left", DatatypeSelfType());
316     node.addArg("right", DatatypeSelfType());
317     tree.addConstructor(node);
318 
319     Debug("datatypes") << tree << std::endl;
320     DatatypeType treeType = d_em->mkDatatypeType(tree);
321     Debug("datatypes") << treeType << std::endl;
322 
323     TS_ASSERT(! treeType.getDatatype().isParametric());
324     TS_ASSERT(! treeType.getDatatype().isFinite());
325     TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
326     TS_ASSERT(! treeType.getDatatype().isWellFounded());
327     TS_ASSERT_THROWS_ANYTHING( treeType.mkGroundTerm() );
328     TS_ASSERT_THROWS_ANYTHING( treeType.getDatatype().mkGroundTerm( treeType ) );
329   }
330 
testParametricDatatype()331   void testParametricDatatype() {
332     vector<Type> v;
333     Type t1, t2;
334     v.push_back(t1 = d_em->mkSort("T1"));
335     v.push_back(t2 = d_em->mkSort("T2"));
336     Datatype pair("pair", v);
337 
338     DatatypeConstructor mkpair("mk-pair");
339     mkpair.addArg("first", t1);
340     mkpair.addArg("second", t2);
341     pair.addConstructor(mkpair);
342     DatatypeType pairType = d_em->mkDatatypeType(pair);
343 
344     TS_ASSERT(pairType.getDatatype().isParametric());
345     v.clear();
346     v.push_back(d_em->integerType());
347     v.push_back(d_em->integerType());
348     DatatypeType pairIntInt = pairType.getDatatype().getDatatypeType(v);
349     v.clear();
350     v.push_back(d_em->realType());
351     v.push_back(d_em->realType());
352     DatatypeType pairRealReal = pairType.getDatatype().getDatatypeType(v);
353     v.clear();
354     v.push_back(d_em->realType());
355     v.push_back(d_em->integerType());
356     DatatypeType pairRealInt = pairType.getDatatype().getDatatypeType(v);
357     v.clear();
358     v.push_back(d_em->integerType());
359     v.push_back(d_em->realType());
360     DatatypeType pairIntReal = pairType.getDatatype().getDatatypeType(v);
361 
362     TS_ASSERT_DIFFERS(pairIntInt, pairRealReal);
363     TS_ASSERT_DIFFERS(pairIntReal, pairRealReal);
364     TS_ASSERT_DIFFERS(pairRealInt, pairRealReal);
365     TS_ASSERT_DIFFERS(pairIntInt, pairIntReal);
366     TS_ASSERT_DIFFERS(pairIntInt, pairRealInt);
367     TS_ASSERT_DIFFERS(pairIntReal, pairRealInt);
368 
369     TS_ASSERT(pairRealReal.isComparableTo(pairRealReal));
370     TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal));
371     TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal));
372     TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal));
373     TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt));
374     TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt));
375     TS_ASSERT(pairRealInt.isComparableTo(pairRealInt));
376     TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt));
377     TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal));
378     TS_ASSERT(pairIntReal.isComparableTo(pairIntReal));
379     TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal));
380     TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal));
381     TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt));
382     TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt));
383     TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt));
384     TS_ASSERT(pairIntInt.isComparableTo(pairIntInt));
385 
386     TS_ASSERT(pairRealReal.isSubtypeOf(pairRealReal));
387     TS_ASSERT(!pairIntReal.isSubtypeOf(pairRealReal));
388     TS_ASSERT(!pairRealInt.isSubtypeOf(pairRealReal));
389     TS_ASSERT(!pairIntInt.isSubtypeOf(pairRealReal));
390     TS_ASSERT(!pairRealReal.isSubtypeOf(pairRealInt));
391     TS_ASSERT(!pairIntReal.isSubtypeOf(pairRealInt));
392     TS_ASSERT(pairRealInt.isSubtypeOf(pairRealInt));
393     TS_ASSERT(!pairIntInt.isSubtypeOf(pairRealInt));
394     TS_ASSERT(!pairRealReal.isSubtypeOf(pairIntReal));
395     TS_ASSERT(pairIntReal.isSubtypeOf(pairIntReal));
396     TS_ASSERT(!pairRealInt.isSubtypeOf(pairIntReal));
397     TS_ASSERT(!pairIntInt.isSubtypeOf(pairIntReal));
398     TS_ASSERT(!pairRealReal.isSubtypeOf(pairIntInt));
399     TS_ASSERT(!pairIntReal.isSubtypeOf(pairIntInt));
400     TS_ASSERT(!pairRealInt.isSubtypeOf(pairIntInt));
401     TS_ASSERT(pairIntInt.isSubtypeOf(pairIntInt));
402 
403     TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealReal)).toType(), pairRealReal);
404     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealReal)).isNull());
405     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealReal)).isNull());
406     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealReal)).isNull());
407     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealInt)).isNull());
408     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealInt)).isNull());
409     TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealInt)).toType(), pairRealInt);
410     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealInt)).isNull());
411     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntReal)).isNull());
412     TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntReal)).toType(), pairIntReal);
413     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntReal)).isNull());
414     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntReal)).isNull());
415     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntInt)).isNull());
416     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntInt)).isNull());
417     TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntInt)).isNull());
418     TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt);
419   }
420 
421 };/* class DatatypeBlack */
422