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