From c2d88c4cf9fd2d6a8b0eb8d28019eacd29b913de Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 26 Oct 2012 23:32:38 +0000
Subject: [PATCH] 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.)
---
 src/theory/arith/type_enumerator.h       | 11 +++-----
 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() {
-- 
2.30.2