Fix non-termination in datatype type enumerator (#3369)

13 files changed, 378 insertions, 143 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 2356f74bc..2edb1f53b 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -30,6 +30,7 @@
 #include "expr/type.h"
 #include "options/datatypes_options.h"
 #include "options/set_language.h"
+#include "theory/type_enumerator.h"
 
 using namespace std;
 
@@ -479,32 +480,48 @@ bool Datatype::computeWellFounded(std::vector<Type>& processing) const
 Expr Datatype::mkGroundTerm(Type t) const
 {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  return mkGroundTermInternal(t, false);
+}
+
+Expr Datatype::mkGroundValue(Type t) const
+{
+  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  return mkGroundTermInternal(t, true);
+}
+
+Expr Datatype::mkGroundTermInternal(Type t, bool isValue) const
+{
   ExprManagerScope ems(d_self);
-  Debug("datatypes") << "mkGroundTerm of type " << t << std::endl;
+  Debug("datatypes") << "mkGroundTerm of type " << t
+                     << ", isValue = " << isValue << std::endl;
   // is this already in the cache ?
-  std::map< Type, Expr >::iterator it = d_ground_term.find( t );
-  if( it != d_ground_term.end() ){
+  std::map<Type, Expr>& cache = isValue ? d_ground_value : d_ground_term;
+  std::map<Type, Expr>::iterator it = cache.find(t);
+  if (it != cache.end())
+  {
     Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl;
     return it->second;
-  } else {
-    std::vector< Type > processing;
-    Expr groundTerm = computeGroundTerm( t, processing );
-    if(!groundTerm.isNull() ) {
-      // we found a ground-term-constructing constructor!
-      d_ground_term[t] = 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
-        IllegalArgument(*this, "datatype is not well-founded, cannot construct a ground term!");
-      }else{
-        return groundTerm;
-      }
-    }else{
-      return groundTerm;
+  }
+  std::vector<Type> processing;
+  Expr groundTerm = computeGroundTerm(t, processing, isValue);
+  if (!groundTerm.isNull())
+  {
+    // we found a ground-term-constructing constructor!
+    cache[t] = 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
+      IllegalArgument(
+          *this,
+          "datatype is not well-founded, cannot construct a ground term!");
     }
   }
+  return groundTerm;
 }
 
 Expr getSubtermWithType( Expr e, Type t, bool isTop ){
@@ -521,7 +538,9 @@ Expr getSubtermWithType( Expr e, Type t, bool isTop ){
   }
 }
 
-Expr Datatype::computeGroundTerm(Type t, std::vector<Type>& processing) const
+Expr Datatype::computeGroundTerm(Type t,
+                                 std::vector<Type>& processing,
+                                 bool isValue) const
 {
   if( std::find( processing.begin(), processing.end(), t )==processing.end() ){
     processing.push_back( t );
@@ -530,7 +549,8 @@ Expr Datatype::computeGroundTerm(Type t, std::vector<Type>& processing) const
         //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, d_ground_term );
+          Expr e =
+              (*i).computeGroundTerm(t, processing, d_ground_term, isValue);
           if( !e.isNull() ){
             //must check subterms for the same type to avoid infinite loops in type enumeration
             Expr se = getSubtermWithType( e, t, true );
@@ -1078,7 +1098,8 @@ bool DatatypeConstructor::isInterpretedFinite(Type t) const
 
 Expr DatatypeConstructor::computeGroundTerm(Type t,
                                             std::vector<Type>& processing,
-                                            std::map<Type, Expr>& gt) const
+                                            std::map<Type, Expr>& gt,
+                                            bool isValue) const
 {
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
@@ -1089,13 +1110,16 @@ Expr DatatypeConstructor::computeGroundTerm(Type t,
   // for each selector, get a ground term
   std::vector< Type > instTypes;
   std::vector< Type > paramTypes;
-  if( DatatypeType(t).isParametric() ){
+  bool isParam = static_cast<DatatypeType>(t).isParametric();
+  if (isParam)
+  {
     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() ){
+    if (isParam)
+    {
       selType = selType.substitute( paramTypes, instTypes );
     }
     Expr arg;
@@ -1105,10 +1129,13 @@ Expr DatatypeConstructor::computeGroundTerm(Type t,
         arg = itgt->second;
       }else{
         const Datatype & dt = DatatypeType(selType).getDatatype();
-        arg = dt.computeGroundTerm( selType, processing );
+        arg = dt.computeGroundTerm(selType, processing, isValue);
       }
-    }else{
-      arg = selType.mkGroundTerm();
+    }
+    else
+    {
+      // call mkGroundValue or mkGroundTerm based on isValue
+      arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm();
     }
     if( arg.isNull() ){
       Debug("datatypes") << "...unable to construct arg of " << (*i).getName() << std::endl;
@@ -1120,9 +1147,10 @@ Expr DatatypeConstructor::computeGroundTerm(Type t,
   }
 
   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
+  if (isParam)
+  {
+    Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
+    // type is parametric, 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))),
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index b7a2721ab..b32001a89 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -528,10 +528,24 @@ class CVC4_PUBLIC DatatypeConstructor {
   Cardinality computeCardinality(Type t, std::vector<Type>& processing) const;
   /** compute whether this datatype is well-founded */
   bool computeWellFounded(std::vector<Type>& processing) const;
-  /** compute ground term */
+  /** compute ground term
+   *
+   * This method is used for constructing a term that is an application
+   * of this constructor whose type is t.
+   *
+   * The argument processing is the set of datatype types we are currently
+   * traversing. This is used to avoid infinite loops.
+   *
+   * The argument gt caches the ground terms we have computed so far.
+   *
+   * The argument isValue is whether we are constructing a constant value. If
+   * this flag is false, we are constructing a canonical ground term that is
+   * not necessarily constant.
+   */
   Expr computeGroundTerm(Type t,
                          std::vector<Type>& processing,
-                         std::map<Type, Expr>& gt) const;
+                         std::map<Type, Expr>& gt,
+                         bool isValue) const;
   /** compute shared selectors
    * This computes the maps d_shared_selectors and d_shared_selector_index.
    */
@@ -821,6 +835,16 @@ public:
    * type if this datatype is parametric.
    */
   Expr mkGroundTerm(Type t) const;
+  /** Make ground value
+   *
+   * Same as above, but constructs a constant value instead of a ground term.
+   * These two notions typically coincide. However, for uninterpreted sorts,
+   * they do not: mkGroundTerm returns a fresh variable whereas mkValue returns
+   * an uninterpreted constant. The motivation for mkGroundTerm is that
+   * unintepreted constants should never appear in lemmas. The motivation for
+   * mkGroundValue is for things like type enumeration and model construction.
+   */
+  Expr mkGroundValue(Type t) const;
 
   /**
    * Get the DatatypeType associated to this Datatype.  Can only be
@@ -994,6 +1018,8 @@ public:
   mutable int d_well_founded;
   /** cache of ground term for this datatype */
   mutable std::map<Type, Expr> d_ground_term;
+  /** cache of ground values for this datatype */
+  mutable std::map<Type, Expr> d_ground_value;
   /** cache of shared selectors for this datatype */
   mutable std::map<Type, std::map<Type, std::map<unsigned, Expr> > >
       d_shared_sel;
@@ -1043,8 +1069,21 @@ public:
                                       std::vector<Type>& u_assume) const;
   /** compute whether this datatype is well-founded */
   bool computeWellFounded(std::vector<Type>& processing) const;
-  /** compute ground term */
-  Expr computeGroundTerm(Type t, std::vector<Type>& processing) const;
+  /** compute ground term
+   *
+   * This method checks if there is a term of this datatype whose type is t
+   * that is finitely constructable. As needed, it traverses its subfield types.
+   *
+   * The argument processing is the set of datatype types we are currently
+   * traversing.
+   *
+   * The argument isValue is whether we are constructing a constant value. If
+   * this flag is false, we are constructing a canonical ground term that is
+   * not necessarily constant.
+   */
+  Expr computeGroundTerm(Type t,
+                         std::vector<Type>& processing,
+                         bool isValue) const;
   /** Get the shared selector
    *
    * This returns the index^th (constructor-agnostic)
@@ -1056,6 +1095,10 @@ public:
    * this returns the term sel_{dtt}^{t,index}.
    */
   Expr getSharedSelector(Type dtt, Type t, unsigned index) const;
+  /**
+   * Helper for mkGroundTerm and mkGroundValue above.
+   */
+  Expr mkGroundTermInternal(Type t, bool isValue) const;
 };/* class Datatype */
 
 /**
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 76c318b2e..31f21667a 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -101,6 +101,12 @@ Expr Type::mkGroundTerm() const {
   return d_typeNode->mkGroundTerm().toExpr();
 }
 
+Expr Type::mkGroundValue() const
+{
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->mkGroundValue().toExpr();
+}
+
 bool Type::isSubtypeOf(Type t) const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSubtypeOf(*t.d_typeNode);
diff --git a/src/expr/type.h b/src/expr/type.h
index 587df07ee..529c40930 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -191,6 +191,20 @@ protected:
   Expr mkGroundTerm() const;
 
   /**
+   * Construct and return a ground value for this Type.  Throws an
+   * exception if this type is not well-founded.
+   *
+   * This is the same as mkGroundTerm, but constructs a constant value instead
+   * of a canonical ground term. These two notions typically coincide. However,
+   * for uninterpreted sorts, they do not: mkGroundTerm returns a fresh variable
+   * whereas mkValue returns an uninterpreted constant. The motivation for
+   * mkGroundTerm is that unintepreted constants should never appear in lemmas.
+   * The motivation for mkGroundValue is for e.g. type enumeration and model
+   * construction.
+   */
+  Expr mkGroundValue() const;
+
+  /**
    * Is this type a subtype of the given type?
    */
   bool isSubtypeOf(Type t) const;
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index b3c8592ed..0a04d7efe 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -23,6 +23,7 @@
 #include "options/expr_options.h"
 #include "options/quantifiers_options.h"
 #include "options/uf_options.h"
+#include "theory/type_enumerator.h"
 
 using namespace std;
 
@@ -292,6 +293,12 @@ Node TypeNode::mkGroundTerm() const {
   return kind::mkGroundTerm(*this);
 }
 
+Node TypeNode::mkGroundValue() const
+{
+  theory::TypeEnumerator te(*this);
+  return *te;
+}
+
 bool TypeNode::isSubtypeOf(TypeNode t) const {
   if(*this == t) {
     return true;
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 1fcd64fc7..610dd3b62 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -475,6 +475,14 @@ public:
   Node mkGroundTerm() const;
 
   /**
+   * Construct and return a ground value of this type.  If the type is
+   * not well founded, this function throws an exception.
+   *
+   * @return a ground value of the type
+   */
+  Node mkGroundValue() const;
+
+  /**
    * Is this type a subtype of the given type?
    */
   bool isSubtypeOf(TypeNode t) const;
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index de97227e0..5de04a9c3 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -97,27 +97,41 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    }
  }
 
- Node DatatypesEnumerator::getCurrentTerm( unsigned index ){
-   Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type << std::endl;
+ 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 ){
-     if( d_child_enum ){
-       ret = NodeManager::currentNM()->mkConst(UninterpretedConstant(d_type.toType(), d_size_limit));
-     }else{
-       //no top-level variables
+   if (index < d_has_debruijn)
+   {
+     if (d_child_enum)
+     {
+       ret = NodeManager::currentNM()->mkConst(
+           UninterpretedConstant(d_type.toType(), d_size_limit));
+     }
+     else
+     {
+       // no top-level variables
        return Node::null();
      }
-   }else{
-     Debug("dt-enum-debug") << "Look at constructor " << (index - d_has_debruijn) << std::endl;
+   }
+   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
+     // 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 ){
+     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() ){
+       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();
        }
@@ -125,37 +139,49 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
      Debug("dt-enum-debug") << "Get constructor..." << std::endl;
      NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
      Type typ;
-     if( d_datatype.isParametric() ){
+     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 << 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 ){
+     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] );
+       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;
+     Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
      ret = nnn;
    }
 
-   if( !d_child_enum && d_has_debruijn ){
-     Node nret = DatatypesRewriter::normalizeCodatatypeConstant( ret );
-     if( nret!=ret ){
-       if( nret.isNull() ){
+   if (!d_child_enum && d_has_debruijn)
+   {
+     Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret);
+     if (nret != ret)
+     {
+       if (nret.isNull())
+       {
          Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl;
-       }else{
+       }
+       else
+       {
          Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
          Trace("dt-enum-nn") << "  ...normal form is : " << nret << std::endl;
        }
@@ -166,59 +192,133 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    return ret;
  }
 
- void DatatypesEnumerator::init(){
-   //Assert(type.isDatatype());
-   Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
+ void DatatypesEnumerator::init()
+ {
+   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( d_type.toType() );
-   Debug("dt-enum") << " " << d_datatype.isInterpretedFinite( d_type.toType() ) << std::endl;
+   Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " "
+                    << d_datatype.isRecursiveSingleton(d_type.toType());
+   Debug("dt-enum") << " " << d_datatype.isInterpretedFinite(d_type.toType())
+                    << std::endl;
 
-   if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
-     //start with uninterpreted constant
-     d_zeroCtor = 0;
+   if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
+   {
+     // start with uninterpreted constant
      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
+     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" term via mkGroundTerm
      Debug("dt-enum-debug") << "make ground term..." << std::endl;
-     Node t = d_type.mkGroundTerm();
-     Debug("dt-enum-debug") << "done : " << t << std::endl;
-     Assert(t.getKind() == kind::APPLY_CONSTRUCTOR);
-     // start with the constructor for which a ground term is constructed
-     d_zeroCtor = datatypes::utils::indexOf(t.getOperator());
+     // Start with the ground term constructed via mkGroundValue, which does
+     // a traversal over the structure of the datatype to find a finite term.
+     // Notice that mkGroundValue may be dependent upon extracting the first
+     // value of type enumerators for *other non-datatype* subfield types of
+     // this datatype. Since datatypes can not be embedded in non-datatype
+     // types (e.g. (Array D D) cannot be a subfield type of datatype D), this
+     // call is guaranteed to avoid infinite recursion.
+     d_zeroTerm = Node::fromExpr(d_datatype.mkGroundValue(d_type.toType()));
+     d_zeroTermActive = true;
+     Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
+     Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
      d_has_debruijn = 0;
    }
-   Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl;
-   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 );
+   Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl;
+   d_ctor = 0;
+   for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++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() ){
+     if (d_datatype.isParametric())
+     {
        typ = ctor.getSpecializedConstructorType(d_type.toType());
      }
-     for( unsigned a = 0; a < ctor.getNumArgs(); ++a ){
+     for (unsigned a = 0; a < ctor.getNumArgs(); ++a)
+     {
        TypeNode tn;
-       if( d_datatype.isParametric() ){
-         tn = TypeNode::fromType( typ )[a];
-       }else{
+       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 );
+       d_sel_types.back().push_back(tn);
+       d_sel_index.back().push_back(0);
      }
-     if( !d_sel_index.back().empty() ){
+     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 );
+   if (!d_zeroTermActive)
+   {
+     // Set up initial conditions (should always succeed). Here, we are calling
+     // the increment function of this class, which ensures a term is ready to
+     // read via a dereference of this class. We use the same method for
+     // setting up the first term, if it is not already set up
+     // (d_zeroTermActive) using the increment function, for uniformity.
+     ++*this;
+   }
    AlwaysAssert(!isFinished());
-}
+ }
+
+ DatatypesEnumerator& DatatypesEnumerator::operator++()
+ {
+   Debug("dt-enum-debug") << ": increment " << this << std::endl;
+   if (d_zeroTermActive)
+   {
+     d_zeroTermActive = false;
+   }
+   unsigned prevSize = d_size_limit;
+   while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
+   {
+     // increment at index
+     while (increment(d_ctor))
+     {
+       Node n = getCurrentTerm(d_ctor);
+       if (!n.isNull())
+       {
+         if (n == d_zeroTerm)
+         {
+           d_zeroTerm = Node::null();
+         }
+         else
+         {
+           return *this;
+         }
+       }
+     }
+     // Here, we need to step from the current constructor to the next one
 
+     // Go to the next constructor
+     d_ctor = d_ctor + 1;
+     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(d_type.toType()))
+       {
+         d_size_limit++;
+         d_ctor = 0;
+         for (unsigned i = 0; i < d_sel_sum.size(); i++)
+         {
+           d_sel_sum[i] = -1;
+         }
+       }
+     }
+   }
+   return *this;
+ }
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index a294324fa..6f7fc4286 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -41,8 +41,10 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   TypeNode d_type;
   /** The datatype constructor we're currently enumerating */
   unsigned d_ctor;
-  /** The "first" constructor to consider; it's non-recursive */
-  unsigned d_zeroCtor;
+  /** The first term to consider in the enumeration */
+  Node d_zeroTerm;
+  /** Whether we are currently considering the above term */
+  bool d_zeroTermActive;
   /** list of type enumerators (one for each type in a selector argument) */
   std::map< TypeNode, unsigned > d_te_index;
   std::vector< TypeEnumerator > d_children;
@@ -85,7 +87,9 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
       : TypeEnumeratorBase<DatatypesEnumerator>(type),
         d_tep(tep),
         d_datatype(DatatypeType(type.toType()).getDatatype()),
-        d_type(type)
+        d_type(type),
+        d_ctor(0),
+        d_zeroTermActive(false)
   {
     d_child_enum = false;
     init();
@@ -96,19 +100,22 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
       : TypeEnumeratorBase<DatatypesEnumerator>(type),
         d_tep(tep),
         d_datatype(DatatypeType(type.toType()).getDatatype()),
-        d_type(type)
+        d_type(type),
+        d_ctor(0),
+        d_zeroTermActive(false)
   {
     d_child_enum = childEnum;
     init();
   }
-  DatatypesEnumerator(const DatatypesEnumerator& de) :
-    TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
-    d_tep(de.d_tep),
-    d_datatype(de.d_datatype),
-    d_type(de.d_type),
-    d_ctor(de.d_ctor),
-    d_zeroCtor(de.d_zeroCtor) {
-
+  DatatypesEnumerator(const DatatypesEnumerator& de)
+      : TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
+        d_tep(de.d_tep),
+        d_datatype(de.d_datatype),
+        d_type(de.d_type),
+        d_ctor(de.d_ctor),
+        d_zeroTerm(de.d_zeroTerm),
+        d_zeroTermActive(de.d_zeroTermActive)
+  {
     for( std::map< TypeNode, unsigned >::const_iterator it = de.d_te_index.begin(); it != de.d_te_index.end(); ++it ){
       d_te_index[it->first] = it->second;
     }
@@ -134,45 +141,18 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   Node operator*() override
   {
     Debug("dt-enum-debug") << ": get term " << this << std::endl;
-    if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) {
+    if (d_zeroTermActive)
+    {
+      return d_zeroTerm;
+    }
+    else if (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
+    {
       return getCurrentTerm( d_ctor );
-    } else {
-      throw NoMoreValuesException(getType());
     }
+    throw NoMoreValuesException(getType());
   }
 
-  DatatypesEnumerator& operator++() override
-  {
-    Debug("dt-enum-debug") << ": increment " << this << std::endl;
-    unsigned prevSize = d_size_limit;
-    while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) {
-      //increment at index
-      while( increment( d_ctor ) ){
-        Node n = getCurrentTerm( d_ctor );
-        if( !n.isNull() ){
-          return *this;
-        }
-      }
-      // Here, we need to step from the current constructor to the next one
-
-      // Find the next constructor (only complicated by the notion of the "zero" constructor
-      d_ctor = (d_ctor == d_zeroCtor) ? 0 : d_ctor + 1;
-      if(d_ctor == d_zeroCtor) {
-        ++d_ctor;
-      }
-      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( d_type.toType() ) ){
-          d_size_limit++;
-          d_ctor = d_zeroCtor;
-          for( unsigned i=0; i<d_sel_sum.size(); i++ ){
-            d_sel_sum[i] = -1;
-          }
-        }
-      }
-    }
-    return *this;
-  }
+  DatatypesEnumerator& operator++() override;
 
   bool isFinished() override
   {
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index f6edd3195..f397b9a0a 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -307,6 +307,7 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
   }
 
   //must ensure model basis terms exists in model for each relevant type
+  Trace("fmc") << "preInitialize types..." << std::endl;
   fm->initialize();
   for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
     Node op = it->first;
@@ -315,8 +316,10 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
     for( unsigned i=0; i<tno.getNumChildren(); i++) {
       Trace("fmc") << "preInitializeType " << tno[i] << std::endl;
       preInitializeType( fm, tno[i] );
+      Trace("fmc") << "finished preInitializeType " << tno[i] << std::endl;
     }
   }
+  Trace("fmc") << "Finish preInitialize types" << std::endl;
   //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
   if( !options::fmfEmptySorts() ){
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
@@ -522,7 +525,9 @@ void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn )
     d_preinitialized_types[tn] = true;
     if (!tn.isFunction() || options::ufHo())
     {
+      Trace("fmc") << "Get model basis term " << tn << "..." << std::endl;
       Node mb = fm->getModelBasisTerm(tn);
+      Trace("fmc") << "...return " << mb << std::endl;
       // if the model basis term does not exist in the model,
       // either add it directly to the model's equality engine if no other terms
       // of this type exist, or otherwise assert that it is equal to the first
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index b1171f152..47355aa81 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -306,6 +306,8 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
     return false;
   }
 
+  Trace("model-builder")
+      << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl;
   // model-builder specific initialization
   if (!preProcessBuildModel(tm))
   {
@@ -315,6 +317,8 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
     return false;
   }
 
+  Trace("model-builder")
+      << "TheoryEngineModelBuilder: Add assignable subterms..." << std::endl;
   // Loop through all terms and make sure that assignable sub-terms are in the
   // equality engine
   // Also, record #eqc per type (for finite model finding)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 134f42610..7e52501c2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1158,6 +1158,7 @@ set(regress_1_tests
   regress1/datatypes/dt-param-card4-unsat.smt2
   regress1/datatypes/error.cvc
   regress1/datatypes/issue3266-small.smt2
+  regress1/datatypes/issue-variant-dt-zero.smt2
   regress1/datatypes/manos-model.smt2
   regress1/decision/error3.smtv1.smt2
   regress1/decision/quant-Arrays_Q1-noinfer.smt2
@@ -1392,6 +1393,7 @@ set(regress_1_tests
   regress1/quantifiers/isaplanner-goal20.smt2
   regress1/quantifiers/issue2970-string-var-elim.smt2
   regress1/quantifiers/issue3250-syg-inf-q.smt2
+  regress1/quantifiers/issue3316.smt2
   regress1/quantifiers/issue3317.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
diff --git a/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2 b/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2
new file mode 100644
index 000000000..f2a5b81c8
--- /dev/null
+++ b/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --fmf-fun-rlv --no-check-models
+; EXPECT: sat
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes () ((a0(c0$0)(c0$1(c0$1$0 String)(c0$1$1 Int))(c0$2(c0$2$0 Bool)(c0$2$1 Int)(c0$2$2 String)))
+                       (a1(c1$0)(c1$1)(c1$2))
+                       (a2(c2$0(c2$0$0 Int)(c2$0$1 a0)(c2$0$2 String)(c2$0$3 a3)(c2$0$4 String)(c2$0$5 Bool)))
+                       (a3(c3$0(c3$0$0 a7)(c3$0$1 a1)(c3$0$2 a5)(c3$0$3 a6)(c3$0$4 Int)(c3$0$5 Bool)(c3$0$6 Bool))(c3$1(c3$1$0 String)))
+                       (a4(c4$0(c4$0$0 String)(c4$0$1 a2)(c4$0$2 String))(c4$1(c4$1$0 a0)(c4$1$1 a4)(c4$1$2 a4)(c4$1$3 a7))(c4$2))
+                       (a5(c5$0(c5$0$0 a2))(c5$1)(c5$2)(c5$3(c5$3$0 a0))(c5$4)(c5$5(c5$5$0 a4)(c5$5$1 Int))(c5$6))
+                       (a6(c6$0(c6$0$0 a7)(c6$0$1 a7)(c6$0$2 String))(c6$1)(c6$2)(c6$3)(c6$4)(c6$5)(c6$6))
+                       (a7(c7$0(c7$0$0 a2)(c7$0$1 Int))(c7$1(c7$1$0 a4)(c7$1$1 Int)(c7$1$2 Bool)))))
+(define-funs-rec ((f0((v0 a6))a4))
+                  (c4$2))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/issue3316.smt2 b/test/regress/regress1/quantifiers/issue3316.smt2
new file mode 100644
index 000000000..320a57790
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue3316.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --fmf-fun-rlv --no-check-models
+; EXPECT: sat
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes () ((a0(c0$0)(c0$1(c0$1$0 String)(c0$1$1 Int))(c0$2(c0$2$0 Bool)(c0$2$1 Int)(c0$2$2 String)))
+                       (a1(c1$0)(c1$1)(c1$2))
+                       (a2(c2$0(c2$0$0 Int)(c2$0$1 a0)(c2$0$2 String)(c2$0$3 a3)(c2$0$4 String)(c2$0$5 Bool)))
+                       (a3(c3$0(c3$0$0 a7)(c3$0$1 a1)(c3$0$2 a5)(c3$0$3 a6)(c3$0$4 Int)(c3$0$5 Bool)(c3$0$6 Bool))(c3$1(c3$1$0 String)))
+                       (a4(c4$0(c4$0$0 String)(c4$0$1 a2)(c4$0$2 String))(c4$1(c4$1$0 a0)(c4$1$1 a4)(c4$1$2 a4)(c4$1$3 a7))(c4$2))
+                       (a5(c5$0(c5$0$0 a2))(c5$1)(c5$2)(c5$3(c5$3$0 a0))(c5$4)(c5$5(c5$5$0 a4)(c5$5$1 Int))(c5$6))
+                       (a6(c6$0(c6$0$0 a7)(c6$0$1 a7)(c6$0$2 String))(c6$1)(c6$2)(c6$3)(c6$4)(c6$5)(c6$6))
+                       (a7(c7$0(c7$0$0 a2)(c7$0$1 Int))(c7$1(c7$1$0 a4)(c7$1$1 Int)(c7$1$2 Bool)))))
+(define-funs-rec ((f3((v4 Bool))a7)
+                  (f2()a6)
+                  (f1((v1 a3)(v2 a1)(v3 Bool))String)
+                  (f0((v0 a6))a4))
+                  ((c7$0 (c2$0 0 c0$0 "" (c3$1 "") "" true) 0) 
+                  c6$2 
+                  "" 
+                  c4$2))
+(check-sat)