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

3 files changed, 64 insertions, 0 deletions

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 */