Handle recursive singleton case for codatatypes, add regression. Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.

12 files changed, 457 insertions, 226 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index aa91a5a1e..10a729420 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -362,7 +362,15 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
     // complained of a bad substitution if anything is left unresolved.
     // Clear out the set.
     d_unresolved.clear();
-
+    
+    //throw exception if any datatype is not well-founded
+    for(unsigned i = 0; i < datatypes.size(); ++i) {
+      const Datatype& dt = types[i].getDatatype();
+      if( !dt.isCodatatype() && !dt.isWellFounded() ){
+        throw ParserException(dt.getName() + " is not well-founded");
+      }
+    }
+    
     return types;
   } catch(IllegalArgumentException& ie) {
     throw ParserException(ie.getMessage());
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 29a95b38f..ec9318e99 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -146,14 +146,14 @@ public:
           gt = *te;
         }else{
           //check whether well-founded
-          bool isWellFounded = true;
-          if( isTypeDatatype( tn ) ){
-            const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
-            isWellFounded = dta.isWellFounded();
-          }
-          if( isWellFounded || in[0].isConst() ){
-            gt = tn.mkGroundTerm();
-          }
+          //bool isWf = true;
+          //if( isTypeDatatype( tn ) ){
+          //  const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
+          //  isWf = dta.isWellFounded();
+          //}
+          //if( isWf || in[0].isConst() ){
+          gt = tn.mkGroundTerm();
+          //}
         }
         if( !gt.isNull() ){
           //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 24bd69854..299ae5678 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -56,7 +56,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_conflict( c, false ),
   d_collectTermsCache( c ),
   d_consTerms( c ),
-  d_selTerms( c ){
+  d_selTerms( c ),
+  d_singleton_eq( u ){
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
@@ -175,6 +176,7 @@ void TheoryDatatypes::check(Effort e) {
     Debug("datatypes-split") << "Check for splits " << e << endl;
     addedFact = false;
     do {
+      std::map< TypeNode, Node > rec_singletons;
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
       while( !eqcs_i.isFinished() ){
         Node n = (*eqcs_i);
@@ -186,89 +188,128 @@ void TheoryDatatypes::check(Effort e) {
           if( !hasLabel( eqc, n ) ){
             Trace("datatypes-debug") << "No constructor..." << std::endl;
             const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-
-            std::vector< bool > pcons;
-            getPossibleCons( eqc, n, pcons );
-            //std::cout << "pcons " << n << " = ";
-            //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; }
-            //std::cout << std::endl;
-            //check if we do not need to resolve the constructor type for this equivalence class.
-            // this is if there are no selectors for this equivalence class, its possible values are infinite,
-            //  and we are not producing a model, then do not split.
-            int consIndex = -1;
-            bool needSplit = true;
-            for( unsigned int j=0; j<pcons.size(); j++ ) {
-              if( pcons[j] ) {
-                if( consIndex==-1 ){
-                  consIndex = j;
-                }
-                if( !dt[ j ].isFinite() && ( !eqc || !eqc->d_selectors ) ) {
-                  needSplit = false;
+            bool continueProc = true;
+            if( dt.isRecursiveSingleton() ){
+              //handle recursive singleton case
+              std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn );
+              if( itrs!=rec_singletons.end() ){
+                Node eq = n.eqNode( itrs->second );
+                if( d_singleton_eq.find( eq )==d_singleton_eq.end() ){
+                  d_singleton_eq[eq] = true;
+                  // get assumptions
+                  bool success = true;
+                  std::vector< Node > assumptions;
+                  //if there is at least one uninterpreted sort occurring within the datatype and the logic is not quantified, add lemmas ensuring cardinality is more than one,
+                  //  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 ) );
+                    if( getQuantifiersEngine() ){
+                      // under the assumption that the cardinality of this type is one
+                      Node a = getSingletonLemma( tn, true );
+                      assumptions.push_back( a.negate() );
+                    }else{
+                      success = false;
+                      // assert that the cardinality of this type is more than one
+                      getSingletonLemma( tn, false );
+                    }
+                  }
+                  if( success ){
+                    Node eq = n.eqNode( itrs->second );
+                    assumptions.push_back( eq );
+                    Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions );
+                    Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl;
+                    d_out->lemma( lemma );
+                  }
                 }
+              }else{
+                rec_singletons[tn] = n;
               }
+              //do splitting for quantified logics (incomplete anyways)
+              continueProc = ( getQuantifiersEngine()!=NULL );
             }
-            //d_dtfCounter++;
-            if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
-              //for the sake of termination, we must choose the constructor of a ground term
-              //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
-              // TODO: this is probably not good enough, actually need fair enumeration strategy
-              if( !n.getType().isRecord() ){ //FIXME
-                Node groundTerm = n.getType().mkGroundTerm();
-                if( groundTerm.getOperator().getType().isConstructor() ){ //FIXME
-                  int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
-                  if( pcons[index] ){
-                    consIndex = index;
+            if( continueProc ){
+              //all other cases
+              std::vector< bool > pcons;
+              getPossibleCons( eqc, n, pcons );
+              //check if we do not need to resolve the constructor type for this equivalence class.
+              // this is if there are no selectors for this equivalence class, its possible values are infinite,
+              //  and we are not producing a model, then do not split.
+              int consIndex = -1;
+              bool needSplit = true;
+              for( unsigned int j=0; j<pcons.size(); j++ ) {
+                if( pcons[j] ) {
+                  if( consIndex==-1 ){
+                    consIndex = j;
+                  }
+                  if( !dt[ j ].isFinite() && ( !eqc || !eqc->d_selectors ) ) {
+                    needSplit = false;
+                  }
+                }
+              }
+              //d_dtfCounter++;
+              if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
+                //for the sake of termination, we must choose the constructor of a ground term
+                //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
+                // TODO: this is probably not good enough, actually need fair enumeration strategy
+                if( !n.getType().isRecord() ){ //FIXME
+                  Node groundTerm = n.getType().mkGroundTerm();
+                  if( groundTerm.getOperator().getType().isConstructor() ){ //FIXME
+                    int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
+                    if( pcons[index] ){
+                      consIndex = index;
+                    }
+                    needSplit = true;
                   }
-                  needSplit = true;
                 }
               }
-            }
 
-            if( needSplit && consIndex!=-1 ) {
-              //if only one constructor, then this term must be this constructor
-              if( dt.getNumConstructors()==1 ){
-                Node t = DatatypesRewriter::mkTester( n, 0, dt );
-                d_pending.push_back( t );
-                d_pending_exp[ t ] = d_true;
-                Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
-                d_infer.push_back( t );
-              }else{
-                if( options::dtBinarySplit() ){
-                  Node test = DatatypesRewriter::mkTester( n, consIndex, dt );
-                  Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
-                  test = Rewriter::rewrite( test );
-                  NodeBuilder<> nb(kind::OR);
-                  nb << test << test.notNode();
-                  Node lemma = nb;
-                  d_out->lemma( lemma );
-                  d_out->requirePhase( test, true );
+              if( needSplit && consIndex!=-1 ) {
+                //if only one constructor, then this term must be this constructor
+                if( dt.getNumConstructors()==1 ){
+                  Node t = DatatypesRewriter::mkTester( n, 0, dt );
+                  d_pending.push_back( t );
+                  d_pending_exp[ t ] = d_true;
+                  Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
+                  d_infer.push_back( t );
                 }else{
-                  Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
-                  std::vector< Node > children;
-                  if( dt.isSygus() && d_sygus_split ){
-                    std::vector< Node > lemmas;
-                    d_sygus_split->getSygusSplits( n, dt, children, lemmas );
-                    for( unsigned i=0; i<lemmas.size(); i++ ){
-                      Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
-                      d_out->lemma( lemmas[i] );
-                    }
+                  if( options::dtBinarySplit() ){
+                    Node test = DatatypesRewriter::mkTester( n, consIndex, dt );
+                    Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
+                    test = Rewriter::rewrite( test );
+                    NodeBuilder<> nb(kind::OR);
+                    nb << test << test.notNode();
+                    Node lemma = nb;
+                    d_out->lemma( lemma );
+                    d_out->requirePhase( test, true );
                   }else{
-                    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-                      Node test = DatatypesRewriter::mkTester( n, i, dt );
-                      children.push_back( test );
+                    Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
+                    std::vector< Node > children;
+                    if( dt.isSygus() && d_sygus_split ){
+                      std::vector< Node > lemmas;
+                      d_sygus_split->getSygusSplits( n, dt, children, lemmas );
+                      for( unsigned i=0; i<lemmas.size(); i++ ){
+                        Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
+                        d_out->lemma( lemmas[i] );
+                      }
+                    }else{
+                      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+                        Node test = DatatypesRewriter::mkTester( n, i, dt );
+                        children.push_back( test );
+                      }
                     }
+                    Assert( !children.empty() );
+                    Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
+                    Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
+                    d_out->lemma( lemma );
                   }
-                  Assert( !children.empty() );
-                  Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
-                  Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
-                  d_out->lemma( lemma );
+                  return;
                 }
-                return;
+              }else{
+                Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl;
               }
-            }else{
-              Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl;
             }
-
           }else{
             Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl;
           }
@@ -1415,6 +1456,30 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c
   }
 }
 
+Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
+  int index = pol ? 0 : 1;
+  std::map< TypeNode, Node >::iterator it = d_singleton_lemma[index].find( tn );
+  if( it==d_singleton_lemma[index].end() ){
+    Node a;
+    if( pol ){
+      Node v1 = NodeManager::currentNM()->mkBoundVar( tn );
+      Node v2 = NodeManager::currentNM()->mkBoundVar( tn );
+      a = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, v1, v2 ), v1.eqNode( v2 ) );
+    }else{
+      Node v1 = NodeManager::currentNM()->mkSkolem( "k1", tn );
+      Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
+      a = v1.eqNode( v2 ).negate();
+      //send out immediately as lemma
+      d_out->lemma( a );
+      Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl;
+    }
+    d_singleton_lemma[index][tn] = a;
+    return a;
+  }else{
+    return it->second;
+  } 
+}
+
 void TheoryDatatypes::collectTerms( Node n ) {
   if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){
     d_collectTermsCache[n] = true;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 6604e5548..ab40f07db 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -181,6 +181,11 @@ private:
   SygusSplit * d_sygus_split;
   SygusSymBreak * d_sygus_sym_break;
 private:
+  /** singleton lemmas (for degenerate co-datatype case) */
+  std::map< TypeNode, Node > d_singleton_lemma[2];
+  /** Cache for singleton equalities processed */
+  BoolMap d_singleton_eq;
+private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
   /** flush pending facts */
@@ -262,6 +267,8 @@ private:
                           std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp );
   /** build model */
   Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap, std::vector< Node >& fv );
+  /** get singleton lemma */
+  Node getSingletonLemma( TypeNode tn, bool pol );
   /** collect terms */
   void collectTerms( Node n );
   /** get instantiate cons */
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 616c51f54..f9c8e42fd 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -528,7 +528,7 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
                     for( unsigned k=0; k<vars[lhs].size(); k++ ){
                       int v = vars[lhs][k];
                       Trace("cegqi-si-debug") << "        variable " << v << std::endl;
-                      Assert( vars[lhs].size()==vn );
+                      Assert( (int)vars[lhs].size()==vn );
                       //check if already processed
                       bool proc = d_eq_processed[lhs][rhs].find( v )!=d_eq_processed[lhs][rhs].end();
                       if( proc==(p==1) ){
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index d37aa1b7d..244cb303d 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Clark Barrett
  ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Tim King, Liana Hadarean, Peter Collingbourne
+ ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Tim King, Liana Hadarean, Peter Collingbourne, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -197,6 +197,14 @@ void UnconstrainedSimplifier::processUnconstrained()
               break;
             }
           }
+          if( parent[0].getType().isDatatype() ){
+            TypeNode tn = parent[0].getType();
+            const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+            if( dt.isRecursiveSingleton() ){
+              //domain size may be 1
+              break;
+            }
+          }
         case kind::BITVECTOR_COMP:
         case kind::LT:
         case kind::LEQ:
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 524d9cda4..113cb954c 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -156,6 +156,10 @@ public:
   bool isFinite() const throw() {
     return d_card > 0;
   }
+  /** Returns true iff this cardinality is one */
+  bool isOne() const throw() {
+    return d_card == 1;
+  }
 
   /**
    * Returns true iff this cardinality is finite and large (i.e.,
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 06a8187f2..cd27a897b 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -151,25 +151,100 @@ void Datatype::setSygus( Type st, Expr bvl ){
 
 Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  std::vector< Type > processing;
+  computeCardinality( processing );
+  return d_card;
+}
 
-  // already computed?
-  if(!d_card.isUnknown()) {
-    return d_card;
+Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){
+  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
+    d_card = Cardinality::INTEGERS;
+  }else{
+    processing.push_back( d_self );
+    Cardinality c = 0;
+    for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+      c += (*i).computeCardinality( processing );
+    }
+    d_card = c;
+    processing.pop_back();
   }
+  return d_card;
+}
 
-  RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
-
-  if(breaker.isRecursion()) {
-    return d_card = Cardinality::INTEGERS;
+bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
+  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  if( d_card_rec_singleton==0 ){
+    Assert( d_card_u_assume.empty() );
+    std::vector< Type > processing;
+    if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){
+      d_card_rec_singleton = 1;
+    }else{
+      d_card_rec_singleton = -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;
+      }
+      Trace("dt-card") << std::endl;
+    }
   }
+  return d_card_rec_singleton==1;
+}
 
-  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();
-  }
+unsigned Datatype::getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException) {
+  return d_card_u_assume.size();
+}
+Type Datatype::getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException) {
+  return d_card_u_assume[i];
+}
 
-  return d_card = c;
+bool Datatype::computeCardinalityRecSingleton( 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 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();
+          //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 it is a datatype, recurse
+          }else if( t.isDatatype() ){
+            const Datatype & dt = ((DatatypeType)t).getDatatype();
+            if( !dt.computeCardinalityRecSingleton( processing, u_assume ) ){
+              return false;
+            }else{
+              success = true;
+            }
+          //if it is a builtin type, it must have cardinality one
+          }else if( !t.getCardinality().isOne() ){
+            return false;
+          }
+        }
+        processing.pop_back();
+        return success;
+      }else{
+        return false;
+      }
+    }else if( d_card_rec_singleton==-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] );
+        }
+      }
+      return true;
+    }
+  }
 }
 
 bool Datatype::isFinite() const throw(IllegalArgumentException) {
@@ -200,44 +275,42 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) {
 
 bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
   CheckArgument(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);
-
-  TypeNode self = TypeNode::fromType(d_self);
-
-  // is this already in the cache ?
-  if(self.getAttribute(DatatypeWellFoundedComputedAttr())) {
-    return self.getAttribute(DatatypeWellFoundedAttr());
-  }
-
-  RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
-  if(breaker.isRecursion()) {
-    // This *path* is cyclic, so may not be well-founded.  The
-    // datatype itself might still be well-founded, though (we'll find
-    // the well-foundedness along another path).
-    return false;
+  if( d_well_founded==0 ){
+    // we're using some internals, so we have to set up this library context
+    ExprManagerScope ems(d_self);
+    std::vector< Type > processing;
+    if( computeWellFounded( processing ) ){
+      d_well_founded = 1;
+    }else{
+      d_well_founded = -1;
+    }
   }
+  return d_well_founded==1;
+}
 
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if((*i).isWellFounded()) {
-      self.setAttribute(DatatypeWellFoundedComputedAttr(), true);
-      self.setAttribute(DatatypeWellFoundedAttr(), true);
-      return true;
+bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException) {
+  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
+    return d_isCo;
+  }else{
+    processing.push_back( d_self );
+    for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+      if( (*i).computeWellFounded( processing ) ){
+        processing.pop_back();
+        return true;
+      }else{
+        Trace("dt-wf") << "Constructor " << (*i).getName() << " is not well-founded." << std::endl;
+      }
     }
+    processing.pop_back();
+    Trace("dt-wf") << "Datatype " << getName() << " is not well-founded." << std::endl;
+    return false;
   }
-
-  self.setAttribute(DatatypeWellFoundedComputedAttr(), true);
-  self.setAttribute(DatatypeWellFoundedAttr(), false);
-  return false;
 }
 
 Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
   CheckArgument(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);
-  Debug("datatypes") << "dt mkGroundTerm " << t << std::endl;
 
   TypeNode self = TypeNode::fromType(d_self);
 
@@ -246,72 +319,18 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
   if(!groundTerm.isNull()) {
     Debug("datatypes") << "\nin cache: " << d_self << " => " << groundTerm << std::endl;
   } else {
-    Debug("datatypes") << "\nNOT in cache: " << d_self << std::endl;
-    // look for a nullary ctor and use that
-    for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-      // prefer the nullary constructor
-      if( groundTerm.isNull() && (*i).getNumArgs() == 0) {
-        groundTerm = d_constructors[indexOf((*i).getConstructor())].mkGroundTerm( t );
-        //groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor());
-        self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
-        Debug("datatypes-gt") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl;
-      }
-    }
-    // No ctors are nullary, but we can't just use the first ctor
-    // because that might recurse!  In fact, since this datatype is
-    // well-founded by assumption, we know that at least one constructor
-    // doesn't contain a self-reference.  We search for that one and use
-    // it to construct the ground term, as that is often a simpler
-    // ground term (e.g. in a tree datatype, something like "(leaf 0)"
-    // is simpler than "(node (leaf 0) (leaf 0))".
-    //
-    // Of course this check doesn't always work, if the self-reference
-    // is through other Datatypes (or other non-Datatype types), but it
-    // does simplify a common case.  It requires a bit of extra work,
-    // but since we cache the results of these, it only happens once,
-    // ever, per Datatype.
-    //
-    // If the datatype is not actually well-founded, something below
-    // will throw an exception.
-    for(const_iterator i = begin(), i_end = end();
-        i != i_end;
-        ++i) {
-      if( groundTerm.isNull() ){
-        DatatypeConstructor::const_iterator j = (*i).begin(), j_end = (*i).end();
-        for(; j != j_end; ++j) {
-          SelectorType stype((*j).getSelector().getType());
-          if(stype.getDomain() == stype.getRangeType()) {
-            Debug("datatypes") << "self-reference, skip " << getName() << "::" << (*i).getName() << std::endl;
-            // the constructor contains a direct self-reference
-            break;
-          }
-        }
-
-        if(j == j_end && (*i).isWellFounded()) {
-          groundTerm = (*i).mkGroundTerm( t );
-          // DatatypeConstructor::mkGroundTerm() doesn't ever return null when
-          // called from the outside.  But in recursive invocations, it
-          // can: say you have dt = a(one:dt) | b(two:INT), and you ask
-          // the "a" constructor for a ground term.  It asks "dt" for a
-          // ground term, which in turn asks the "a" constructor for a
-          // ground term!  Thus, even though "a" is a well-founded
-          // constructor, it cannot construct a ground-term by itself.  We
-          // have to skip past it, and we do that with a
-          // RecursionBreaker<> in DatatypeConstructor::mkGroundTerm().  In the
-          // case of recursion, it returns null.
-          if(!groundTerm.isNull()) {
-            // we found a ground-term-constructing constructor!
-            self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
-            Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
-          }
-        }
-      }
+    std::vector< Type > processing;
+    groundTerm = computeGroundTerm( t, processing );
+    if(!groundTerm.isNull() && !isParametric() ) {
+      // we found a ground-term-constructing constructor!
+      self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
+      Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
     }
   }
   if( groundTerm.isNull() ){
     if( !d_isCo ){
       // if we get all the way here, we aren't well-founded
-      CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!");
+      CheckArgument(false, *this, "datatype is not well-founded, cannot construct a ground term!");
     }else{
       return groundTerm;
     }
@@ -320,6 +339,31 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
   }
 }
 
+Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
+  if( std::find( processing.begin(), processing.end(), d_self )==processing.end() ){
+    processing.push_back( d_self );
+    for( unsigned r=0; r<2; r++ ){
+      for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
+        //do nullary constructors first
+        if( ((*i).getNumArgs()==0)==(r==0)){
+          Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl;
+          Expr e = (*i).computeGroundTerm( t, processing );
+          if( !e.isNull() ){
+            processing.pop_back();
+            return e;
+          }else{
+            Debug("datatypes") << "...failed." << std::endl;
+          }
+        }
+      }
+    }
+    processing.pop_back();
+  }else{
+    Debug("datatypes") << "...already processing " << t << std::endl;
+  }
+  return Expr();
+}
+
 DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
   CheckArgument(!d_self.isNull(), *this);
@@ -654,6 +698,35 @@ Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentExc
   return c;
 }
 
+/** compute the cardinality of this datatype */
+Cardinality DatatypeConstructor::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){
+  Cardinality c = 1;
+  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 );
+    }else{
+      c *= t.getCardinality();
+    }
+  }
+  return c;
+}
+
+bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException){
+  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();
+      if( !dt.computeWellFounded( processing ) ){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+
 bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
@@ -685,43 +758,8 @@ bool DatatypeConstructor::isWellFounded() const throw(IllegalArgumentException)
 
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
-
-  TNode self = Node::fromExpr(d_constructor);
-
-  // is this already in the cache ?
-  if(self.getAttribute(DatatypeWellFoundedComputedAttr())) {
-    return self.getAttribute(DatatypeWellFoundedAttr());
-  }
-
-  RecursionBreaker<const DatatypeConstructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
-  if(breaker.isRecursion()) {
-    // This *path* is cyclic, sso may not be well-founded.  The
-    // constructor itself might still be well-founded, though (we'll
-    // find the well-foundedness along another path).
-    return false;
-  }
-
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if(! SelectorType((*i).getSelector().getType()).getRangeType().isWellFounded()) {
-      /* FIXME - we can't cache a negative result here, because a
-         Datatype might tell us it's not well founded along this
-         *path*, due to recursion, when it really is well-founded.
-         This should be fixed by creating private functions to do the
-         recursion here, and leaving the (public-facing)
-         isWellFounded() call as the base of that recursion.  Then we
-         can distinguish the cases.
-      */
-      /*
-      self.setAttribute(DatatypeWellFoundedComputedAttr(), true);
-      self.setAttribute(DatatypeWellFoundedAttr(), false);
-      */
-      return false;
-    }
-  }
-
-  self.setAttribute(DatatypeWellFoundedComputedAttr(), true);
-  self.setAttribute(DatatypeWellFoundedAttr(), true);
-  return true;
+  std::vector< Type > processing;
+  return computeWellFounded( processing );
 }
 
 Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
