Bug fixes and refactoring of parametric datatypes, add some regressions.

5 files changed, 106 insertions, 80 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 537fc2b1a..bc39ced13 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -173,14 +173,14 @@ void Datatype::setRecord() {
   d_isRecord = true;
 }
 
-Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
+Cardinality Datatype::getCardinality( Type t ) const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   std::vector< Type > processing;
-  computeCardinality( processing );
+  computeCardinality( t, processing );
   return d_card;
 }
 
-Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){
+Cardinality Datatype::computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException){
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
     d_card = Cardinality::INTEGERS;
@@ -188,7 +188,7 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons
     processing.push_back( d_self );
     Cardinality c = 0;
     for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-      c += (*i).computeCardinality( processing );
+      c += (*i).computeCardinality( t, processing );
     }
     d_card = c;
     processing.pop_back();
@@ -196,64 +196,64 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons
   return d_card;
 }
 
-bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
+bool Datatype::isRecursiveSingleton( Type t ) const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  if( d_card_rec_singleton==0 ){
+  if( d_card_rec_singleton[t]==0 ){
     if( isCodatatype() ){
-      Assert( d_card_u_assume.empty() );
+      Assert( d_card_u_assume[t].empty() );
       std::vector< Type > processing;
-      if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){
-        d_card_rec_singleton = 1;
+      if( computeCardinalityRecSingleton( t, processing, d_card_u_assume[t] ) ){
+        d_card_rec_singleton[t] = 1;
       }else{
-        d_card_rec_singleton = -1;
+        d_card_rec_singleton[t] = -1;
       }
-      if( d_card_rec_singleton==1 ){
-        Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl;
-        for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
-          Trace("dt-card") << "  " << d_card_u_assume [i] << std::endl;
+      if( d_card_rec_singleton[t]==1 ){
+        Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume[t].size() << " uninterpreted sorts: " << std::endl;
+        for( unsigned i=0; i<d_card_u_assume[t].size(); i++ ){
+          Trace("dt-card") << "  " << d_card_u_assume[t][i] << std::endl;
         }
         Trace("dt-card") << std::endl;
       }
     }else{
-      d_card_rec_singleton = -1;
+      d_card_rec_singleton[t] = -1;
     }
   }
-  return d_card_rec_singleton==1;
+  return d_card_rec_singleton[t]==1;
 }
 
-unsigned Datatype::getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException) {
-  return d_card_u_assume.size();
+unsigned Datatype::getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException) {
+  return d_card_u_assume[t].size();
 }
-Type Datatype::getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException) {
-  return d_card_u_assume[i];
+Type Datatype::getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException) {
+  return d_card_u_assume[t][i];
 }
 
-bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException){
+bool Datatype::computeCardinalityRecSingleton( Type t, std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException){
   if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
     return true;
   }else{
-    if( d_card_rec_singleton==0 ){
+    if( d_card_rec_singleton[t]==0 ){
       //if not yet computed
       if( d_constructors.size()==1 ){
         bool success = false;
         processing.push_back( d_self );
         for(unsigned i = 0; i<d_constructors[0].getNumArgs(); i++ ) {
-          Type t = ((SelectorType)d_constructors[0][i].getType()).getRangeType();
+          Type tc = ((SelectorType)d_constructors[0][i].getType()).getRangeType();
           //if it is an uninterpreted sort, then we depend on it having cardinality one
-          if( t.isSort() ){
-            if( std::find( u_assume.begin(), u_assume.end(), t )==u_assume.end() ){
-              u_assume.push_back( t );
+          if( tc.isSort() ){
+            if( std::find( u_assume.begin(), u_assume.end(), tc )==u_assume.end() ){
+              u_assume.push_back( tc );
             }
           //if it is a datatype, recurse
-          }else if( t.isDatatype() ){
-            const Datatype & dt = ((DatatypeType)t).getDatatype();
-            if( !dt.computeCardinalityRecSingleton( processing, u_assume ) ){
+          }else if( tc.isDatatype() ){
+            const Datatype & dt = ((DatatypeType)tc).getDatatype();
+            if( !dt.computeCardinalityRecSingleton( t, processing, u_assume ) ){
               return false;
             }else{
               success = true;
             }
           //if it is a builtin type, it must have cardinality one
-          }else if( !t.getCardinality().isOne() ){
+          }else if( !tc.getCardinality().isOne() ){
             return false;
           }
         }
@@ -262,12 +262,12 @@ bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing,
       }else{
         return false;
       }
-    }else if( d_card_rec_singleton==-1 ){
+    }else if( d_card_rec_singleton[t]==-1 ){
       return false;
     }else{
-      for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
-        if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[i] )==u_assume.end() ){
-          u_assume.push_back( d_card_u_assume[i] );
+      for( unsigned i=0; i<d_card_u_assume[t].size(); i++ ){
+        if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[t][i] )==u_assume.end() ){
+          u_assume.push_back( d_card_u_assume[t][i] );
         }
       }
       return true;
@@ -275,7 +275,7 @@ bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing,
   }
 }
 
-bool Datatype::isFinite() const throw(IllegalArgumentException) {
+bool Datatype::isFinite( Type t ) const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -286,7 +286,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) {
     return self.getAttribute(DatatypeFiniteAttr());
   }
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if(! (*i).isFinite()) {
+    if(! (*i).isFinite( t )) {
       self.setAttribute(DatatypeFiniteComputedAttr(), true);
       self.setAttribute(DatatypeFiniteAttr(), false);
       return false;
@@ -297,7 +297,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) {
   return true;
 }
 
-bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) {
+bool Datatype::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_self);
@@ -310,7 +310,7 @@ bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) {
   self.setAttribute(DatatypeUFiniteComputedAttr(), true);
   self.setAttribute(DatatypeUFiniteAttr(), false);
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if(! (*i).isInterpretedFinite()) {
+    if(! (*i).isInterpretedFinite( t )) {
       return false;
     }
   }
@@ -787,7 +787,7 @@ bool DatatypeConstructor::isSygusIdFunc() const {
   return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
 }
 
-Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
+Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   Cardinality c = 1;
@@ -800,15 +800,24 @@ Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentExc
 }
 
 /** compute the cardinality of this datatype */
-Cardinality DatatypeConstructor::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){
+Cardinality DatatypeConstructor::computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException){
   Cardinality c = 1;
+  std::vector< Type > instTypes;
+  std::vector< Type > paramTypes;
+  if( DatatypeType(t).isParametric() ){
+    paramTypes = DatatypeType(t).getDatatype().getParameters();
+    instTypes = DatatypeType(t).getParamTypes();
+  }  
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type t = SelectorType((*i).getSelector().getType()).getRangeType();
-    if( t.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)t).getDatatype();
-      c *= dt.computeCardinality( processing );
+    Type tc = SelectorType((*i).getSelector().getType()).getRangeType();
+    if( DatatypeType(t).isParametric() ){
+      tc = tc.substitute( paramTypes, instTypes );
+    }
+    if( tc.isDatatype() ){
+      const Datatype& dt = ((DatatypeType)tc).getDatatype();
+      c *= dt.computeCardinality( t, processing );
     }else{
-      c *= t.getCardinality();
+      c *= tc.getCardinality();
     }
   }
   return c;
@@ -828,7 +837,7 @@ bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing )
 }
 
 
-bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
+bool DatatypeConstructor::isFinite( Type t ) const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -838,8 +847,18 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
   if(self.getAttribute(DatatypeFiniteComputedAttr())) {
     return self.getAttribute(DatatypeFiniteAttr());
   }
+  std::vector< Type > instTypes;
+  std::vector< Type > paramTypes;
+  if( DatatypeType(t).isParametric() ){
+    paramTypes = DatatypeType(t).getDatatype().getParameters();
+    instTypes = DatatypeType(t).getParamTypes();
+  }  
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if(! (*i).getRangeType().getCardinality().isFinite()) {
+    Type tc = (*i).getRangeType();
+    if( DatatypeType(t).isParametric() ){
+      tc = tc.substitute( paramTypes, instTypes );
+    }
+    if(! tc.getCardinality().isFinite()) {
       self.setAttribute(DatatypeFiniteComputedAttr(), true);
       self.setAttribute(DatatypeFiniteAttr(), false);
       return false;
@@ -850,7 +869,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
   return true;
 }
 
-bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentException) {
+bool DatatypeConstructor::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
@@ -859,9 +878,19 @@ bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentExcep
   if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
     return self.getAttribute(DatatypeUFiniteAttr());
   }
