diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-02 19:32:14 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-02 20:47:48 -0500 |
commit | 866941628950af27f33b03311a8839570ed92eca (patch) | |
tree | f3b3a48bf0091e9c6445a575c5faa5bbfeef7af8 /test/unit | |
parent | fe31c46e11df64da6a9c4741525e09952ba016cf (diff) |
Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a subtype of (Pair Real Real). Resolves bug #541.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/util/datatype_black.h | 107 |
1 files changed, 107 insertions, 0 deletions
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index d88d72b85..0bb98c3f2 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -21,6 +21,8 @@ #include "expr/expr.h" #include "expr/expr_manager.h" +#include "expr/expr_manager_scope.h" +#include "expr/type_node.h" using namespace CVC4; using namespace std; @@ -28,16 +30,19 @@ using namespace std; class DatatypeBlack : public CxxTest::TestSuite { ExprManager* d_em; + ExprManagerScope* d_scope; public: void setUp() { d_em = new ExprManager(); + d_scope = new ExprManagerScope(*d_em); Debug.on("datatypes"); Debug.on("groundterms"); } void tearDown() { + delete d_scope; delete d_em; } @@ -68,6 +73,7 @@ public: TS_ASSERT_THROWS(colorsDT["blue"].getSelector("foo"), IllegalArgumentException); TS_ASSERT_THROWS(colorsDT["blue"]["foo"], IllegalArgumentException); + TS_ASSERT(! colorsType.getDatatype().isParametric()); TS_ASSERT(colorsType.getDatatype().isFinite()); TS_ASSERT(colorsType.getDatatype().getCardinality().compare(4) == Cardinality::EQUAL); TS_ASSERT(ctor.getType().getCardinality().compare(1) == Cardinality::EQUAL); @@ -105,6 +111,7 @@ public: Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor); Debug("datatypes") << apply << std::endl; + TS_ASSERT(! natType.getDatatype().isParametric()); TS_ASSERT(! natType.getDatatype().isFinite()); TS_ASSERT(natType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(natType.getDatatype().isWellFounded()); @@ -146,6 +153,7 @@ public: TS_ASSERT(treeType.getConstructor("leaf") == ctor); TS_ASSERT_THROWS(treeType.getConstructor("leff"), IllegalArgumentException); + TS_ASSERT(! treeType.getDatatype().isParametric()); TS_ASSERT(! treeType.getDatatype().isFinite()); TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(treeType.getDatatype().isWellFounded()); @@ -180,6 +188,7 @@ public: DatatypeType listType = d_em->mkDatatypeType(list); Debug("datatypes") << listType << std::endl; + TS_ASSERT(! listType.getDatatype().isParametric()); TS_ASSERT(! listType.getDatatype().isFinite()); TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(listType.getDatatype().isWellFounded()); @@ -214,6 +223,7 @@ public: DatatypeType listType = d_em->mkDatatypeType(list); Debug("datatypes") << listType << std::endl; + TS_ASSERT(! listType.getDatatype().isParametric()); TS_ASSERT(! listType.getDatatype().isFinite()); TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL); TS_ASSERT(listType.getDatatype().isWellFounded()); @@ -378,6 +388,7 @@ public: TS_ASSERT((*i).mkGroundTerm( dtts2[0] ).getType() == dtts2[0]); } + TS_ASSERT(! dtts2[1].getDatatype().isParametric()); TS_ASSERT(! dtts2[1].getDatatype().isFinite()); TS_ASSERT(dtts2[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(dtts2[1].getDatatype().isWellFounded()); @@ -408,6 +419,7 @@ public: DatatypeType treeType = d_em->mkDatatypeType(tree); Debug("datatypes") << treeType << std::endl; + TS_ASSERT(! treeType.getDatatype().isParametric()); TS_ASSERT(! treeType.getDatatype().isFinite()); TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(! treeType.getDatatype().isWellFounded()); @@ -423,4 +435,99 @@ public: } } + void testParametricDatatype() { + vector<Type> v; + Type t1, t2; + v.push_back(t1 = d_em->mkSort("T1")); + v.push_back(t2 = d_em->mkSort("T2")); + Datatype pair("pair", v); + + DatatypeConstructor mkpair("mk-pair"); + mkpair.addArg("first", t1); + mkpair.addArg("second", t2); + pair.addConstructor(mkpair); + DatatypeType pairType = d_em->mkDatatypeType(pair); + + TS_ASSERT(pairType.getDatatype().isParametric()); + v.clear(); + v.push_back(d_em->integerType()); + v.push_back(d_em->integerType()); + DatatypeType pairIntInt = pairType.getDatatype().getDatatypeType(v); + v.clear(); + v.push_back(d_em->realType()); + v.push_back(d_em->realType()); + DatatypeType pairRealReal = pairType.getDatatype().getDatatypeType(v); + v.clear(); + v.push_back(d_em->realType()); + v.push_back(d_em->integerType()); + DatatypeType pairRealInt = pairType.getDatatype().getDatatypeType(v); + v.clear(); + v.push_back(d_em->integerType()); + v.push_back(d_em->realType()); + DatatypeType pairIntReal = pairType.getDatatype().getDatatypeType(v); + + TS_ASSERT_DIFFERS(pairIntInt, pairRealReal); + TS_ASSERT_DIFFERS(pairIntReal, pairRealReal); + TS_ASSERT_DIFFERS(pairRealInt, pairRealReal); + TS_ASSERT_DIFFERS(pairIntInt, pairIntReal); + 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(pairRealInt.isComparableTo(pairRealInt)); + 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(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(!pairRealReal.isSubtypeOf(pairRealInt)); + TS_ASSERT(!pairIntReal.isSubtypeOf(pairRealInt)); + TS_ASSERT(pairRealInt.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(!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_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_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_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt); + } + };/* class DatatypeBlack */ |