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

3 files changed, 70 insertions, 0 deletions

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