diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 15 | ||||
-rw-r--r-- | src/util/datatype.h | 3 |
2 files changed, 12 insertions, 6 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 4d45d9148..f0ddc2cf6 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -124,6 +124,14 @@ void Datatype::resolve(ExprManager* em, Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } d_self = self; + + d_involvesExt = false; + for(const_iterator i = begin(); i != end(); ++i) { + if( (*i).involvesExternalType() ){ + d_involvesExt = true; + break; + } + } } void Datatype::addConstructor(const DatatypeConstructor& c) { @@ -404,12 +412,7 @@ Expr Datatype::getConstructor(std::string name) const { } bool Datatype::involvesExternalType() const{ - for(const_iterator i = begin(); i != end(); ++i) { - if( (*i).involvesExternalType() ){ - return true; - } - } - return false; + return d_involvesExt; } void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, diff --git a/src/util/datatype.h b/src/util/datatype.h index a8f3b404a..befb3428d 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -452,6 +452,7 @@ private: std::vector<DatatypeConstructor> d_constructors; bool d_resolved; Type d_self; + bool d_involvesExt; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache @@ -673,6 +674,7 @@ inline Datatype::Datatype(std::string name, bool isCo) : d_constructors(), d_resolved(false), d_self(), + d_involvesExt(false), d_card(CardinalityUnknown()) { } @@ -683,6 +685,7 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo d_constructors(), d_resolved(false), d_self(), + d_involvesExt(false), d_card(CardinalityUnknown()) { } |