Fix datatypes compute ground value (#5671)

We were using the wrong cache on one call, leading to non-constant values being enumerated.

Fixes #5659, for that benchmark, CVC4 now answers "unknown".

3 files changed, 31 insertions, 14 deletions

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 4c93e5727..5cb76858a 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -598,6 +598,7 @@ bool DType::computeWellFounded(std::vector<TypeNode>& processing) const
 
 Node DType::mkGroundTerm(TypeNode t) const
 {
+  Trace("datatypes-init") << "DType::mkGroundTerm of type " << t << std::endl;
   Assert(isResolved());
   return mkGroundTermInternal(t, false);
 }
@@ -605,7 +606,9 @@ Node DType::mkGroundTerm(TypeNode t) const
 Node DType::mkGroundValue(TypeNode t) const
 {
   Assert(isResolved());
-  return mkGroundTermInternal(t, true);
+  Trace("datatypes-init") << "DType::mkGroundValue of type " << t << std::endl;
+  Node v = mkGroundTermInternal(t, true);
+  return v;
 }
 
 Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const
@@ -631,7 +634,8 @@ Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const
         << "constructed: " << getName() << " => " << groundTerm << std::endl;
   }
   // if ground term is null, we are not well-founded
-  Trace("datatypes-init") << "DType::mkGroundTerm for " << t << " returns "
+  Trace("datatypes-init") << "DType::mkGroundTerm for " << t
+                          << ", isValue=" << isValue << " returns "
                           << groundTerm << std::endl;
   return groundTerm;
 }
@@ -790,11 +794,12 @@ Node DType::computeGroundTerm(TypeNode t,
 {
   if (std::find(processing.begin(), processing.end(), t) != processing.end())
   {
-    Debug("datatypes-gt") << "...already processing " << t << " " << d_self
-                          << std::endl;
+    Trace("datatypes-init")
+        << "...already processing " << t << " " << d_self << std::endl;
     return Node();
   }
   processing.push_back(t);
+  std::map<TypeNode, Node>& gtCache = isValue ? d_groundValue : d_groundTerm;
   for (unsigned r = 0; r < 2; r++)
   {
     for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
@@ -804,10 +809,10 @@ Node DType::computeGroundTerm(TypeNode t,
       {
         continue;
       }
-      Trace("datatypes-init")
-          << "Try constructing for " << ctor->getName()
-          << ", processing = " << processing.size() << std::endl;
-      Node e = ctor->computeGroundTerm(t, processing, d_groundTerm, isValue);
+      Trace("datatypes-init") << "Try constructing for " << ctor->getName()
+                              << ", processing = " << processing.size()
+                              << ", isValue=" << isValue << std::endl;
+      Node e = ctor->computeGroundTerm(t, processing, gtCache, isValue);
       if (!e.isNull())
       {
         // must check subterms for the same type to avoid infinite loops in
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index d63db28d5..b378985be 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -377,6 +377,9 @@ Node DTypeConstructor::computeGroundTerm(TypeNode t,
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> groundTerms;
   groundTerms.push_back(getConstructor());
+  Trace("datatypes-init") << "cons " << d_constructor
+                          << " computeGroundTerm, isValue = " << isValue
+                          << std::endl;
 
   // for each selector, get a ground term
   std::vector<TypeNode> instTypes;
@@ -418,13 +421,18 @@ Node DTypeConstructor::computeGroundTerm(TypeNode t,
     }
     if (arg.isNull())
     {
-      Trace("datatypes") << "...unable to construct arg of "
-                         << d_args[i]->getName() << std::endl;
+      Trace("datatypes-init") << "...unable to construct arg of "
+                              << d_args[i]->getName() << std::endl;
       return Node();
     }
     else
     {
-      Trace("datatypes") << "...constructed arg " << arg.getType() << std::endl;
+      Trace("datatypes-init")
+          << "...constructed arg " << arg << " of type " << arg.getType()
+          << ", isConst = " << arg.isConst() << std::endl;
+      Assert(!isValue || arg.isConst())
+          << "Expected non-constant constructor argument : " << arg
+          << " of type " << arg.getType();
       groundTerms.push_back(arg);
     }
   }
@@ -434,14 +442,17 @@ Node DTypeConstructor::computeGroundTerm(TypeNode t,
   {
     Assert(DType::datatypeOf(d_constructor).isParametric());
     // type is parametric, must apply type ascription
-    Debug("datatypes-gt") << "ambiguous type for " << groundTerm
-                          << ", ascribe to " << t << std::endl;
+    Trace("datatypes-init") << "ambiguous type for " << groundTerm
+                            << ", ascribe to " << t << std::endl;
     groundTerms[0] = nm->mkNode(
         APPLY_TYPE_ASCRIPTION,
         nm->mkConst(AscriptionType(getSpecializedConstructorType(t))),
         groundTerms[0]);
     groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms);
   }
+  Trace("datatypes-init") << "...return " << groundTerm << std::endl;
+  Assert(!isValue || groundTerm.isConst()) << "Non-constant term " << groundTerm
+                                           << " returned for computeGroundTerm";
   return groundTerm;
 }
 
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index b77fdcd9f..3aeb55897 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -156,7 +156,8 @@ class TypeEnumerator {
 #if defined(CVC4_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__))
     try {
       Node n = **d_te;
-      Assert(n.isConst());
+      Assert(n.isConst()) << "Term " << n
+                          << " from type enumerator is not constant";
       Assert(!isFinished());
       return n;
     } catch(NoMoreValuesException&) {