diff options
| -rw-r--r-- | src/theory/arith/type_enumerator.h | 11 | ||||
| -rw-r--r-- | test/unit/theory/type_enumerator_white.h | 33 |
2 files changed, 36 insertions, 8 deletions
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index 6d8402913..55ebc38c9 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -129,7 +129,7 @@ public: Assert(d_direction || !d_bounds.lower.hasBound()); } - Node operator*() throw() { + Node operator*() throw(NoMoreValuesException) { if(isFinished()) { throw NoMoreValuesException(getType()); } @@ -145,19 +145,14 @@ public: // if we're counting down, there's no lower bound d_int -= 1; } - // sequence is 0, 1, -1, 2, -2, 3, -3, ... - if(d_int <= 0) { - d_int = -d_int + 1; - } else { - d_int = -d_int; - } return *this; } bool isFinished() throw() { // if we're counting down, there's no lower bound return d_direction && - (!d_bounds.upper.hasBound() || d_int <= d_bounds.upper.getBound()); + d_bounds.upper.hasBound() && + d_int > d_bounds.upper.getBound(); } };/* class SubrangeEnumerator */ 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() { |