Simplify approach for collapsed selectors over non-closed enumerable types (#5223)

This simplifies the approach for wrongly-applied selectors whose range type involves e.g. uninterpreted sorts. These cases are particularly tricky since uninterpreted constants should never appear in facts or lemmas.

Previously, the rewriter had special cases for either making a ground term or value, and a purify step was used to eliminate the occurrences of uninterpreted sorts afterwards.

This PR leverages mkGroundTerm in this inference instead, and makes the rewriter uniformly use mkGroundValue.

This also required making the type enumerator for datatypes more uniform. In particular, we require that the first value enumerated by the type enumerator is of the same shape as the term required by mkGroundTerm, or else debug-check-model will fail. This is due to the fact that now the inference for wrongly applied selectors uses terms while the rewriter uses values. The type enumerator is updated so that recursive codatatypes also first take mkGroundValue as the zero term, when they are well-founded. Previously this was skipped since the codatatype enumerator uses a different algorithm for computing its ground terms.

This is in preparation for further work on optimizations and proofs for datatypes.

4 files changed, 44 insertions, 88 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index b7a7061f3..fa5f2fe33 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -390,41 +390,21 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
     }
     else if (k == kind::APPLY_SELECTOR_TOTAL)
     {
-      Node gt;
-      bool useTe = true;
-      // if( !tn.isSort() ){
-      //  useTe = false;
-      //}
-      if (tn.isDatatype())
+      // evaluates to the first ground value of type tn.
+      Node gt = tn.mkGroundValue();
+      Assert(!gt.isNull());
+      if (tn.isDatatype() && !tn.isInstantiatedDatatype())
       {
-        const DType& dta = tn.getDType();
-        useTe = !dta.isCodatatype();
-      }
-      if (useTe)
-      {
-        TypeEnumerator te(tn);
-        gt = *te;
-      }
-      else
-      {
-        gt = tn.mkGroundTerm();
-      }
-      if (!gt.isNull())
-      {
-        // Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
-        if (tn.isDatatype() && !tn.isInstantiatedDatatype())
-        {
-          gt = NodeManager::currentNM()->mkNode(
-              kind::APPLY_TYPE_ASCRIPTION,
-              NodeManager::currentNM()->mkConst(AscriptionType(tn.toType())),
-              gt);
-        }
-        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
-                                   << "Rewrite trivial selector " << in
-                                   << " to distinguished ground term " << gt
-                                   << std::endl;
-        return RewriteResponse(REWRITE_DONE, gt);
+        gt = NodeManager::currentNM()->mkNode(
+            kind::APPLY_TYPE_ASCRIPTION,
+            NodeManager::currentNM()->mkConst(AscriptionType(tn.toType())),
+            gt);
       }
+      Trace("datatypes-rewrite")
+          << "DatatypesRewriter::postRewrite: "
+          << "Rewrite trivial selector " << in
+          << " to distinguished ground term " << gt << std::endl;
+      return RewriteResponse(REWRITE_DONE, gt);
     }
   }
   return RewriteResponse(REWRITE_DONE, in);
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c7ba82024..3266c7ef4 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1045,41 +1045,6 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
   eqc->d_constructor.set( c );
 }
 
-Node TheoryDatatypes::removeUninterpretedConstants( Node n, std::map< Node, Node >& visited ){
-  std::map< Node, Node >::iterator it = visited.find( n );
-  if( it==visited.end() ){
-    Node ret = n;
-    if( n.getKind()==UNINTERPRETED_CONSTANT ){
-      std::map< Node, Node >::iterator itu = d_uc_to_fresh_var.find( n );
-      if( itu==d_uc_to_fresh_var.end() ){
-        Node k = NodeManager::currentNM()->mkSkolem( "w", n.getType(), "Skolem for wrongly applied selector." );
-        d_uc_to_fresh_var[n] = k;
-        ret = k;
-      }else{
-        ret = itu->second;
-      }
-    }else if( n.getNumChildren()>0 ){
-      std::vector< Node > children;
-      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.push_back( n.getOperator() );
-      }
-      bool childChanged = false;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node nc = removeUninterpretedConstants( n[i], visited ); 
-        childChanged = childChanged || nc!=n[i];
-        children.push_back( nc );
-      }
-      if( childChanged ){
-        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-    }
-    visited[n] = ret;
-    return ret;
-  }else{
-    return it->second;
-  }
-} 
-
 void TheoryDatatypes::collapseSelector( Node s, Node c ) {
   Assert(c.getKind() == APPLY_CONSTRUCTOR);
   Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
@@ -1096,14 +1061,23 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
     r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
   }
   if( !r.isNull() ){
-    Node rr = Rewriter::rewrite( r );
-    Node rrs = rr;
-    if( wrong ){
-      // we have inference S_i( C_j( t ) ) = t' for i != j, where t' is result of mkGroundTerm.
-      // we must eliminate uninterpreted constants for datatypes that have uninterpreted sort subfields,
-      // since uninterpreted constants should not appear in lemmas
-      std::map< Node, Node > visited;
-      rrs = removeUninterpretedConstants( rr, visited );
+    Node rrs;
+    if (wrong)
+    {
+      // Must use make ground term here instead of the rewriter, since we
+      // do not want to introduce arbitrary values. This is important so that
+      // we avoid constants for types that are not "closed enumerable", e.g.
+      // uninterpreted sorts and arrays, where the solver does not fully
+      // handle values of the sort. The call to mkGroundTerm does not introduce
+      // values for these sorts.
+      rrs = r.getType().mkGroundTerm();
+      Trace("datatypes-wrong-sel")
+          << "Bad apply " << r << " term = " << rrs
+          << ", value = " << r.getType().mkGroundValue() << std::endl;
+    }
+    else
+    {
+      rrs = Rewriter::rewrite(r);
     }
     if (s != rrs)
     {
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index b4003f4c7..97fa9600a 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -253,8 +253,6 @@ private:
   void merge( Node t1, Node t2 );
   /** collapse selector, s is of the form sel( n ) where n = c */
   void collapseSelector( Node s, Node c );
-  /** remove uninterpreted constants */
-  Node removeUninterpretedConstants( Node n, std::map< Node, Node >& visited );
   /** for checking if cycles exist */
   void checkCycles();
   Node searchForCycle(TNode n,
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 39880fd93..2946070c7 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -201,7 +201,20 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
                     << d_datatype.isRecursiveSingleton(d_type);
    Debug("dt-enum") << " " << d_datatype.isInterpretedFinite(d_type)
                     << std::endl;
-
+   // 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. It is important that we
+   // start with this term, since it has the same shape as the one returned by
+   // TypeNode::mkGroundTerm for d_type, which avoids debug check model
+   // failures.
+   d_zeroTerm = d_datatype.mkGroundValue(d_type);
+   // Only use the zero term if it was successfully constructed. This may
+   // fail for codatatype types whose only values are infinite.
+   d_zeroTermActive = !d_zeroTerm.isNull();
    if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
    {
      // start with uninterpreted constant
@@ -214,15 +227,6 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    {
      // find the "zero" term via mkGroundTerm
      Debug("dt-enum-debug") << "make ground term..." << std::endl;
-     // 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 = d_datatype.mkGroundValue(d_type);
-     d_zeroTermActive = true;
      Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
      Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
      d_has_debruijn = 0;