Type enumerator infrastructure and uninterpreted constant support. No support yet for enumerating arrays, or for enumerating non-trivial datatypes.

24 files changed, 739 insertions, 4 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index bca96f7d7..1aae03aa5 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -13,6 +13,7 @@ libtheory_la_SOURCES = \
 	logic_info.cpp \
 	output_channel.h \
 	interrupted.h \
+	type_enumerator.h \
 	theory_engine.h \
 	theory_engine.cpp \
 	theory_test_utils.h \
@@ -50,7 +51,8 @@ libtheory_la_SOURCES = \
 nodist_libtheory_la_SOURCES = \
 	rewriter_tables.h \
 	instantiator_tables.cpp \
-	theory_traits.h
+	theory_traits.h \
+	type_enumerator.cpp
 
 libtheory_la_LIBADD = \
 	@builddir@/builtin/libbuiltin.la \
@@ -67,6 +69,7 @@ EXTRA_DIST = \
 	rewriter_tables_template.h \
 	instantiator_tables_template.cpp \
 	theory_traits_template.h \
+	type_enumerator_template.cpp \
 	mktheorytraits \
 	mkrewriter \
 	mkinstantiator \
@@ -75,12 +78,14 @@ EXTRA_DIST = \
 BUILT_SOURCES = \
 	rewriter_tables.h \
 	instantiator_tables.cpp \
-	theory_traits.h
+	theory_traits.h \
+	type_enumerator.cpp
 
 CLEANFILES = \
 	rewriter_tables.h \
 	instantiator_tables.cpp \
-	theory_traits.h
+	theory_traits.h \
+	type_enumerator.cpp
 
 include @top_srcdir@/src/theory/Makefile.subdirs
 
@@ -107,3 +112,11 @@ theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theo
 		$< \
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
+
+type_enumerator.cpp: type_enumerator_template.cpp mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+	$(AM_V_at)chmod +x @srcdir@/mktheorytraits
+	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
+	$(AM_V_GEN)(@srcdir@/mktheorytraits \
+		$< \
+		`cat @top_builddir@/src/theory/.subdirs` \
+	> $@) || (rm -f $@ && exit 1)
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index b1e8855c7..68b580c54 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libarith.la
 
 libarith_la_SOURCES = \
 	theory_arith_type_rules.h \
+	type_enumerator.h \
 	arithvar.h \
 	arith_rewriter.h \
 	arith_rewriter.cpp \
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index c06cbc140..7883bd92b 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -55,6 +55,13 @@ constant CONST_RATIONAL \
     "util/rational.h" \
     "a multiple-precision rational constant"
 
+enumerator REAL_TYPE \
+    "::CVC4::theory::arith::RationalEnumerator" \
+    "theory/arith/type_enumerator.h"
+enumerator INTEGER_TYPE \
+    "::CVC4::theory::arith::IntegerEnumerator" \
+    "theory/arith/type_enumerator.h"
+
 operator LT 2 "less than, x < y"
 operator LEQ 2 "less than or equal, x <= y"
 operator GT 2 "greater than, x > y"
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
new file mode 100644
index 000000000..3561e3c7b
--- /dev/null
+++ b/src/theory/arith/type_enumerator.h
@@ -0,0 +1,109 @@
+/*********************                                                        */
+/*! \file type_enumerator.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Enumerators for rationals and integers
+ **
+ ** Enumerators for rationals and integers.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
+
+#include "util/integer.h"
+#include "util/rational.h"
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> {
+  Rational d_rat;
+
+public:
+
+  RationalEnumerator(TypeNode type) throw(AssertionException) :
+    TypeEnumeratorBase(type),
+    d_rat(0) {
+    Assert(type.getKind() == kind::TYPE_CONSTANT &&
+           type.getConst<TypeConstant>() == REAL_TYPE);
+  }
+
+  Node operator*() throw() {
+    return NodeManager::currentNM()->mkConst(d_rat);
+  }
+
+  RationalEnumerator& operator++() throw() {
+    // sequence is 0, then diagonal with negatives interleaved
+    // ( 0, 1/1, -1/1, 2/1, -2/1, 1/2, -1/2, 3/1, -3/1, 1/3, -1/3,
+    // 4/1, -4/1, 3/2, -3/2, 2/3, -2/3, 1/4, -1/4, ...)
+    if(d_rat == 0) {
+      d_rat = 1;
+    } else if(d_rat < 0) {
+      d_rat = -d_rat;
+      Integer num = d_rat.getNumerator();
+      Integer den = d_rat.getDenominator();
+      do {
+        num -= 1;
+        den += 1;
+        if(num == 0) {
+          num = den;
+          den = 1;
+        }
+        d_rat = Rational(num, den);
+      } while(d_rat.getNumerator() != num);
+    } else {
+      d_rat = -d_rat;
+    }
+    return *this;
+  }
+
+};/* class RationalEnumerator */
+
+class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
+  Integer d_int;
+
+public:
+
+  IntegerEnumerator(TypeNode type) throw(AssertionException) :
+    TypeEnumeratorBase(type),
+    d_int(0) {
+    Assert(type.getKind() == kind::TYPE_CONSTANT &&
+           type.getConst<TypeConstant>() == INTEGER_TYPE);
+  }
+
+  Node operator*() throw() {
+    return NodeManager::currentNM()->mkConst(Rational(d_int));
+  }
+
+  IntegerEnumerator& operator++() throw() {
+    // 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;
+  }
+
+};/* class IntegerEnumerator */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index 57c55d765..c429fc0c6 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libarrays.la
 
 libarrays_la_SOURCES = \
 	theory_arrays_type_rules.h \
