diff options
Diffstat (limited to 'src')
31 files changed, 885 insertions, 5 deletions
diff --git a/src/expr/mkexpr b/src/expr/mkexpr index e113a1e8f..8b21814dc 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -114,6 +114,12 @@ function endtheory { 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]} diff --git a/src/expr/mkkind b/src/expr/mkkind index 2f361cb63..89e77754f 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -124,6 +124,12 @@ function endtheory { 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]} diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 2e94e41be..654a1f94f 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -99,6 +99,12 @@ function endtheory { 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]} diff --git a/src/expr/type.h b/src/expr/type.h index 8e9190ac5..a813aec02 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -91,7 +91,6 @@ class CVC4_PUBLIC Type { 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); diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index bca96f7d7..1aae03aa5 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -13,6 +13,7 @@ libtheory_la_SOURCES = \ logic_info.cpp \ output_channel.h \ interrupted.h \ + type_enumerator.h \ theory_engine.h \ theory_engine.cpp \ theory_test_utils.h \ @@ -50,7 +51,8 @@ libtheory_la_SOURCES = \ 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 \ @@ -67,6 +69,7 @@ EXTRA_DIST = \ rewriter_tables_template.h \ instantiator_tables_template.cpp \ theory_traits_template.h \ + type_enumerator_template.cpp \ mktheorytraits \ mkrewriter \ mkinstantiator \ @@ -75,12 +78,14 @@ EXTRA_DIST = \ 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 @@ -107,3 +112,11 @@ theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theo $< \ `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) diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index b1e8855c7..68b580c54 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libarith.la libarith_la_SOURCES = \ theory_arith_type_rules.h \ + type_enumerator.h \ arithvar.h \ arith_rewriter.h \ arith_rewriter.cpp \ diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index c06cbc140..7883bd92b 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -55,6 +55,13 @@ constant CONST_RATIONAL \ "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" diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h new file mode 100644 index 000000000..3561e3c7b --- /dev/null +++ b/src/theory/arith/type_enumerator.h @@ -0,0 +1,109 @@ +/********************* */ +/*! \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 */ 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 */ 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 */ 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 */ 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 */ diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am index d6622b19a..14bbf64d4 100644 --- a/src/theory/datatypes/Makefile.am +++ b/src/theory/datatypes/Makefile.am @@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libdatatypes.la libdatatypes_la_SOURCES = \ theory_datatypes_type_rules.h \ + type_enumerator.h \ theory_datatypes.h \ datatypes_rewriter.h \ theory_datatypes.cpp \ diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 4b6bfd8f6..b83450723 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -55,6 +55,10 @@ well-founded DATATYPE_TYPE \ "%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()" \ diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h new file mode 100644 index 000000000..fe6a54ba7 --- /dev/null +++ b/src/theory/datatypes/type_enumerator.h @@ -0,0 +1,97 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/mkinstantiator b/src/theory/mkinstantiator index 1908d2e96..73b88986b 100755 --- a/src/theory/mkinstantiator +++ b/src/theory/mkinstantiator @@ -125,6 +125,12 @@ function endtheory { " } +function enumerator { + # enumerator KIND enumerator-class header + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function typechecker { # typechecker header lineno=${BASH_LINENO[0]} diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index 71a8ea097..ffdc1d4c6 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -100,6 +100,12 @@ function endtheory { 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]} diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 297df1f36..3607d5232 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -16,9 +16,11 @@ 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. ** @@ -40,6 +42,9 @@ theory_includes= 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" @@ -61,6 +66,9 @@ instantiator_header= theory_id= theory_class= +type_constants= +type_kinds= + seen_theory=false seen_theory_builtin=false @@ -177,7 +185,39 @@ struct TheoryTraits<${theory_id}> { 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 { @@ -285,6 +325,7 @@ function register_sort { 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 { @@ -293,6 +334,7 @@ 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 { @@ -342,6 +384,9 @@ for var in \ 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 diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h new file mode 100644 index 000000000..a03f1f35a --- /dev/null +++ b/src/theory/type_enumerator.h @@ -0,0 +1,106 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp new file mode 100644 index 000000000..426bf52a0 --- /dev/null +++ b/src/theory/type_enumerator_template.cpp @@ -0,0 +1,61 @@ +/********************* */ +/*! \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 */ + diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 43cc15ec9..08b5d05f5 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -74,6 +74,8 @@ libutil_la_SOURCES = \ ite_removal.cpp \ node_visitor.h \ index.h \ + uninterpreted_constant.h \ + uninterpreted_constant.cpp \ model.h \ model.cpp diff --git a/src/util/uninterpreted_constant.cpp b/src/util/uninterpreted_constant.cpp new file mode 100644 index 000000000..766d86428 --- /dev/null +++ b/src/util/uninterpreted_constant.cpp @@ -0,0 +1,40 @@ +/********************* */ +/*! \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 */ diff --git a/src/util/uninterpreted_constant.h b/src/util/uninterpreted_constant.h new file mode 100644 index 000000000..a6e7a7256 --- /dev/null +++ b/src/util/uninterpreted_constant.h @@ -0,0 +1,86 @@ +/********************* */ +/*! \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 */ |