@@ -778,6 +816,55 @@ Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(IllegalArgumentExce
   return groundTerm;
 }
 
+Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
+// we're using some internals, so we have to set up this library context
+  ExprManagerScope ems(d_constructor);
+
+  std::vector<Expr> groundTerms;
+  groundTerms.push_back(getConstructor());
+
+  // for each selector, get a ground term
+  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 selType = SelectorType((*i).getSelector().getType()).getRangeType();
+    if( DatatypeType(t).isParametric() ){
+      selType = selType.substitute( paramTypes, instTypes );
+    }
+    Expr arg;
+    if( selType.isDatatype() ){
+      const Datatype & dt = DatatypeType(selType).getDatatype();
+      arg = dt.computeGroundTerm( selType, processing );
+    }else{
+      arg = selType.mkGroundTerm();
+    }
+    if( arg.isNull() ){
+      Debug("datatypes") << "...unable to construct arg of " << (*i).getName() << std::endl;
+      return Expr();
+    }else{
+      Debug("datatypes") << "...constructed arg " << arg.getType() << std::endl;
+      groundTerms.push_back(arg);
+    }
+  }
+
+  Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
+  if( groundTerm.getType()!=t ){
+    Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
+    //type is ambiguous, must apply type ascription
+    Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
+    groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
+                       getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))),
+                       groundTerms[0]);
+    groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
+  }
+  return groundTerm;
+}
+
+
 const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
   CheckArgument(index < getNumArgs(), index, "index out of bounds");
   return d_args[index];