+	type_enumerator.h \
 	theory_arrays_rewriter.h \
 	theory_arrays.h \
 	theory_arrays.cpp \
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 195a60035..eaef3746e 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -19,6 +19,10 @@ cardinality ARRAY_TYPE \
     "theory/arrays/theory_arrays_type_rules.h"
 well-founded ARRAY_TYPE false
 
+enumerator ARRAY_TYPE \
+    "::CVC4::theory::arrays::ArrayEnumerator" \
+    "theory/arrays/type_enumerator.h"
+
 # select a i  is  a[i]
 operator SELECT 2 "array select"
 
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
new file mode 100644
index 000000000..adea9a9e8
--- /dev/null
+++ b/src/theory/arrays/type_enumerator.h
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file type_enumerator.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An enumerator for arrays
+ **
+ ** An enumerator for arrays.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
+
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
+  TypeEnumerator d_index;
+  TypeEnumerator d_constituent;
+
+public:
+
+  ArrayEnumerator(TypeNode type) throw(AssertionException) :
+    TypeEnumeratorBase(type),
+    d_index(TypeEnumerator(type.getArrayIndexType())),
+    d_constituent(TypeEnumerator(type.getArrayConstituentType())) {
+  }
+
+  Node operator*() throw(NoMoreValuesException) {
+    return Node::null();
+    //return NodeManager::currentNM()->mkConst(Array(d_size, d_bits));
+  }
+
+  ArrayEnumerator& operator++() throw() {
+    return *this;
+  }
+
+};/* class ArrayEnumerator */
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H */
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index 524a39b69..c591ef7fb 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 noinst_LTLIBRARIES = libbooleans.la
 
 libbooleans_la_SOURCES = \
+	type_enumerator.h \
 	theory_bool.h \
 	theory_bool.cpp \
 	theory_bool_type_rules.h \
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index 5580418e5..92a9a937f 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -24,6 +24,10 @@ constant CONST_BOOLEAN \
     "util/bool.h" \
     "truth and falsity"
 
+enumerator BOOLEAN_TYPE \
+    "::CVC4::theory::booleans::BooleanEnumerator" \
+    "theory/booleans/type_enumerator.h"
+
 operator NOT 1 "logical not"
 operator AND 2: "logical and"
 operator IFF 2 "logical equivalence"
diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h
new file mode 100644
index 000000000..36fb6d855
--- /dev/null
+++ b/src/theory/booleans/type_enumerator.h
@@ -0,0 +1,71 @@
+/*********************                                                        */
+/*! \file type_enumerator.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An enumerator for Booleans
+ **
+ ** An enumerator for Booleans.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
+
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+class BooleanEnumerator : public TypeEnumeratorBase<BooleanEnumerator> {
+  enum { FALSE, TRUE, DONE } d_value;
+
+public:
+
+  BooleanEnumerator(TypeNode type) :
+    TypeEnumeratorBase(type),
+    d_value(FALSE) {
+    Assert(type.getKind() == kind::TYPE_CONSTANT &&
+           type.getConst<TypeConstant>() == BOOLEAN_TYPE);
+  }
+
+  Node operator*() throw(NoMoreValuesException) {
+    switch(d_value) {
+    case FALSE:
+      return NodeManager::currentNM()->mkConst(false);
+    case TRUE:
+      return NodeManager::currentNM()->mkConst(true);
+    default:
+      throw NoMoreValuesException(getType());
+    }
+  }
+
+  BooleanEnumerator& operator++() throw() {
+    // sequence is FALSE, TRUE
+    if(d_value == FALSE) {
+      d_value = TRUE;
+    } else {
+      d_value = DONE;
+    }
+    return *this;
+  }
+
+};/* class BooleanEnumerator */
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H */
diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am
index 9856cdbe6..4b2d566b4 100644
--- a/src/theory/builtin/Makefile.am
+++ b/src/theory/builtin/Makefile.am
@@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libbuiltin.la
 
 libbuiltin_la_SOURCES = \
 	theory_builtin_type_rules.h \
+	type_enumerator.h \
 	theory_builtin_rewriter.h \
 	theory_builtin_rewriter.cpp \
 	theory_builtin.h \
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 519536c81..39945e081 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -265,6 +265,15 @@ well-founded SORT_TYPE \
     "::CVC4::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
     "::CVC4::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)"
 
+constant UNINTERPRETED_CONSTANT \
+    ::CVC4::UninterpretedConstant \
+    ::CVC4::UninterpretedConstantHashStrategy \
+    "util/uninterpreted_constant.h" \
+    "The kind of nodes representing uninterpreted constants"
+enumerator SORT_TYPE \
+    ::CVC4::theory::builtin::UninterpretedSortEnumerator \
+    "theory/builtin/type_enumerator.h"
+
 # A kind representing "inlined" operators defined with OPERATOR
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
 # not stored that way.  If you ask for the operator of (EQUAL a b),
diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
new file mode 100644
index 000000000..4893c2100
--- /dev/null
+++ b/src/theory/builtin/type_enumerator.h
@@ -0,0 +1,60 @@
+/*********************                                                        */
+/*! \file type_enumerator.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Enumerator for uninterpreted sorts
+ **
+ ** Enumerator for uninterpreted sorts.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H
+
+#include "util/integer.h"
+#include "util/uninterpreted_constant.h"
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace theory {
+namespace builtin {
+
+class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortEnumerator> {
+  Integer d_count;
+
+public:
+
+  UninterpretedSortEnumerator(TypeNode type) throw(AssertionException) :
+    TypeEnumeratorBase(type),
+    d_count(0) {
+    Assert(type.getKind() == kind::SORT_TYPE);
+  }
+
+  Node operator*() throw() {
+    return NodeManager::currentNM()->mkConst(UninterpretedConstant(getType().toType(), d_count));
+  }
+
+  UninterpretedSortEnumerator& operator++() throw() {
+    d_count += 1;
+    return *this;
+  }
+
+};/* class UninterpretedSortEnumerator */
+
+}/* CVC4::theory::builtin namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 7748817e3..1f698de0f 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -9,6 +9,7 @@ noinst_LTLIBRARIES = libbv.la
 
 libbv_la_SOURCES = \
 	theory_bv_utils.h \
+	type_enumerator.h \
 	bitblaster.h \
 	bitblaster.cpp \
 	bv_subtheory.h \
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 6ef2cb0a9..36e27c66c 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -27,6 +27,10 @@ constant CONST_BITVECTOR \
     "util/bitvector.h" \
     "a fixed-width bit-vector constant"
 
+enumerator BITVECTOR_TYPE \
+    "::CVC4::theory::bv::BitVectorEnumerator" \
+    "theory/bv/type_enumerator.h"
+
 operator BITVECTOR_CONCAT 2: "bit-vector concatenation"
 operator BITVECTOR_AND 2: "bitwise and"
 operator BITVECTOR_OR 2: "bitwise or"
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
new file mode 100644
index 000000000..01d431303
--- /dev/null
+++ b/src/theory/bv/type_enumerator.h
@@ -0,0 +1,64 @@
+/*********************                                                        */
+/*! \file type_enumerator.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An enumerator for bitvectors
+ **
+ ** An enumerator for bitvectors.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__BV__TYPE_ENUMERATOR_H
+
+#include "util/bitvector.h"
+#include "util/integer.h"
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class BitVectorEnumerator : public TypeEnumeratorBase<BitVectorEnumerator> {
+  size_t d_size;
+  Integer d_bits;
+
+public:
+
+  BitVectorEnumerator(TypeNode type) throw(AssertionException) :
+    TypeEnumeratorBase(type),
+    d_size(type.getBitVectorSize()),
+    d_bits(0) {
+  }
+
+  Node operator*() throw(NoMoreValuesException) {
+    if(d_bits != d_bits.modByPow2(d_size)) {
+      throw NoMoreValuesException(getType());
+    }
+    return NodeManager::currentNM()->mkConst(BitVector(d_size, d_bits));
+  }
+
+  BitVectorEnumerator& operator++() throw() {
+    d_bits += 1;
+    return *this;
+  }
+
+};/* BitVectorEnumerator */
+
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BV__TYPE_ENUMERATOR_H */
diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am
index d6622b19a..14bbf64d4 100644
--- a/src/theory/datatypes/Makefile.am
+++ b/src/theory/datatypes/Makefile.am
@@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libdatatypes.la
 
 libdatatypes_la_SOURCES = \
 	theory_datatypes_type_rules.h \
