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

23 files changed, 236 insertions, 194 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 */
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 51ae0fd11..ba7902d32 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -137,13 +137,17 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
   TypeNode in_t = in.getType();
   if( processing.find( in_t )==processing.end() ){
     processing[in_t] = true;
-    if(in.getType().isDatatype()) {
-      if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
-        processing.erase( in_t );
-        return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in);
+    if(in.getType().isParametricDatatype() &&
+      in.getType().isInstantiatedDatatype()) {
+      // We have something here like (Pair Bool Bool)---need to dig inside
+      // and make it (Pair BV1 BV1)
+      Assert(as.isParametricDatatype() && as.isInstantiatedDatatype());
+      const Datatype* dt2 = &as[0].getDatatype();
+      std::vector<TypeNode> fromParams, toParams;
+      for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
+        fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
+        toParams.push_back(as[i + 1]);
       }
-      Assert(as.isDatatype());
-      const Datatype* dt2 = &as.getDatatype();
       const Datatype* dt1;
       if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
         dt1 = d_datatypeCache[dt2];
@@ -151,14 +155,16 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
         dt1 = d_datatypeReverseCache[dt2];
       }
       Assert(dt1 != NULL, "expected datatype in cache");
-      Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
+      Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
       Node out;
       for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
         DatatypeConstructor ctor = (*dt1)[i];
         NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
         appctorb << (*dt2)[i].getConstructor();
         for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
-          appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing);
+          TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
+          asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
+          appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType, processing);
         }
         Node appctor = appctorb;
         if(i == 0) {
@@ -171,35 +177,13 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
       processing.erase( in_t );
       return out;
     }
-    if(in.getType().isArray()) {
-      // convert in to in'
-      // e.g. in : (Array Int Bool)
-      // for in' : (Array Int (_ BitVec 1))
-      // then subs  in  |=>  \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
-      Assert(as.isArray());
-      Assert(as.getArrayIndexType() == in.getType().getArrayIndexType());
-      Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType());
-      Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType());
-      Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x);
-      Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x);
-      Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing);
-      Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
-      Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
-      Assert(out.getType() == as);
-      processing.erase( in_t );
-      return out;
-    }
-    if(in.getType().isParametricDatatype() &&
-      in.getType().isInstantiatedDatatype()) {
-      // We have something here like (Pair Bool Bool)---need to dig inside
-      // and make it (Pair BV1 BV1)
-      Assert(as.isParametricDatatype() && as.isInstantiatedDatatype());
-      const Datatype* dt2 = &as[0].getDatatype();
-      std::vector<TypeNode> fromParams, toParams;
-      for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
-        fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
-        toParams.push_back(as[i + 1]);
+    if(in.getType().isDatatype()) {
+      if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
+        processing.erase( in_t );
+        return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in);
       }
+      Assert(as.isDatatype());
+      const Datatype* dt2 = &as.getDatatype();
       const Datatype* dt1;
       if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
         dt1 = d_datatypeCache[dt2];
@@ -207,16 +191,14 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
         dt1 = d_datatypeReverseCache[dt2];
       }
       Assert(dt1 != NULL, "expected datatype in cache");
-      Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
+      Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
       Node out;
       for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
         DatatypeConstructor ctor = (*dt1)[i];
         NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
         appctorb << (*dt2)[i].getConstructor();
         for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
-          TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
-          asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
-          appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType, processing);
+          appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing);
         }
         Node appctor = appctorb;
         if(i == 0) {
@@ -229,6 +211,24 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
       processing.erase( in_t );
       return out;
     }
