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.)

diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 6d84029139ae5bb458cc66880aa311fdcdfe6ef6..55ebc38c966554e9085fb86f1980a07d42494495 100644 (file)
--- 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 b9d357e00baaa52190eda60b5f006fdffa01d569..62426ab86241c080b786cc23068ad366ac5b2917 100644 (file)
--- 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() {