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

6 files changed, 80 insertions, 57 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index d6165b435..cd4c66664 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1467,7 +1467,7 @@ postfixTerm[CVC4::Expr& f]
           Expr e = f.getOperator();
           const Datatype::Constructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)];
           v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
-                               MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator()[0] ));
+                               MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() ));
           v.insert(v.end(), f.begin(), f.end());
           f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
         } else {
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;
   }
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index a06a7c2b5..926f31847 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -52,6 +52,7 @@ typedef expr::Attribute<expr::attr::DatatypeWellFoundedComputedTag, bool> Dataty
 typedef expr::Attribute<expr::attr::DatatypeGroundTermTag, Node> DatatypeGroundTermAttr;
 
 const Datatype& Datatype::datatypeOf(Expr item) {
+  ExprManagerScope ems(item);
   TypeNode t = Node::fromExpr(item).getType();
   switch(t.getKind()) {
   case kind::CONSTRUCTOR_TYPE:
@@ -65,14 +66,19 @@ const Datatype& Datatype::datatypeOf(Expr item) {
 }
 
 size_t Datatype::indexOf(Expr item) {
+  ExprManagerScope ems(item);
   AssertArgument(item.getType().isConstructor() ||
                  item.getType().isTester() ||
                  item.getType().isSelector(),
                  item,
                  "arg must be a datatype constructor, selector, or tester");
   TNode n = Node::fromExpr(item);
-  Assert(n.hasAttribute(DatatypeIndexAttr()));
-  return n.getAttribute(DatatypeIndexAttr());
+  if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
+    return indexOf( item[0] );
+  }else{
+    Assert(n.hasAttribute(DatatypeIndexAttr()));
+    return n.getAttribute(DatatypeIndexAttr());
+  }
 }
 
 void Datatype::resolve(ExprManager* em,
@@ -201,7 +207,8 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
     for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
       // prefer the nullary constructor
       if( groundTerm.isNull() && (*i).getNumArgs() == 0) {
-        groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor());
+        groundTerm = d_constructors[indexOf((*i).getConstructor())].mkGroundTerm( t );
+        //groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor());
         self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
         Debug("datatypes-gt") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl;
       }
@@ -261,10 +268,6 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
     // if we get all the way here, we aren't well-founded
     CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!");
   }else{
-    if( t!=groundTerm.getType() ){
-      groundTerm = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                                    NodeManager::currentNM()->mkConst(AscriptionType(t)), groundTerm).toExpr();
-    }
     return groundTerm;
   }
 }
@@ -522,7 +525,7 @@ Type Datatype::Constructor::getSpecializedConstructorType(Type returnType) const
   vector<Type> subst;
   m.getMatches(subst);
   vector<Type> params = dt.getParameters();
-  return d_constructor.getType().substitute(subst, params);
+  return d_constructor.getType().substitute(params, subst);
 }
 
 Expr Datatype::Constructor::getTester() const {
@@ -615,7 +618,6 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) {
 Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
-  Debug("datatypes-gt") << "mkGroundTerm " << t << std::endl;
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
 
@@ -652,8 +654,17 @@ Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionExceptio
     }
     groundTerms.push_back(selType.mkGroundTerm());
   }
-
+  
   groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
+  if( groundTerm.getType()!=t ){
+    Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
+    //type is ambiguous, must apply type ascription
+    Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
+    groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
+                       getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))),
+                       groundTerms[0]);
+    groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
+  }
   self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
   return groundTerm;
 }
diff --git a/src/util/matcher.h b/src/util/matcher.h
index 2c55309d3..5dc511bc2 100644
--- a/src/util/matcher.h
+++ b/src/util/matcher.h
@@ -38,6 +38,11 @@ private:
 public:
   Matcher(){}
   Matcher( DatatypeType dt ){
+    addTypesFromDatatype( dt );
+  }
+  ~Matcher(){}
+
+  void addTypesFromDatatype( DatatypeType dt ){
     std::vector< Type > argTypes = dt.getParamTypes();
     addTypes( argTypes );
     Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl;
@@ -48,8 +53,6 @@ public:
       }
     }
   }
-  ~Matcher(){}
-
   void addType( Type t ){
     d_types.push_back( TypeNode::fromType( t ) );
     d_match.push_back( TypeNode::null() );
@@ -60,25 +63,24 @@ public:
     }
   }
 
-  bool doMatching( TypeNode base, TypeNode match ){
-    Debug("typecheck-idt") << "doMatching() : " << base << " : " << match << std::endl;
-    std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), base );
+  bool doMatching( TypeNode pattern, TypeNode tn ){
+    Debug("typecheck-idt") << "doMatching() : " << pattern << " : " << tn << std::endl;
+    std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), pattern );
     if( i!=d_types.end() ){
       int index = i - d_types.begin();
-      Debug("typecheck-idt") << "++ match on " << index << " : " << d_match[index] << std::endl;
-      if( !d_match[index].isNull() && d_match[index]!=match ){
+      if( !d_match[index].isNull() && d_match[index]!=tn ){
         return false;
       }else{
-        d_match[ i - d_types.begin() ] = match;
+        d_match[ i - d_types.begin() ] = tn;
         return true;
       }
-    }else if( base==match ){
+    }else if( pattern==tn ){
       return true;
-    }else if( base.getKind()!=match.getKind() || base.getNumChildren()!=match.getNumChildren() ){
+    }else if( pattern.getKind()!=tn.getKind() || pattern.getNumChildren()!=tn.getNumChildren() ){
       return false;
     }else{
-      for( int i=0; i<(int)base.getNumChildren(); i++ ){
-        if( !doMatching( base[i], match[i] ) ){
+      for( int i=0; i<(int)pattern.getNumChildren(); i++ ){
+        if( !doMatching( pattern[i], tn[i] ) ){
           return false;
         }
       }