From ab2924e8a6cc34f29167b1ff50273d59dd7a6707 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Sep 2017 14:12:22 -0500 Subject: 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)). --- test/unit/util/datatype_black.h | 63 +++++++++++++++++++---------------------- 1 file changed, 29 insertions(+), 34 deletions(-) (limited to 'test/unit/util') diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 9f26312dc..15c380c31 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -363,60 +363,55 @@ public: TS_ASSERT_DIFFERS(pairIntInt, pairRealInt); TS_ASSERT_DIFFERS(pairIntReal, pairRealInt); - TS_ASSERT_EQUALS(pairRealReal.getBaseType(), pairRealReal); - TS_ASSERT_EQUALS(pairRealInt.getBaseType(), pairRealReal); - TS_ASSERT_EQUALS(pairIntReal.getBaseType(), pairRealReal); - TS_ASSERT_EQUALS(pairIntInt.getBaseType(), pairRealReal); - TS_ASSERT(pairRealReal.isComparableTo(pairRealReal)); - TS_ASSERT(pairIntReal.isComparableTo(pairRealReal)); - TS_ASSERT(pairRealInt.isComparableTo(pairRealReal)); - TS_ASSERT(pairIntInt.isComparableTo(pairRealReal)); - TS_ASSERT(pairRealReal.isComparableTo(pairRealInt)); - TS_ASSERT(pairIntReal.isComparableTo(pairRealInt)); + TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal)); + TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal)); + TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal)); + TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt)); + TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt)); TS_ASSERT(pairRealInt.isComparableTo(pairRealInt)); - TS_ASSERT(pairIntInt.isComparableTo(pairRealInt)); - TS_ASSERT(pairRealReal.isComparableTo(pairIntReal)); + TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt)); + TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal)); TS_ASSERT(pairIntReal.isComparableTo(pairIntReal)); - TS_ASSERT(pairRealInt.isComparableTo(pairIntReal)); - TS_ASSERT(pairIntInt.isComparableTo(pairIntReal)); - TS_ASSERT(pairRealReal.isComparableTo(pairIntInt)); - TS_ASSERT(pairIntReal.isComparableTo(pairIntInt)); - TS_ASSERT(pairRealInt.isComparableTo(pairIntInt)); + TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal)); + TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal)); + TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt)); + TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt)); + TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt)); TS_ASSERT(pairIntInt.isComparableTo(pairIntInt)); TS_ASSERT(pairRealReal.isSubtypeOf(pairRealReal)); - TS_ASSERT(pairIntReal.isSubtypeOf(pairRealReal)); - TS_ASSERT(pairRealInt.isSubtypeOf(pairRealReal)); - TS_ASSERT(pairIntInt.isSubtypeOf(pairRealReal)); + TS_ASSERT(!pairIntReal.isSubtypeOf(pairRealReal)); + TS_ASSERT(!pairRealInt.isSubtypeOf(pairRealReal)); + TS_ASSERT(!pairIntInt.isSubtypeOf(pairRealReal)); TS_ASSERT(!pairRealReal.isSubtypeOf(pairRealInt)); TS_ASSERT(!pairIntReal.isSubtypeOf(pairRealInt)); TS_ASSERT(pairRealInt.isSubtypeOf(pairRealInt)); - TS_ASSERT(pairIntInt.isSubtypeOf(pairRealInt)); + TS_ASSERT(!pairIntInt.isSubtypeOf(pairRealInt)); TS_ASSERT(!pairRealReal.isSubtypeOf(pairIntReal)); TS_ASSERT(pairIntReal.isSubtypeOf(pairIntReal)); TS_ASSERT(!pairRealInt.isSubtypeOf(pairIntReal)); - TS_ASSERT(pairIntInt.isSubtypeOf(pairIntReal)); + TS_ASSERT(!pairIntInt.isSubtypeOf(pairIntReal)); TS_ASSERT(!pairRealReal.isSubtypeOf(pairIntInt)); TS_ASSERT(!pairIntReal.isSubtypeOf(pairIntInt)); TS_ASSERT(!pairRealInt.isSubtypeOf(pairIntInt)); TS_ASSERT(pairIntInt.isSubtypeOf(pairIntInt)); TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealReal)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealReal)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealReal)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealReal)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealInt)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealInt)).toType(), pairRealReal); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealReal)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealReal)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealReal)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealInt)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealInt)).isNull()); TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealInt)).toType(), pairRealInt); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealInt)).toType(), pairRealInt); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntReal)).toType(), pairRealReal); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealInt)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntReal)).isNull()); TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntReal)).toType(), pairIntReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntReal)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntReal)).toType(), pairIntReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntInt)).toType(), pairRealReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntInt)).toType(), pairIntReal); - TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntInt)).toType(), pairRealInt); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntReal)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntReal)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntInt)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntInt)).isNull()); + TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntInt)).isNull()); TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt); } -- cgit v1.2.3