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

3 files changed, 76 insertions, 0 deletions

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