seen_endtheory=true
}
+function enumerator {
+ # enumerator KIND enumerator-class header
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function typechecker {
# typechecker header
lineno=${BASH_LINENO[0]}
seen_endtheory=true
}
+function enumerator {
+ # enumerator KIND enumerator-class header
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function typechecker {
# typechecker header
lineno=${BASH_LINENO[0]}
seen_endtheory=true
}
+function enumerator {
+ # enumerator KIND enumerator-class header
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function typechecker {
# typechecker header
lineno=${BASH_LINENO[0]}
friend class ExprManager;
friend class NodeManager;
friend class TypeNode;
- friend struct TypeHashStrategy;
friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t);
friend TypeNode expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
logic_info.cpp \
output_channel.h \
interrupted.h \
+ type_enumerator.h \
theory_engine.h \
theory_engine.cpp \
theory_test_utils.h \
nodist_libtheory_la_SOURCES = \
rewriter_tables.h \
instantiator_tables.cpp \
- theory_traits.h
+ theory_traits.h \
+ type_enumerator.cpp
libtheory_la_LIBADD = \
@builddir@/builtin/libbuiltin.la \
rewriter_tables_template.h \
instantiator_tables_template.cpp \
theory_traits_template.h \
+ type_enumerator_template.cpp \
mktheorytraits \
mkrewriter \
mkinstantiator \
BUILT_SOURCES = \
rewriter_tables.h \
instantiator_tables.cpp \
- theory_traits.h
+ theory_traits.h \
+ type_enumerator.cpp
CLEANFILES = \
rewriter_tables.h \
instantiator_tables.cpp \
- theory_traits.h
+ theory_traits.h \
+ type_enumerator.cpp
include @top_srcdir@/src/theory/Makefile.subdirs
$< \
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
+
+type_enumerator.cpp: type_enumerator_template.cpp mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+ $(AM_V_at)chmod +x @srcdir@/mktheorytraits
+ $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
+ $(AM_V_GEN)(@srcdir@/mktheorytraits \
+ $< \
+ `cat @top_builddir@/src/theory/.subdirs` \
+ > $@) || (rm -f $@ && exit 1)
libarith_la_SOURCES = \
theory_arith_type_rules.h \
+ type_enumerator.h \
arithvar.h \
arith_rewriter.h \
arith_rewriter.cpp \
"util/rational.h" \
"a multiple-precision rational constant"
+enumerator REAL_TYPE \
+ "::CVC4::theory::arith::RationalEnumerator" \
+ "theory/arith/type_enumerator.h"
+enumerator INTEGER_TYPE \
+ "::CVC4::theory::arith::IntegerEnumerator" \
+ "theory/arith/type_enumerator.h"
+
operator LT 2 "less than, x < y"
operator LEQ 2 "less than or equal, x <= y"
operator GT 2 "greater than, x > y"
--- /dev/null
+/********************* */
+/*! \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 Enumerators for rationals and integers
+ **
+ ** Enumerators for rationals and integers.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
+
+#include "util/integer.h"
+#include "util/rational.h"
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> {
+ Rational d_rat;
+
+public:
+
+ RationalEnumerator(TypeNode type) throw(AssertionException) :
+ TypeEnumeratorBase(type),
+ d_rat(0) {
+ Assert(type.getKind() == kind::TYPE_CONSTANT &&
+ type.getConst<TypeConstant>() == REAL_TYPE);
+ }
+
+ Node operator*() throw() {
+ return NodeManager::currentNM()->mkConst(d_rat);
+ }
+
+ RationalEnumerator& operator++() throw() {
+ // sequence is 0, then diagonal with negatives interleaved
+ // ( 0, 1/1, -1/1, 2/1, -2/1, 1/2, -1/2, 3/1, -3/1, 1/3, -1/3,
+ // 4/1, -4/1, 3/2, -3/2, 2/3, -2/3, 1/4, -1/4, ...)
+ if(d_rat == 0) {
+ d_rat = 1;
+ } else if(d_rat < 0) {
+ d_rat = -d_rat;
+ Integer num = d_rat.getNumerator();
+ Integer den = d_rat.getDenominator();
+ do {
+ num -= 1;
+ den += 1;
+ if(num == 0) {
+ num = den;
+ den = 1;
+ }
+ d_rat = Rational(num, den);
+ } while(d_rat.getNumerator() != num);
+ } else {
+ d_rat = -d_rat;
+ }
+ return *this;
+ }
+
+};/* class RationalEnumerator */
+
+class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
+ Integer d_int;
+
+public:
+
+ IntegerEnumerator(TypeNode type) throw(AssertionException) :
+ TypeEnumeratorBase(type),
+ d_int(0) {
+ Assert(type.getKind() == kind::TYPE_CONSTANT &&
+ type.getConst<TypeConstant>() == INTEGER_TYPE);
+ }
+
+ Node operator*() throw() {
+ return NodeManager::currentNM()->mkConst(Rational(d_int));
+ }
+
+ IntegerEnumerator& operator++() throw() {
+ // sequence is 0, 1, -1, 2, -2, 3, -3, ...
+ if(d_int <= 0) {
+ d_int = -d_int + 1;
+ } else {
+ d_int = -d_int;
+ }
+ return *this;
+ }
+
+};/* class IntegerEnumerator */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */
libarrays_la_SOURCES = \
theory_arrays_type_rules.h \
+ type_enumerator.h \
theory_arrays_rewriter.h \
theory_arrays.h \
theory_arrays.cpp \
"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"
--- /dev/null
+/********************* */
+/*! \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 */
noinst_LTLIBRARIES = libbooleans.la
libbooleans_la_SOURCES = \
+ type_enumerator.h \
theory_bool.h \
theory_bool.cpp \
theory_bool_type_rules.h \
"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"
--- /dev/null
+/********************* */
+/*! \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 */
libbuiltin_la_SOURCES = \
theory_builtin_type_rules.h \
+ type_enumerator.h \
theory_builtin_rewriter.h \
theory_builtin_rewriter.cpp \
theory_builtin.h \
"::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),
--- /dev/null
+/********************* */
+/*! \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 */
libbv_la_SOURCES = \
theory_bv_utils.h \
+ type_enumerator.h \
bitblaster.h \
bitblaster.cpp \
bv_subtheory.h \
"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"
--- /dev/null
+/********************* */
+/*! \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 */
libdatatypes_la_SOURCES = \
theory_datatypes_type_rules.h \
+ type_enumerator.h \
theory_datatypes.h \
datatypes_rewriter.h \
theory_datatypes.cpp \
"%TYPE%.getConst<Datatype>().mkGroundTerm(%TYPE%.toType())" \
"util/datatype.h"
+enumerator DATATYPE_TYPE \
+ "::CVC4::theory::datatypes::DatatypesEnumerator" \
+ "theory/datatypes/type_enumerator.h"
+
operator PARAMETRIC_DATATYPE 1: "parametric datatype"
cardinality PARAMETRIC_DATATYPE \
"DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \
--- /dev/null
+/********************* */
+/*! \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__DATATYPES__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H
+
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/type.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
+ const Datatype& d_datatype;
+ size_t d_count;
+ size_t d_ctor;
+ size_t d_numArgs;
+ size_t *d_argDistance;
+ TypeEnumerator** d_argEnumerators;
+
+public:
+
+ DatatypesEnumerator(TypeNode type) throw() :
+ TypeEnumeratorBase(type),
+ d_datatype(DatatypeType(type.toType()).getDatatype()),
+ d_count(0),
+ d_ctor(0),
+ d_numArgs(0),
+ d_argDistance(NULL),
+ d_argEnumerators(NULL) {
+ for(size_t c = 0; c < d_datatype.getNumConstructors(); ++c) {
+ if(d_datatype[c].getNumArgs() > d_numArgs) {
+ d_numArgs = d_datatype[c].getNumArgs();
+ }
+ }
+ d_argDistance = new size_t[d_numArgs];
+ d_argEnumerators = new TypeEnumerator*[d_numArgs];
+ size_t a;
+ for(a = 0; a < d_datatype[0].getNumArgs(); ++a) {
+ d_argDistance[a] = 0;
+ d_argEnumerators[a] = new TypeEnumerator(TypeNode::fromType(d_datatype[0][a].getType()));
+ }
+ while(a < d_numArgs) {
+ d_argDistance[a] = 0;
+ d_argEnumerators[a++] = NULL;
+ }
+ }
+
+ ~DatatypesEnumerator() throw() {
+ delete [] d_argDistance;
+ for(size_t a = 0; a < d_numArgs; ++a) {
+ delete d_argEnumerators[a];
+ }
+ delete [] d_argEnumerators;
+ }
+
+ Node operator*() throw(NoMoreValuesException) {
+ if(d_ctor < d_datatype.getNumConstructors()) {
+ DatatypeConstructor ctor = d_datatype[d_ctor];
+ return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, ctor.getConstructor());
+ } else {
+ throw NoMoreValuesException(getType());
+ }
+ }
+
+ DatatypesEnumerator& operator++() throw() {
+ ++d_ctor;
+ return *this;
+ }
+
+};/* DatatypesEnumerator */
+
+}/* CVC4::theory::datatypes namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__DATATYPES__TYPE_ENUMERATOR_H */
"
}
+function enumerator {
+ # enumerator KIND enumerator-class header
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function typechecker {
# typechecker header
lineno=${BASH_LINENO[0]}
seen_endtheory=true
}
+function enumerator {
+ # enumerator KIND enumerator-class header
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function typechecker {
# typechecker header
lineno=${BASH_LINENO[0]}
copyright=2010-2012
+filename=`basename "$1" | sed 's,_template,,'`
+
cat <<EOF
/********************* */
-/** theory_traits.h
+/** $filename
**
** Copyright $copyright The AcSys Group, New York University, and as below.
**
theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\
"
+type_enumerator_includes=
+mk_type_enumerator_cases=
+
theory_has_check="false"
theory_has_propagate="false"
theory_has_staticLearning="false"
theory_id=
theory_class=
+type_constants=
+type_kinds=
+
seen_theory=false
seen_theory_builtin=false
theory_id=
theory_class=
+ type_constants=
+ type_kinds=
+
+ lineno=${BASH_LINENO[0]}
+}
+
+function enumerator {
+ # enumerator KIND enumerator-class header
lineno=${BASH_LINENO[0]}
+ check_theory_seen
+ type_enumerator_includes="${type_enumerator_includes}
+#line $lineno \"$kf\"
+#include \"$3\""
+ if expr "$type_constants" : '.* '"$1"' ' &>/dev/null; then
+ mk_type_enumerator_type_constant_cases="${mk_type_enumerator_type_constant_cases}
+#line $lineno \"$kf\"
+ case $1:
+#line $lineno \"$kf\"
+ return new $2(type);
+"
+ elif expr "$type_kinds" : '.* '"$1"' ' &>/dev/null; then
+ mk_type_enumerator_cases="${mk_type_enumerator_cases}
+#line $lineno \"$kf\"
+ case kind::$1:
+#line $lineno \"$kf\"
+ return new $2(type);
+"
+ else
+ echo "$kf:$lineno: error: don't know anything about $1; enumerator must appear after definition" >&2
+ echo "type_constants: $type_constants" >&2
+ echo "type_kinds : $type_kinds" >&2
+ exit 1
+ fi
}
function typechecker {
comment=$3
type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break;
"
+ type_constants="${type_constants} $1 "
}
function register_kind {
comment=$3
kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break;
"
+ type_kinds="${type_kinds} $1 "
}
function check_theory_seen {
theory_for_each_macro \
theory_includes \
template \
+ type_enumerator_includes \
+ mk_type_enumerator_type_constant_cases \
+ mk_type_enumerator_cases \
; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
--- /dev/null
+/********************* */
+/*! \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 Enumerators for types
+ **
+ ** Enumerators for types.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__TYPE_ENUMERATOR_H
+
+#include "util/exception.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace theory {
+
+class NoMoreValuesException : public Exception {
+public:
+ NoMoreValuesException(TypeNode n) throw() :
+ Exception("No more values for type `" + n.toString() + "'") {
+ }
+};/* class NoMoreValuesException */
+
+class TypeEnumeratorInterface {
+ TypeNode d_type;
+
+public:
+
+ TypeEnumeratorInterface(TypeNode type) :
+ d_type(type) {
+ }
+
+ virtual ~TypeEnumeratorInterface() {}
+
+ virtual Node operator*() throw(NoMoreValuesException) = 0;
+
+ virtual TypeEnumeratorInterface& operator++() throw() = 0;
+
+ virtual TypeEnumeratorInterface* clone() const = 0;
+
+ TypeNode getType() const throw() { return d_type; }
+
+};/* class TypeEnumeratorInterface */
+
+template <class T>
+class TypeEnumeratorBase : public TypeEnumeratorInterface {
+public:
+
+ TypeEnumeratorBase(TypeNode type) :
+ TypeEnumeratorInterface(type) {
+ }
+
+ TypeEnumeratorInterface* clone() const { return new T(static_cast<const T&>(*this)); }
+
+};/* class TypeEnumeratorBase */
+
+class TypeEnumerator {
+ TypeEnumeratorInterface* d_te;
+
+ static TypeEnumeratorInterface* mkTypeEnumerator(TypeNode type)
+ throw(AssertionException);
+
+public:
+
+ TypeEnumerator(TypeNode type) throw() :
+ d_te(mkTypeEnumerator(type)) {
+ }
+
+ TypeEnumerator(const TypeEnumerator& te) :
+ d_te(te.d_te->clone()) {
+ }
+ TypeEnumerator& operator=(const TypeEnumerator& te) {
+ delete d_te;
+ d_te = te.d_te->clone();
+ return *this;
+ }
+
+ ~TypeEnumerator() { delete d_te; }
+
+ Node operator*() throw(NoMoreValuesException) { return **d_te; }
+ TypeEnumerator& operator++() throw() { ++*d_te; return *this; }
+ TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; }
+
+ TypeNode getType() const throw() { return d_te->getType(); }
+
+};/* class TypeEnumerator */
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__TYPE_ENUMERATOR_H */
--- /dev/null
+/********************* */
+/*! \file type_enumerator_template.cpp
+ ** \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 Enumerators for types
+ **
+ ** Enumerators for types.
+ **/
+
+#include <sstream>
+
+#include "theory/type_enumerator.h"
+
+#include "expr/kind.h"
+#include "util/Assert.h"
+
+${type_enumerator_includes}
+#line 28 "${template}"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+
+TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(TypeNode type) throw(AssertionException) {
+ switch(type.getKind()) {
+ case kind::TYPE_CONSTANT:
+ switch(type.getConst<TypeConstant>()) {
+${mk_type_enumerator_type_constant_cases}
+ default:
+ {
+ stringstream ss;
+ ss << "No type enumerator for type `" << type << "'";
+ Unhandled(ss.str());
+ }
+ }
+ Unreachable();
+${mk_type_enumerator_cases}
+#line 49 "${template}"
+ default:
+ {
+ stringstream ss;
+ ss << "No type enumerator for type `" << type << "'";
+ Unhandled(ss.str());
+ }
+ }
+ Unreachable();
+}
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
ite_removal.cpp \
node_visitor.h \
index.h \
+ uninterpreted_constant.h \
+ uninterpreted_constant.cpp \
model.h \
model.cpp
--- /dev/null
+/********************* */
+/*! \file uninterpreted_constant.cpp
+ ** \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 Representation of constants of uninterpreted sorts
+ **
+ ** Representation of constants of uninterpreted sorts.
+ **/
+
+#include "util/uninterpreted_constant.h"
+#include <iostream>
+#include <sstream>
+#include <string>
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) {
+ stringstream ss;
+ ss << uc.getType();
+ string t = ss.str();
+ size_t i = 0;
+ // replace everything that isn't in [a-zA-Z0-9_] with an _
+ while((i = t.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ1234567890_", i)) != string::npos) {
+ t.replace(i, 1, 1, '_');
+ }
+ return out << "_uc_" << t << '_' << uc.getIndex();
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file uninterpreted_constant.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 Representation of constants of uninterpreted sorts
+ **
+ ** Representation of constants of uninterpreted sorts.
+ **/
+
+#include "cvc4_public.h"
+
+#pragma once
+
+#include "expr/type.h"
+#include <iostream>
+
+namespace CVC4 {
+
+class CVC4_PUBLIC UninterpretedConstant {
+ const Type d_type;
+ const Integer d_index;
+
+public:
+
+ UninterpretedConstant(Type type, Integer index) throw() :
+ d_type(type),
+ d_index(index) {
+ CheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
+ CheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
+ }
+
+ ~UninterpretedConstant() throw() {
+ }
+
+ Type getType() const throw() {
+ return d_type;
+ }
+ const Integer& getIndex() const throw() {
+ return d_index;
+ }
+
+ bool operator==(const UninterpretedConstant& uc) const throw() {
+ return d_type == uc.d_type && d_index == uc.d_index;
+ }
+ bool operator!=(const UninterpretedConstant& uc) const throw() {
+ return !(*this == uc);
+ }
+
+ bool operator<(const UninterpretedConstant& uc) const throw() {
+ return d_type < uc.d_type ||
+ (d_type == uc.d_type && d_index < uc.d_index);
+ }
+ bool operator<=(const UninterpretedConstant& uc) const throw() {
+ return d_type < uc.d_type ||
+ (d_type == uc.d_type && d_index <= uc.d_index);
+ }
+ bool operator>(const UninterpretedConstant& uc) const throw() {
+ return !(*this <= uc);
+ }
+ bool operator>=(const UninterpretedConstant& uc) const throw() {
+ return !(*this < uc);
+ }
+
+};/* class UninterpretedConstant */
+
+std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC4_PUBLIC;
+
+/**
+ * Hash function for the BitVector constants.
+ */
+struct CVC4_PUBLIC UninterpretedConstantHashStrategy {
+ static inline size_t hash(const UninterpretedConstant& uc) {
+ return TypeHashFunction()(uc.getType()) * IntegerHashStrategy::hash(uc.getIndex());
+ }
+};/* struct UninterpretedConstantHashStrategy */
+
+}/* CVC4 namespace */
theory/theory_arith_white \
theory/union_find_black \
theory/theory_bv_white \
+ theory/type_enumerator_white \
expr/expr_public \
expr/expr_manager_public \
expr/node_white \
--- /dev/null
+/********************* */
+/*! \file type_enumerator_white.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 White box testing of CVC4::theory::TypeEnumerator
+ **
+ ** White box testing of CVC4::theory::TypeEnumerator. (These tests depends
+ ** on the ordering that the TypeEnumerators use, so it's a white-box test.)
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "expr/node_manager.h"
+#include "expr/expr_manager.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+#include "theory/type_enumerator.h"
+#include "util/language.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::kind;
+
+using namespace std;
+
+class TypeEnumeratorWhite : public CxxTest::TestSuite {
+ ExprManager* d_em;
+ NodeManager* d_nm;
+ NodeManagerScope* d_scope;
+
+public:
+
+ void setUp() {
+ d_em = new ExprManager();
+ d_nm = NodeManager::fromExprManager(d_em);
+ d_scope = new NodeManagerScope(d_nm);
+ }
+
+ void tearDown() {
+ delete d_scope;
+ delete d_em;
+ }
+
+ void testBooleans() {
+ TypeEnumerator te(d_nm->booleanType());
+ TS_ASSERT_EQUALS(*te, d_nm->mkConst(false));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(true));
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ }
+
+ void testUF() {
+ TypeNode sortn = d_nm->mkSort("T");
+ Type sort = sortn.toType();
+ TypeNode sortn2 = d_nm->mkSort("U");
+ Type sort2 = sortn2.toType();
+ TypeEnumerator te(sortn);
+ TS_ASSERT_EQUALS(*te, d_nm->mkConst(UninterpretedConstant(sort, 0)));
+ for(size_t i = 1; i < 100; ++i) {
+ TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i)));
+ TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort2, i)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(UninterpretedConstant(sort, i)));
+ TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i + 2)));
+ }
+ }
+
+ void testArith() {
+ TypeEnumerator te(d_nm->integerType());
+ TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0)));
+ for(int i = 1; i <= 100; ++i) {
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(i)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-i)));
+ }
+
+ te = TypeEnumerator(d_nm->realType());
+ TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 2)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 2)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 3)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 3)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 2)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 2)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 3)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 3)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 4)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 4)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 5)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 5)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(6, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-6, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 2)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 2)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 3)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 3)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 4)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 4)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 5)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 5)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 6)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 6)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(7, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-7, 1)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 3)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 3)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 5)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 5)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 7)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 7)));
+ }
+
+ void testDatatypesFinite() {
+ Datatype dt("Colors");
+ dt.addConstructor(DatatypeConstructor("red"));
+ dt.addConstructor(DatatypeConstructor("orange"));
+ dt.addConstructor(DatatypeConstructor("yellow"));
+ dt.addConstructor(DatatypeConstructor("green"));
+ dt.addConstructor(DatatypeConstructor("blue"));
+ dt.addConstructor(DatatypeConstructor("violet"));
+ TypeNode datatype = TypeNode::fromType(d_em->mkDatatypeType(dt));
+ TypeEnumerator te(datatype);
+ TS_ASSERT_EQUALS(*te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("red")));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("orange")));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("yellow")));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("green")));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("blue")));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("violet")));
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ }
+
+ void NOtestDatatypesInfinite() {
+ TypeNode datatype;
+ TypeEnumerator te(datatype);
+ TS_FAIL("unimplemented");
+ }
+
+ void NOtestArraysInfinite() {
+ TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType()));
+
+ TS_FAIL("unimplemented");
+ }
+
+ // remove this when ArrayConst is available
+ template <class T, class U> inline bool ArrayConst(const T&, const U&) { return false; }
+
+ void NOtestArraysFinite() {
+ TypeEnumerator te(d_nm->mkArrayType(d_nm->mkBitVectorType(2), d_nm->booleanType()));
+ TS_ASSERT_EQUALS(*te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(0)), d_nm->mkConst(false))));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(0)), d_nm->mkConst(true))));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(1)), d_nm->mkConst(false))));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(1)), d_nm->mkConst(true))));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(2)), d_nm->mkConst(false))));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(2)), d_nm->mkConst(true))));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(3)), d_nm->mkConst(false))));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(3)), d_nm->mkConst(true))));
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ }
+
+ void testBV() {
+ TypeEnumerator te(d_nm->mkBitVectorType(3));
+ TS_ASSERT_EQUALS(*te, d_nm->mkConst(BitVector(3u, 0u)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 1u)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 2u)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 3u)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 4u)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 5u)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 6u)));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 7u)));
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ }
+
+};/* class TypeEnumeratorWhite */
projects / cvc5.git / commitdiff