Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a subtype of (Pair Real Real). Resolves bug #541.

3 files changed, 115 insertions, 1 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 8ae9b3ae2..4748ca5f9 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -151,7 +151,8 @@ BUG_TESTS = \
 	bug520.smt2 \
 	bug521.smt2 \
 	bug521.minimized.smt2 \
-	bug522.smt2
+	bug522.smt2 \
+	bug541.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug541.smt2 b/test/regress/regress0/bug541.smt2
new file mode 100644
index 000000000..482823985
--- /dev/null
+++ b/test/regress/regress0/bug541.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
+(assert (= (mk-pair 0.0 0.0) (mk-pair 1.5 2.5)))
+(check-sat)
+(exit)
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 */