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

3 files changed, 69 insertions, 0 deletions

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