diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/util/datatype_black.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index ea8d8a900..6d5584924 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -64,6 +64,12 @@ public: Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor); Debug("datatypes") << apply << std::endl; + const Datatype& colorsDT = colorsType.getDatatype(); + TS_ASSERT(colorsDT.getConstructor("blue") == ctor); + TS_ASSERT(colorsDT["blue"].getConstructor() == ctor); + TS_ASSERT_THROWS(colorsDT["blue"].getSelector("foo"), IllegalArgumentException); + TS_ASSERT_THROWS(colorsDT["blue"]["foo"], IllegalArgumentException); + TS_ASSERT(colorsType.getDatatype().isFinite()); TS_ASSERT(colorsType.getDatatype().getCardinality() == 4); TS_ASSERT(ctor.getType().getCardinality() == 1); @@ -137,6 +143,11 @@ public: DatatypeType treeType = d_em->mkDatatypeType(tree); Debug("datatypes") << treeType << std::endl; + Expr ctor = treeType.getDatatype()[1].getConstructor(); + TS_ASSERT(treeType.getConstructor("leaf") == ctor); + TS_ASSERT(treeType.getConstructor("leaf") == ctor); + TS_ASSERT_THROWS(treeType.getConstructor("leff"), IllegalArgumentException); + TS_ASSERT(! treeType.getDatatype().isFinite()); TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS); TS_ASSERT(treeType.getDatatype().isWellFounded()); |