+	type_enumerator.h \
 	theory_datatypes.h \
 	datatypes_rewriter.h \
 	theory_datatypes.cpp \
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 4b6bfd8f6..b83450723 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -55,6 +55,10 @@ well-founded DATATYPE_TYPE \
     "%TYPE%.getConst<Datatype>().mkGroundTerm(%TYPE%.toType())" \
     "util/datatype.h"
 
+enumerator DATATYPE_TYPE \
+    "::CVC4::theory::datatypes::DatatypesEnumerator" \
+    "theory/datatypes/type_enumerator.h"
+
 operator PARAMETRIC_DATATYPE 1: "parametric datatype"
 cardinality PARAMETRIC_DATATYPE \
     "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
new file mode 100644
index 000000000..fe6a54ba7
--- /dev/null
+++ b/src/theory/datatypes/type_enumerator.h
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \file type_enumerator.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An enumerator for bitvectors
+ **
+ ** An enumerator for bitvectors.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
+
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/type.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
+  const Datatype& d_datatype;
+  size_t d_count;
+  size_t d_ctor;
+  size_t d_numArgs;
+  size_t *d_argDistance;
+  TypeEnumerator** d_argEnumerators;
+
+public:
+
+  DatatypesEnumerator(TypeNode type) throw() :
+    TypeEnumeratorBase(type),
+    d_datatype(DatatypeType(type.toType()).getDatatype()),
+    d_count(0),
+    d_ctor(0),
+    d_numArgs(0),
+    d_argDistance(NULL),
+    d_argEnumerators(NULL) {
+    for(size_t c = 0; c < d_datatype.getNumConstructors(); ++c) {
+      if(d_datatype[c].getNumArgs() > d_numArgs) {
+        d_numArgs = d_datatype[c].getNumArgs();
+      }
+    }
+    d_argDistance = new size_t[d_numArgs];
+    d_argEnumerators = new TypeEnumerator*[d_numArgs];
+    size_t a;
+    for(a = 0; a < d_datatype[0].getNumArgs(); ++a) {
+      d_argDistance[a] = 0;
+      d_argEnumerators[a] = new TypeEnumerator(TypeNode::fromType(d_datatype[0][a].getType()));
+    }
+    while(a < d_numArgs) {
+      d_argDistance[a] = 0;
+      d_argEnumerators[a++] = NULL;
+    }
+  }
+
+  ~DatatypesEnumerator() throw() {
+    delete [] d_argDistance;
+    for(size_t a = 0; a < d_numArgs; ++a) {
+      delete d_argEnumerators[a];
+    }
+    delete [] d_argEnumerators;
+  }
+
+  Node operator*() throw(NoMoreValuesException) {
+    if(d_ctor < d_datatype.getNumConstructors()) {
+      DatatypeConstructor ctor = d_datatype[d_ctor];
+      return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, ctor.getConstructor());
+    } else {
+      throw NoMoreValuesException(getType());
+    }
+  }
+
+  DatatypesEnumerator& operator++() throw() {
+    ++d_ctor;
+    return *this;
+  }
+
+};/* DatatypesEnumerator */
+
+}/* CVC4::theory::datatypes namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */
diff --git a/src/theory/mkinstantiator b/src/theory/mkinstantiator
index 1908d2e96..73b88986b 100755
--- a/src/theory/mkinstantiator
+++ b/src/theory/mkinstantiator
@@ -125,6 +125,12 @@ function endtheory {
 "
 }
 
