test/unit/util/datatype_black.h

   1 /*********************                                                        */
   2 /*! \file datatype_black.h
   3  ** \verbatim
   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
  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 "util/datatype.h"
  21
  22 #include "expr/expr.h"
  23 #include "expr/expr_manager.h"
  24
  25 using namespace CVC4;
  26 using namespace std;
  27
  28 class DatatypeBlack : public CxxTest::TestSuite {
  29
  30   ExprManager* d_em;
  31
  32 public:
  33
  34   void setUp() {
  35     d_em = new ExprManager();
  36     Debug.on("datatypes");
  37     Debug.on("groundterms");
  38   }
  39
  40   void tearDown() {
  41     delete d_em;
  42   }
  43
  44   void testEnumeration() {
  45     Datatype colors("colors");
  46
  47     DatatypeConstructor yellow("yellow", "is_yellow");
  48     DatatypeConstructor blue("blue", "is_blue");
  49     DatatypeConstructor green("green", "is_green");
  50     DatatypeConstructor red("red", "is_red");
  51
  52     colors.addConstructor(yellow);
  53     colors.addConstructor(blue);
  54     colors.addConstructor(green);
  55     colors.addConstructor(red);
  56
  57     Debug("datatypes") << colors << std::endl;
  58     DatatypeType colorsType = d_em->mkDatatypeType(colors);
  59     Debug("datatypes") << colorsType << std::endl;
  60
  61     Expr ctor = colorsType.getDatatype()[1].getConstructor();
  62     Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor);
  63     Debug("datatypes") << apply << std::endl;
  64
  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);
  70
  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();
  81         i != i_end;
  82         ++i) {
  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);
  87     }
  88   }
  89
  90   void testNat() {
  91     Datatype nat("nat");
  92
  93     DatatypeConstructor succ("succ", "is_succ");
  94     succ.addArg("pred", DatatypeSelfType());
  95     nat.addConstructor(succ);
  96
  97     DatatypeConstructor zero("zero", "is_zero");
  98     nat.addConstructor(zero);
  99
 100     Debug("datatypes") << nat << std::endl;
 101     DatatypeType natType = d_em->mkDatatypeType(nat);
 102     Debug("datatypes") << natType << std::endl;
 103
 104     Expr ctor = natType.getDatatype()[1].getConstructor();
 105     Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor);
 106     Debug("datatypes") << apply << std::endl;
 107
 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();
 117         i != i_end;
 118         ++i) {
 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);
 124     }
 125   }
 126
 127   void testTree() {
 128     Datatype tree("tree");
 129     Type integerType = d_em->integerType();
 130
 131     DatatypeConstructor node("node", "is_node");
 132     node.addArg("left", DatatypeSelfType());
 133     node.addArg("right", DatatypeSelfType());
 134     tree.addConstructor(node);
 135
 136     DatatypeConstructor leaf("leaf", "is_leaf");
 137     leaf.addArg("leaf", integerType);
 138     tree.addConstructor(leaf);
 139
 140     Debug("datatypes") << tree << std::endl;
 141     DatatypeType treeType = d_em->mkDatatypeType(tree);
 142     Debug("datatypes") << treeType << std::endl;
 143
 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);
 148
 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();
 158         i != i_end;
 159         ++i) {
 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);
 164     }
 165   }
 166
 167   void testListInt() {
 168     Datatype list("list");
 169     Type integerType = d_em->integerType();
 170
 171     DatatypeConstructor cons("cons", "is_cons");
 172     cons.addArg("car", integerType);
 173     cons.addArg("cdr", DatatypeSelfType());
 174     list.addConstructor(cons);
 175
 176     DatatypeConstructor nil("nil", "is_nil");
 177     list.addConstructor(nil);
 178
 179     Debug("datatypes") << list << std::endl;
 180     DatatypeType listType = d_em->mkDatatypeType(list);
 181     Debug("datatypes") << listType << std::endl;
 182
 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();
 192         i != i_end;
 193         ++i) {
 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);
 198     }
 199   }
 200
 201   void testListReal() {
 202     Datatype list("list");
 203     Type realType = d_em->realType();
 204
 205     DatatypeConstructor cons("cons", "is_cons");
 206     cons.addArg("car", realType);
 207     cons.addArg("cdr", DatatypeSelfType());
 208     list.addConstructor(cons);
 209
 210     DatatypeConstructor nil("nil", "is_nil");
 211     list.addConstructor(nil);
 212
 213     Debug("datatypes") << list << std::endl;
 214     DatatypeType listType = d_em->mkDatatypeType(list);
 215     Debug("datatypes") << listType << std::endl;
 216
 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();
 226         i != i_end;
 227         ++i) {
 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);
 232     }
 233   }
 234
 235   void testListBoolean() {
 236     Datatype list("list");
 237     Type booleanType = d_em->booleanType();
 238
 239     DatatypeConstructor cons("cons", "is_cons");
 240     cons.addArg("car", booleanType);
 241     cons.addArg("cdr", DatatypeSelfType());
 242     list.addConstructor(cons);
 243
 244     DatatypeConstructor nil("nil", "is_nil");
 245     list.addConstructor(nil);
 246
 247     Debug("datatypes") << list << std::endl;
 248     DatatypeType listType = d_em->mkDatatypeType(list);
 249     Debug("datatypes") << listType << std::endl;
 250
 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();
 260         i != i_end;
 261         ++i) {
 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);
 266     }
 267   }
 268
 269   void testMutualListTrees() {
 270     /* Create two mutual datatypes corresponding to this definition
 271      * block:
 272      *
 273      *   DATATYPE
 274      *     tree = node(left: tree, right: tree) | leaf(list),
 275      *     list = cons(car: tree, cdr: list) | nil
 276      *   END;
 277      */
 278     Datatype tree("tree");
 279     DatatypeConstructor node("node", "is_node");
 280     node.addArg("left", DatatypeSelfType());
 281     node.addArg("right", DatatypeSelfType());
 282     tree.addConstructor(node);
 283
 284     DatatypeConstructor leaf("leaf", "is_leaf");
 285     leaf.addArg("leaf", DatatypeUnresolvedType("list"));
 286     tree.addConstructor(leaf);
 287
 288     Debug("datatypes") << tree << std::endl;
 289
 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);
 295
 296     DatatypeConstructor nil("nil", "is_nil");
 297     list.addConstructor(nil);
 298
 299     Debug("datatypes") << list << std::endl;
 300
 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());
 307
 308     vector<Datatype> dts;
 309     dts.push_back(tree);
 310     dts.push_back(list);
 311     vector<DatatypeType> dtts = d_em->mkMutualDatatypeTypes(dts);
 312
 313     TS_ASSERT(dtts[0].getDatatype().isResolved());
 314     TS_ASSERT(dtts[1].getDatatype().isResolved());
 315
 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();
 325         i != i_end;
 326         ++i) {
 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]);
 331     }
 332
 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();
 342         i != i_end;
 343         ++i) {
 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]);
 348     }
 349
 350     // add another constructor to list datatype resulting in an
 351     // "otherNil-list"
 352     DatatypeConstructor otherNil("otherNil", "is_otherNil");
 353     dts[1].addConstructor(otherNil);
 354
 355     // remake the types
 356     vector<DatatypeType> dtts2 = d_em->mkMutualDatatypeTypes(dts);
 357
 358     TS_ASSERT_DIFFERS(dtts, dtts2);
 359     TS_ASSERT_DIFFERS(dtts[1], dtts2[1]);
 360
 361     // tree is also different because it's a tree of otherNil-lists
 362     TS_ASSERT_DIFFERS(dtts[0], dtts2[0]);
 363
 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();
 373         i != i_end;
 374         ++i) {
 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]);
 379     }
 380
 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();
 390         i != i_end;
 391         ++i) {
 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]);
 396     }
 397   }
 398
 399   void testNotSoWellFounded() {
 400     Datatype tree("tree");
 401
 402     DatatypeConstructor node("node", "is_node");
 403     node.addArg("left", DatatypeSelfType());
 404     node.addArg("right", DatatypeSelfType());
 405     tree.addConstructor(node);
 406
 407     Debug("datatypes") << tree << std::endl;
 408     DatatypeType treeType = d_em->mkDatatypeType(tree);
 409     Debug("datatypes") << treeType << std::endl;
 410
 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();
 419         i != i_end;
 420         ++i) {
 421       TS_ASSERT(! (*i).isWellFounded());
 422       TS_ASSERT_THROWS_ANYTHING( (*i).mkGroundTerm( treeType ) );
 423     }
 424   }
 425
 426 };/* class DatatypeBlack */