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

6 files changed, 141 insertions, 35 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;