Working towards a fair enumerator for codatatypes.

6 files changed, 321 insertions, 158 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 0cd4cff44..90a4d6f5b 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -232,6 +232,7 @@ libcvc4_la_SOURCES = \
 	theory/builtin/theory_builtin.cpp \
 	theory/datatypes/theory_datatypes_type_rules.h \
 	theory/datatypes/type_enumerator.h \
+        theory/datatypes/type_enumerator.cpp \
 	theory/datatypes/theory_datatypes.h \
 	theory/datatypes/datatypes_rewriter.h \
 	theory/datatypes/theory_datatypes.cpp \
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 6fafbca42..14d966458 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -384,7 +384,75 @@ public:
     return tn.isDatatype() || tn.isParametricDatatype() ||
            tn.isTuple() || tn.isRecord();
   }
-
+private:
+  static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending ){
+    Assert( n.isConst() );
+    TypeNode tn = n.getType();
+    if( tn.isDatatype() ){
+      if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
+        sk.push_back( n );
+        rf_pending.push_back( Node::null() );
+        std::vector< Node > children;
+        children.push_back( n.getOperator() );
+        bool childChanged = false;
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          Node nc = collectRef( n[i], sk, rf, rf_pending );
+          if( nc.isNull() ){
+            return Node::null();
+          }
+          childChanged = nc!=n[i] || childChanged;
+          children.push_back( nc );
+        }
+        sk.pop_back();
+        Node ret;
+        if( childChanged ){
+          ret = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
+          if( !rf_pending.back().isNull() ){
+            rf[rf_pending.back()] = ret;
+          }
+        }else{
+          ret = n;
+          Assert( rf_pending.back().isNull() );
+        }
+        rf_pending.pop_back();
+        return ret;
+      }else{
+        const Integer& i = n.getConst<UninterpretedConstant>().getIndex();
+        uint32_t index = i.toUnsignedInt();
+        if( index>=sk.size() ){
+          return Node::null();
+        }else{
+          Assert( sk.size()==rf_pending.size() );
+          Node r = rf_pending[ rf_pending.size()-1-index ];
+          if( r.isNull() ){
+            r = NodeManager::currentNM()->mkBoundVar( sk[ rf_pending.size()-1-index ].getType() );
+            rf_pending[ rf_pending.size()-1-index ] = r;
+          }
+          return r;
+        }
+      }
+    }else{
+      return n;
+    }
+  }
+public:
+  static Node normalizeMuConstant( Node n ){
+    Trace("dt-nconst") << "Normalize " << n << std::endl;
+    std::map< Node, Node > rf;
+    std::vector< Node > sk;
+    std::vector< Node > rf_pending;
+    Node s = collectRef( n, sk, rf, rf_pending );
+    if( !s.isNull() ){
+      Trace("dt-nconst") << "...symbolic normalized is : " << s << std::endl;
+      for( std::map< Node, Node >::iterator it = rf.begin(); it != rf.end(); ++it ){
+        Trace("dt-nconst") << "  " << it->first << " = " << it->second << std::endl;
+      }
+      return n;
+    }else{
+      Trace("dt-nconst") << "...invalid." << std::endl;
+      return Node::null();
+    }
+  }
 };/* class DatatypesRewriter */
 
 }/* CVC4::theory::datatypes namespace */
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
new file mode 100755
index 000000000..a4af183c5
--- /dev/null
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -0,0 +1,208 @@
+/*********************                                                        */
+/*! \file type_enumerator.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** 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
+ ** information.\endverbatim
+ **
+ ** \brief Enumerators for datatypes
+ **
+ ** Enumerators for datatypes.
+ **/
+
+ #include "theory/datatypes/type_enumerator.h"
+ #include "theory/datatypes/datatypes_rewriter.h"
+
+using namespace CVC4;
+using namespace theory;
+using namespace datatypes;
+
+Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
+   Node ret;
+   if( i<d_terms[tn].size() ){
+     ret = d_terms[tn][i];
+   }else{
+     Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
+     std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn );
+     unsigned tei;
+     if( it==d_te_index.end() ){
+       //initialize child enumerator for type
+       tei = d_children.size();
+       d_te_index[tn] = tei;
+       if( tn.isDatatype() && d_has_debruijn ){
+         //must indicate that this is a child enumerator (do not normalize constants for it)
+         DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true );
+         d_children.push_back( TypeEnumerator( dte ) );
+       }else{
+         d_children.push_back( TypeEnumerator( tn ) );
+       }
+       d_terms[tn].push_back( *d_children[tei] );
+     }else{
+       tei = it->second;
+     }
+     //enumerate terms until index is reached
+     while( i>=d_terms[tn].size() ){
+       ++d_children[tei];
+       if( d_children[tei].isFinished() ){
+         Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl;
+         return Node::null();
+       }
+       d_terms[tn].push_back( *d_children[tei] );
+     }
+     Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl;
+     ret = d_terms[tn][i];
+   }
+   return ret;
+ }
+
+ bool DatatypesEnumerator::increment( unsigned index ){
+   Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl;
+   if( d_sel_sum[index]==-1 ){
+     //first time
+     d_sel_sum[index] = 0;
+     //special case: no children to iterate
+     if( index>=d_has_debruijn && d_sel_types[index].empty() ){
+       Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl;
+       return d_size_limit==0;
+     }else{
+       Debug("dt-enum") << "...success" << std::endl;
+       return true;
+     }
+   }else{
+     unsigned i = 0;
+     while( i < d_sel_index[index].size() ){
+       //increment if the sum of iterations on arguments is less than the limit
+       if( d_sel_sum[index]<(int)d_size_limit ){
+         //also check if child enumerator has enough terms
+         if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){
+           Debug("dt-enum") << "...success increment child " << i << std::endl;
+           d_sel_index[index][i]++;
+           d_sel_sum[index]++;
+           return true;
+         }
+       }
+       Debug("dt-enum") << "......failed increment child " << i << std::endl;
+       //reset child, iterate next
+       d_sel_sum[index] -= d_sel_index[index][i];
+       d_sel_index[index][i] = 0;
+       i++;
+     }
+     Debug("dt-enum") << "...failure." << std::endl;
+     return false;
+   }
+ }
+
+ Node DatatypesEnumerator::getCurrentTerm( unsigned index ){
+   Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type << std::endl;
+   Node ret;
+   if( index<d_has_debruijn ){
+     ret = NodeManager::currentNM()->mkConst(UninterpretedConstant(d_type.toType(), d_size_limit));
+   }else{
+     Debug("dt-enum-debug") << "Look at constructor " << (index - d_has_debruijn) << std::endl;
+     DatatypeConstructor ctor = d_datatype[index - d_has_debruijn];
+     Debug("dt-enum-debug") << "Check last term..." << std::endl;
+     //we first check if the last argument (which is forced to make sum of iterated arguments equal to d_size_limit) is defined
+     Node lc;
+     if( ctor.getNumArgs()>0 ){
+       Assert( index<d_sel_types.size() );
+       Assert( ctor.getNumArgs()-1<d_sel_types[index].size() );
+       lc = getTermEnum( d_sel_types[index][ctor.getNumArgs()-1], d_size_limit - d_sel_sum[index] );
+       if( lc.isNull() ){
+         Debug("dt-enum-debug") << "Current infeasible." << std::endl;
+         return Node::null();
+       }
+     }
+     Debug("dt-enum-debug") << "Get constructor..." << std::endl;
+     NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
+     Type typ;
+     if( d_datatype.isParametric() ){
+       typ = ctor.getSpecializedConstructorType(d_type.toType());
+       b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                                             NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) );
+     }else{
+       b << ctor.getConstructor();
+     }
+     Debug("dt-enum-debug") << "Get arguments..." << std::endl;
+     if( ctor.getNumArgs()>0 ){
+       Assert( index<d_sel_types.size() );
+       Assert( index<d_sel_index.size() );
+       Assert( d_sel_types[index].size()==ctor.getNumArgs() );
+       Assert( d_sel_index[index].size()==ctor.getNumArgs()-1 );
+       for( int i=0; i<(int)(ctor.getNumArgs()-1); i++ ){
+         Node c = getTermEnum( d_sel_types[index][i], d_sel_index[index][i] );
+         Assert( !c.isNull() );
+         b << c;
+       }
+       b << lc;
+     }
+     Node nnn = Node(b);
+     Debug("dt-enum-debug") << "Return... " <<  nnn  << std::endl;
+     ret = nnn;
+   }
+
+   if( !d_child_enum && d_has_debruijn ){
+     Node nret = DatatypesRewriter::normalizeMuConstant( ret );
+     if( nret!=ret ){
+       Debug("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
+       return Node::null();
+     }
+   }
+
+   return ret;
+ }
+
+ void DatatypesEnumerator::init(){
+   //Assert(type.isDatatype());
+   Debug("te") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
+   Debug("te") << "datatype is kind " << d_type.getKind() << std::endl;
+   Debug("te") << "datatype is " << d_type << std::endl;
+   Debug("te") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl;
+
+   if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
+     //start with uninterpreted constant
+     d_zeroCtor = 0;
+     d_has_debruijn = 1;
+     d_sel_types.push_back( std::vector< TypeNode >() );
+     d_sel_index.push_back( std::vector< unsigned >() );
+     d_sel_sum.push_back( -1 );
+   }else{
+     // find the "zero" constructor via mkGroundTerm
+     Node t = d_type.mkGroundTerm();
+     Assert( t.getKind()==kind::APPLY_CONSTRUCTOR );
+     // start with the constructor for which a ground term is constructed
+     d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() );
+     d_has_debruijn = 0;
+   }
+   d_ctor = d_zeroCtor;
+   for( unsigned i=0; i<d_datatype.getNumConstructors(); ++i ){
+     d_sel_types.push_back( std::vector< TypeNode >() );
+     d_sel_index.push_back( std::vector< unsigned >() );
+     d_sel_sum.push_back( -1 );
+     DatatypeConstructor ctor = d_datatype[i];
+     Type typ;
+     if( d_datatype.isParametric() ){
+       typ = ctor.getSpecializedConstructorType(d_type.toType());
+     }
+     for( unsigned a = 0; a < ctor.getNumArgs(); ++a ){
+       TypeNode tn;
+       if( d_datatype.isParametric() ){
+         tn = TypeNode::fromType( typ )[a];
+       }else{
+         tn = Node::fromExpr(ctor[a].getSelector()).getType()[1];
+       }
+       d_sel_types.back().push_back( tn );
+       d_sel_index.back().push_back( 0 );
+     }
+     if( !d_sel_index.back().empty() ){
+       d_sel_index.back().pop_back();
+     }
+   }
+   d_size_limit = 0;
+   //set up initial conditions (should always succeed)
+   ++*this; //increment( d_ctor );
+   AlwaysAssert( !isFinished() );
+}
\ No newline at end of file
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index dc2a83841..0e5aad640 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -9,9 +9,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief An enumerator for bitvectors
+ ** \brief An enumerator for datatypes
  **
