Remove unhandled subtypes (#1098)

* Remove unhandled subtypes, which consequently makes typing rules uniformly stricter based on weakening the subtype relation. Ensure coercions in the smt2 and cvc parser for Real decimal constants whose type is Integer. Ensure type annotations are computed during preRewrite to ensure rewriting (which does not preserve types) does not impact term construction for parametric datatypes. This fixes issue #1048 (we now give an type exception).

* Update unit test for parametric datatypes to reflect new subtyping relation.

* Remove deprecated test.

* Make array construction for lambdas work with new subtype relations to handle lambdas like (lambda ((x Int) (y Int)) (ite (= x 0) 0.5 0.0)).

7 files changed, 82 insertions, 156 deletions

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index a4ab2f3b7..c06691d08 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -106,50 +106,11 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
       return false;
     }
   }
-  if(isTuple() && t.isTuple()) {
-    const Datatype& dt1 = getDatatype();
-    const Datatype& dt2 = t.getDatatype();
-    if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){
-      return false;
-    }
-    // r1's fields must be subtypes of r2's, in order
-    for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
-      if( !dt1[0][i].getRangeType().isSubtypeOf( dt2[0][i].getRangeType() ) ){
-        return false;
-      }
-    }
-    return true;
-  }else if( t.isRecord() && t.isRecord() ){
-    //records are not subtypes of each other in current implementation
-  }
-  if(isFunction()) {
-    // A function is a subtype of another if the args are the same type, and
-    // the return type is a subtype of the other's.  This is enough for now
-    // (and it's necessary for model generation, since a Real-valued function
-    // might return a constant Int and thus the model value is typed differently).
-    return t.isFunction() && getArgTypes() == t.getArgTypes() && getRangeType().isSubtypeOf(t.getRangeType());
-  }
-  if(isParametricDatatype() && t.isParametricDatatype()) {
-    Assert(getKind() == kind::PARAMETRIC_DATATYPE);
-    Assert(t.getKind() == kind::PARAMETRIC_DATATYPE);
-    if((*this)[0] != t[0] || getNumChildren() != t.getNumChildren()) {
-      return false;
-    }
-    for(size_t i = 1; i < getNumChildren(); ++i) {
-      if(!((*this)[i].isSubtypeOf(t[i]))) {
-        return false;
-      }
-    }
-    return true;
-  }
   if(isSet() && t.isSet()) {
     return getSetElementType().isSubtypeOf(t.getSetElementType());
   }
-  if(isArray() && t.isArray()) {
-    //reverse for index type
-    return t.getArrayIndexType().isSubtypeOf(getArrayIndexType()) && 
-           getArrayConstituentType().isSubtypeOf(t.getArrayConstituentType());
-  }
+  // this should only return true for types T1, T2 where we handle equalities between T1 and T2
+  // (more cases go here, if we want to support such cases)
   return false;
 }
 
@@ -160,39 +121,9 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   if(isSubtypeOf(NodeManager::currentNM()->realType())) {
     return t.isSubtypeOf(NodeManager::currentNM()->realType());
   }
-  if(isTuple() && t.isTuple()) {
-    const Datatype& dt1 = getDatatype();
-    const Datatype& dt2 = t.getDatatype();
-    if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){
-      return false;
-    }
-    // r1's fields must be subtypes of r2's, in order
-    for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
-      if( !dt1[0][i].getRangeType().isComparableTo( dt2[0][i].getRangeType() ) ){
-        return false;
-      }
-    }
-    return true;
-  //}else if( isRecord() && t.isRecord() ){
-    //record types are incomparable in current implementation
-  } else if(isParametricDatatype() && t.isParametricDatatype()) {
-    Assert(getKind() == kind::PARAMETRIC_DATATYPE);
-    Assert(t.getKind() == kind::PARAMETRIC_DATATYPE);
-    if((*this)[0] != t[0] || getNumChildren() != t.getNumChildren()) {
-      return false;
-    }
-    for(size_t i = 1; i < getNumChildren(); ++i) {
-      if(!((*this)[i].isComparableTo(t[i]))) {
-        return false;
-      }
-    }
-    return true;
-  } else if(isSet() && t.isSet()) {
+  if(isSet() && t.isSet()) {
     return getSetElementType().isComparableTo(t.getSetElementType());
   }
-  if(isArray() && t.isArray()) {
-    return getArrayIndexType().isComparableTo(t.getArrayIndexType()) && getArrayConstituentType().isComparableTo(t.getArrayConstituentType());
-  }
   return false;
 }
 
