From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 14 Nov 2013 02:03:16 +0000 (-0500)
Subject: Datatype::getCardinality() caching
X-Git-Tag: cvc5-1.0.0~7253
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ebd4ce25c64b1b4ea204d942512473f2ce7519c;p=cvc5.git

Datatype::getCardinality() caching
---

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() {