- ** An enumerator for bitvectors.
+ ** An enumerator for datatypes.
  **/
 
 #include "cvc4_private.h"
@@ -32,6 +32,8 @@ namespace datatypes {
 class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   /** The datatype we're enumerating */
   const Datatype& d_datatype;
+  /** extra cons */
+  unsigned d_has_debruijn;
   /** type */
   TypeNode d_type;
   /** The datatype constructor we're currently enumerating */
@@ -41,6 +43,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   /** list of type enumerators (one for each type in a selector argument) */
   std::map< TypeNode, unsigned > d_te_index;
   std::vector< TypeEnumerator > d_children;
+  //std::vector< DatatypesEnumerator > d_dt_children;
   /** terms produced for types */
   std::map< TypeNode, std::vector< Node > > d_terms;
   /** arg type of each selector, for each constructor */
@@ -51,165 +54,44 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   std::vector< int > d_sel_sum;
   /** current bound on the number of times we can iterate argument enumerators */
   unsigned d_size_limit;
+  /** child */
+  bool d_child_enum;
 
-  Node getTermEnum( TypeNode tn, unsigned i ){
-    if( i<d_terms[tn].size() ){
-      return d_terms[tn][i];
-    }else{
-      Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
-      std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn );
-      unsigned tei;
-      if( it==d_te_index.end() ){
-        //initialize child enumerator for type
-        tei = d_children.size();
-        d_te_index[tn] = tei;
-        d_children.push_back( TypeEnumerator( tn ) );
-        d_terms[tn].push_back( *d_children[tei] );
-      }else{
-        tei = it->second;
-      }
-      //enumerate terms until index is reached
-      while( i>=d_terms[tn].size() ){
-        ++d_children[tei];
-        if( d_children[tei].isFinished() ){
-          Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl;
-          return Node::null();
-        }
-        d_terms[tn].push_back( *d_children[tei] );
-      }
-      Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl;
-      return d_terms[tn][i];
-    }
+  bool hasCyclesDt( const Datatype& dt ) {
+    return dt.isRecursiveSingleton() || !dt.isFinite();
   }
-
-  bool increment( unsigned index ){
-    Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl;
-    if( d_sel_sum[index]==-1 ){
-      //first time
-      d_sel_sum[index] = 0;
-      //special case: no children to iterate
-      if( d_sel_types[index].size()==0 ){
-        Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl;
-        return d_size_limit==0;
-      }else{
-        Debug("dt-enum") << "...success" << std::endl;
-        return true;
-      }
+  bool hasCycles( TypeNode tn ){
+    if( tn.isDatatype() ){
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      return hasCyclesDt( dt );
     }else{
-      unsigned i = 0;
-      while( i < d_sel_index[index].size() ){
-        //increment if the sum of iterations on arguments is less than the limit
-        if( d_sel_sum[index]<(int)d_size_limit ){
-          //also check if child enumerator has enough terms
-          if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){
-            Debug("dt-enum") << "...success increment child " << i << std::endl;
-            d_sel_index[index][i]++;
-            d_sel_sum[index]++;
-            return true;
-          }
-        }
-        Debug("dt-enum") << "......failed increment child " << i << std::endl;
-        //reset child, iterate next
-        d_sel_sum[index] -= d_sel_index[index][i];
-        d_sel_index[index][i] = 0;
-        i++;
-      }
-      Debug("dt-enum") << "...failure." << std::endl;
       return false;
     }
   }
 
-  Node getCurrentTerm( unsigned index ){
-    Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type << "..." << std::endl;
-    DatatypeConstructor ctor = d_datatype[index];
-    Debug("dt-enum-debug") << "Check last term..." << std::endl;
-    //we first check if the last argument (which is forced to make sum of iterated arguments equal to d_size_limit) is defined
-    Node lc;
-    if( ctor.getNumArgs()>0 ){
-      lc = getTermEnum( d_sel_types[index][ctor.getNumArgs()-1], d_size_limit - d_sel_sum[index] );
-      if( lc.isNull() ){
-        Debug("dt-enum-debug") << "Current infeasible." << std::endl;
-        return Node::null();
-      }
-    }
-    Debug("dt-enum-debug") << "Get constructor..." << std::endl;
-    NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
-    Type typ;
-    if( d_datatype.isParametric() ){
-      typ = ctor.getSpecializedConstructorType(d_type.toType());
-      b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                            NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) );
-    }else{
-      b << ctor.getConstructor();
-    }
-    Debug("dt-enum-debug") << "Get arguments..." << std::endl;
-    if( ctor.getNumArgs()>0 ){
-      Assert( index<d_sel_types.size() );
-      Assert( index<d_sel_index.size() );
-      Assert( d_sel_types[index].size()==ctor.getNumArgs() );
-      Assert( d_sel_index[index].size()==ctor.getNumArgs()-1 );
-      for( int i=0; i<(int)(ctor.getNumArgs()-1); i++ ){
-        Node c = getTermEnum( d_sel_types[index][i], d_sel_index[index][i] );
-        Assert( !c.isNull() );
-        b << c;
-      }
-      b << lc;
-    }
-    Node nnn = Node(b);
-    Debug("dt-enum-debug") << "Return... " <<  nnn  << std::endl;
-    return nnn;
-  }
+  Node getTermEnum( TypeNode tn, unsigned i );
+
+  bool increment( unsigned index );
+
+  Node getCurrentTerm( unsigned index );
 