@@ -361,9 +292,11 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
   case kind::CONSTRUCTOR_TYPE:
   case kind::SELECTOR_TYPE:
   case kind::TESTER_TYPE:
-    return TypeNode();
   case kind::FUNCTION_TYPE:
-    return TypeNode(); // Not sure if this is right
+  case kind::ARRAY_TYPE:
+  case kind::DATATYPE_TYPE:
+  case kind::PARAMETRIC_DATATYPE:
+    return TypeNode();
   case kind::SET_TYPE: {
     // take the least common subtype of element types
     TypeNode elementType;
@@ -373,54 +306,9 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
       return TypeNode();
     }
   }
-  case kind::ARRAY_TYPE: {
-    TypeNode indexType, elementType;
-    if(t1.isArray() &&
-       ! (indexType = commonTypeNode(t0[0], t1[0], !isLeast)).isNull() && 
-       ! (elementType = commonTypeNode(t0[1], t1[1], isLeast)).isNull() ) {
-      return NodeManager::currentNM()->mkArrayType(indexType, elementType);
-    } else {
-      return TypeNode();
-    }
-  }
   case kind::SEXPR_TYPE:
     Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
     return TypeNode();
-  case kind::DATATYPE_TYPE:
-    if( t0.isTuple() && t1.isTuple() ){
-      const Datatype& dt1 = t0.getDatatype();
-      const Datatype& dt2 = t1.getDatatype();
-      if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
-        std::vector< TypeNode > lc_types;
-        for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
-          TypeNode tc = commonTypeNode( TypeNode::fromType( dt1[0][i].getRangeType() ), TypeNode::fromType( dt2[0][i].getRangeType() ), isLeast );
-          if( tc.isNull() ){
-            return tc;
-          }else{
-            lc_types.push_back( tc );
-          }
-        }
-        return NodeManager::currentNM()->mkTupleType( lc_types );
-      }
-    }
-    //else if( t0.isRecord() && t1.isRecord() ){
-      //record types are not related in current implementation
-    //}
-    // otherwise no common ancestor
-    return TypeNode();
-  case kind::PARAMETRIC_DATATYPE: {
-    if(!t1.isParametricDatatype()) {
-      return TypeNode();
-    }
-    if(t0[0] != t1[0] || t0.getNumChildren() != t1.getNumChildren()) {
-      return TypeNode();
-    }
-    vector<Type> v;
-    for(size_t i = 1; i < t0.getNumChildren(); ++i) {
-      v.push_back(commonTypeNode(t0[i], t1[i], isLeast).toType());
-    }
-    return TypeNode::fromType(t0[0].getDatatype().getDatatypeType(v));
-  }
   default:
     Unimplemented("don't have a commonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
     return TypeNode();
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 6cc5c29a4..d0324cc45 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2104,7 +2104,12 @@ simpleTerm[CVC4::Expr& f]
     /* syntactic predicate: never match INTEGER.DIGIT as an integer and a dot!
      * This is a rational constant!  Otherwise the parser interprets it as a tuple
      * selector! */
-  | DECIMAL_LITERAL { f = MK_CONST(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
+  | DECIMAL_LITERAL { 
+      f = MK_CONST(AntlrInput::tokenToRational($DECIMAL_LITERAL));
+      if(f.getType().isInteger()) {
+        f = MK_EXPR(kind::TO_REAL, f);
+      } 
+    }
   | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
     /* bitvector literals */
   | HEX_LITERAL
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 86c0b3126..92f6b36d8 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2254,7 +2254,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | DECIMAL_LITERAL
     { // FIXME: This doesn't work because an SMT rational is not a
       // valid GMP rational string
-      expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
+      expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); 
+      if(expr.getType().isInteger()) {
+        //must cast to Real to ensure correct type is passed to parametric type constructors
+        expr = MK_EXPR(kind::TO_REAL, expr);
+      }  
+    }
 
   | LPAREN_TOK INDEX_TOK 
     ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL 
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 57249e181..4948216e5 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -150,7 +150,7 @@ Node TheoryBuiltinRewriter::getLambdaForArrayRepresentation( TNode a, TNode bvl
   }
 }
 
-Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqConst ){
+Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec( TNode n, bool reqConst, TypeNode retType ){
   Assert( n.getKind()==kind::LAMBDA );
   Trace("builtin-rewrite-debug") << "Get array representation for : " << n << std::endl;
 
@@ -165,7 +165,6 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo
   }
 
   Trace("builtin-rewrite-debug2") << "  process body..." << std::endl;
-  TypeNode retType;
   std::vector< Node > conds;
   std::vector< Node > vals;
   Node curr = n[1];
@@ -214,7 +213,7 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo
     if( !curr_index.isNull() ){
       if( !rec_bvl.isNull() ){
         curr_val = NodeManager::currentNM()->mkNode( kind::LAMBDA, rec_bvl, curr_val );
-        curr_val = getArrayRepresentationForLambda( curr_val, reqConst );
+        curr_val = getArrayRepresentationForLambdaRec( curr_val, reqConst, retType );
         if( curr_val.isNull() ){
           Trace("builtin-rewrite-debug2") << "  ...non-constant value." << std::endl;
           return Node::null();
@@ -228,18 +227,22 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo
     conds.push_back( curr_index );
     vals.push_back( curr_val );
     TypeNode vtype = curr_val.getType();
-    retType = retType.isNull() ? vtype : TypeNode::leastCommonTypeNode( retType, vtype );
     //recurse
     curr = next;
   }
   if( !rec_bvl.isNull() ){
     curr = NodeManager::currentNM()->mkNode( kind::LAMBDA, rec_bvl, curr );
-    curr = getArrayRepresentationForLambda( curr );
+    curr = getArrayRepresentationForLambdaRec( curr, reqConst, retType );
   }
   if( !curr.isNull() && curr.isConst() ){
-    TypeNode ctype = curr.getType();
-    retType = retType.isNull() ? ctype : TypeNode::leastCommonTypeNode( retType, ctype );
-    TypeNode array_type = NodeManager::currentNM()->mkArrayType( first_arg.getType(), retType );
+    // compute the return type
+    TypeNode array_type = retType;
+    for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+      unsigned index = (n[0].getNumChildren()-1)-i;
+      array_type = NodeManager::currentNM()->mkArrayType( n[0][index].getType(), array_type );
+    }
+    Trace("builtin-rewrite-debug2") << "  make array store all " << curr.getType() << " annotated : " << array_type << std::endl;
+    Assert( curr.getType().isSubtypeOf( array_type.getArrayConstituentType() ) );
     curr = NodeManager::currentNM()->mkConst(ArrayStoreAll(((ArrayType)array_type.toType()), curr.toExpr()));
     Trace("builtin-rewrite-debug2") << "  build array..." << std::endl;
     // can only build if default value is constant (since array store all must be constant)
@@ -257,6 +260,13 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqCo
   }
 }
 
+Node TheoryBuiltinRewriter::getArrayRepresentationForLambda( TNode n, bool reqConst ){
+  Assert( n.getKind()==kind::LAMBDA );
+  // must carry the overall return type to deal with cases like (lambda ((x Int)(y Int)) (ite (= x _) 0.5 0.0)),
+  //  where the inner construction for the else case about should be (arraystoreall (Array Int Real) 0.0)
+  return getArrayRepresentationForLambdaRec( n, reqConst, n[1].getType() );
+}
+
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index d9ae5b447..3667cf159 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -59,6 +59,8 @@ private:
   /** recursive helper for getLambdaForArrayRepresentation */
   static Node getLambdaForArrayRepresentationRec( TNode a, TNode bvl, unsigned bvlIndex, 
                                                   std::unordered_map< TNode, Node, TNodeHashFunction >& visited );
+  /** recursive helper for getArrayRepresentationForLambda */
+  static Node getArrayRepresentationForLambdaRec( TNode n, bool reqConst, TypeNode retType );
 public:
   /** 
    * Given an array constant a, returns a lambda expression that it corresponds to, with bound variable list bvl. 
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 025fe0349..49e8a6888 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -36,29 +36,11 @@ public:
     Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl;
 
     if(in.getKind() == kind::APPLY_CONSTRUCTOR ){
+      /*
       TypeNode tn = in.getType();
       Type t = tn.toType();
       DatatypeType dt = DatatypeType(t);
-      //check for parametric datatype constructors
-      // to ensure a normal form, all parameteric datatype constructors must have a type ascription
-      if( dt.isParametric() ){
-        if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){
-          Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl;
-          Node op = in.getOperator();
-          //get the constructor object
-          const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
-          //create ascribed constructor type
-          Node tc = NodeManager::currentNM()->mkConst(AscriptionType(dtc.getSpecializedConstructorType(t)));
-          Node op_new = NodeManager::currentNM()->mkNode( kind::APPLY_TYPE_ASCRIPTION, tc, op );
-          //make new node
-          std::vector< Node > children;
-          children.push_back( op_new );
-          children.insert( children.end(), in.begin(), in.end() );
-          Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
-          Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl;
-          return RewriteResponse(REWRITE_DONE, inr);
-        }
-      }
+      // enable this rewrite if we support subtypes of tuples
       if( tn.isTuple() ){
         Node nn = normalizeTupleConstructorApp( in );
         if( nn!=in ){
@@ -66,6 +48,7 @@ public:
           return RewriteResponse(REWRITE_AGAIN_FULL, nn);
         }
       }
+      */
       if( in.isConst() ){
         Trace("datatypes-rewrite-debug") << "Normalizing constant " << in << std::endl;
         Node inn = normalizeConstant( in );
@@ -241,6 +224,33 @@ public:
 
   static RewriteResponse preRewrite(TNode in) {
     Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl;
+    //must prewrite to apply type ascriptions since rewriting does not preserve types
+    if(in.getKind() == kind::APPLY_CONSTRUCTOR ){
+      TypeNode tn = in.getType();
+      Type t = tn.toType();
+      DatatypeType dt = DatatypeType(t);
+      
+      //check for parametric datatype constructors
+      // to ensure a normal form, all parameteric datatype constructors must have a type ascription
+      if( dt.isParametric() ){
+        if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){
+          Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl;
+          Node op = in.getOperator();
+          //get the constructor object
+          const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
+          //create ascribed constructor type
+          Node tc = NodeManager::currentNM()->mkConst(AscriptionType(dtc.getSpecializedConstructorType(t)));
+          Node op_new = NodeManager::currentNM()->mkNode( kind::APPLY_TYPE_ASCRIPTION, tc, op );
+          //make new node
+          std::vector< Node > children;
+          children.push_back( op_new );
+          children.insert( children.end(), in.begin(), in.end() );
+          Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
+          Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl;
+          return RewriteResponse(REWRITE_DONE, inr);
+        }
+      }
+    }
     return RewriteResponse(REWRITE_DONE, in);
   }
 
@@ -251,10 +261,11 @@ public:
     Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl;
     if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
       if( n1.getOperator() != n2.getOperator()) {
-        if( n1.getNumChildren() != n2.getNumChildren() || !n1.getType().isTuple() || !n2.getType().isTuple() ){
-          Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
-          return true;
-        }
+        //enable this check if we support subtypes with tuples
+        //if( n1.getNumChildren() != n2.getNumChildren() || !n1.getType().isTuple() || !n2.getType().isTuple() ){
+        Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
+        return true;
+        //}
       }
       Assert( n1.getNumChildren() == n2.getNumChildren() );
       for( unsigned i=0; i<n1.getNumChildren(); i++ ) {
@@ -649,9 +660,11 @@ public:
   static Node normalizeConstant( Node n ){
     TypeNode tn = n.getType();
     if( tn.isDatatype() ){
-      if( tn.isTuple() ){
-        return normalizeTupleConstructorApp( n );
-      }else if( tn.isCodatatype() ){
+      // enable this if we support subtyping with tuples
+      //if( tn.isTuple() ){
+      //  return normalizeTupleConstructorApp( n );
+      //} 
+      if( tn.isCodatatype() ){
         return normalizeCodatatypeConstant( n );
       }else{
         std::vector< Node > children;
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index e787ebc49..d6045404d 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -101,6 +101,8 @@ struct DatatypeConstructorTypeRule {
         return false;
       }
     }
+    //if we support subtyping for tuples, enable this
+    /*
     //check whether it is in normal form?
     TypeNode tn = n.getType();
     if( tn.isTuple() ){
@@ -114,6 +116,7 @@ struct DatatypeConstructorTypeRule {
     }else if( tn.isCodatatype() ){
       //TODO?
     }
+    */
     return true;
   }
 }; /* struct DatatypeConstructorTypeRule */