fixed various bugs related to ambiguous parametric datatype constructors, parametric datatype versions of paper benchmarks are now working

3 files changed, 44 insertions, 34 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 20668a5ff..6aed9e9fa 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -120,7 +120,7 @@ void TheoryDatatypes::check(Effort e) {
   while(!done()) {
     Node assertion = get();
     if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles")
-        || Debug.isOn("datatypes-debug-pf") ) {
+        || Debug.isOn("datatypes-debug-pf") || Debug.isOn("datatypes-conflict") ) {
       cout << "*** TheoryDatatypes::check(): " << assertion << endl;
       d_currAsserts.push_back( assertion );
     }
@@ -211,7 +211,10 @@ void TheoryDatatypes::check(Effort e) {
     //if there is now a conflict
     if( hasConflict() ) {
       Debug("datatypes-conflict") << "Constructing conflict..." << endl;
-      Debug("datatypes-conflict") << d_cc << std::endl;
+      for( int i=0; i<(int)d_currAsserts.size(); i++ ) {
+        Debug("datatypes-conflict") << "currAsserts[" << i << "] = " << d_currAsserts[i] << endl;
+      }
+      //Debug("datatypes-conflict") << d_cc << std::endl;
       Node conflict = d_em.getConflict();
       if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || 
           Debug.isOn("datatypes-cycles") || Debug.isOn("datatypes-conflict") ){
@@ -472,9 +475,19 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
     }
     if( cn.isFinite() || foundSel ) {
       d_inst_map[ te ] = true;
-      //instantiate, add equality
       Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals );
-      val = doTypeAscription( val, te.getType() );      //IDT-param
+      //instantiate, add equality
+      if( val.getType()!=te.getType() ){ //IDT-param
+        Assert( Datatype::datatypeOf( cons.toExpr() ).isParametric() );
+        Debug("datatypes-gt") << "Inst: ambiguous type for " << cons << ", ascribe to " << te.getType() << std::endl;
+        const Datatype::Constructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())];
+        Debug("datatypes-gt") << "constructor is " << dtc << std::endl;
+        Type tspec = dtc.getSpecializedConstructorType(te.getType().toType());
+        Debug("datatypes-gt") << "tpec is " << tspec << std::endl;
+        selectorVals[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, 
+                                            NodeManager::currentNM()->mkConst(AscriptionType(tspec)), cons);
+        val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals );
+      }
       if( find( val ) != find( te ) ) {
         //build explaination
         NodeBuilder<> nb(kind::AND);
@@ -533,8 +546,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) {
         retNode = tmp[ Datatype::indexOf( sel.toExpr() ) ];
       } else {
         Debug("datatypes") << "Applied selector " << t << " to wrong constructor." << endl;
-        retNode = doTypeAscription( retTyp.mkGroundTerm(), selType[1] );    //IDT-param
-        //retNode = selType[1].mkGroundTerm();
+        retNode = retTyp.mkGroundTerm();    //IDT-param
       }
       if( tmp!=t[0] ){
         t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp );
@@ -577,8 +589,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) {
           tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), t[0] );
           d_em.addNode( tester.notNode(), exp, Reason::idt_tcong );
         }
-        retNode = doTypeAscription( retTyp.mkGroundTerm(), retTyp );    //IDT-param
-        //retNode = selType[1].mkGroundTerm();
+        retNode = retTyp.mkGroundTerm();    //IDT-param
         Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
 
         d_em.addNode( neq, tester.notNode(), Reason::idt_collapse2 );
@@ -1048,14 +1059,3 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on,
   }
   return false;
 }
-
-Node TheoryDatatypes::doTypeAscription( Node t, TypeNode typ )
-{
-  TypeNode tt = t.getType();
-  if( (tt.isDatatype() || tt.isParametricDatatype()) && !tt.isInstantiatedDatatype() ){
-    return NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, 
-                                            NodeManager::currentNM()->mkConst(AscriptionType(typ.toType())), t);
-  }else{
-    return t;
-  }
-}
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 9dfb8c818..1b9e357ed 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -178,7 +178,6 @@ private:
   bool searchForCycle( Node n, Node on,
                        std::map< Node, bool >& visited,
                        NodeBuilder<>& explanation );
-  Node doTypeAscription( Node t, TypeNode typ );
 };/* class TheoryDatatypes */
 
 inline bool TheoryDatatypes::hasConflict() { 
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 5ff01924b..578de69a2 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -163,22 +163,33 @@ struct DatatypeAscriptionTypeRule {
     TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
     if(check) {
       TypeNode childType = n[0].getType(check);
-      if(!t.getKind() == kind::DATATYPE_TYPE) {
-        throw TypeCheckingExceptionPrivate(n, "bad type for datatype type ascription");
+      //if(!t.getKind() == kind::DATATYPE_TYPE) {
+      //  throw TypeCheckingExceptionPrivate(n, "bad type for datatype type ascription");
+      //}
+      //DatatypeType dt = DatatypeType(childType.toType());
+      //if( dt.isParametric() ){
+      //  Debug("typecheck-idt") << "typecheck parameterized ascription: " << n << std::endl;
+      //  Matcher m( dt );
+      //  if( !m.doMatching( childType, t ) ){
+      //    throw TypeCheckingExceptionPrivate(n, "matching failed for type ascription argument of parameterized datatype");
+      //  }
+      //}else{
+      //  Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
+      //  if(t != childType) {
+      //    throw TypeCheckingExceptionPrivate(n, "bad type for type ascription argument");
+      //  }
+      //}
+
+      Matcher m;
+      if( childType.getKind() == kind::CONSTRUCTOR_TYPE ){
+        m.addTypesFromDatatype( ConstructorType(childType.toType()).getRangeType() );
+      }else if( childType.getKind() == kind::DATATYPE_TYPE ){
+        m.addTypesFromDatatype( DatatypeType(childType.toType()) );
       }
-      DatatypeType dt = DatatypeType(childType.toType());
-      if( dt.isParametric() ){
-        Debug("typecheck-idt") << "typecheck parameterized ascription: " << n << std::endl;
-        Matcher m( dt );
-        if( !m.doMatching( childType, t ) ){
-          throw TypeCheckingExceptionPrivate(n, "matching failed for type ascription argument of parameterized datatype");
-        }
-      }else{
-        Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
-        if(t != childType) {
-          throw TypeCheckingExceptionPrivate(n, "bad type for type ascription argument");
-        }
+      if( !m.doMatching( childType, t ) ){
+        throw TypeCheckingExceptionPrivate(n, "matching failed for type ascription argument of parameterized datatype");
       }
+
     }
     return t;
   }