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)).

2 files changed, 20 insertions, 8 deletions

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.