bug fix for parametric datatypes, previously datatypes theory/rewriter was not recognizing parametric datatype types as being datatype types

2 files changed, 66 insertions, 60 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 21d4f0d07..42b999561 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -31,12 +31,12 @@ class DatatypesRewriter {
 public:
 
   static RewriteResponse postRewrite(TNode in) {
-    Debug("datatypes-rewrite") << "post-rewriting " << in << std::endl;
+    Trace("datatypes-rewrite") << "post-rewriting " << in << std::endl;
 
     if(in.getKind() == kind::APPLY_TESTER) {
       if(in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
         bool result = Datatype::indexOf(in.getOperator().toExpr()) == Datatype::indexOf(in[0].getOperator().toExpr());
-        Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
                                    << "Rewrite trivial tester " << in
                                    << " " << result << std::endl;
         return RewriteResponse(REWRITE_DONE,
@@ -45,7 +45,7 @@ public:
         const Datatype& dt = DatatypeType(in[0].getType().toType()).getDatatype();
         if(dt.getNumConstructors() == 1) {
           // only one constructor, so it must be
-          Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+          Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
                                      << "only one ctor for " << dt.getName()
                                      << " and that is " << dt[0].getName()
                                      << std::endl;
@@ -69,7 +69,7 @@ public:
       const DatatypeConstructor& c = dt[constructorIndex];
       if(c.getNumArgs() > selectorIndex &&
          c[selectorIndex].getSelector() == selectorExpr) {
-        Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
                                    << "Rewrite trivial selector " << in
                                    << std::endl;
         return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
@@ -82,7 +82,7 @@ public:
             gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
                                                   NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
           }
-          Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+          Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
                                      << "Rewrite trivial selector " << in
                                      << " to distinguished ground term "
                                      << in.getType().mkGroundTerm() << std::endl;
@@ -105,7 +105,7 @@ public:
   }
 
   static RewriteResponse preRewrite(TNode in) {
-    Debug("datatypes-rewrite") << "pre-rewriting " << in << std::endl;
+    Trace("datatypes-rewrite") << "pre-rewriting " << in << std::endl;
     return RewriteResponse(REWRITE_DONE, in);
   }
 
@@ -124,7 +124,7 @@ public:
           }
         }
       }
-    }else if( !n1.getType().isDatatype() ){
+    }else if( !isTermDatatype( n1 ) ){
       //also check for clashes between non-datatypes
       Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
       eq = Rewriter::rewrite( eq );
@@ -134,7 +134,11 @@ public:
     }
     return false;
   }
-
+  /** is this term a datatype */
+  static bool isTermDatatype( Node n ){
+    TypeNode tn = n.getType();
+    return tn.isDatatype() || tn.isParametricDatatype();
+  }
 
 };/* class DatatypesRewriter */
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 34e7c6f11..6b576cba8 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -34,54 +34,6 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
-void TheoryDatatypes::printModelDebug( const char* c ){
-  Trace( c ) << "Datatypes model : " << std::endl;
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  while( !eqcs_i.isFinished() ){
-    Node eqc = (*eqcs_i);
-    if( eqc.getType().isDatatype()){
-      Trace( c ) << "DATATYPE : ";
-    }
-    Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
-    Trace( c ) << "   { ";
-    //add terms to model
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-    while( !eqc_i.isFinished() ){
-      Trace( c ) << (*eqc_i) << " ";
-      ++eqc_i;
-    }
-    Trace( c ) << "}" << std::endl;
-    if( eqc.getType().isDatatype() ){
-      EqcInfo* ei = getOrMakeEqcInfo( eqc );
-      if( ei ){
-        Trace( c ) << "   Instantiated : " << ei->d_inst.get() << std::endl;
-        if( ei->d_constructor.get().isNull() ){
-          Trace("model-warn") << eqc << " has no constructor in equivalence class!" << std::endl;
-          Trace("model-warn") << "  Type : " << eqc.getType() << std::endl;
-          Trace( c ) << "   Constructor : " << std::endl;
-          Trace( c ) << "   Labels : ";
-          if( hasLabel( ei, eqc ) ){
-            Trace( c ) << getLabel( eqc );
-          }else{
-            NodeListMap::iterator lbl_i = d_labels.find( eqc );
-            if( lbl_i != d_labels.end() ){
-              NodeList* lbl = (*lbl_i).second;
-              for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
-                Trace( c ) << *j << " ";
-              }
-            }
-          }
-          Trace( c ) << std::endl;
-        }else{
-          Trace( c ) << "   Constructor : " << ei->d_constructor.get() << std::endl;
-        }
-        Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl;
-      }
-    }
-    ++eqcs_i;
-  }
-}
-
 
 TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, qe),