+function enumerator {
+  # enumerator KIND enumerator-class header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function typechecker {
   # typechecker header
   lineno=${BASH_LINENO[0]}
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 71a8ea097..ffdc1d4c6 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -100,6 +100,12 @@ function endtheory {
   seen_endtheory=true
 }
 
+function enumerator {
+  # enumerator KIND enumerator-class header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function typechecker {
   # typechecker header
   lineno=${BASH_LINENO[0]}
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 297df1f36..3607d5232 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -16,9 +16,11 @@
 
 copyright=2010-2012
 
+filename=`basename "$1" | sed 's,_template,,'`
+
 cat <<EOF
 /*********************                                                        */
-/** theory_traits.h
+/** $filename
  **
  ** Copyright $copyright  The AcSys Group, New York University, and as below.
  **
@@ -40,6 +42,9 @@ theory_includes=
 theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\
 "
 
+type_enumerator_includes=
+mk_type_enumerator_cases=
+
 theory_has_check="false"
 theory_has_propagate="false"
 theory_has_staticLearning="false"
@@ -61,6 +66,9 @@ instantiator_header=
 theory_id=
 theory_class=
 
+type_constants=
+type_kinds=
+
 seen_theory=false
 seen_theory_builtin=false
 
@@ -177,7 +185,39 @@ struct TheoryTraits<${theory_id}> {
   theory_id=
   theory_class=
 
+  type_constants=
+  type_kinds=
+
+  lineno=${BASH_LINENO[0]}
+}
+
+function enumerator {
+  # enumerator KIND enumerator-class header
   lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  type_enumerator_includes="${type_enumerator_includes}
+#line $lineno \"$kf\"
+#include \"$3\""
+  if expr "$type_constants" : '.* '"$1"' ' &>/dev/null; then
+    mk_type_enumerator_type_constant_cases="${mk_type_enumerator_type_constant_cases}
+#line $lineno \"$kf\"
+    case $1:
+#line $lineno \"$kf\"
+      return new $2(type);
+"
+  elif expr "$type_kinds" : '.* '"$1"' ' &>/dev/null; then
+    mk_type_enumerator_cases="${mk_type_enumerator_cases}
+#line $lineno \"$kf\"
+  case kind::$1:
+#line $lineno \"$kf\"
+    return new $2(type);
+"
+  else
+    echo "$kf:$lineno: error: don't know anything about $1; enumerator must appear after definition" >&2
+    echo "type_constants: $type_constants" >&2
+    echo "type_kinds    : $type_kinds" >&2
+    exit 1
+  fi
 }
 
 function typechecker {
@@ -285,6 +325,7 @@ function register_sort {
   comment=$3
   type_constant_to_theory_id="${type_constant_to_theory_id}   case $id: return $theory_id; break;
 "
+  type_constants="${type_constants} $1 "
 }
 
 function register_kind {
@@ -293,6 +334,7 @@ function register_kind {
   comment=$3
   kind_to_theory_id="${kind_to_theory_id}   case kind::$r: return $theory_id; break;
 "
+  type_kinds="${type_kinds} $1 "
 }
 
 function check_theory_seen {
@@ -342,6 +384,9 @@ for var in \
     theory_for_each_macro \
     theory_includes \
     template \
+    type_enumerator_includes \
+    mk_type_enumerator_type_constant_cases \
+    mk_type_enumerator_cases \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
new file mode 100644
index 000000000..a03f1f35a
--- /dev/null
+++ b/src/theory/type_enumerator.h
@@ -0,0 +1,106 @@
+/*********************                                                        */
+/*! \file type_enumerator.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Enumerators for types
+ **
+ ** Enumerators for types.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__TYPE_ENUMERATOR_H
+
+#include "util/exception.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace theory {
+
+class NoMoreValuesException : public Exception {
+public:
+  NoMoreValuesException(TypeNode n) throw() :
+    Exception("No more values for type `" + n.toString() + "'") {
+  }
+};/* class NoMoreValuesException */
+
+class TypeEnumeratorInterface {
+  TypeNode d_type;
+
+public:
+
+  TypeEnumeratorInterface(TypeNode type) :
+    d_type(type) {
+  }
+
+  virtual ~TypeEnumeratorInterface() {}
+
+  virtual Node operator*() throw(NoMoreValuesException) = 0;
+
+  virtual TypeEnumeratorInterface& operator++() throw() = 0;
+
+  virtual TypeEnumeratorInterface* clone() const = 0;
+
+  TypeNode getType() const throw() { return d_type; }
+
+};/* class TypeEnumeratorInterface */
+
+template <class T>
+class TypeEnumeratorBase : public TypeEnumeratorInterface {
+public:
+
+  TypeEnumeratorBase(TypeNode type) :
+    TypeEnumeratorInterface(type) {
+  }
+
+  TypeEnumeratorInterface* clone() const { return new T(static_cast<const T&>(*this)); }
+
+};/* class TypeEnumeratorBase */
+
+class TypeEnumerator {
+  TypeEnumeratorInterface* d_te;
+
+  static TypeEnumeratorInterface* mkTypeEnumerator(TypeNode type)
+    throw(AssertionException);
+
+public:
+
+  TypeEnumerator(TypeNode type) throw() :
+    d_te(mkTypeEnumerator(type)) {
+  }
+
+  TypeEnumerator(const TypeEnumerator& te) :
+    d_te(te.d_te->clone()) {
+  }
+  TypeEnumerator& operator=(const TypeEnumerator& te) {
+    delete d_te;
+    d_te = te.d_te->clone();
+    return *this;
+  }
+
+  ~TypeEnumerator() { delete d_te; }
+
+  Node operator*() throw(NoMoreValuesException) { return **d_te; }
+  TypeEnumerator& operator++() throw() { ++*d_te; return *this; }
+  TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; }
+
+  TypeNode getType() const throw() { return d_te->getType(); }
+
+};/* class TypeEnumerator */
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__TYPE_ENUMERATOR_H */
diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp
new file mode 100644
index 000000000..426bf52a0
--- /dev/null
+++ b/src/theory/type_enumerator_template.cpp
@@ -0,0 +1,61 @@
+/*********************                                                        */
+/*! \file type_enumerator_template.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Enumerators for types
+ **
+ ** Enumerators for types.
+ **/
+
+#include <sstream>
+
+#include "theory/type_enumerator.h"
+
+#include "expr/kind.h"
+#include "util/Assert.h"
+
+${type_enumerator_includes}
+#line 28 "${template}"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+
+TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(TypeNode type) throw(AssertionException) {
+  switch(type.getKind()) {
+  case kind::TYPE_CONSTANT:
+    switch(type.getConst<TypeConstant>()) {
+${mk_type_enumerator_type_constant_cases}
+    default:
+      {
+        stringstream ss;
+        ss << "No type enumerator for type `" << type << "'";
+        Unhandled(ss.str());
+      }
+    }
+    Unreachable();
+${mk_type_enumerator_cases}
+#line 49 "${template}"
+  default:
+    {
+      stringstream ss;
+      ss << "No type enumerator for type `" << type << "'";
+      Unhandled(ss.str());
+    }
+  }
+  Unreachable();
+}
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+