diff --git a/src/util/datatype.h b/src/util/datatype.h
index adb423c96..445048440 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -209,6 +209,13 @@ private:
   Type doParametricSubstitution(Type range,
                                 const std::vector< SortConstructorType >& paramTypes,
                                 const std::vector< DatatypeType >& paramReplacements);
+  
+  /** compute the cardinality of this datatype */
+  Cardinality computeCardinality( 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 */
+  Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException);
 public:
   /**
    * Create a new Datatype constructor with the given name for the
@@ -427,6 +434,7 @@ public:
  *
  */
 class CVC4_PUBLIC Datatype {
+  friend class DatatypeConstructor;
 public:
   /**
    * Get the datatype of a constructor, selector, or tester operator.
@@ -466,6 +474,16 @@ private:
   // "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;
+  
+  // is this type a recursive singleton type
+  mutable 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;
+  // is this well-founded
+  mutable int d_well_founded;
+  // ground term for this datatype
+  mutable Expr d_ground_term;
 
   /**
    * Datatypes refer to themselves, recursively, and we have a
@@ -502,6 +520,14 @@ private:
     throw(IllegalArgumentException, DatatypeResolutionException);
   friend class ExprManager;// for access to resolve()
 
+  /** compute the cardinality of this datatype */
+  Cardinality computeCardinality( 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);
+  /** compute whether this datatype is well-founded */
+  bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException);
+  /** compute ground term */
+  Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException);
 public:
 
   /** Create a new Datatype of the given name. */