+  void init();
 public:
 
   DatatypesEnumerator(TypeNode type) throw() :
     TypeEnumeratorBase<DatatypesEnumerator>(type),
     d_datatype(DatatypeType(type.toType()).getDatatype()),
-    d_type(type),
-    d_ctor(0),
-    d_zeroCtor(0) {
-
-    //Assert(type.isDatatype());
-    Debug("te") << "datatype is datatype? " << type.isDatatype() << std::endl;
-    Debug("te") << "datatype is kind " << type.getKind() << std::endl;
-    Debug("te") << "datatype is " << type << std::endl;
-
-    /* find the "zero" constructor via mkGroundTerm */
-    Node t = type.mkGroundTerm();
-    Assert( t.getKind()==kind::APPLY_CONSTRUCTOR );
-    d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() );
-    /* start with the constructor for which a ground term is constructed */
-    d_ctor = d_zeroCtor;
-
-    for( unsigned i=0; i<d_datatype.getNumConstructors(); ++i ){
-      d_sel_types.push_back( std::vector< TypeNode >() );
-      d_sel_index.push_back( std::vector< unsigned >() );
-      d_sel_sum.push_back( -1 );
-      DatatypeConstructor ctor = d_datatype[i];
-      Type typ;
-      if( d_datatype.isParametric() ){
-        typ = ctor.getSpecializedConstructorType(d_type.toType());
-      }
-      for( unsigned a = 0; a < ctor.getNumArgs(); ++a ){
-        TypeNode tn;
-        if( d_datatype.isParametric() ){
-          tn = TypeNode::fromType( typ )[a];
-        }else{
-          tn = Node::fromExpr(ctor[a].getSelector()).getType()[1];
-        }
-        d_sel_types[i].push_back( tn );
-        d_sel_index[i].push_back( 0 );
-      }
-      if( !d_sel_index[i].empty() ){
-        d_sel_index[i].pop_back();
-      }
-    }
-    d_size_limit = 0;
-    //set up initial conditions (should always succeed)
-    bool init_inc = increment( d_ctor );
-    AlwaysAssert( init_inc );
+    d_type(type) {
+    d_child_enum = false;
+    init();
+  }
+  DatatypesEnumerator(TypeNode type, bool childEnum) throw() :
+    TypeEnumeratorBase<DatatypesEnumerator>(type),
+    d_datatype(DatatypeType(type.toType()).getDatatype()),
+    d_type(type) {
+    d_child_enum = childEnum;
+    init();
   }