+    if(in.getType().isArray()) {
+      // convert in to in'
+      // e.g. in : (Array Int Bool)
+      // for in' : (Array Int (_ BitVec 1))
+      // then subs  in  |=>  \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
+      Assert(as.isArray());
+      Assert(as.getArrayIndexType() == in.getType().getArrayIndexType());
+      Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType());
+      Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType());
+      Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x);
+      Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x);
+      Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing);
+      Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
+      Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
+      Assert(out.getType() == as);
+      processing.erase( in_t );
+      return out;
+    }
     Unhandled(in);
   }else{
     Message() << "Type " << in_t << " involving Boolean sort is not supported." << std::endl;
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index dd2803d30..e58289568 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -134,7 +134,7 @@ public:
         //if( !tn.isSort() ){
         //  useTe = false;
         //}
-        if( isTypeDatatype( tn ) ){
+        if( tn.isDatatype() ){
           const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
           useTe = !dta.isCodatatype();
         }
@@ -376,15 +376,6 @@ public:
     }
     return true;
   }
-
-  /** is this term a datatype */
-  static bool isTermDatatype( TNode n ){
-    TypeNode tn = n.getType();
-    return tn.isDatatype() || tn.isParametricDatatype();
-  }
-  static bool isTypeDatatype( TypeNode tn ){
-    return tn.isDatatype() || tn.isParametricDatatype();
-  }
 private:
   static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending,
                           std::vector< Node >& terms, std::map< Node, bool >& cdts ){
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 0ecc6e547..fe07e44da 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -57,7 +57,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
         if( sIndex==1 && pdt[csIndex].getNumArgs()==2 ){
           arg1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] );
           tn1 = arg1.getType();
-          if( !DatatypesRewriter::isTypeDatatype( tn1 ) ){
+          if( !tn1.isDatatype() ){
             arg1 = Node::null();
           }
         }
