added (temporary) support for ensuring that all ambiguously typed constructor nodes created internally are given a type ascription

7 files changed, 117 insertions, 71 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index b493b8c41..b4ff7e135 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -75,11 +75,18 @@ public:
                                    << std::endl;
         return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
       } else {
+        TNode gt = in.getType().mkGroundTerm();
+        TypeNode gtt = gt.getType();
+        Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
+        if( !gtt.isInstantiatedDatatype() ){
+          gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, 
+                                                NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
+        }
         Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
                                    << "Rewrite trivial selector " << in
                                    << " to distinguished ground term "
                                    << in.getType().mkGroundTerm() << std::endl;
-        return RewriteResponse(REWRITE_DONE,in.getType().mkGroundTerm() );
+        return RewriteResponse(REWRITE_DONE,gt );
       }
     }
 
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index a11990075..1cdefa60b 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -50,7 +50,7 @@ cardinality DATATYPE_TYPE \
     "util/datatype.h"
 well-founded DATATYPE_TYPE \
     "%TYPE%.getConst<Datatype>().isWellFounded()" \
-    "%TYPE%.getConst<Datatype>().mkGroundTerm()" \
+    "%TYPE%.getConst<Datatype>().mkGroundTerm(%TYPE%.toType())" \
     "util/datatype.h"
 
 operator PARAMETRIC_DATATYPE 1: "parametric datatype"
@@ -59,7 +59,7 @@ cardinality PARAMETRIC_DATATYPE \
     "util/datatype.h"
 well-founded PARAMETRIC_DATATYPE\
     "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
-    "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm()" \
+    "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm(%TYPE%.toType())" \
     "util/datatype.h"
 
 parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 2f0b82f7c..20668a5ff 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -474,6 +474,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
       d_inst_map[ te ] = true;
       //instantiate, add equality
       Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals );
