diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-10-06 04:05:19 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-10-06 04:05:19 +0000 |
| commit | 9b871cceb0f9c3372504f9f7b786a7c1dd7cd700 (patch) | |
| tree | da76170cfa5311ce3b72b25e8e8179a4f1aa6f6c /test/unit | |
| parent | 04b89b1a5256a8a70df1615c9a7873a2d870fe82 (diff) | |
* Fix some regressions' expected outputs.
* Ensure Rewriter::init() is called before ::rewrite().
The array type enumerator recently gave us an end-run around
::init(). TheoryEngine no longer calls these, they're done
via static initialization.
* Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412).
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/theory/type_enumerator_white.h | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index 6ff36b900..8fa3b029e 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -238,7 +238,6 @@ public: for(size_t i = 0; i < 1000; ++i) { TS_ASSERT( ! te.isFinished() ); Node elt = *te++; - std::cout << elt << std::endl; // ensure no duplicates TS_ASSERT( elts.find(elt) == elts.end() ); elts.insert(elt); @@ -271,34 +270,6 @@ public: //TS_ASSERT( elts.find( d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, twos, three, zero), two, zero), one, zero), zero, zero) ) != elts.end() ); } - void testArraysFinite() { - ArrayType arrType(d_em->mkArrayType(d_em->mkBitVectorType(2), d_em->booleanType())); - TypeEnumerator te(TypeNode::fromType(arrType)); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false)))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true)))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false)))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true)))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false)))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true)))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false)))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true)))); - TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_THROWS(*++te, NoMoreValuesException); - TS_ASSERT( te.isFinished() ); - TS_ASSERT_THROWS(*++te, NoMoreValuesException); - TS_ASSERT( te.isFinished() ); - TS_ASSERT_THROWS(*++te, NoMoreValuesException); - TS_ASSERT( te.isFinished() ); - } - void testBV() { TypeEnumerator te(d_nm->mkBitVectorType(3)); TS_ASSERT_EQUALS(*te, d_nm->mkConst(BitVector(3u, 0u))); |