+  std::vector< Type > instTypes;
+  std::vector< Type > paramTypes;
+  if( DatatypeType(t).isParametric() ){
+    paramTypes = DatatypeType(t).getDatatype().getParameters();
+    instTypes = DatatypeType(t).getParamTypes();
+  }  
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    TypeNode t = TypeNode::fromType( (*i).getRangeType() );
-    if(!t.isInterpretedFinite()) {
+    Type tc = (*i).getRangeType();
+    if( DatatypeType(t).isParametric() ){
+      tc = tc.substitute( paramTypes, instTypes );
+    }
+    TypeNode tcn = TypeNode::fromType( tc );
+    if(!tcn.isInterpretedFinite()) {
       self.setAttribute(DatatypeUFiniteComputedAttr(), true);
       self.setAttribute(DatatypeUFiniteAttr(), false);
       return false;
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index f81d2358d..49189959b 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -221,7 +221,7 @@ private:
                                 const std::vector< DatatypeType >& paramReplacements);
 
   /** compute the cardinality of this datatype */
-  Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException);
+  Cardinality computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException);
   /** compute whether this datatype is well-founded */
   bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException);
   /** compute ground term */
@@ -329,21 +329,21 @@ public:
    * Return the cardinality of this constructor (the product of the
    * cardinalities of its arguments).
    */
-  Cardinality getCardinality() const throw(IllegalArgumentException);
+  Cardinality getCardinality( Type t ) const throw(IllegalArgumentException);
 
   /**
    * Return true iff this constructor is finite (it is nullary or
    * each of its argument types are finite).  This function can
    * only be called for resolved constructors.
    */
-  bool isFinite() const throw(IllegalArgumentException);
+  bool isFinite( Type t ) const throw(IllegalArgumentException);
   /**
    * Return true iff this constructor is finite (it is nullary or
    * each of its argument types are finite) under assumption
    * uninterpreted sorts are finite.  This function can
    * only be called for resolved constructors.
    */
-  bool isInterpretedFinite() const throw(IllegalArgumentException);
+  bool isInterpretedFinite( Type t ) const throw(IllegalArgumentException);
 
   /**
    * Returns true iff this Datatype constructor has already been
@@ -497,10 +497,10 @@ private:
   mutable Cardinality d_card;
 
   // is this type a recursive singleton type
-  mutable int d_card_rec_singleton;
+  mutable std::map< Type, int > d_card_rec_singleton;
   // if d_card_rec_singleton is true,
   // infinite cardinality depends on at least one of the following uninterpreted sorts having cardinality > 1
-  mutable std::vector< Type > d_card_u_assume;
+  mutable std::map< Type, std::vector< Type > > d_card_u_assume;
   // is this well-founded
   mutable int d_well_founded;
   // ground term for this datatype
@@ -542,9 +542,9 @@ private:
   friend class ExprManager;// for access to resolve()
 
   /** compute the cardinality of this datatype */
-  Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException);
+  Cardinality computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException);
   /** compute whether this datatype is a recursive singleton */
-  bool computeCardinalityRecSingleton( std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException);
+  bool computeCardinalityRecSingleton( Type t, std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException);
   /** compute whether this datatype is well-founded */
   bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException);
   /** compute ground term */
@@ -619,7 +619,7 @@ public:
    * cardinalities of its constructors).  The Datatype must be
    * resolved.
    */
-  Cardinality getCardinality() const throw(IllegalArgumentException);
+  Cardinality getCardinality( Type t ) const throw(IllegalArgumentException);
 
   /**
    * Return  true iff this  Datatype is  finite (all  constructors are
@@ -627,7 +627,7 @@ public:
    * datatype is  not well-founded, this function  returns false.  The
    * Datatype must be resolved or an exception is thrown.
    */