@@ -570,6 +596,16 @@ public:
    */
   bool isWellFounded() const throw(IllegalArgumentException);
 
+  /** 
+   * Return true iff this datatype is a recursive singleton
+   */
+  bool isRecursiveSingleton() const throw(IllegalArgumentException);
+  
+  
+  /** get number of recursive singleton argument types */
+  unsigned getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException);
+  Type getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException);
+  
   /**
    * Construct and return a ground term of this Datatype.  The
    * Datatype must be both resolved and well-founded, or else an
@@ -698,7 +734,9 @@ inline Datatype::Datatype(std::string name, bool isCo) :
   d_resolved(false),
   d_self(),
   d_involvesExt(false),
-  d_card(CardinalityUnknown()) {
+  d_card(CardinalityUnknown()),
+  d_card_rec_singleton(0),
+  d_well_founded(0) {
 }
 
 inline Datatype::Datatype(std::string name, const std::vector<Type>& params, bool isCo) :
@@ -709,7 +747,9 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo
   d_resolved(false),
   d_self(),
   d_involvesExt(false),
-  d_card(CardinalityUnknown()) {
+  d_card(CardinalityUnknown()),
+  d_card_rec_singleton(0),
+  d_well_founded(0) {
 }
 
 inline std::string Datatype::getName() const throw() {
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 80fea45fc..88f588aa0 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -61,7 +61,8 @@ TESTS =	\
 	bug438b.cvc \
 	wrong-sel-simp.cvc \
 	tenum-bug.smt2 \
-	cdt-non-canon-stream.smt2
+	cdt-non-canon-stream.smt2 \
+	stream-singleton.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/stream-singleton.smt2 b/test/regress/regress0/datatypes/stream-singleton.smt2
new file mode 100644
index 000000000..6884059ca
--- /dev/null
+++ b/test/regress/regress0/datatypes/stream-singleton.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-codatatypes () ((Stream (S (s Stream)))))
+
+(declare-fun x () Stream)
+(declare-fun y () Stream)
+
+(assert (not (= x y)))
+
+(check-sat)
\ No newline at end of file
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index c157db8c4..61da34460 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -228,8 +228,8 @@ public:
     //tryGoodInput("a : [0..0]; b : [-5..5]; c : [-1..1]; d : [ _ .._];"); // subranges
     tryGoodInput("a : [ _..1]; b : [_.. 0]; c :[_..-1];");
     tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;");
-    tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) END;");
-    tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
+    tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil END;");
+    //tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
     tryGoodInput("DATATYPE trex = Foo | Bar END; DATATYPE tree = node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
   }