diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-20 05:37:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-20 05:37:38 +0000 |
commit | 12c1e41862e4b12c3953272416a1edc103d299ee (patch) | |
tree | 9c7d3a044c33ffc3be177e6ca692eb4149add27c /src/expr | |
parent | 08df44e6b61999a14dd24a7a134146694dcb3596 (diff) |
Tuesday end-of-day commit.
Expected performance impact outside of datatypes/CVC parser is
negligible.
* CVC language LAMBDA, functional LET, type LET, precedence fixes,
bitvectors, and arrays, with partial parsing support also for
quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
these are complicated because they have to be left unresolved
at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
(not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/declaration_scope.cpp | 12 | ||||
-rw-r--r-- | src/expr/declaration_scope.h | 11 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 128 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 41 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 22 | ||||
-rw-r--r-- | src/expr/expr_template.h | 2 | ||||
-rw-r--r-- | src/expr/kind_template.h | 24 | ||||
-rwxr-xr-x | src/expr/mkkind | 14 | ||||
-rw-r--r-- | src/expr/node.h | 3 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 14 | ||||
-rw-r--r-- | src/expr/node_manager.h | 18 | ||||
-rw-r--r-- | src/expr/type.cpp | 42 | ||||
-rw-r--r-- | src/expr/type.h | 11 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 12 | ||||
-rw-r--r-- | src/expr/type_node.h | 22 |
15 files changed, 311 insertions, 65 deletions
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 09aa3ed9f..cfcc62335 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -2,10 +2,10 @@ /*! \file declaration_scope.cpp ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: mdeters + ** 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 @@ -174,4 +174,8 @@ void DeclarationScope::pushScope() throw() { d_context->push(); } -} // namespace CVC4 +size_t DeclarationScope::getLevel() const throw() { + return d_context->getLevel(); +} + +}/* CVC4 namespace */ diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 17140c850..6d89f5f4e 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -2,10 +2,10 @@ /*! \file declaration_scope.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: 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 @@ -49,7 +49,7 @@ class CVC4_PUBLIC ScopeException : public Exception { */ class CVC4_PUBLIC DeclarationScope { /** The context manager for the scope maps. */ - context::Context *d_context; + context::Context* d_context; /** A map for expressions. */ context::CDMap<std::string, Expr, StringHashFunction> *d_exprMap; @@ -180,6 +180,9 @@ public: /** Push a scope level. */ void pushScope() throw(); + /** Get the current level of this declaration scope. */ + size_t getLevel() const throw(); + };/* class DeclarationScope */ }/* CVC4 namespace */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 870c77383..b116a4671 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -475,47 +475,137 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { } 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; + // Not worth a special implementation; this doesn't need to be fast + // code anyway.. + vector<Datatype> datatypes; + datatypes.push_back(datatype); + vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes); + Assert(result.size() == 1); + return result.front(); } -std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { +std::vector<DatatypeType> +ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { + return mkMutualDatatypeTypes(datatypes, set<SortType>()); +} + +std::vector<DatatypeType> +ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, + const std::set<SortType>& unresolvedTypes) { NodeManagerScope nms(d_nodeManager); - std::map<std::string, DatatypeType> resolutions; + std::map<std::string, DatatypeType> nameResolutions; std::vector<DatatypeType> dtts; - for(std::vector<Datatype>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); + + // First do some sanity checks, set up the final Type to be used for + // each datatype, and set up the "named resolutions" used to handle + // simple self- and mutual-recursion, for example in the definition + // "nat = succ(pred:nat) | zero", a named resolution can handle the + // pred selector. + 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(), + CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(), datatypes, - "cannot construct two datatypes at the same time with the same name `%s'", + "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)); + nameResolutions.insert(std::make_pair((*i).getName(), dtt)); dtts.push_back(dtt); } - for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end(); + + // Second, set up the type substitution map for complex type + // resolution (e.g. if "list" is the type we're defining, and it has + // a selector of type "ARRAY INT OF list", this can't be taken care + // of using the named resolutions that we set up above. A + // preliminary array type was set up, and now needs to have "list" + // substituted in it for the correct type. + // + // @TODO get rid of named resolutions altogether and handle + // everything with these resolutions? + std::vector<Type> placeholders;// to hold the "unresolved placeholders" + std::vector<Type> replacements;// to hold our final, resolved types + for(std::set<SortType>::const_iterator i = unresolvedTypes.begin(), + i_end = unresolvedTypes.end(); + i != i_end; + ++i) { + std::string name = (*i).getName(); + std::map<std::string, DatatypeType>::const_iterator resolver = + nameResolutions.find(name); + CheckArgument(resolver != nameResolutions.end(), + unresolvedTypes, + "cannot resolve type `%s'; it's not among " + "the datatypes being defined", name.c_str()); + // We will instruct the Datatype to substitute "*i" (the + // unresolved SortType used as a placeholder in complex types) + // with "(*resolver).second" (the DatatypeType we created in the + // first step, above). + placeholders.push_back(*i); + replacements.push_back((*resolver).second); + } + + // Lastly, perform the final resolutions and checks. + 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); + const_cast<Datatype&>(dt).resolve(this, nameResolutions, + placeholders, replacements); } + + // Now run some checks, including a check to make sure that no + // selector is function-valued. + checkResolvedDatatype(*i); } + return dtts; } +void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { + const Datatype& dt = dtt.getDatatype(); + + AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved"); + + // for all constructors... + for(Datatype::const_iterator i = dt.begin(), i_end = dt.end(); + i != i_end; + ++i) { + const Datatype::Constructor& c = *i; + Type testerType CVC4_UNUSED = c.getTester().getType(); + Assert(c.isResolved() && + testerType.isTester() && + TesterType(testerType).getDomain() == dtt && + TesterType(testerType).getRangeType() == booleanType(), + "malformed tester in datatype post-resolution"); + Type ctorType CVC4_UNUSED = c.getConstructor().getType(); + Assert(ctorType.isConstructor() && + ConstructorType(ctorType).getArity() == c.getNumArgs() && + ConstructorType(ctorType).getReturnType() == dtt, + "malformed constructor in datatype post-resolution"); + // for all selectors... + for(Datatype::Constructor::const_iterator j = c.begin(), j_end = c.end(); + j != j_end; + ++j) { + const Datatype::Constructor::Arg& a = *j; + Type selectorType = a.getSelector().getType(); + Assert(a.isResolved() && + selectorType.isSelector() && + SelectorType(selectorType).getDomain() == dtt, + "malformed selector in datatype post-resolution"); + // This next one's a "hard" check, performed in non-debug builds + // as well; the other ones should all be guaranteed by the + // CVC4::Datatype class, but this actually needs to be checked. + AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(), + "cannot put function-like things in datatypes"); + } + } +} + 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))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 31ce7855a..b7f376811 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -72,6 +72,11 @@ private: context::Context* getContext() const; /** + * Check some things about a newly-created DatatypeType. + */ + void checkResolvedDatatype(DatatypeType dtt) const; + + /** * SmtEngine will use all the internals, so it will grab the * NodeManager. */ @@ -319,7 +324,41 @@ public: * Make a set of types representing the given datatypes, which may be * mutually recursive. */ - std::vector<DatatypeType> mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); + std::vector<DatatypeType> + mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); + + /** + * Make a set of types representing the given datatypes, which may + * be mutually recursive. unresolvedTypes is a set of SortTypes + * that were used as placeholders in the Datatypes for the Datatypes + * of the same name. This is just a more complicated version of the + * above mkMutualDatatypeTypes() function, but is required to handle + * complex types. + * + * For example, unresolvedTypes might contain the single sort "list" + * (with that name reported from SortType::getName()). The + * datatypes list might have the single datatype + * + * DATATYPE + * list = cons(car:ARRAY INT OF list, cdr:list) | nil; + * END; + * + * To represent the Type of the array, the user had to create a + * placeholder type (an uninterpreted sort) to stand for "list" in + * the type of "car". It is this placeholder sort that should be + * passed in unresolvedTypes. If the datatype was of the simpler + * form: + * + * DATATYPE + * list = cons(car:list, cdr:list) | nil; + * END; + * + * then no complicated Type needs to be created, and the above, + * simpler form of mkMutualDatatypeTypes() is enough. + */ + std::vector<DatatypeType> + mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, + const std::set<SortType>& unresolvedTypes); /** * Make a type representing a constructor with the given parameterization. diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index f6d346630..51a734757 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -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 @@ -117,10 +117,24 @@ Expr& Expr::operator=(const Expr& e) { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); - ExprManagerScope ems(*this); - *d_node = *e.d_node; - d_exprManager = e.d_exprManager; + if(this != &e) { + if(d_exprManager == e.d_exprManager) { + ExprManagerScope ems(*this); + *d_node = *e.d_node; + } else { + // This happens more than you think---every time you set to or + // from the null Expr. It's tricky because each node manager + // must be in play at the right time. + + ExprManagerScope ems1(*this); + *d_node = Node::null(); + ExprManagerScope ems2(e); + *d_node = *e.d_node; + + d_exprManager = e.d_exprManager; + } + } return *this; } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 489564d5f..c45cc9b99 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -754,7 +754,7 @@ public: ${getConst_instantiations} -#line 682 "${template}" +#line 758 "${template}" namespace expr { diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 932ec31c8..6b9787f6c 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -2,10 +2,10 @@ /*! \file kind_template.h ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: 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 @@ -95,7 +95,7 @@ struct KindHashStrategy { * The enumeration for the built-in atomic types. */ enum TypeConstant { - ${type_constant_list} +${type_constant_list} LAST_TYPE };/* enum TypeConstant */ @@ -110,7 +110,7 @@ struct TypeConstantHashStrategy { inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { switch(typeConstant) { - ${type_constant_descriptions} +${type_constant_descriptions} default: out << "UNKNOWN_TYPE_CONSTANT"; break; @@ -121,13 +121,13 @@ inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { namespace theory { enum TheoryId { - ${theory_enum} +${theory_enum} THEORY_LAST }; inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { switch(theoryId) { - ${theory_descriptions} +${theory_descriptions} default: out << "UNKNOWN_THEORY"; break; @@ -136,18 +136,18 @@ inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { } inline TheoryId kindToTheoryId(::CVC4::Kind k) { - switch (k) { - ${kind_to_theory_id} + switch(k) { +${kind_to_theory_id} default: - Unreachable(); + Unhandled(k); } } inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) { - switch (typeConstant) { - ${type_constant_to_theory_id} + switch(typeConstant) { +${type_constant_to_theory_id} default: - Unreachable(); + Unhandled(typeConstant); } } diff --git a/src/expr/mkkind b/src/expr/mkkind index f7f6ba836..fa80894b2 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -73,9 +73,9 @@ function theory { fi theory_id="$1" - theory_enum="$1, - ${theory_enum}" - theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; + theory_enum="${theory_enum} $1, +" + theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; " } @@ -144,11 +144,11 @@ function register_sort { id=$1 comment=$2 - type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ + type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ " - type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break; + type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break; " - type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; + type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; " } @@ -161,7 +161,7 @@ function register_kind { " kind_printers="${kind_printers} case $r: out << \"$r\"; break; " - kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; + kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; " } diff --git a/src/expr/node.h b/src/expr/node.h index d3775cb3f..6fe1e7d0e 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -720,7 +720,7 @@ public: } /** - * Converst this node into a string representation and sends it to the + * Converts this node into a string representation and sends it to the * given stream * * @param out the stream to serialize this node to @@ -790,6 +790,7 @@ public: /** * Serializes a given node to the given stream. + * * @param out the output stream to use * @param n the node to output to the stream * @return the stream diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 9449594e3..716e2a3b3 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -519,18 +519,26 @@ TypeNode NodeManager::getType(TNode n, bool check) return typeNode; } -TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, TypeNode range) { +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]; + TypeNode selectorType = *(*i).getSelector().getType().d_typeNode; + Debug("datatypes") << selectorType << std::endl; + TypeNode sort = selectorType[1]; + + // should be guaranteed here already, but just in case + Assert(!sort.isFunctionLike()); + Debug("datatypes") << "ctor sort: " << sort << std::endl; sorts.push_back(sort); } Debug("datatypes") << "ctor range: " << range << std::endl; + CheckArgument(!range.isFunctionLike(), range, + "cannot create higher-order function types"); sorts.push_back(range); return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 94b7e5c40..9974df6ca 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -799,6 +799,8 @@ NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) { Assert(sorts.size() >= 2); std::vector<TypeNode> sortNodes; for (unsigned i = 0; i < sorts.size(); ++ i) { + CheckArgument(!sorts[i].isFunctionLike(), sorts, + "cannot create higher-order function types"); sortNodes.push_back(sorts[i]); } return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); @@ -809,6 +811,8 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { Assert(sorts.size() >= 1); std::vector<TypeNode> sortNodes; for (unsigned i = 0; i < sorts.size(); ++ i) { + CheckArgument(!sorts[i].isFunctionLike(), sorts, + "cannot create higher-order function types"); sortNodes.push_back(sorts[i]); } sortNodes.push_back(booleanType()); @@ -819,6 +823,10 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { Assert(types.size() >= 2); std::vector<TypeNode> typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { + /* FIXME when congruence closure no longer abuses tuples + CheckArgument(!types[i].isFunctionLike(), types, + "cannot put function-like types in tuples"); + */ typeNodes.push_back(types[i]); } return mkTypeNode(kind::TUPLE_TYPE, typeNodes); @@ -830,14 +838,24 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) { inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { + CheckArgument(!indexType.isFunctionLike(), domain, + "cannot index arrays by a function-like type"); + CheckArgument(!constituentType.isFunctionLike(), domain, + "cannot store function-like types in arrays"); return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) { + CheckArgument(!domain.isFunctionLike(), domain, + "cannot create higher-order function types"); + CheckArgument(!range.isFunctionLike(), range, + "cannot create higher-order function types"); return mkTypeNode(kind::SELECTOR_TYPE, domain, range); } inline TypeNode NodeManager::mkTesterType(TypeNode domain) { + CheckArgument(!domain.isFunctionLike(), domain, + "cannot create higher-order function types"); return mkTypeNode(kind::TESTER_TYPE, domain ); } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 6dd9c5cec..4ea425aa7 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -69,10 +69,26 @@ bool Type::isNull() const { } Type& Type::operator=(const Type& t) { - NodeManagerScope nms(t.d_nodeManager); + Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!"); + Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!"); + if(this != &t) { - *d_typeNode = *t.d_typeNode; - d_nodeManager = t.d_nodeManager; + if(d_nodeManager == t.d_nodeManager) { + NodeManagerScope nms(d_nodeManager); + *d_typeNode = *t.d_typeNode; + } else { + // This happens more than you think---every time you set to or + // from the null Type. It's tricky because each node manager + // must be in play at the right time. + + NodeManagerScope nms1(d_nodeManager); + *d_typeNode = TypeNode::null(); + + NodeManagerScope nms2(t.d_nodeManager); + *d_typeNode = *t.d_typeNode; + + d_nodeManager = t.d_nodeManager; + } } return *this; } @@ -85,6 +101,10 @@ bool Type::operator!=(const Type& t) const { return *d_typeNode != *t.d_typeNode; } +bool Type::operator<(const Type& t) const { + return *d_typeNode < *t.d_typeNode; +} + Type Type::substitute(const Type& type, const Type& replacement) const { NodeManagerScope nms(d_nodeManager); return makeType(d_typeNode->substitute(*type.d_typeNode, @@ -468,6 +488,22 @@ Type ConstructorType::getReturnType() const { return makeType(d_typeNode->getConstructorReturnType()); } +size_t ConstructorType::getArity() const { + return d_typeNode->getNumChildren() - 1; +} + +std::vector<Type> ConstructorType::getArgTypes() const { + NodeManagerScope nms(d_nodeManager); + vector<Type> args; + vector<TypeNode> argNodes = d_typeNode->getArgTypes(); + vector<TypeNode>::iterator it = argNodes.begin(); + vector<TypeNode>::iterator it_end = argNodes.end(); + for(; it != it_end; ++ it) { + args.push_back(makeType(*it)); + } + return args; +} + const Datatype& DatatypeType::getDatatype() const { return d_typeNode->getConst<Datatype>(); } diff --git a/src/expr/type.h b/src/expr/type.h index 3b476ddf5..290bb360a 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -174,6 +174,11 @@ public: bool operator!=(const Type& t) const; /** + * An ordering on Types so they can be stored in maps, etc. + */ + bool operator<(const Type& t) const; + + /** * Is this the Boolean type? * @return true if the type is a Boolean type */ @@ -533,6 +538,12 @@ public: /** Get the return type */ Type getReturnType() const; + /** Get the argument types */ + std::vector<Type> getArgTypes() const; + + /** Get the number of constructor arguments */ + size_t getArity() const; + };/* class ConstructorType */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 7549af895..0b22fdf0f 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -2,8 +2,8 @@ /*! \file type_node.cpp ** \verbatim ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): taking + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -85,6 +85,14 @@ bool TypeNode::isFunction() const { return getKind() == kind::FUNCTION_TYPE; } +bool TypeNode::isFunctionLike() const { + return + getKind() == kind::FUNCTION_TYPE || + getKind() == kind::CONSTRUCTOR_TYPE || + getKind() == kind::SELECTOR_TYPE || + getKind() == kind::TESTER_TYPE; +} + bool TypeNode::isPredicate() const { return isFunction() && getRangeType().isBoolean(); } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 049173867..c04bef0c7 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -371,6 +371,19 @@ public: bool isFunction() const; /** + * Is this a function-LIKE type? Function-like things + * (e.g. datatype selectors) that aren't actually functions ARE + * considered functions, here. The main point is that this is used + * to avoid anything higher-order: anything function-like cannot be + * the argument or return value for anything else function-like. + * + * Arrays are explicitly *not* function-like for the purposes of + * this test. However, functions still cannot contain anything + * function-like. + */ + bool isFunctionLike() const; + + /** * Get the argument types of a function, datatype constructor, * datatype selector, or datatype tester. */ @@ -383,9 +396,9 @@ public: TypeNode getRangeType() const; /** - * Is this a predicate type? - * NOTE: all predicate types are also function types (so datatype - * testers are not considered "predicates" for the purpose of this function). + * Is this a predicate type? NOTE: all predicate types are also + * function types (so datatype testers are NOT considered + * "predicates" for the purpose of this function). */ bool isPredicate() const; @@ -451,7 +464,8 @@ private: inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { n.toStream(out, Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out)); + Node::printtypes::getPrintTypes(out), + Node::setlanguage::getLanguage(out)); return out; } |