-  bool isFinite() const throw(IllegalArgumentException);
+  bool isFinite( Type t ) const throw(IllegalArgumentException);
   /**
    * Return  true iff this  Datatype is  finite (all  constructors are
    * finite,  i.e., there  are finitely  many ground  terms) under the
@@ -635,7 +635,7 @@ public:
    * datatype is  not well-founded, this function  returns false.  The
    * Datatype must be resolved or an exception is thrown.
    */
-  bool isInterpretedFinite() const throw(IllegalArgumentException);
+  bool isInterpretedFinite( Type t ) const throw(IllegalArgumentException);
 
   /**
    * Return true iff this datatype is well-founded (there exist ground
@@ -646,12 +646,12 @@ public:
   /**
    * Return true iff this datatype is a recursive singleton
    */
-  bool isRecursiveSingleton() const throw(IllegalArgumentException);
+  bool isRecursiveSingleton( Type t ) const throw(IllegalArgumentException);
 
 
   /** get number of recursive singleton argument types */
-  unsigned getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException);
-  Type getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException);
+  unsigned getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException);
+  Type getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException);
 
   /**
    * Construct and return a ground term of this Datatype.  The
@@ -836,7 +836,6 @@ inline Datatype::Datatype(std::string name, bool isCo) :
   d_involvesExt(false),
   d_involvesUt(false),
   d_card(CardinalityUnknown()),
-  d_card_rec_singleton(0),
   d_well_founded(0) {
 }
 
@@ -853,7 +852,6 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo
   d_involvesExt(false),
   d_involvesUt(false),
   d_card(CardinalityUnknown()),
-  d_card_rec_singleton(0),
   d_well_founded(0) {
 }
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 11a45db79..5f62317ee 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -250,7 +250,7 @@ bool Type::isFloatingPoint() const {
 /** Is this a datatype type? */
 bool Type::isDatatype() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype();
+  return d_typeNode->isDatatype();
 }
 
 /** Is this the Constructor type? */
@@ -564,13 +564,7 @@ std::vector<Type> ConstructorType::getArgTypes() const {
 
 const Datatype& DatatypeType::getDatatype() const {
   NodeManagerScope nms(d_nodeManager);
-  if( d_typeNode->isParametricDatatype() ) {
-    PrettyCheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
-    const Datatype& dt = (*d_typeNode)[0].getDatatype();
-    return dt;
-  } else {
-    return d_typeNode->getDatatype();
-  }
+  return d_typeNode->getDatatype();
 }
 
 bool DatatypeType::isParametric() const {
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index ede710dad..f11aa019e 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -72,9 +72,10 @@ bool TypeNode::isInterpretedFinite() const {
     if( options::finiteModelFind() ){
       if( isSort() ){
         return true;
-      }else if( isDatatype() || isParametricDatatype() ){
+      }else if( isDatatype() ){
+        TypeNode tn = *this;
         const Datatype& dt = getDatatype();
-        return dt.isInterpretedFinite();
+        return dt.isInterpretedFinite( tn.toType() );
       }else if( isArray() ){
         return getArrayIndexType().isInterpretedFinite() && getArrayConstituentType().isInterpretedFinite();
       }else if( isSet() ) {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 9fffbdeb2..0abbc9a1b 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -969,7 +969,7 @@ inline bool TypeNode::isBitVector() const {
 
 /** Is this a datatype type */
 inline bool TypeNode::isDatatype() const {
-  return getKind() == kind::DATATYPE_TYPE ||
+  return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE ||
     ( isPredicateSubtype() && getSubtypeParentType().isDatatype() );
 }
 
@@ -1023,9 +1023,13 @@ inline bool TypeNode::isBitVector(unsigned size) const {
 /** Get the datatype specification from a datatype type */
 inline const Datatype& TypeNode::getDatatype() const {
   Assert(isDatatype());
-  //return getConst<Datatype>();
-  DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
-  return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() );
+  if( getKind() == kind::DATATYPE_TYPE ){
+    DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
+    return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() );
+  }else{
+    Assert( getKind() == kind::PARAMETRIC_DATATYPE );
+    return (*this)[0].getDatatype();
+  }
 }
 
 /** Get the exponent size of this floating-point type */