+      val = doTypeAscription( val, te.getType() );      //IDT-param
       if( find( val ) != find( te ) ) {
         //build explaination
         NodeBuilder<> nb(kind::AND);
@@ -518,6 +519,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
 bool TheoryDatatypes::collapseSelector( Node t ) {
   if( !hasConflict() && t.getKind() == APPLY_SELECTOR ) {
     //collapse constructor
+    TypeNode retTyp = t.getType(); 
     TypeNode typ = t[0].getType();
     Node sel = t.getOperator();
     TypeNode selType = sel.getType();
@@ -531,7 +533,8 @@ bool TheoryDatatypes::collapseSelector( Node t ) {
         retNode = tmp[ Datatype::indexOf( sel.toExpr() ) ];
       } else {
         Debug("datatypes") << "Applied selector " << t << " to wrong constructor." << endl;
-        retNode = selType[1].mkGroundTerm();
+        retNode = doTypeAscription( retTyp.mkGroundTerm(), selType[1] );    //IDT-param
+        //retNode = selType[1].mkGroundTerm();
       }
       if( tmp!=t[0] ){
         t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp );
@@ -548,7 +551,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) {
       unsigned r;
       checkTester( tester, conflict, r );
       if( !conflict.isNull() ) {
-        Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl;
+        Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor. " << retTyp << endl;
         //conflict is c ^ tester, where conflict => false, but we want to say c => ~tester
         //must remove tester from conflict
         if( conflict.getKind()==kind::AND ){
@@ -574,7 +577,8 @@ 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 = selType[1].mkGroundTerm();
+        retNode = doTypeAscription( retTyp.mkGroundTerm(), retTyp );    //IDT-param
+        //retNode = selType[1].mkGroundTerm();
         Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
 
         d_em.addNode( neq, tester.notNode(), Reason::idt_collapse2 );
@@ -1044,3 +1048,14 @@ 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 1b9e357ed..9dfb8c818 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -178,6 +178,7 @@ 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 c9c76a15b..270313e0f 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -304,7 +304,7 @@ struct ConstructorProperties {
         i != i_end;
         ++i) {
       if(TypeNode::fromType((*i).getConstructor().getType()) == type) {
-        groundTerm = Node::fromExpr((*i).mkGroundTerm());
+        groundTerm = Node::fromExpr((*i).mkGroundTerm( type.toType() ));
         type.setAttribute(GroundTermAttr(), groundTerm);
         return groundTerm;
       }
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 31b68c9a4..4b84d2955 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -182,7 +182,7 @@ bool Datatype::isWellFounded() const throw(AssertionException) {
   return false;
 }
 
-Expr Datatype::mkGroundTerm() const throw(AssertionException) {
+Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -194,73 +194,78 @@ Expr Datatype::mkGroundTerm() const throw(AssertionException) {
   Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr();
   if(!groundTerm.isNull()) {
     Debug("datatypes") << "\nin cache: " << d_self << " => " << groundTerm << std::endl;
-    return groundTerm;
   } else {
     Debug("datatypes") << "\nNOT in cache: " << d_self << std::endl;
-  }
-
-  // look for a nullary ctor and use that
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    // prefer the nullary constructor
-    if((*i).getNumArgs() == 0) {
-      groundTerm = (*i).getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, (*i).getConstructor());
-      self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
-      Debug("datatypes") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl;
-      return groundTerm;
-    }
-  }
-
-  // No ctors are nullary, but we can't just use the first ctor
-  // because that might recurse!  In fact, since this datatype is
-  // well-founded by assumption, we know that at least one constructor
-  // doesn't contain a self-reference.  We search for that one and use
-  // it to construct the ground term, as that is often a simpler
-  // ground term (e.g. in a tree datatype, something like "(leaf 0)"
-  // is simpler than "(node (leaf 0) (leaf 0))".
-  //
-  // Of course this check doesn't always work, if the self-reference
-  // is through other Datatypes (or other non-Datatype types), but it
-  // does simplify a common case.  It requires a bit of extra work,
-  // but since we cache the results of these, it only happens once,
-  // ever, per Datatype.
-  //
-  // If the datatype is not actually well-founded, something below
-  // will throw an exception.
-  for(const_iterator i = begin(), i_end = end();
-      i != i_end;
-      ++i) {
-    Constructor::const_iterator j = (*i).begin(), j_end = (*i).end();
-    for(; j != j_end; ++j) {
-      SelectorType stype((*j).getSelector().getType());
-      if(stype.getDomain() == stype.getRangeType()) {
-        Debug("datatypes") << "self-reference, skip " << getName() << "::" << (*i).getName() << std::endl;
-        // the constructor contains a direct self-reference
-        break;
+    // look for a nullary ctor and use that
+    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());
+        self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
+        Debug("datatypes-gt") << "constructed nullary: " << getName() << " => " << groundTerm << std::endl;
       }
     }
+    // No ctors are nullary, but we can't just use the first ctor
+    // because that might recurse!  In fact, since this datatype is
+    // well-founded by assumption, we know that at least one constructor
+    // doesn't contain a self-reference.  We search for that one and use
+    // it to construct the ground term, as that is often a simpler
+    // ground term (e.g. in a tree datatype, something like "(leaf 0)"
+    // is simpler than "(node (leaf 0) (leaf 0))".
+    //
+    // Of course this check doesn't always work, if the self-reference
+    // is through other Datatypes (or other non-Datatype types), but it
+    // does simplify a common case.  It requires a bit of extra work,
+    // but since we cache the results of these, it only happens once,
+    // ever, per Datatype.
+    //
+    // If the datatype is not actually well-founded, something below
+    // will throw an exception.
+    for(const_iterator i = begin(), i_end = end();
+        i != i_end;
+        ++i) {
+      if( groundTerm.isNull() ){
+        Constructor::const_iterator j = (*i).begin(), j_end = (*i).end();
+        for(; j != j_end; ++j) {
+          SelectorType stype((*j).getSelector().getType());
+          if(stype.getDomain() == stype.getRangeType()) {
+            Debug("datatypes") << "self-reference, skip " << getName() << "::" << (*i).getName() << std::endl;
+            // the constructor contains a direct self-reference
+            break;
+          }
+        }
 
-    if(j == j_end && (*i).isWellFounded()) {
-      groundTerm = (*i).mkGroundTerm();
-      // Constructor::mkGroundTerm() doesn't ever return null when
-      // called from the outside.  But in recursive invocations, it
-      // can: say you have dt = a(one:dt) | b(two:INT), and you ask
-      // the "a" constructor for a ground term.  It asks "dt" for a
-      // ground term, which in turn asks the "a" constructor for a
-      // ground term!  Thus, even though "a" is a well-founded
-      // constructor, it cannot construct a ground-term by itself.  We
-      // have to skip past it, and we do that with a
-      // RecursionBreaker<> in Constructor::mkGroundTerm().  In the
-      // case of recursion, it returns null.
-      if(!groundTerm.isNull()) {
-        // we found a ground-term-constructing constructor!
-        self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
-        Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
-        return groundTerm;
+        if(j == j_end && (*i).isWellFounded()) {
+          groundTerm = (*i).mkGroundTerm( t );
+          // Constructor::mkGroundTerm() doesn't ever return null when
+          // called from the outside.  But in recursive invocations, it
+          // can: say you have dt = a(one:dt) | b(two:INT), and you ask
+          // the "a" constructor for a ground term.  It asks "dt" for a
+          // ground term, which in turn asks the "a" constructor for a
+          // ground term!  Thus, even though "a" is a well-founded
+          // constructor, it cannot construct a ground-term by itself.  We
+          // have to skip past it, and we do that with a
+          // RecursionBreaker<> in Constructor::mkGroundTerm().  In the
+          // case of recursion, it returns null.
+          if(!groundTerm.isNull()) {
+            // we found a ground-term-constructing constructor!
+            self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
+            Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
+          }
+        }
       }
     }
   }
-  // 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!");
+  if( groundTerm.isNull() ){
+    // 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;
+  }
 }
 
 DatatypeType Datatype::getDatatypeType() const throw(AssertionException) {
@@ -593,9 +598,10 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) {
   return true;
 }
 
-Expr Datatype::Constructor::mkGroundTerm() 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);
 
@@ -618,8 +624,18 @@ Expr Datatype::Constructor::mkGroundTerm() const throw(AssertionException) {
   groundTerms.push_back(getConstructor());
 
   // for each selector, get a ground term
+  Assert( t.isDatatype() );
+  std::vector< Type > instTypes; 
+  std::vector< Type > paramTypes = DatatypeType(t).getDatatype().getParameters();
+  if( DatatypeType(t).isParametric() ){
+    instTypes = DatatypeType(t).getParamTypes();
+  }
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    groundTerms.push_back(SelectorType((*i).getSelector().getType()).getRangeType().mkGroundTerm());
+    Type selType = SelectorType((*i).getSelector().getType()).getRangeType();
+    if( DatatypeType(t).isParametric() ){
+      selType = selType.substitute( paramTypes, instTypes );
+    }
+    groundTerms.push_back(selType.mkGroundTerm());
   }
 
   groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 90dd8775f..3506616d6 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -297,7 +297,7 @@ public:
      * constructor must be both resolved and well-founded, or else an
      * exception is thrown.
      */
-    Expr mkGroundTerm() const throw(AssertionException);
+    Expr mkGroundTerm( Type t ) const throw(AssertionException);
 
     /**
      * Returns true iff this Datatype constructor has already been
@@ -375,6 +375,9 @@ public:
   /** Get parameter */
   inline Type getParameter( unsigned int i ) const;
 
+  /** Get parameters */
+  inline std::vector<Type> getParameters() const;
+
   /**
    * Return the cardinality of this datatype (the sum of the
    * cardinalities of its constructors).  The Datatype must be
@@ -401,7 +404,7 @@ public:
    * Datatype must be both resolved and well-founded, or else an
    * exception is thrown.
    */
-  Expr mkGroundTerm() const throw(AssertionException);
+  Expr mkGroundTerm( Type t ) const throw(AssertionException);
 
   /**
    * Get the DatatypeType associated to this Datatype.  Can only be
@@ -532,6 +535,10 @@ inline Type Datatype::getParameter( unsigned int i ) const {
   return d_params[i];
 }
 
+inline std::vector<Type> Datatype::getParameters() const {
+  return d_params;
+}
+
 inline bool Datatype::operator!=(const Datatype& other) const throw() {
   return !(*this == other);
 }