test/unit/util/datatype_black.h

   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-2020 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::DType
  13  **
  14  ** Black box testing of CVC4::DType.
  15  **/
  16
  17 #include <cxxtest/TestSuite.h>
  18
  19 #include <sstream>
  20
  21 #include "api/cvc4cpp.h"
  22 #include "expr/dtype.h"
  23 #include "expr/expr.h"
  24 #include "expr/expr_manager.h"
  25 #include "expr/expr_manager_scope.h"
  26 #include "expr/type_node.h"
  27
  28 using namespace CVC4;
  29 using namespace std;
  30
  31 class DatatypeBlack : public CxxTest::TestSuite {
  32  public:
  33   void setUp() override
  34   {
  35     d_slv = new api::Solver();
  36     d_nm = d_slv->getNodeManager();
  37     d_scope = new NodeManagerScope(d_nm);
  38     Debug.on("datatypes");
  39     Debug.on("groundterms");
  40   }
  41
  42   void tearDown() override
  43   {
  44     delete d_scope;
  45     delete d_slv;
  46   }
  47
  48   void testEnumeration() {
  49     DType colors("colors");
  50
  51     std::shared_ptr<DTypeConstructor> yellow =
  52         std::make_shared<DTypeConstructor>("yellow");
  53     std::shared_ptr<DTypeConstructor> blue =
  54         std::make_shared<DTypeConstructor>("blue");
  55     std::shared_ptr<DTypeConstructor> green =
  56         std::make_shared<DTypeConstructor>("green");
  57     std::shared_ptr<DTypeConstructor> red =
  58         std::make_shared<DTypeConstructor>("red");
  59
  60     colors.addConstructor(yellow);
  61     colors.addConstructor(blue);
  62     colors.addConstructor(green);
  63     colors.addConstructor(red);
  64
  65     Debug("datatypes") << colors << std::endl;
  66     TypeNode colorsType = d_nm->mkDatatypeType(colors);
  67     Debug("datatypes") << colorsType << std::endl;
  68
  69     Node ctor = colorsType.getDType()[1].getConstructor();
  70     Node apply = d_nm->mkNode(kind::APPLY_CONSTRUCTOR, ctor);
  71     Debug("datatypes") << apply << std::endl;
  72
  73     TS_ASSERT(!colorsType.getDType().isParametric());
  74     TS_ASSERT(colorsType.getDType().isFinite());
  75     TS_ASSERT(colorsType.getDType().getCardinality().compare(4)
  76               == Cardinality::EQUAL);
  77     TS_ASSERT(ctor.getType().getCardinality().compare(1) == Cardinality::EQUAL);
  78     TS_ASSERT(colorsType.getDType().isWellFounded());
  79     Debug("groundterms") << "ground term of " << colorsType.getDType().getName()
  80                          << endl
  81                          << "  is " << colorsType.mkGroundTerm() << endl;
  82     TS_ASSERT(colorsType.mkGroundTerm().getType() == colorsType);
  83   }
  84
  85   void testNat() {
  86     DType nat("nat");
  87
  88     std::shared_ptr<DTypeConstructor> succ =
  89         std::make_shared<DTypeConstructor>("succ");
  90     succ->addArgSelf("pred");
  91     nat.addConstructor(succ);
  92
  93     std::shared_ptr<DTypeConstructor> zero =
  94         std::make_shared<DTypeConstructor>("zero");
  95     nat.addConstructor(zero);
  96
  97     Debug("datatypes") << nat << std::endl;
  98     TypeNode natType = d_nm->mkDatatypeType(nat);
  99     Debug("datatypes") << natType << std::endl;
 100
 101     Node ctor = natType.getDType()[1].getConstructor();
 102     Node apply = d_nm->mkNode(kind::APPLY_CONSTRUCTOR, ctor);
 103     Debug("datatypes") << apply << std::endl;
 104
 105     TS_ASSERT(!natType.getDType().isParametric());
 106     TS_ASSERT(!natType.getDType().isFinite());
 107     TS_ASSERT(natType.getDType().getCardinality().compare(Cardinality::INTEGERS)
 108               == Cardinality::EQUAL);
 109     TS_ASSERT(natType.getDType().isWellFounded());
 110     Debug("groundterms") << "ground term of " << natType.getDType().getName()
 111                          << endl
 112                          << "  is " << natType.mkGroundTerm() << endl;
 113     TS_ASSERT(natType.mkGroundTerm().getType() == natType);
 114   }
 115
 116   void testTree() {
 117     DType tree("tree");
 118     TypeNode integerType = d_nm->integerType();
 119
 120     std::shared_ptr<DTypeConstructor> node =
 121         std::make_shared<DTypeConstructor>("node");
 122     node->addArgSelf("left");
 123     node->addArgSelf("right");
 124     tree.addConstructor(node);
 125
 126     std::shared_ptr<DTypeConstructor> leaf =
 127         std::make_shared<DTypeConstructor>("leaf");
 128     leaf->addArg("leaf", integerType);
 129     tree.addConstructor(leaf);
 130
 131     Debug("datatypes") << tree << std::endl;
 132     TypeNode treeType = d_nm->mkDatatypeType(tree);
 133     Debug("datatypes") << treeType << std::endl;
 134
 135     TS_ASSERT(!treeType.getDType().isParametric());
 136     TS_ASSERT(!treeType.getDType().isFinite());
 137     TS_ASSERT(
 138         treeType.getDType().getCardinality().compare(Cardinality::INTEGERS)
 139         == Cardinality::EQUAL);
 140     TS_ASSERT(treeType.getDType().isWellFounded());
 141     Debug("groundterms") << "ground term of " << treeType.getDType().getName()
 142                          << endl
 143                          << "  is " << treeType.mkGroundTerm() << endl;
 144     TS_ASSERT(treeType.mkGroundTerm().getType() == treeType);
 145   }
 146
 147   void testListInt() {
 148     DType list("list");
 149     TypeNode integerType = d_nm->integerType();
 150
 151     std::shared_ptr<DTypeConstructor> cons =
 152         std::make_shared<DTypeConstructor>("cons");
 153     cons->addArg("car", integerType);
 154     cons->addArgSelf("cdr");
 155     list.addConstructor(cons);
 156
 157     std::shared_ptr<DTypeConstructor> nil =
 158         std::make_shared<DTypeConstructor>("nil");
 159     list.addConstructor(nil);
 160
 161     Debug("datatypes") << list << std::endl;
 162     TypeNode listType = d_nm->mkDatatypeType(list);
 163     Debug("datatypes") << listType << std::endl;
 164
 165     TS_ASSERT(!listType.getDType().isParametric());
 166     TS_ASSERT(!listType.getDType().isFinite());
 167     TS_ASSERT(
 168         listType.getDType().getCardinality().compare(Cardinality::INTEGERS)
 169         == Cardinality::EQUAL);
 170     TS_ASSERT(listType.getDType().isWellFounded());
 171     Debug("groundterms") << "ground term of " << listType.getDType().getName()
 172                          << endl
 173                          << "  is " << listType.mkGroundTerm() << endl;
 174     TS_ASSERT(listType.mkGroundTerm().getType() == listType);
 175   }
 176
 177   void testListReal() {
 178     DType list("list");
 179     TypeNode realType = d_nm->realType();
 180
 181     std::shared_ptr<DTypeConstructor> cons =
 182         std::make_shared<DTypeConstructor>("cons");
 183     cons->addArg("car", realType);
 184     cons->addArgSelf("cdr");
 185     list.addConstructor(cons);
 186
 187     std::shared_ptr<DTypeConstructor> nil =
 188         std::make_shared<DTypeConstructor>("nil");
 189     list.addConstructor(nil);
 190
 191     Debug("datatypes") << list << std::endl;
 192     TypeNode listType = d_nm->mkDatatypeType(list);
 193     Debug("datatypes") << listType << std::endl;
 194
 195     TS_ASSERT(!listType.getDType().isParametric());
 196     TS_ASSERT(!listType.getDType().isFinite());
 197     TS_ASSERT(listType.getDType().getCardinality().compare(Cardinality::REALS)
 198               == Cardinality::EQUAL);
 199     TS_ASSERT(listType.getDType().isWellFounded());
 200     Debug("groundterms") << "ground term of " << listType.getDType().getName()
 201                          << endl
 202                          << "  is " << listType.mkGroundTerm() << endl;
 203     TS_ASSERT(listType.mkGroundTerm().getType() == listType);
 204   }
 205
 206   void testListBoolean() {
 207     DType list("list");
 208     TypeNode booleanType = d_nm->booleanType();
 209
 210     std::shared_ptr<DTypeConstructor> cons =
 211         std::make_shared<DTypeConstructor>("cons");
 212     cons->addArg("car", booleanType);
 213     cons->addArgSelf("cdr");
 214     list.addConstructor(cons);
 215
 216     std::shared_ptr<DTypeConstructor> nil =
 217         std::make_shared<DTypeConstructor>("nil");
 218     list.addConstructor(nil);
 219
 220     Debug("datatypes") << list << std::endl;
 221     TypeNode listType = d_nm->mkDatatypeType(list);
 222     Debug("datatypes") << listType << std::endl;
 223
 224     TS_ASSERT(!listType.getDType().isFinite());
 225     TS_ASSERT(
 226         listType.getDType().getCardinality().compare(Cardinality::INTEGERS)
 227         == Cardinality::EQUAL);
 228     TS_ASSERT(listType.getDType().isWellFounded());
 229     Debug("groundterms") << "ground term of " << listType.getDType().getName()
 230                          << endl
 231                          << "  is " << listType.mkGroundTerm() << endl;
 232     TS_ASSERT(listType.mkGroundTerm().getType() == listType);
 233   }
 234
 235   void testMutualListTrees() {
 236     /* Create two mutual datatypes corresponding to this definition
 237      * block:
 238      *
 239      *   DATATYPE
 240      *     tree = node(left: tree, right: tree) | leaf(list),
 241      *     list = cons(car: tree, cdr: list) | nil
 242      *   END;
 243      */
 244     std::set<TypeNode> unresolvedTypes;
 245     TypeNode unresList =
 246         d_nm->mkSort("list", ExprManager::SORT_FLAG_PLACEHOLDER);
 247     unresolvedTypes.insert(unresList);
 248     TypeNode unresTree =
 249         d_nm->mkSort("tree", ExprManager::SORT_FLAG_PLACEHOLDER);
 250     unresolvedTypes.insert(unresTree);
 251
 252     DType tree("tree");
 253     std::shared_ptr<DTypeConstructor> node =
 254         std::make_shared<DTypeConstructor>("node");
 255     node->addArgSelf("left");
 256     node->addArgSelf("right");
 257     tree.addConstructor(node);
 258
 259     std::shared_ptr<DTypeConstructor> leaf =
 260         std::make_shared<DTypeConstructor>("leaf");
 261     leaf->addArg("leaf", unresList);
 262     tree.addConstructor(leaf);
 263
 264     Debug("datatypes") << tree << std::endl;
 265
 266     DType list("list");
 267     std::shared_ptr<DTypeConstructor> cons =
 268         std::make_shared<DTypeConstructor>("cons");
 269     cons->addArg("car", unresTree);
 270     cons->addArgSelf("cdr");
 271     list.addConstructor(cons);
 272
 273     std::shared_ptr<DTypeConstructor> nil =
 274         std::make_shared<DTypeConstructor>("nil");
 275     list.addConstructor(nil);
 276
 277     Debug("datatypes") << list << std::endl;
 278
 279     TS_ASSERT(! tree.isResolved());
 280     TS_ASSERT(! list.isResolved());
 281
 282     vector<DType> dts;
 283     dts.push_back(tree);
 284     dts.push_back(list);
 285     vector<TypeNode> dtts = d_nm->mkMutualDatatypeTypes(dts, unresolvedTypes);
 286
 287     TS_ASSERT(dtts[0].getDType().isResolved());
 288     TS_ASSERT(dtts[1].getDType().isResolved());
 289
 290     TS_ASSERT(!dtts[0].getDType().isFinite());
 291     TS_ASSERT(dtts[0].getDType().getCardinality().compare(Cardinality::INTEGERS)
 292               == Cardinality::EQUAL);
 293     TS_ASSERT(dtts[0].getDType().isWellFounded());
 294     Debug("groundterms") << "ground term of " << dtts[0].getDType().getName()
 295                          << endl
 296                          << "  is " << dtts[0].mkGroundTerm() << endl;
 297     TS_ASSERT(dtts[0].mkGroundTerm().getType() == dtts[0]);
 298
 299     TS_ASSERT(!dtts[1].getDType().isFinite());
 300     TS_ASSERT(dtts[1].getDType().getCardinality().compare(Cardinality::INTEGERS)
 301               == Cardinality::EQUAL);
 302     TS_ASSERT(dtts[1].getDType().isWellFounded());
 303     Debug("groundterms") << "ground term of " << dtts[1].getDType().getName()
 304                          << endl
 305                          << "  is " << dtts[1].mkGroundTerm() << endl;
 306     TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]);
 307   }
 308   void testMutualListTrees2()
 309   {
 310     std::set<TypeNode> unresolvedTypes;
 311     TypeNode unresList =
 312         d_nm->mkSort("list", ExprManager::SORT_FLAG_PLACEHOLDER);
 313     unresolvedTypes.insert(unresList);
 314     TypeNode unresTree =
 315         d_nm->mkSort("tree", ExprManager::SORT_FLAG_PLACEHOLDER);
 316     unresolvedTypes.insert(unresTree);
 317
 318     DType tree("tree");
 319     std::shared_ptr<DTypeConstructor> node =
 320         std::make_shared<DTypeConstructor>("node");
 321     node->addArgSelf("left");
 322     node->addArgSelf("right");
 323     tree.addConstructor(node);
 324
 325     std::shared_ptr<DTypeConstructor> leaf =
 326         std::make_shared<DTypeConstructor>("leaf");
 327     leaf->addArg("leaf", unresList);
 328     tree.addConstructor(leaf);
 329
 330     DType list("list");
 331     std::shared_ptr<DTypeConstructor> cons =
 332         std::make_shared<DTypeConstructor>("cons");
 333     cons->addArg("car", unresTree);
 334     cons->addArgSelf("cdr");
 335     list.addConstructor(cons);
 336
 337     std::shared_ptr<DTypeConstructor> nil =
 338         std::make_shared<DTypeConstructor>("nil");
 339     list.addConstructor(nil);
 340
 341     // add another constructor to list datatype resulting in an
 342     // "otherNil-list"
 343     std::shared_ptr<DTypeConstructor> otherNil =
 344         std::make_shared<DTypeConstructor>("otherNil");
 345     list.addConstructor(otherNil);
 346
 347     vector<DType> dts;
 348     dts.push_back(tree);
 349     dts.push_back(list);
 350     // remake the types
 351     vector<TypeNode> dtts2 = d_nm->mkMutualDatatypeTypes(dts, unresolvedTypes);
 352
 353     TS_ASSERT(!dtts2[0].getDType().isFinite());
 354     TS_ASSERT(
 355         dtts2[0].getDType().getCardinality().compare(Cardinality::INTEGERS)
 356         == Cardinality::EQUAL);
 357     TS_ASSERT(dtts2[0].getDType().isWellFounded());
 358     Debug("groundterms") << "ground term of " << dtts2[0].getDType().getName()
 359                          << endl
 360                          << "  is " << dtts2[0].mkGroundTerm() << endl;
 361     TS_ASSERT(dtts2[0].mkGroundTerm().getType() == dtts2[0]);
 362
 363     TS_ASSERT(!dtts2[1].getDType().isParametric());
 364     TS_ASSERT(!dtts2[1].getDType().isFinite());
 365     TS_ASSERT(
 366         dtts2[1].getDType().getCardinality().compare(Cardinality::INTEGERS)
 367         == Cardinality::EQUAL);
 368     TS_ASSERT(dtts2[1].getDType().isWellFounded());
 369     Debug("groundterms") << "ground term of " << dtts2[1].getDType().getName()
 370                          << endl
 371                          << "  is " << dtts2[1].mkGroundTerm() << endl;
 372     TS_ASSERT(dtts2[1].mkGroundTerm().getType() == dtts2[1]);
 373   }
 374
 375   void testNotSoWellFounded() {
 376     DType tree("tree");
 377
 378     std::shared_ptr<DTypeConstructor> node =
 379         std::make_shared<DTypeConstructor>("node");
 380     node->addArgSelf("left");
 381     node->addArgSelf("right");
 382     tree.addConstructor(node);
 383
 384     Debug("datatypes") << tree << std::endl;
 385     TypeNode treeType = d_nm->mkDatatypeType(tree);
 386     Debug("datatypes") << treeType << std::endl;
 387
 388     TS_ASSERT(!treeType.getDType().isParametric());
 389     TS_ASSERT(!treeType.getDType().isFinite());
 390     TS_ASSERT(
 391         treeType.getDType().getCardinality().compare(Cardinality::INTEGERS)
 392         == Cardinality::EQUAL);
 393     TS_ASSERT(!treeType.getDType().isWellFounded());
 394     TS_ASSERT(treeType.mkGroundTerm().isNull());
 395     TS_ASSERT(treeType.getDType().mkGroundTerm(treeType).isNull());
 396   }
 397
 398   void testParametricDType()
 399   {
 400     vector<TypeNode> v;
 401     TypeNode t1, t2;
 402     v.push_back(t1 = d_nm->mkSort("T1"));
 403     v.push_back(t2 = d_nm->mkSort("T2"));
 404     DType pair("pair", v);
 405
 406     std::shared_ptr<DTypeConstructor> mkpair =
 407         std::make_shared<DTypeConstructor>("mk-pair");
 408     mkpair->addArg("first", t1);
 409     mkpair->addArg("second", t2);
 410     pair.addConstructor(mkpair);
 411     TypeNode pairType = d_nm->mkDatatypeType(pair);
 412
 413     TS_ASSERT(pairType.getDType().isParametric());
 414     v.clear();
 415     v.push_back(d_nm->integerType());
 416     v.push_back(d_nm->integerType());
 417     TypeNode pairIntInt = pairType.getDType().getTypeNode(v);
 418     v.clear();
 419     v.push_back(d_nm->realType());
 420     v.push_back(d_nm->realType());
 421     TypeNode pairRealReal = pairType.getDType().getTypeNode(v);
 422     v.clear();
 423     v.push_back(d_nm->realType());
 424     v.push_back(d_nm->integerType());
 425     TypeNode pairRealInt = pairType.getDType().getTypeNode(v);
 426     v.clear();
 427     v.push_back(d_nm->integerType());
 428     v.push_back(d_nm->realType());
 429     TypeNode pairIntReal = pairType.getDType().getTypeNode(v);
 430
 431     TS_ASSERT_DIFFERS(pairIntInt, pairRealReal);
 432     TS_ASSERT_DIFFERS(pairIntReal, pairRealReal);
 433     TS_ASSERT_DIFFERS(pairRealInt, pairRealReal);
 434     TS_ASSERT_DIFFERS(pairIntInt, pairIntReal);
 435     TS_ASSERT_DIFFERS(pairIntInt, pairRealInt);
 436     TS_ASSERT_DIFFERS(pairIntReal, pairRealInt);
 437
 438     TS_ASSERT(pairRealReal.isComparableTo(pairRealReal));
 439     TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal));
 440     TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal));
 441     TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal));
 442     TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt));
 443     TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt));
 444     TS_ASSERT(pairRealInt.isComparableTo(pairRealInt));
 445     TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt));
 446     TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal));
 447     TS_ASSERT(pairIntReal.isComparableTo(pairIntReal));
 448     TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal));
 449     TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal));
 450     TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt));
 451     TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt));
 452     TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt));
 453     TS_ASSERT(pairIntInt.isComparableTo(pairIntInt));
 454
 455     TS_ASSERT(pairRealReal.isSubtypeOf(pairRealReal));
 456     TS_ASSERT(!pairIntReal.isSubtypeOf(pairRealReal));
 457     TS_ASSERT(!pairRealInt.isSubtypeOf(pairRealReal));
 458     TS_ASSERT(!pairIntInt.isSubtypeOf(pairRealReal));
 459     TS_ASSERT(!pairRealReal.isSubtypeOf(pairRealInt));
 460     TS_ASSERT(!pairIntReal.isSubtypeOf(pairRealInt));
 461     TS_ASSERT(pairRealInt.isSubtypeOf(pairRealInt));
 462     TS_ASSERT(!pairIntInt.isSubtypeOf(pairRealInt));
 463     TS_ASSERT(!pairRealReal.isSubtypeOf(pairIntReal));
 464     TS_ASSERT(pairIntReal.isSubtypeOf(pairIntReal));
 465     TS_ASSERT(!pairRealInt.isSubtypeOf(pairIntReal));
 466     TS_ASSERT(!pairIntInt.isSubtypeOf(pairIntReal));
 467     TS_ASSERT(!pairRealReal.isSubtypeOf(pairIntInt));
 468     TS_ASSERT(!pairIntReal.isSubtypeOf(pairIntInt));
 469     TS_ASSERT(!pairRealInt.isSubtypeOf(pairIntInt));
 470     TS_ASSERT(pairIntInt.isSubtypeOf(pairIntInt));
 471
 472     TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairRealReal, pairRealReal),
 473                      pairRealReal);
 474     TS_ASSERT(
 475         TypeNode::leastCommonTypeNode(pairIntReal, pairRealReal).isNull());
 476     TS_ASSERT(
 477         TypeNode::leastCommonTypeNode(pairRealInt, pairRealReal).isNull());
 478     TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairRealReal).isNull());
 479     TS_ASSERT(
 480         TypeNode::leastCommonTypeNode(pairRealReal, pairRealInt).isNull());
 481     TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntReal, pairRealInt).isNull());
 482     TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairRealInt, pairRealInt),
 483                      pairRealInt);
 484     TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairRealInt).isNull());
 485     TS_ASSERT(
 486         TypeNode::leastCommonTypeNode(pairRealReal, pairIntReal).isNull());
 487     TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairIntReal, pairIntReal),
 488                      pairIntReal);
 489     TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealInt, pairIntReal).isNull());
 490     TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairIntReal).isNull());
 491     TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealReal, pairIntInt).isNull());
 492     TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntReal, pairIntInt).isNull());
 493     TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealInt, pairIntInt).isNull());
 494     TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairIntInt, pairIntInt),
 495                      pairIntInt);
 496   }
 497
 498  private:
 499   api::Solver* d_slv;
 500   NodeManager* d_nm;
 501   NodeManagerScope* d_scope;
 502 }; /* class DTypeBlack */