@@ -193,7 +193,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
 
 void SygusSplit::registerSygusType( TypeNode tn ) {
   if( d_register.find( tn )==d_register.end() ){
-    if( !DatatypesRewriter::isTypeDatatype( tn ) ){
+    if( !tn.isDatatype() ){
       d_register[tn] = TypeNode::null();
     }else{
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
@@ -319,7 +319,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
       if( parentKind!=UNDEFINED_KIND && pdt[csIndex].getNumArgs()==2 ){
         int osIndex = sIndex==0 ? 1 : 0;
         TypeNode tnno = d_tds->getArgType( pdt[csIndex], osIndex );
-        if( DatatypesRewriter::isTypeDatatype( tnno ) ){
+        if( tnno.isDatatype() ){
           const Datatype& dto = ((DatatypeType)(tnno).toType()).getDatatype();
           registerSygusTypeConstructorArg( tnno, dto, tnnp, pdt, csIndex, osIndex );
           //compute relationships when doing 0-arg
@@ -700,7 +700,7 @@ int SygusSplit::getFirstArgOccurrence( const DatatypeConstructor& c, const Datat
 
 bool SygusSplit::isArgDatatype( const DatatypeConstructor& c, int i, const Datatype& dt ) {
   TypeNode tni = d_tds->getArgType( c, i );
-  if( datatypes::DatatypesRewriter::isTypeDatatype( tni ) ){
+  if( tni.isDatatype() ){
     const Datatype& adt = ((DatatypeType)(tni).toType()).getDatatype();
     if( adt==dt ){
       return true;
@@ -784,7 +784,7 @@ void SygusSymBreak::addTester( int tindex, Node n, Node exp ) {
     if( it==d_prog_search.end() ){
       //check if sygus type
       TypeNode tn = a.getType();
-      Assert( DatatypesRewriter::isTypeDatatype( tn ) );
+      Assert( tn.isDatatype() );
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       if( dt.isSygus() ){
         ps = new ProgSearch( this, a, d_context );
@@ -837,7 +837,7 @@ void SygusSymBreak::ProgSearch::addTester( int tindex, Node n, Node exp ) {
 bool SygusSymBreak::ProgSearch::assignTester( int tindex, Node n, int depth ) {
   Trace("sygus-sym-break-debug") << "SymBreak : Assign tester : " << tindex << " " << n << ", depth = " << depth << " of " << d_anchor << std::endl;
   TypeNode tn = n.getType();
-  Assert( DatatypesRewriter::isTypeDatatype( tn ) );
+  Assert( tn.isDatatype() );
   const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
   std::vector< Node > tst_waiting;
   for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
@@ -941,7 +941,7 @@ Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog
     int tindex = DatatypesRewriter::isTester( tst );//Datatype::indexOf( tst.getOperator().toExpr() );
     Assert( tindex!=-1 );
     TypeNode tn = prog.getType();
-    Assert( DatatypesRewriter::isTypeDatatype( tn ) );
+    Assert( tn.isDatatype() );
     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
     std::map< int, Node > pre;
     if( curr_depth<depth ){
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 42399d61f..efee5e876 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -44,7 +44,7 @@ constant DATATYPE_TYPE \
     "expr/datatype.h" \
     "a datatype type index"
 cardinality DATATYPE_TYPE \
-    "%TYPE%.getDatatype().getCardinality()" \
+    "%TYPE%.getDatatype().getCardinality(%TYPE%.toType())" \
     "expr/datatype.h"
 well-founded DATATYPE_TYPE \
     "%TYPE%.getDatatype().isWellFounded()" \
@@ -57,7 +57,7 @@ enumerator DATATYPE_TYPE \
 
 operator PARAMETRIC_DATATYPE 1: "parametric datatype"
 cardinality PARAMETRIC_DATATYPE \
-    "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \
+    "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality(%TYPE%.toType())" \
     "expr/datatype.h"
 well-founded PARAMETRIC_DATATYPE \
     "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 59b9f1d96..3d114f9f1 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -185,16 +185,17 @@ void TheoryDatatypes::check(Effort e) {
       while( !eqcs_i.isFinished() ){
         Node n = (*eqcs_i);
         TypeNode tn = n.getType();
-        if( DatatypesRewriter::isTypeDatatype( tn ) ){
+        if( tn.isDatatype() ){
           Trace("datatypes-debug") << "Process equivalence class " << n << std::endl;
           EqcInfo* eqc = getOrMakeEqcInfo( n );
           //if there are more than 1 possible constructors for eqc
           if( !hasLabel( eqc, n ) ){
             Trace("datatypes-debug") << "No constructor..." << std::endl;
-            const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-            Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isInterpretedFinite() << " " << dt.isRecursiveSingleton() << std::endl;
+            Type tt = tn.toType();
+            const Datatype& dt = ((DatatypeType)tt).getDatatype();
+            Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite( tt ) << " " << dt.isInterpretedFinite( tt ) << " " << dt.isRecursiveSingleton( tt ) << std::endl;
             bool continueProc = true;
-            if( dt.isRecursiveSingleton() ){
+            if( dt.isRecursiveSingleton( tt ) ){
               Trace("datatypes-debug") << "Check recursive singleton..." << std::endl;
               //handle recursive singleton case
               std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn );
@@ -209,8 +210,8 @@ void TheoryDatatypes::check(Effort e) {
                   //  do not infer the equality if at least one sort was processed.
                   //otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one,
                   //  infer the equality.
-                  for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes(); i++ ){
-                    TypeNode tn = TypeNode::fromType( dt.getRecursiveSingletonArgType( i ) );
+                  for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes( tt ); i++ ){
+                    TypeNode tn = TypeNode::fromType( dt.getRecursiveSingletonArgType( tt, i ) );
                     if( getQuantifiersEngine() ){
                       // under the assumption that the cardinality of this type is one
                       Node a = getSingletonLemma( tn, true );
@@ -253,7 +254,7 @@ void TheoryDatatypes::check(Effort e) {
                   if( consIndex==-1 ){
                     consIndex = j;
                   }
-                  if( !dt[ j ].isInterpretedFinite() ) {
+                  if( !dt[ j ].isInterpretedFinite( tt ) ) {
                     if( !eqc || !eqc->d_selectors ){
                       needSplit = false;
                     }
@@ -773,7 +774,7 @@ void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){
 
 /** called when two equivalance classes have merged */
 void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){
-  if( DatatypesRewriter::isTermDatatype( t1 ) ){
+  if( t1.getType().isDatatype() ){
     Trace("datatypes-debug") << "NotifyPostMerge : " << t1 << " " << t2 << std::endl;
     d_pending_merge.push_back( t1.eqNode( t2 ) );
   }
@@ -1441,7 +1442,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
   while( !eqccs_i.isFinished() ){
     Node eqc = (*eqccs_i);
     //for all equivalence classes that are datatypes
-    if( DatatypesRewriter::isTermDatatype( eqc ) ){
+    if( eqc.getType().isDatatype() ){
       EqcInfo* ei = getOrMakeEqcInfo( eqc );
       if( ei && !ei->d_constructor.get().isNull() ){
         Node c = ei->d_constructor.get();
@@ -1467,7 +1468,8 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
     Node eqc = nodes[index];
     Node neqc;
     bool addCons = false;
-    const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
+    Type tt = eqc.getType().toType();
+    const Datatype& dt = ((DatatypeType)tt).getDatatype();
     if( !d_equalityEngine.hasTerm( eqc ) ){
       Assert( false );
       /*
@@ -1533,12 +1535,12 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
         if( neqc.isNull() ){
           for( unsigned i=0; i<pcons.size(); i++ ){
             //must try the infinite ones first
-            bool cfinite = dt[ i ].isInterpretedFinite();
+            bool cfinite = dt[ i ].isInterpretedFinite( tt );
             if( pcons[i] && (r==1)==cfinite ){
               neqc = DatatypesRewriter::getInstCons( eqc, dt, i );
               //for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
-              //  //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
-              //  if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
+              //  //if( sels[i].find( j )==sels[i].end() && neqc[j].getType().isDatatype() ){
+              //  if( !d_equalityEngine.hasTerm( neqc[j] ) && neqc[j].getType().isDatatype() ){
               //    nodes.push_back( neqc[j] );
               //  }
               //}
@@ -1586,7 +1588,7 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c
   if( itv!=vmap.end() ){
     int debruijn = depth - 1 - itv->second;
     return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn));
-  }else if( DatatypesRewriter::isTermDatatype( n ) ){
+  }else if( n.getType().isDatatype() ){
     Node nc = eqc_cons[n];
     if( !nc.isNull() ){
       vmap[n] = depth;
@@ -1789,7 +1791,7 @@ void TheoryDatatypes::checkCycles() {
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
     TypeNode tn = eqc.getType();
-    if( DatatypesRewriter::isTypeDatatype( tn ) ) {
+    if( tn.isDatatype() ) {
       if( !tn.isCodatatype() ){
         if( options::dtCyclic() ){
           //do cycle checks
@@ -1895,7 +1897,7 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector<
       if( !mkExp ){ Trace("dt-cdt-debug") << "  - " << part[j] << " is looping at index " << it_rec->second << std::endl; }
       new_part_rec[ it_rec->second ].push_back( part[j] );
     }else{
-      if( DatatypesRewriter::isTermDatatype( c ) ){
+      if( c.getType().isDatatype() ){
         Node ncons = getEqcConstructor( c );
         if( ncons.getKind()==APPLY_CONSTRUCTOR ) {
           Node cc = ncons.getOperator();
@@ -2021,7 +2023,7 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
     return Node::null();
   }else{
     TypeNode tn = nn.getType();
-    if( DatatypesRewriter::isTypeDatatype( tn ) ) {
+    if( tn.isDatatype() ) {
       if( !tn.isCodatatype() ){
         return nn;
       }
@@ -2045,7 +2047,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
     addLemma = true;    
   }else if( n.getKind()==EQUAL ){
     TypeNode tn = n[0].getType();
-    if( !DatatypesRewriter::isTypeDatatype( tn ) ){
+    if( !tn.isDatatype() ){
       addLemma = true;
     }else{
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
@@ -2109,7 +2111,7 @@ void TheoryDatatypes::printModelDebug( const char* c ){
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
     if( !eqc.getType().isBoolean() ){
-      if( DatatypesRewriter::isTermDatatype( eqc ) ){
+      if( eqc.getType().isDatatype() ){
         Trace( c ) << "DATATYPE : ";
       }
       Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
@@ -2123,7 +2125,7 @@ void TheoryDatatypes::printModelDebug( const char* c ){
         ++eqc_i;
       }
       Trace( c ) << "}" << std::endl;
-      if( DatatypesRewriter::isTermDatatype( eqc ) ){
+      if( eqc.getType().isDatatype() ){
         EqcInfo* ei = getOrMakeEqcInfo( eqc );
         if( ei ){
           Trace( c ) << "   Instantiated : " << ei->d_inst.get() << std::endl;
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index c0539743f..60d319da3 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -170,9 +170,9 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
    Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
    Debug("dt-enum") << "datatype is " << d_type << std::endl;
-   Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton();
-   Debug("dt-enum") << " " << d_datatype.isFinite() << std::endl;
-   Debug("dt-enum") << " " << d_datatype.isInterpretedFinite() << std::endl;
+   Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton( d_type.toType() );
+   Debug("dt-enum") << " " << d_datatype.isFinite( d_type.toType() ) << std::endl;
+   Debug("dt-enum") << " " << d_datatype.isInterpretedFinite( d_type.toType() ) << std::endl;
 
    if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
      //start with uninterpreted constant
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 8473b5d69..83c938299 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -61,7 +61,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   bool d_child_enum;
 
   bool hasCyclesDt( const Datatype& dt ) {
-    return dt.isRecursiveSingleton() || !dt.isFinite();
+    return dt.isRecursiveSingleton( d_type.toType() ) || !dt.isFinite( d_type.toType() );
   }
   bool hasCycles( TypeNode tn ){
     if( tn.isDatatype() ){
@@ -159,7 +159,7 @@ public:
       }
       if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){
         //try next size limit as long as new terms were generated at last size, or other cases
-        if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite() ){
+        if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite( d_type.toType() ) ){
           d_size_limit++;
           d_ctor = d_zeroCtor;
           for( unsigned i=0; i<d_sel_sum.size(); i++ ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index ecf4bb74d..f4b63f929 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -17,7 +17,6 @@
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
@@ -277,7 +276,7 @@ void CegInstantiation::preRegisterQuantifier( Node q ) {
       Node pat = q[2][0][0];
       if( pat.getKind()==APPLY_UF ){
         TypeNode tn = pat[0].getType();
-        if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+        if( tn.isDatatype() ){
           const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
           if( dt.isSygus() ){
             //do unfolding if it induces Boolean structure, 
@@ -696,7 +695,7 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited )
     if( n.getKind()==APPLY_UF ){
       TypeNode tn = n[0].getType();
       Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
-      if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+      if( tn.isDatatype() ){
         const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
         if( dt.isSygus() ){ 
           Trace("cegqi-eager") << "Unfold eager : " << n << std::endl;
@@ -769,7 +768,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       std::string f(ss.str());
       f.erase(f.begin());
       TypeNode tn = prog.getType();
-      Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) );
+      Assert( tn.isDatatype() );
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       Assert( dt.isSygus() );
       //get the solution
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index e0bbbf8ac..44ac135a7 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -16,7 +16,6 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/ce_guided_single_inv_ei.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -147,7 +146,7 @@ void CegConjectureSingleInv::initialize( Node q ) {
         d_has_ites = false;
       }
     }
-    Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+    Assert( tn.isDatatype() );
     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
     Assert( dt.isSygus() );
     if( !dt.getSygusAllowAll() ){
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 240c2ed12..5cc46d163 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -16,7 +16,6 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/ce_guided_single_inv.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -655,7 +654,7 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int
     if( Trace.isOn("csi-rcons") ){
       for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){
         TypeNode tn = it->first;
-        Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+        Assert( tn.isDatatype() );
         const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
         Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName() << " : " << std::endl;
         for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
@@ -732,7 +731,7 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in
     int id = allocate( t, stn );
     d_rcons_to_status[stn][t] = -1;
     TypeNode tn = t.getType();
-    Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) );
+    Assert( stn.isDatatype() );
     const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
     Assert( dt.isSygus() );
     Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl;
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 5f73fe6d0..c88430dbf 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -43,16 +43,16 @@ void QuantDSplit::preRegisterQuantifier( Node q ) {
     TypeNode tn = q[0][i].getType();
     if( tn.isDatatype() ){
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      if( dt.isRecursiveSingleton() ){
+      if( dt.isRecursiveSingleton( tn.toType() ) ){
         Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
       }else{
         int score = -1;
         if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
-          score = dt.isInterpretedFinite() ? 1 : 0;
+          score = dt.isInterpretedFinite( tn.toType() ) ? 1 : 0;
         }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
-          score = dt.isInterpretedFinite() ? 1 : -1;
+          score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1;
         }
-        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite() << " " << dt.isFinite() << ")" << std::endl;
+        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl;
         if( score>max_score ){
           max_index = i;
           max_score = score;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index de8875ae3..fcd8d1829 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -15,7 +15,6 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 
 #include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 2c6bfb7d3..0bdfa2d24 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -17,7 +17,6 @@
 #include "expr/datatype.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fun_def_engine.h"
@@ -1088,7 +1087,7 @@ void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, Type
       }
     }
     /* TODO: more than weak structural induction
-    else if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
+    else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
       visited.push_back( tn );
       const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
       std::vector< Node > disj;
@@ -1160,7 +1159,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes
     Node nret = ret.substitute( ind_vars[0], k );
     //note : everything is under a negation
     //the following constructs ~( R( x, k ) => ~P( x ) )
-    if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+    if( options::dtStcInduction() && tn.isDatatype() ){
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       std::vector< Node > disj;
       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
@@ -1273,7 +1272,7 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) {
       ret = false;
     }else if( tn.isSet() ){
       ret = isClosedEnumerableType( tn.getSetElementType() );
-    }else if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+    }else if( tn.isDatatype() ){
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
         for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
@@ -1978,8 +1977,9 @@ void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
 }
 
 bool TermDb::isInductionTerm( Node n ) {
-  if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTermDatatype( n ) ){
-    const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
+  TypeNode tn = n.getType();
+  if( options::dtStcInduction() && tn.isDatatype() ){
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
     return !dt.isCodatatype();
   }
   if( options::intWfInduction() && n.getType().isInteger() ){
@@ -2295,7 +2295,7 @@ TNode TermDbSygus::getVar( TypeNode tn, int i ) {
   while( i>=(int)d_fv[tn].size() ){
     std::stringstream ss;
     TypeNode vtn = tn;
-    if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ){
+    if( tn.isDatatype() ){
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       ss << "fv_" << dt.getName() << "_" << i;
       if( !dt.getSygusType().isNull() ){
@@ -2373,7 +2373,7 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect
 }
 
 bool TermDbSygus::getMatch( Node t, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc, int index_start ) {
-  Assert( datatypes::DatatypesRewriter::isTypeDatatype( st ) );
+  Assert( st.isDatatype() );
   const Datatype& dt = ((DatatypeType)(st).toType()).getDatatype();
   Assert( dt.isSygus() );
   std::map< Kind, std::vector< Node > > kgens;
@@ -2530,7 +2530,7 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) {
     Node sc;
     d_builtin_const_to_sygus[tn][c] = sc;
     Assert( c.isConst() );
-    Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) );
+    Assert( tn.isDatatype() );
     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
     Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in " << dt.getName() << std::endl;
     Assert( dt.isSygus() );
@@ -2839,7 +2839,7 @@ struct sortConstants {
 
 void TermDbSygus::registerSygusType( TypeNode tn ){
   if( d_register.find( tn )==d_register.end() ){
-    if( !datatypes::DatatypesRewriter::isTypeDatatype( tn ) ){
+    if( !tn.isDatatype() ){
       d_register[tn] = TypeNode::null();
     }else{
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
@@ -3234,7 +3234,7 @@ void TermDbSygus::registerEvalTerm( Node n ) {
     if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
       Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl;
       TypeNode tn = n[0].getType();
-      if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+      if( tn.isDatatype() ){
         const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
         if( dt.isSygus() ){
           Node f = n.getOperator();
@@ -3242,7 +3242,7 @@ void TermDbSygus::registerEvalTerm( Node n ) {
           if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
             d_evals[n[0]].push_back( n );
             TypeNode tn = n[0].getType();
-            Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+            Assert( tn.isDatatype() );
             const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
             Node var_list = Node::fromExpr( dt.getSygusVarList() );
             Assert( dt.isSygus() );
@@ -3281,7 +3281,7 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems
         unsigned start = d_node_mv_args_proc[n][vn];
         Node antec = n.eqNode( vn ).negate();
         TypeNode tn = n.getType();
-        Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+        Assert( tn.isDatatype() );
         const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
         Assert( dt.isSygus() );
         Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl;
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 71d82d5e4..8579ad55f 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -819,7 +819,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       bool isCorecursive = false;
       if( t.isDatatype() ){
         const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
-        isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() );
+        isCorecursive = dt.isCodatatype() && ( !dt.isFinite( t.toType() ) || dt.isRecursiveSingleton( t.toType() ) );
       }
 #ifdef CVC4_ASSERTIONS
       bool isUSortFiniteRestricted = false;
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index d13cc1f03..8284f6ff4 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -202,7 +202,7 @@ void UnconstrainedSimplifier::processUnconstrained()
           if( parent[0].getType().isDatatype() ){
             TypeNode tn = parent[0].getType();
             const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-            if( dt.isRecursiveSingleton() ){
+            if( dt.isRecursiveSingleton( tn.toType() ) ){
               //domain size may be 1
               break;
             }
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 8631a4f32..a8a637377 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -69,7 +69,9 @@ TESTS =	\
 	sc-cdt1.smt2  \
 	conqueue-dt-enum-iloop.smt2 \
 	coda_simp_model.smt2 \
-	Test1-tup-mp.cvc
+	Test1-tup-mp.cvc \
+	dt-param-card4-unsat.smt2 \
+	dt-param-card4-bool-sat.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2
new file mode 100644
index 000000000..ca5791ce2
--- /dev/null
+++ b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes (T S) ( (Pair (pair (first T) (second S)) ) ) )
+
+(declare-fun p1 () (Pair Bool Bool))
+(declare-fun p2 () (Pair Bool Bool))
+(declare-fun p3 () (Pair Bool Bool))
+(declare-fun p4 () (Pair Bool Bool))
+
+(assert (distinct p1 p2 p3 p4))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2 b/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2
new file mode 100644
index 000000000..9676745b4
--- /dev/null
+++ b/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes (T S) ( (Pair (pair (first T) (second S)) ) ) )
+
+(declare-datatypes () ((Color (red) (blue))))
+
+(declare-fun p1 () (Pair Color Color))
+(declare-fun p2 () (Pair Color Color))
+(declare-fun p3 () (Pair Color Color))
+(declare-fun p4 () (Pair Color Color))
+(declare-fun p5 () (Pair Color Color))
+
+(assert (distinct p1 p2 p3 p4 p5))
+(check-sat)