diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-25 18:50:04 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-25 18:50:04 -0400 |
| commit | d9533928947a207b795d90a97879b8212e99c50e (patch) | |
| tree | cf3a2fd1bc76cc8998a7bc4c1c66964d9d6a8b4c /test | |
| parent | 23146b787570f80594faf7813b5d0d04a583eb62 (diff) | |
fix unit test for new fair datatype enumeration
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/type_enumerator_white.h | 30 |
1 files changed, 8 insertions, 22 deletions
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index 3dcb2db85..d9963f78c 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -218,41 +218,27 @@ std::cout<<"here\n"; 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")); + Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("orange")); + Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("yellow")); TS_ASSERT_EQUALS(*te, nil); TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)); TS_ASSERT( ! te.isFinished() ); TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); TS_ASSERT( ! te.isFinished() ); - 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, orange, nil)); TS_ASSERT( ! te.isFinished() ); 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))))); + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))); TS_ASSERT( ! te.isFinished() ); - 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, orange, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); TS_ASSERT( ! te.isFinished() ); - 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, yellow, nil)); TS_ASSERT( ! te.isFinished() ); 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)))))))); + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil))); TS_ASSERT( ! te.isFinished() ); } |