-
   DatatypesEnumerator(const DatatypesEnumerator& de) throw() :
     TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
     d_datatype(de.d_datatype),
@@ -235,14 +117,16 @@ public:
     d_children.insert( d_children.end(), de.d_children.begin(), de.d_children.end() );
     d_sel_sum.insert( d_sel_sum.end(), de.d_sel_sum.begin(), de.d_sel_sum.end() );
     d_size_limit = de.d_size_limit;
+    d_has_debruijn = de.d_has_debruijn;
+    d_child_enum = de.d_child_enum;
   }
 
-  ~DatatypesEnumerator() throw() {
+  virtual ~DatatypesEnumerator() throw() {
   }
 
   Node operator*() throw(NoMoreValuesException) {
     Debug("dt-enum-debug") << ": get term " << this << std::endl;
-    if(d_ctor < d_datatype.getNumConstructors()) {
+    if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) {
       return getCurrentTerm( d_ctor );
     } else {
       throw NoMoreValuesException(getType());
@@ -252,7 +136,7 @@ public:
   DatatypesEnumerator& operator++() throw() {
     Debug("dt-enum-debug") << ": increment " << this << std::endl;
     unsigned prevSize = d_size_limit;
-    while(d_ctor < d_datatype.getNumConstructors()) {
+    while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) {
       //increment at index
       while( increment( d_ctor ) ){
         Node n = getCurrentTerm( d_ctor );
@@ -267,9 +151,9 @@ public:
       if(d_ctor == d_zeroCtor) {
         ++d_ctor;
       }
-      if( d_ctor>=d_datatype.getNumConstructors() ){
-        //try next size limit as long as new terms were generated at last size
-        if( prevSize==d_size_limit ){
+      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.isFinite() ){
           d_size_limit++;
           d_ctor = d_zeroCtor;
           for( unsigned i=0; i<d_sel_sum.size(); i++ ){
@@ -282,7 +166,7 @@ public:
   }
 
   bool isFinished() throw() {
-    return d_ctor >= d_datatype.getNumConstructors();
+    return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors();
   }
 
 };/* DatatypesEnumerator */
@@ -328,7 +212,7 @@ public:
     }
   }
 
-  ~TupleEnumerator() throw() {
+  virtual ~TupleEnumerator() throw() {
     deleteEnumerators();
   }
 
@@ -413,7 +297,7 @@ public:
     }
   }
 
-  ~RecordEnumerator() throw() {
+  virtual ~RecordEnumerator() throw() {
     deleteEnumerators();
   }
 
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index f0a76ee8a..d8006a5a4 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -89,6 +89,8 @@ public:
   TypeEnumerator(const TypeEnumerator& te) :
     d_te(te.d_te->clone()) {
   }
+  TypeEnumerator(TypeEnumeratorInterface* te) : d_te(te){
+  }
   TypeEnumerator& operator=(const TypeEnumerator& te) {
     delete d_te;
     d_te = te.d_te->clone();
diff --git a/src/util/uninterpreted_constant.h b/src/util/uninterpreted_constant.h
index c4fb776bc..13a80a19d 100644
--- a/src/util/uninterpreted_constant.h
+++ b/src/util/uninterpreted_constant.h
@@ -32,7 +32,7 @@ public:
   UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException) :
     d_type(type),
     d_index(index) {
-    CheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
+    //CheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
     CheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
   }