From 76da4764db903c503ac339584db667aa50748179 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Dec 2014 23:21:40 +0100
Subject: [PATCH] Do not collapse wrongly applied selectors for
 non-well-founded codatatypes pre-model.

---
 src/theory/datatypes/datatypes_rewriter.h | 24 ++++++++++++-----------
 src/theory/datatypes/theory_datatypes.cpp | 22 ---------------------
 src/util/datatype.cpp                     |  1 +
 3 files changed, 14 insertions(+), 33 deletions(-)

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 0bbb97076..02339dc26 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -143,20 +143,22 @@ public:
         if( in.getType().isSort() ){
           TypeEnumerator te(in.getType());
           gt = *te;
-        }else{
+        }else if( dt.isWellFounded() || in[0].isConst() ){
           gt = in.getType().mkGroundTerm();
         }
-        TypeNode gtt = gt.getType();
-        //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
-        if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){
-          gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                                NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
+        if( !gt.isNull() ){
+          TypeNode gtt = gt.getType();
+          //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
+          if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){
+            gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                                                  NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
+          }
+          Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                                     << "Rewrite trivial selector " << in
+                                     << " to distinguished ground term "
+                                     << in.getType().mkGroundTerm() << std::endl;
+          return RewriteResponse(REWRITE_DONE,gt );
         }
-        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
-                                   << "Rewrite trivial selector " << in
-                                   << " to distinguished ground term "
-                                   << in.getType().mkGroundTerm() << std::endl;
-        return RewriteResponse(REWRITE_DONE,gt );
       }
     }
     if(in.getKind() == kind::DT_SIZE && in[0].getKind()==kind::APPLY_CONSTRUCTOR ){
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index edb548ca4..0429c3aab 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -802,28 +802,6 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         }
       }
     }
-    //add this to the transitive closure module
-    Node oldRep = trep2;
-    Node newRep = trep1;
-    if( trep1.getKind()!=APPLY_CONSTRUCTOR && trep2.getKind()==APPLY_CONSTRUCTOR ){
-      oldRep = trep1;
-      newRep = trep2;
-    }
-    /*
-    bool result = d_cycle_check.addEdgeNode( oldRep, newRep );
-    //d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
-    Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << result << " " << d_hasSeenCycle.get() << endl;
-    if( result ){
-      checkCycles();
-      if( d_conflict ){
-        Debug("datatypes-cycles-find") << "Cycle found." << std::endl;
-        return;
-      }else{
-        Debug("datatypes-cycles-find") << "WARNING : no cycle found." << std::endl;
-        d_cycle_check.debugPrint();
-      }
-    }
-    */
   }
 }
 
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index f0704520a..7813626a7 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -228,6 +228,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
 
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_self);
+  Debug("datatypes") << "dt mkGroundTerm " << t << std::endl;
 
   TypeNode self = TypeNode::fromType(d_self);
 
-- 
2.30.2