Do not collapse wrongly applied selectors for non-well-founded codatatypes pre-model.

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 0bbb9707696b3256adf23567aca0871634576d07..02339dc26e36d1d9ae84d5762fcad01247f51ae5 100644 (file)
--- 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 edb548ca4d9d05b80649caa205c70a347878cf42..0429c3aab7580176114adf88e2e053777ab74e25 100644 (file)
--- 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 f0704520afeaa40789746c741cdf36c6bf2f1b7a..7813626a795b40f2ff8388bd2ef85ed525d5ac31 100644 (file)
--- 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);