@@ -148,7 +100,7 @@ void TheoryDatatypes::check(Effort e) {
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
     while( !eqcs_i.isFinished() ){
       Node n = (*eqcs_i);
-      if( n.getType().isDatatype() ){
+      if( DatatypesRewriter::isTermDatatype( n ) ){
         EqcInfo* eqc = getOrMakeEqcInfo( n, true );
         //if there are more than 1 possible constructors for eqc
         if( eqc->d_constructor.get().isNull() && !hasLabel( eqc, n ) ) {
@@ -184,6 +136,7 @@ void TheoryDatatypes::check(Effort e) {
             if( !needSplit && mustSpecifyModel() ){
               //for the sake of termination, we must choose the constructor of a ground term
               //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
+              //** TODO: this is probably not good enough, actually need fair enumeration strategy
               Node groundTerm = n.getType().mkGroundTerm();
               int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
               if( pcons[index] ){
@@ -396,7 +349,7 @@ void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){
 
 /** called when two equivalance classes have merged */
 void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){
-  if( t1.getType().isDatatype() ){
+  if( DatatypesRewriter::isTermDatatype( t1 ) ){
     d_pending_merge.push_back( t1.eqNode( t2 ) );
   }
 }
@@ -683,7 +636,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
     //for all equivalence classes that are datatypes
-    if( eqc.getType().isDatatype() ){
+    if( DatatypesRewriter::isTermDatatype( eqc ) ){
       EqcInfo* ei = getOrMakeEqcInfo( eqc );
       if( ei ){
         if( !ei->d_constructor.get().isNull() ){
@@ -928,7 +881,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
     addLemma = dt.involvesExternalType();
 #else
     for( int j=0; j<(int)n[1].getNumChildren(); j++ ){
-      if( !n[1][j].getType().isDatatype() ){
+      if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){
         addLemma = true;
         break;
       }
@@ -979,3 +932,52 @@ Node TheoryDatatypes::getRepresentative( Node a ){
     return a;
   }
 }
+
+
+void TheoryDatatypes::printModelDebug( const char* c ){
+  Trace( c ) << "Datatypes model : " << std::endl;
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs_i.isFinished() ){
+    Node eqc = (*eqcs_i);
+    if( DatatypesRewriter::isTermDatatype( eqc ) ){
+      Trace( c ) << "DATATYPE : ";
+    }
+    Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
+    Trace( c ) << "   { ";
+    //add terms to model
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+    while( !eqc_i.isFinished() ){
+      Trace( c ) << (*eqc_i) << " ";
+      ++eqc_i;
+    }
+    Trace( c ) << "}" << std::endl;
+    if( DatatypesRewriter::isTermDatatype( eqc ) ){
+      EqcInfo* ei = getOrMakeEqcInfo( eqc );
+      if( ei ){
+        Trace( c ) << "   Instantiated : " << ei->d_inst.get() << std::endl;
+        if( ei->d_constructor.get().isNull() ){
+          Trace("model-warn") << eqc << " has no constructor in equivalence class!" << std::endl;
+          Trace("model-warn") << "  Type : " << eqc.getType() << std::endl;
+          Trace( c ) << "   Constructor : " << std::endl;
+          Trace( c ) << "   Labels : ";
+          if( hasLabel( ei, eqc ) ){
+            Trace( c ) << getLabel( eqc );
+          }else{
+            NodeListMap::iterator lbl_i = d_labels.find( eqc );
+            if( lbl_i != d_labels.end() ){
+              NodeList* lbl = (*lbl_i).second;
+              for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
+                Trace( c ) << *j << " ";
+              }
+            }
+          }
+          Trace( c ) << std::endl;
+        }else{
+          Trace( c ) << "   Constructor : " << ei->d_constructor.get() << std::endl;
+        }
+        Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl;
+      }
+    }
+    ++eqcs_i;
+  }
+}