diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-07 14:57:38 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-07 14:57:38 +0000 |
| commit | 3a7aafccadbfa1543c435b7dfe4f53116224a11f (patch) | |
| tree | e0ea0bdbf985da520935aeb978890a7b21f33b62 /test/unit/util | |
| parent | 6cb3de0e1370deaf43eeb1fb84dfe1f3a625483f (diff) | |
Some new Datatype public functionality, as per Chris Conway's suggestions on the dev mailing list.
Diffstat (limited to 'test/unit/util')
| -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()); |