diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 35 | ||||
-rw-r--r-- | src/expr/command.h | 18 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 65 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 30 | ||||
-rw-r--r-- | src/expr/expr_template.h | 88 | ||||
-rwxr-xr-x | src/expr/mkexpr | 23 | ||||
-rwxr-xr-x | src/expr/mkkind | 2 | ||||
-rw-r--r-- | src/expr/node.h | 2 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 32 | ||||
-rw-r--r-- | src/expr/node_manager.h | 23 | ||||
-rw-r--r-- | src/expr/type.cpp | 104 | ||||
-rw-r--r-- | src/expr/type.h | 134 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 48 | ||||
-rw-r--r-- | src/expr/type_node.h | 42 |
14 files changed, 584 insertions, 62 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 7c08293be..bcc96637f 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -2,10 +2,10 @@ /*! \file command.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -498,6 +498,35 @@ void GetOptionCommand::toStream(std::ostream& out) const { out << "GetOption(" << d_flag << ")"; } +/* class DatatypeDeclarationCommand */ + +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) : + d_datatypes() { + d_datatypes.push_back(datatype); + Debug("datatypes") << "Create datatype command." << endl; +} + +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) : + d_datatypes(datatypes) { + Debug("datatypes") << "Create datatype command." << endl; +} + +void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) { + Debug("datatypes") << "Invoke datatype command." << endl; + //smtEngine->addDatatypeDefinitions(d_datatype); +} + +void DatatypeDeclarationCommand::toStream(std::ostream& out) const { + out << "DatatypeDeclarationCommand(["; + for(vector<DatatypeType>::const_iterator i = d_datatypes.begin(), + i_end = d_datatypes.end(); + i != i_end; + ++i) { + out << *i << ";" << endl; + } + out << "])"; +} + /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) { diff --git a/src/expr/command.h b/src/expr/command.h index fbb48b6b0..585e60eb4 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -2,10 +2,10 @@ /*! \file command.h ** \verbatim ** Original author: mdeters - ** Major contributors: cconway, dejan - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -28,11 +28,13 @@ #include <sstream> #include <string> #include <vector> +#include <map> #include "expr/expr.h" #include "expr/type.h" #include "util/result.h" #include "util/sexpr.h" +#include "util/datatype.h" namespace CVC4 { @@ -264,6 +266,16 @@ public: void printResult(std::ostream& out) const; };/* class GetOptionCommand */ +class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { +private: + std::vector<DatatypeType> d_datatypes; +public: + DatatypeDeclarationCommand(const DatatypeType& datatype); + DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes); + void invoke(SmtEngine* smtEngine); + void toStream(std::ostream& out) const; +};/* class DatatypeDeclarationCommand */ + class CVC4_PUBLIC CommandSequence : public Command { private: /** All the commands to be executed (in sequence) */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 6e8b6c63c..21fc0a4a1 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -2,10 +2,10 @@ /*! \file expr_manager_template.cpp ** \verbatim ** Original author: dejan - ** Major contributors: mdeters, cconway + ** Major contributors: cconway, mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -22,13 +22,15 @@ #include "util/options.h" #include "util/stats.h" +#include <map> + ${includes} // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 32 "${template}" +#line 34 "${template}" #ifdef CVC4_STATISTICS_ON #define INC_STAT(kind) \ @@ -340,6 +342,63 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)))); } +DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) { + NodeManagerScope nms(d_nodeManager); + TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(datatype)); + Type type(d_nodeManager, typeNode); + DatatypeType dtt(type); + const Datatype& dt = typeNode->getConst<Datatype>(); + if(!dt.isResolved()) { + std::map<std::string, DatatypeType> resolutions; + resolutions.insert(std::make_pair(datatype.getName(), dtt)); + const_cast<Datatype&>(dt).resolve(this, resolutions); + } + return dtt; +} + +std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { + NodeManagerScope nms(d_nodeManager); + std::map<std::string, DatatypeType> resolutions; + std::vector<DatatypeType> dtts; + for(std::vector<Datatype>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); + i != i_end; + ++i) { + TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); + Type type(d_nodeManager, typeNode); + DatatypeType dtt(type); + CheckArgument(resolutions.find((*i).getName()) == resolutions.end(), + datatypes, + "cannot construct two datatypes at the same time with the same name `%s'", + (*i).getName().c_str()); + resolutions.insert(std::make_pair((*i).getName(), dtt)); + dtts.push_back(dtt); + } + for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end(); + i != i_end; + ++i) { + const Datatype& dt = (*i).getDatatype(); + if(!dt.isResolved()) { + const_cast<Datatype&>(dt).resolve(this, resolutions); + } + } + return dtts; +} + +ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode))); +} + +SelectorType ExprManager::mkSelectorType(Type domain, Type range) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode))); +} + +TesterType ExprManager::mkTesterType(Type domain) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode))); +} + SortType ExprManager::mkSort(const std::string& name) const { NodeManagerScope nms(d_nodeManager); return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index f51d6fa28..415d05878 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -241,20 +241,40 @@ public: */ TupleType mkTupleType(const std::vector<Type>& types); - /** Make a type representing a bit-vector of the given size */ + /** Make a type representing a bit-vector of the given size. */ BitVectorType mkBitVectorType(unsigned size) const; - /** Make the type of arrays with the given parameterization */ + /** Make the type of arrays with the given parameterization. */ ArrayType mkArrayType(Type indexType, Type constituentType) const; + /** Make a type representing the given datatype. */ + DatatypeType mkDatatypeType(const Datatype& datatype); + + /** + * Make a set of types representing the given datatypes, which may be + * mutually recursive. + */ + std::vector<DatatypeType> mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); + + /** + * Make a type representing a constructor with the given parameterization. + */ + ConstructorType mkConstructorType(const Datatype::Constructor& constructor, Type range) const; + + /** Make a type representing a selector with the given parameterization. */ + SelectorType mkSelectorType(Type domain, Type range) const; + + /** Make a type representing a tester with the given parameterization. */ + TesterType mkTesterType(Type domain) const; + /** Make a new sort with the given name. */ SortType mkSort(const std::string& name) const; - /** Make a new sort from a constructor */ + /** Make a new sort from a constructor. */ SortType mkSort(SortConstructorType constructor, const std::vector<TypeNode>& children) const; - /** Make a sort constructor from a name and arity */ + /** Make a sort constructor from a name and arity. */ SortConstructorType mkSortConstructor(const std::string& name, size_t arity) const; diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 1a9722939..489564d5f 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -18,6 +18,13 @@ #include "cvc4_public.h" +// putting the constant-payload #includes up here allows circularity +// (some of them may require a completely-defined Expr type). This +// way, those #includes can forward-declare some stuff to get Expr's +// getConst<> template instantiations correct, and then #include +// "expr.h" safely, then go on to completely declare their own stuff. +${includes} + #ifndef __CVC4__EXPR_H #define __CVC4__EXPR_H @@ -28,13 +35,11 @@ #include "util/exception.h" #include "util/language.h" -${includes} - // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 38 "${template}" +#line 43 "${template}" namespace CVC4 { @@ -576,6 +581,31 @@ public: static inline void setDepth(std::ostream& out, long depth) { out.iword(s_iosIndex) = depth; } + + /** + * Set the expression depth on the output stream for the current + * stack scope. This makes sure the old depth is reset on the stream + * after normal OR exceptional exit from the scope, using the RAII + * C++ idiom. + */ + class Scope { + std::ostream& d_out; + long d_oldDepth; + + public: + + inline Scope(std::ostream& out, long depth) : + d_out(out), + d_oldDepth(ExprSetDepth::getDepth(out)) { + ExprSetDepth::setDepth(out, depth); + } + + inline ~Scope() { + ExprSetDepth::setDepth(d_out, d_oldDepth); + } + + };/* class ExprSetDepth::Scope */ + };/* class ExprSetDepth */ /** @@ -621,6 +651,31 @@ public: static inline void setPrintTypes(std::ostream& out, bool printTypes) { out.iword(s_iosIndex) = printTypes; } + + /** + * Set the print-types state on the output stream for the current + * stack scope. This makes sure the old state is reset on the + * stream after normal OR exceptional exit from the scope, using the + * RAII C++ idiom. + */ + class Scope { + std::ostream& d_out; + bool d_oldPrintTypes; + + public: + + inline Scope(std::ostream& out, bool printTypes) : + d_out(out), + d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) { + ExprPrintTypes::setPrintTypes(out, printTypes); + } + + inline ~Scope() { + ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes); + } + + };/* class ExprPrintTypes::Scope */ + };/* class ExprPrintTypes */ /** @@ -668,13 +723,38 @@ public: // (offset by one to detect whether default has been set yet) out.iword(s_iosIndex) = int(l) + 1; } + + /** + * Set a language on the output stream for the current stack scope. + * This makes sure the old language is reset on the stream after + * normal OR exceptional exit from the scope, using the RAII C++ + * idiom. + */ + class Scope { + std::ostream& d_out; + OutputLanguage d_oldLanguage; + + public: + + inline Scope(std::ostream& out, OutputLanguage language) : + d_out(out), + d_oldLanguage(ExprSetLanguage::getLanguage(out)) { + ExprSetLanguage::setLanguage(out, language); + } + + inline ~Scope() { + ExprSetLanguage::setLanguage(d_out, d_oldLanguage); + } + + };/* class ExprSetLanguage::Scope */ + };/* class ExprSetLanguage */ }/* CVC4::expr namespace */ ${getConst_instantiations} -#line 676 "${template}" +#line 682 "${template}" namespace expr { diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 40bf9992c..da2847d84 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -138,25 +138,26 @@ function constant { includes="${includes} #include \"$4\"" mkConst_instantiations="${mkConst_instantiations} -template <> -Expr ExprManager::mkConst($2 const& val); +#line $lineno \"$kf\" +template <> Expr ExprManager::mkConst($2 const& val); " mkConst_implementations="${mkConst_implementations} -template <> -Expr ExprManager::mkConst($2 const& val) { +#line $lineno \"$kf\" +template <> Expr ExprManager::mkConst($2 const& val) { +#line $lineno \"$kf\" return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val))); } " getConst_instantiations="${getConst_instantiations} -template <> -$2 const & Expr::getConst< $2 >() const; +#line $lineno \"$kf\" +template <> $2 const & Expr::getConst< $2 >() const; " getConst_implementations="${getConst_implementations} -template <> -$2 const & Expr::getConst() const { - // check even for production builds - CheckArgument(getKind() == ::CVC4::kind::$1, *this, - \"Improper kind for getConst<$2>()\"); +#line $lineno \"$kf\" +template <> $2 const & Expr::getConst() const { +#line $lineno \"$kf\" + CheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\"); +#line $lineno \"$kf\" return d_node->getConst< $2 >(); } " diff --git a/src/expr/mkkind b/src/expr/mkkind index 631f73a89..f7f6ba836 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -74,7 +74,7 @@ function theory { theory_id="$1" theory_enum="$1, - ${theory_enum}" + ${theory_enum}" theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; " } diff --git a/src/expr/node.h b/src/expr/node.h index 2509640e0..d3775cb3f 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -813,7 +813,7 @@ namespace CVC4 { // for hash_maps, hash_sets.. struct NodeHashFunction { - size_t operator()(const CVC4::Node& node) const { + size_t operator()(CVC4::Node node) const { return (size_t) node.getId(); } };/* struct NodeHashFunction */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 793b701f8..9449594e3 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -2,10 +2,10 @@ /*! \file node_manager.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: cconway, dejan - ** Minor contributors (to current version): acsys, taking + ** Major contributors: cconway + ** Minor contributors (to current version): acsys, taking, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -26,6 +26,7 @@ #include "theory/arith/theory_arith_type_rules.h" #include "theory/arrays/theory_arrays_type_rules.h" #include "theory/bv/theory_bv_type_rules.h" +#include "theory/datatypes/theory_datatypes_type_rules.h" #include "util/Assert.h" #include "util/options.h" @@ -434,6 +435,15 @@ TypeNode NodeManager::computeType(TNode n, bool check) case kind::BITVECTOR_SIGN_EXTEND: typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check); break; + case kind::APPLY_CONSTRUCTOR: + typeNode = CVC4::theory::datatypes::DatatypeConstructorTypeRule::computeType(this, n, check); + break; + case kind::APPLY_SELECTOR: + typeNode = CVC4::theory::datatypes::DatatypeSelectorTypeRule::computeType(this, n, check); + break; + case kind::APPLY_TESTER: + typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check); + break; default: Debug("getType") << "FAILURE" << std::endl; Unhandled(n.getKind()); @@ -509,4 +519,20 @@ TypeNode NodeManager::getType(TNode n, bool check) return typeNode; } +TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, TypeNode range) { + std::vector<TypeNode> sorts; + Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl; + for(Datatype::Constructor::const_iterator i = constructor.begin(); + i != constructor.end(); + ++i) { + Debug("datatypes") << *(*i).getSelector().getType().d_typeNode << std::endl; + TypeNode sort = (*(*i).getSelector().getType().d_typeNode)[1]; + Debug("datatypes") << "ctor sort: " << sort << std::endl; + sorts.push_back(sort); + } + Debug("datatypes") << "ctor range: " << range << std::endl; + sorts.push_back(range); + return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); +} + }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1760f48c7..7f7d37a52 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -5,7 +5,7 @@ ** Major contributors: cconway, dejan ** Minor contributors (to current version): acsys, taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -55,8 +55,8 @@ namespace attr { struct SortArityTag {}; }/* CVC4::expr::attr namespace */ -typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr; -typedef expr::Attribute<attr::SortArityTag, uint64_t> SortArityAttr; +typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; +typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; }/* CVC4::expr namespace */ @@ -542,6 +542,15 @@ public: /** Make the type of arrays with the given parameterization */ inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); + /** Make a type representing a constructor with the given parameterization */ + TypeNode mkConstructorType(const Datatype::Constructor& constructor, TypeNode range); + + /** Make a type representing a selector with the given parameterization */ + inline TypeNode mkSelectorType(TypeNode domain, TypeNode range); + + /** Make a type representing a tester with given parameterization */ + inline TypeNode mkTesterType(TypeNode domain); + /** Make a new (anonymous) sort of arity 0. */ inline TypeNode mkSort(); @@ -796,6 +805,14 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } +inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) { + return mkTypeNode(kind::SELECTOR_TYPE, domain, range); +} + +inline TypeNode NodeManager::mkTesterType(TypeNode domain) { + return mkTypeNode(kind::TESTER_TYPE, domain ); +} + inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); if(find == d_nodeValuePool.end()) { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 78554f61f..6dd9c5cec 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -2,10 +2,10 @@ /*! \file type.cpp ** \verbatim ** Original author: cconway - ** Major contributors: mdeters, dejan + ** Major contributors: dejan, mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -186,6 +186,58 @@ Type::operator BitVectorType() const throw(AssertionException) { return BitVectorType(*this); } +/** Cast to a Constructor type */ +Type::operator DatatypeType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isDatatype()); + return DatatypeType(*this); +} + +/** Is this the Datatype type? */ +bool Type::isDatatype() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isDatatype(); +} + +/** Cast to a Constructor type */ +Type::operator ConstructorType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isConstructor()); + return ConstructorType(*this); +} + +/** Is this the Constructor type? */ +bool Type::isConstructor() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isConstructor(); +} + +/** Cast to a Selector type */ +Type::operator SelectorType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isSelector()); + return SelectorType(*this); +} + +/** Is this the Selector type? */ +bool Type::isSelector() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isSelector(); +} + +/** Cast to a Tester type */ +Type::operator TesterType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isTester()); + return TesterType(*this); +} + +/** Is this the Tester type? */ +bool Type::isTester() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isTester(); +} + /** Is this a function type? */ bool Type::isFunction() const { NodeManagerScope nms(d_nodeManager); @@ -349,6 +401,26 @@ BitVectorType::BitVectorType(const Type& t) throw(AssertionException) : Assert(isBitVector()); } +DatatypeType::DatatypeType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isDatatype()); +} + +ConstructorType::ConstructorType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isConstructor()); +} + +SelectorType::SelectorType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isSelector()); +} + +TesterType::TesterType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isTester()); +} + FunctionType::FunctionType(const Type& t) throw(AssertionException) : Type(t) { Assert(isFunction()); @@ -392,8 +464,32 @@ Type ArrayType::getConstituentType() const { return makeType(d_typeNode->getArrayConstituentType()); } -size_t TypeHashStrategy::hash(const Type& t) { - return TypeNodeHashStrategy::hash(*t.d_typeNode); +Type ConstructorType::getReturnType() const { + return makeType(d_typeNode->getConstructorReturnType()); +} + +const Datatype& DatatypeType::getDatatype() const { + return d_typeNode->getConst<Datatype>(); +} + +DatatypeType SelectorType::getDomain() const { + return DatatypeType(makeType((*d_typeNode)[0])); +} + +Type SelectorType::getRangeType() const { + return makeType((*d_typeNode)[1]); +} + +DatatypeType TesterType::getDomain() const { + return DatatypeType(makeType((*d_typeNode)[0])); +} + +BooleanType TesterType::getRangeType() const { + return BooleanType(makeType(d_nodeManager->booleanType())); +} + +size_t TypeHashFunction::operator()(const Type& t) { + return TypeNodeHashFunction()(NodeManager::fromType(t)); } }/* CVC4 namespace */ diff --git a/src/expr/type.h b/src/expr/type.h index 130aa3122..3b476ddf5 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters, dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -36,6 +36,8 @@ class TypeNode; class SmtEngine; +class Datatype; + template <bool ref_count> class NodeTemplate; @@ -44,6 +46,10 @@ class IntegerType; class RealType; class BitVectorType; class ArrayType; +class DatatypeType; +class ConstructorType; +class SelectorType; +class TesterType; class FunctionType; class TupleType; class KindType; @@ -52,10 +58,10 @@ class SortConstructorType; class Type; /** Strategy for hashing Types */ -struct CVC4_PUBLIC TypeHashStrategy { +struct CVC4_PUBLIC TypeHashFunction { /** Return a hash code for type t */ - static size_t hash(const CVC4::Type& t); -};/* struct TypeHashStrategy */ + size_t operator()(const CVC4::Type& t); +};/* struct TypeHashFunction */ /** * Output operator for types @@ -259,6 +265,54 @@ public: operator ArrayType() const throw(AssertionException); /** + * Is this a datatype type? + * @return true if the type is a datatype type + */ + bool isDatatype() const; + + /** + * Cast this type to a datatype type + * @return the DatatypeType + */ + operator DatatypeType() const throw(AssertionException); + + /** + * Is this a constructor type? + * @return true if the type is a constructor type + */ + bool isConstructor() const; + + /** + * Cast this type to a constructor type + * @return the ConstructorType + */ + operator ConstructorType() const throw(AssertionException); + + /** + * Is this a selector type? + * @return true if the type is a selector type + */ + bool isSelector() const; + + /** + * Cast this type to a selector type + * @return the SelectorType + */ + operator SelectorType() const throw(AssertionException); + + /** + * Is this a tester type? + * @return true if the type is a tester type + */ + bool isTester() const; + + /** + * Cast this type to a tester type + * @return the TesterType + */ + operator TesterType() const throw(AssertionException); + + /** * Is this a sort kind? * @return true if this is a sort kind */ @@ -449,6 +503,78 @@ public: unsigned getSize() const; };/* class BitVectorType */ + +/** + * Class encapsulating the datatype type + */ +class CVC4_PUBLIC DatatypeType : public Type { + +public: + + /** Construct from the base type */ + DatatypeType(const Type& type) throw(AssertionException); + + /** Get the underlying datatype */ + const Datatype& getDatatype() const; + +};/* class DatatypeType */ + + +/** + * Class encapsulating the constructor type + */ +class CVC4_PUBLIC ConstructorType : public Type { + +public: + + /** Construct from the base type */ + ConstructorType(const Type& type) throw(AssertionException); + + /** Get the return type */ + Type getReturnType() const; + +};/* class ConstructorType */ + + +/** + * Class encapsulating the Selector type + */ +class CVC4_PUBLIC SelectorType : public Type { + +public: + + /** Construct from the base type */ + SelectorType(const Type& type) throw(AssertionException); + + /** Get the domain type for this selector (the datatype type) */ + DatatypeType getDomain() const; + + /** Get the range type for this selector (the field type) */ + Type getRangeType() const; + +};/* class SelectorType */ + +/** + * Class encapsulating the Tester type + */ +class CVC4_PUBLIC TesterType : public Type { + +public: + + /** Construct from the base type */ + TesterType(const Type& type) throw(AssertionException); + + /** Get the type that this tester tests (the datatype type) */ + DatatypeType getDomain() const; + + /** + * Get the range type for this tester (included for sake of + * interface completeness), but doesn't give useful information). + */ + BooleanType getRangeType() const; + +};/* class TesterType */ + }/* CVC4 namespace */ #endif /* __CVC4__TYPE_H */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index badc3b72f..7549af895 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -76,28 +76,38 @@ TypeNode TypeNode::getArrayConstituentType() const { return (*this)[1]; } -/** Is this a function type? */ +TypeNode TypeNode::getConstructorReturnType() const { + Assert(isConstructor()); + return (*this)[getNumChildren()-1]; +} + bool TypeNode::isFunction() const { return getKind() == kind::FUNCTION_TYPE; } -/** Is this a predicate type? NOTE: all predicate types are also - function types. */ bool TypeNode::isPredicate() const { return isFunction() && getRangeType().isBoolean(); } -vector<TypeNode> TypeNode::getArgTypes() const { - Assert(isFunction()); +std::vector<TypeNode> TypeNode::getArgTypes() const { vector<TypeNode> args; - for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { - args.push_back((*this)[i]); + if(isTester()) { + Assert(getNumChildren() == 1); + args.push_back((*this)[0]); + } else { + Assert(isFunction() || isConstructor() || isSelector()); + for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { + args.push_back((*this)[i]); + } } return args; } TypeNode TypeNode::getRangeType() const { - Assert(isFunction()); + if(isTester()) { + return NodeManager::currentNM()->booleanType(); + } + Assert(isFunction() || isConstructor() || isSelector()); return (*this)[getNumChildren()-1]; } @@ -137,6 +147,26 @@ bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE; } +/** Is this a datatype type */ +bool TypeNode::isDatatype() const { + return getKind() == kind::DATATYPE_TYPE; +} + +/** Is this a constructor type */ +bool TypeNode::isConstructor() const { + return getKind() == kind::CONSTRUCTOR_TYPE; +} + +/** Is this a selector type */ +bool TypeNode::isSelector() const { + return getKind() == kind::SELECTOR_TYPE; +} + +/** Is this a tester type */ +bool TypeNode::isTester() const { + return getKind() == kind::TESTER_TYPE; +} + /** Is this a bit-vector type of size <code>size</code> */ bool TypeNode::isBitVector(unsigned size) const { return getKind() == kind::BITVECTOR_TYPE && diff --git a/src/expr/type_node.h b/src/expr/type_node.h index ead85cd19..049173867 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -360,18 +360,32 @@ public: /** Get the element type (for array types) */ TypeNode getArrayConstituentType() const; - /** Is this a function type? */ + /** Get the return type (for constructor types) */ + TypeNode getConstructorReturnType() const; + + /** + * Is this a function type? Function-like things (e.g. datatype + * selectors) that aren't actually functions are NOT considered + * functions, here. + */ bool isFunction() const; - /** Get the argument types */ + /** + * Get the argument types of a function, datatype constructor, + * datatype selector, or datatype tester. + */ std::vector<TypeNode> getArgTypes() const; - /** Get the range type (i.e., the type of the result). */ + /** + * Get the range type (i.e., the type of the result) of a function, + * datatype constructor, datatype selector, or datatype tester. + */ TypeNode getRangeType() const; /** * Is this a predicate type? - * NOTE: all predicate types are also function types. + * NOTE: all predicate types are also function types (so datatype + * testers are not considered "predicates" for the purpose of this function). */ bool isPredicate() const; @@ -387,6 +401,18 @@ public: /** Is this a bit-vector type of size <code>size</code> */ bool isBitVector(unsigned size) const; + /** Is this a datatype type */ + bool isDatatype() const; + + /** Is this a constructor type */ + bool isConstructor() const; + + /** Is this a selector type */ + bool isSelector() const; + + /** Is this a tester type */ + bool isTester() const; + /** Get the size of this bit-vector type */ unsigned getBitVectorSize() const; @@ -430,11 +456,11 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { } // for hash_maps, hash_sets.. -struct TypeNodeHashStrategy { - static inline size_t hash(const TypeNode& node) { +struct TypeNodeHashFunction { + size_t operator()(TypeNode node) const { return (size_t) node.getId(); } -};/* struct TypeNodeHashStrategy */ +};/* struct TypeNodeHashFunction */ }/* CVC4 namespace */ |