Datatype::getCardinality() caching

2 files changed, 17 insertions, 9 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 1c5dd3e07..5fa893336 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -108,7 +108,6 @@ void Datatype::resolve(ExprManager* em,
     Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
   }
   d_self = self;
-  //d_card = getCardinality();
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
@@ -119,19 +118,25 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
 
 Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+
+  // already computed?
+  if(!d_card.isUnknown()) {
+    return d_card;
+  }
+
   RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
+
   if(breaker.isRecursion()) {
-    return Cardinality::INTEGERS;
+    return d_card = Cardinality::INTEGERS;
   }
+
   Cardinality c = 0;
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+    // We can't just add to d_card here, since this function is reentrant
     c += (*i).getCardinality();
   }
-  //if( d_card!=c ){
-    //std::cout << "Bad card " << std::endl;
-  //}
 
-  return c;
+  return d_card = c;
 }
 
 bool Datatype::isFinite() const throw(IllegalArgumentException) {
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 01558fd30..802704803 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -404,7 +404,10 @@ private:
   std::vector<DatatypeConstructor> d_constructors;
   bool d_resolved;
   Type d_self;
-  Cardinality d_card;
+
+  // "mutable" because computing the cardinality can be expensive,
+  // and so it's computed just once, on demand---this is the cache
+  mutable Cardinality d_card;
 
   /**
    * Datatypes refer to themselves, recursively, and we have a
@@ -618,7 +621,7 @@ inline Datatype::Datatype(std::string name) :
   d_constructors(),
   d_resolved(false),
   d_self(),
-  d_card(1) {
+  d_card(CardinalityUnknown()) {
 }
 
 inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
@@ -627,7 +630,7 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
   d_constructors(),
   d_resolved(false),
   d_self(),
-  d_card(1) {
+  d_card(CardinalityUnknown()) {
 }
 
 inline std::string Datatype::getName() const throw() {