diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-26 23:32:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-26 23:32:38 +0000 |
commit | c2d88c4cf9fd2d6a8b0eb8d28019eacd29b913de (patch) | |
tree | 16407ca53855adede55099a90ecdfd11d135175c /test/unit | |
parent | b2333e3bb49f84be01ddcc875dc6b01cc6b29307 (diff) |
Fix to subrange type enumerator, and its unit test. Resolves bug 436.
(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 | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index b9d357e00..62426ab86 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -140,6 +140,39 @@ public: TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 7))); TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 7))); TS_ASSERT( ! te.isFinished() ); + + // subrange bounded only below + te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(Integer(0)), SubrangeBound()))); + TS_ASSERT( ! te.isFinished() ); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0))); + for(int i = 1; i <= 100; ++i) { + TS_ASSERT( ! (++te).isFinished() ); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(i))); + } + TS_ASSERT( ! te.isFinished() ); + + // subrange bounded only above + te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(), SubrangeBound(Integer(-5))))); + TS_ASSERT( ! te.isFinished() ); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-5))); + for(int i = 1; i <= 100; ++i) { + TS_ASSERT( ! (++te).isFinished() ); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-5 - i))); + } + TS_ASSERT( ! te.isFinished() ); + + // finite subrange + te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(Integer(-10)), SubrangeBound(Integer(15))))); + TS_ASSERT( ! te.isFinished() ); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-10))); + for(int i = -9; i <= 15; ++i) { + TS_ASSERT( ! (++te).isFinished() ); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(i))); + } + TS_ASSERT( (++te).isFinished() ); + TS_ASSERT_THROWS(*te, NoMoreValuesException); +std::cout<<"here\n"; + TS_ASSERT_THROWS(*++te, NoMoreValuesException); } void testDatatypesFinite() { |