diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-07-26 21:09:10 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-07-26 21:09:10 +0000 |
| commit | 988c97d92fa617c5dccaeb1ef33121bfa6459afc (patch) | |
| tree | a207b24d2f3c8afebc7a5fe8c44b03266f49161a /test | |
| parent | 06077433dd58f92a06e9539b6f17a551421141b4 (diff) | |
Datatype enumerator work. This version is not a "fair" enumerator, but I got it in quickly for Andy.
A "fair" version forthcoming.
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/type_enumerator_white.h | 53 |
1 files changed, 52 insertions, 1 deletions
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index bf76ba801..64dfe6fea 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -149,7 +149,58 @@ public: TS_ASSERT_THROWS(*++te, NoMoreValuesException); } - void NOtestDatatypesInfinite() { + void testDatatypesInfinite1() { + Datatype colors("Colors"); + colors.addConstructor(DatatypeConstructor("red")); + colors.addConstructor(DatatypeConstructor("orange")); + colors.addConstructor(DatatypeConstructor("yellow")); + colors.addConstructor(DatatypeConstructor("green")); + colors.addConstructor(DatatypeConstructor("blue")); + colors.addConstructor(DatatypeConstructor("violet")); + TypeNode colorsType = TypeNode::fromType(d_em->mkDatatypeType(colors)); + Datatype listColors("ListColors"); + DatatypeConstructor consC("cons"); + consC.addArg("car", colorsType.toType()); + consC.addArg("cdr", DatatypeSelfType()); + listColors.addConstructor(consC); + listColors.addConstructor(DatatypeConstructor("nil")); + TypeNode listColorsType = TypeNode::fromType(d_em->mkDatatypeType(listColors)); + TypeEnumerator te(listColorsType); + Node cons = Node::fromExpr(DatatypeType(listColorsType.toType()).getDatatype().getConstructor("cons")); + Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(listColorsType.toType()).getDatatype().getConstructor("nil")); + Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("red")); + TS_ASSERT_EQUALS(*te, nil); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))))))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))))))); + } + + void NOtestDatatypesInfinite2() { TypeNode datatype; TypeEnumerator te(datatype); TS_FAIL("unimplemented"); |