2 files changed, 57 insertions, 0 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 549e9f19b..a724124bd 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -61,6 +61,9 @@ enumerator REAL_TYPE \
 enumerator INTEGER_TYPE \
     "::CVC4::theory::arith::IntegerEnumerator" \
     "theory/arith/type_enumerator.h"
+enumerator SUBRANGE_TYPE \
+    "::CVC4::theory::arith::SubrangeEnumerator" \
+    "theory/arith/type_enumerator.h"
 
 operator LT 2 "less than, x < y"
 operator LEQ 2 "less than or equal, x <= y"
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 4dd139be7..8b30a4ddf 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -110,6 +110,60 @@ public:
 
 };/* class IntegerEnumerator */
 
+class SubrangeEnumerator : public TypeEnumeratorBase<SubrangeEnumerator> {
+  Integer d_int;
+  SubrangeBounds d_bounds;
+  bool d_direction;// true == +, false == -
+
+public:
+
+  SubrangeEnumerator(TypeNode type) throw(AssertionException) :
+    TypeEnumeratorBase<SubrangeEnumerator>(type),
+    d_int(0),
+    d_bounds(type.getConst<SubrangeBounds>()),
+    d_direction(d_bounds.lower.hasBound()) {
+
+    d_int = d_direction ? d_bounds.lower.getBound() : d_bounds.upper.getBound();
+
+    Assert(type.getKind() == kind::SUBRANGE_TYPE);
+
+    // if we're counting down, there's no lower bound
+    Assert(d_direction || !d_bounds.lower.hasBound());
+  }
+
+  Node operator*() throw() {
+    if(isFinished()) {
+      throw NoMoreValuesException(getType());
+    }
+    return NodeManager::currentNM()->mkConst(Rational(d_int));
+  }
+
+  SubrangeEnumerator& operator++() throw() {
+    if(d_direction) {
+      if(!d_bounds.upper.hasBound() || d_int <= d_bounds.upper.getBound()) {
+        d_int += 1;
+      }
+    } else {
+      // 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());
+  }
+
+};/* class SubrangeEnumerator */
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */