diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-14 14:12:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-09-14 14:12:22 -0500 |
commit | ab2924e8a6cc34f29167b1ff50273d59dd7a6707 (patch) | |
tree | d9902a389ae70a21f2d5a3f7acde2ce658fb534d /test/unit | |
parent | e4fc6c7b57668f18ce087c45e001c101375c20ea (diff) |
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)).
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/util/datatype_black.h | 63 |
1 files changed, 29 insertions, 34 deletions
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); } |