diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/Makefile.am | 1 | ||||
-rw-r--r-- | src/theory/arrays/kinds | 4 | ||||
-rw-r--r-- | src/theory/arrays/type_enumerator.h | 59 |
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 */ |