google test: util: Migrate datatype_black. (#6019)

3 files changed, 500 insertions, 503 deletions

diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 54004ff47..b98577646 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -19,7 +19,7 @@ cvc4_add_unit_test_black(boolean_simplification_black util)
 cvc4_add_unit_test_black(cardinality_black util)
 cvc4_add_unit_test_white(check_white util)
 cvc4_add_unit_test_black(configuration_black util)
-cvc4_add_cxx_unit_test_black(datatype_black util)
+cvc4_add_unit_test_black(datatype_black util)
 cvc4_add_unit_test_black(exception_black util)
 if(CVC4_USE_SYMFPU)
 cvc4_add_cxx_unit_test_black(floatingpoint_black util)
diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp
new file mode 100644
index 000000000..0ef095fd9
--- /dev/null
+++ b/test/unit/util/datatype_black.cpp
@@ -0,0 +1,499 @@
+/*********************                                                        */
+/*! \file datatype_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::DType
+ **
+ ** Black box testing of CVC4::DType.
+ **/
+
+#include <sstream>
+
+#include "api/cvc4cpp.h"
+#include "expr/dtype.h"
+#include "expr/expr.h"
+#include "expr/type_node.h"
+#include "test_expr.h"
+
+namespace CVC4 {
+namespace test {
+
+class TestUtilBlackDatatype : public TestExprBlack
+{
+ public:
+  void SetUp() override
+  {
+    TestExprBlack::SetUp();
+    Debug.on("datatypes");
+    Debug.on("groundterms");
+  }
+};
+
+TEST_F(TestUtilBlackDatatype, enumeration)
+{
+  DType colors("colors");
+
+  std::shared_ptr<DTypeConstructor> yellow =
+      std::make_shared<DTypeConstructor>("yellow");
+  std::shared_ptr<DTypeConstructor> blue =
+      std::make_shared<DTypeConstructor>("blue");
+  std::shared_ptr<DTypeConstructor> green =
+      std::make_shared<DTypeConstructor>("green");
+  std::shared_ptr<DTypeConstructor> red =
+      std::make_shared<DTypeConstructor>("red");
+
+  colors.addConstructor(yellow);
+  colors.addConstructor(blue);
+  colors.addConstructor(green);
+  colors.addConstructor(red);
+
+  Debug("datatypes") << colors << std::endl;
+  TypeNode colorsType = d_nodeManager->mkDatatypeType(colors);
+  Debug("datatypes") << colorsType << std::endl;
+
+  Node ctor = colorsType.getDType()[1].getConstructor();
+  Node apply = d_nodeManager->mkNode(kind::APPLY_CONSTRUCTOR, ctor);
+  Debug("datatypes") << apply << std::endl;
+
+  ASSERT_FALSE(colorsType.getDType().isParametric());
+  ASSERT_TRUE(colorsType.getDType().isFinite());
+  ASSERT_EQ(colorsType.getDType().getCardinality().compare(4),
+            Cardinality::EQUAL);
+  ASSERT_EQ(ctor.getType().getCardinality().compare(1), Cardinality::EQUAL);
+  ASSERT_TRUE(colorsType.getDType().isWellFounded());
+  Debug("groundterms") << "ground term of " << colorsType.getDType().getName()
+                       << std::endl
+                       << "  is " << colorsType.mkGroundTerm() << std::endl;
+  ASSERT_EQ(colorsType.mkGroundTerm().getType(), colorsType);
+}
+
+TEST_F(TestUtilBlackDatatype, nat)
+{
+  DType nat("nat");
+
+  std::shared_ptr<DTypeConstructor> succ =
+      std::make_shared<DTypeConstructor>("succ");
+  succ->addArgSelf("pred");
+  nat.addConstructor(succ);
+
+  std::shared_ptr<DTypeConstructor> zero =
+      std::make_shared<DTypeConstructor>("zero");
+  nat.addConstructor(zero);
+
+  Debug("datatypes") << nat << std::endl;
+  TypeNode natType = d_nodeManager->mkDatatypeType(nat);
+  Debug("datatypes") << natType << std::endl;
+
+  Node ctor = natType.getDType()[1].getConstructor();
+  Node apply = d_nodeManager->mkNode(kind::APPLY_CONSTRUCTOR, ctor);
+  Debug("datatypes") << apply << std::endl;
+
+  ASSERT_FALSE(natType.getDType().isParametric());
+  ASSERT_FALSE(natType.getDType().isFinite());
+  ASSERT_TRUE(natType.getDType().getCardinality().compare(Cardinality::INTEGERS)
+              == Cardinality::EQUAL);
+  ASSERT_TRUE(natType.getDType().isWellFounded());
+  Debug("groundterms") << "ground term of " << natType.getDType().getName()
+                       << std::endl
+                       << "  is " << natType.mkGroundTerm() << std::endl;
+  ASSERT_TRUE(natType.mkGroundTerm().getType() == natType);
+}
+
+TEST_F(TestUtilBlackDatatype, tree)
+{
+  DType tree("tree");
+  TypeNode integerType = d_nodeManager->integerType();
+
+  std::shared_ptr<DTypeConstructor> node =
+      std::make_shared<DTypeConstructor>("node");
+  node->addArgSelf("left");
+  node->addArgSelf("right");
+  tree.addConstructor(node);
+
+  std::shared_ptr<DTypeConstructor> leaf =
+      std::make_shared<DTypeConstructor>("leaf");
+  leaf->addArg("leaf", integerType);
+  tree.addConstructor(leaf);
+
+  Debug("datatypes") << tree << std::endl;
+  TypeNode treeType = d_nodeManager->mkDatatypeType(tree);
+  Debug("datatypes") << treeType << std::endl;
+
+  ASSERT_FALSE(treeType.getDType().isParametric());
+  ASSERT_FALSE(treeType.getDType().isFinite());
+  ASSERT_TRUE(
+      treeType.getDType().getCardinality().compare(Cardinality::INTEGERS)
+      == Cardinality::EQUAL);
+  ASSERT_TRUE(treeType.getDType().isWellFounded());
+  Debug("groundterms") << "ground term of " << treeType.getDType().getName()
+                       << std::endl
+                       << "  is " << treeType.mkGroundTerm() << std::endl;
+  ASSERT_TRUE(treeType.mkGroundTerm().getType() == treeType);
+}
+
+TEST_F(TestUtilBlackDatatype, list_int)
+{
+  DType list("list");
+  TypeNode integerType = d_nodeManager->integerType();
+
+  std::shared_ptr<DTypeConstructor> cons =
+      std::make_shared<DTypeConstructor>("cons");
+  cons->addArg("car", integerType);
+  cons->addArgSelf("cdr");
+  list.addConstructor(cons);
+
+  std::shared_ptr<DTypeConstructor> nil =
+      std::make_shared<DTypeConstructor>("nil");
+  list.addConstructor(nil);
+
+  Debug("datatypes") << list << std::endl;
+  TypeNode listType = d_nodeManager->mkDatatypeType(list);
+  Debug("datatypes") << listType << std::endl;
+
+  ASSERT_FALSE(listType.getDType().isParametric());
+  ASSERT_FALSE(listType.getDType().isFinite());
+  ASSERT_TRUE(
+      listType.getDType().getCardinality().compare(Cardinality::INTEGERS)
+      == Cardinality::EQUAL);
+  ASSERT_TRUE(listType.getDType().isWellFounded());
+  Debug("groundterms") << "ground term of " << listType.getDType().getName()
+                       << std::endl
+                       << "  is " << listType.mkGroundTerm() << std::endl;
+  ASSERT_TRUE(listType.mkGroundTerm().getType() == listType);
+}
+
+TEST_F(TestUtilBlackDatatype, list_real)
+{
+  DType list("list");
+  TypeNode realType = d_nodeManager->realType();
+
+  std::shared_ptr<DTypeConstructor> cons =
+      std::make_shared<DTypeConstructor>("cons");
+  cons->addArg("car", realType);
+  cons->addArgSelf("cdr");
+  list.addConstructor(cons);
+
+  std::shared_ptr<DTypeConstructor> nil =
+      std::make_shared<DTypeConstructor>("nil");
+  list.addConstructor(nil);
+
+  Debug("datatypes") << list << std::endl;
+  TypeNode listType = d_nodeManager->mkDatatypeType(list);
+  Debug("datatypes") << listType << std::endl;
+
+  ASSERT_FALSE(listType.getDType().isParametric());
+  ASSERT_FALSE(listType.getDType().isFinite());
+  ASSERT_TRUE(listType.getDType().getCardinality().compare(Cardinality::REALS)
+              == Cardinality::EQUAL);
+  ASSERT_TRUE(listType.getDType().isWellFounded());
+  Debug("groundterms") << "ground term of " << listType.getDType().getName()
+                       << std::endl
+                       << "  is " << listType.mkGroundTerm() << std::endl;
+  ASSERT_TRUE(listType.mkGroundTerm().getType() == listType);
+}
+
+TEST_F(TestUtilBlackDatatype, list_boolean)
+{
+  DType list("list");
+  TypeNode booleanType = d_nodeManager->booleanType();
+
+  std::shared_ptr<DTypeConstructor> cons =
+      std::make_shared<DTypeConstructor>("cons");
+  cons->addArg("car", booleanType);
+  cons->addArgSelf("cdr");
+  list.addConstructor(cons);
+
+  std::shared_ptr<DTypeConstructor> nil =
+      std::make_shared<DTypeConstructor>("nil");
+  list.addConstructor(nil);
+
+  Debug("datatypes") << list << std::endl;
+  TypeNode listType = d_nodeManager->mkDatatypeType(list);
+  Debug("datatypes") << listType << std::endl;
+
+  ASSERT_FALSE(listType.getDType().isFinite());
+  ASSERT_TRUE(
+      listType.getDType().getCardinality().compare(Cardinality::INTEGERS)
+      == Cardinality::EQUAL);
+  ASSERT_TRUE(listType.getDType().isWellFounded());
+  Debug("groundterms") << "ground term of " << listType.getDType().getName()
+                       << std::endl
+                       << "  is " << listType.mkGroundTerm() << std::endl;
+  ASSERT_TRUE(listType.mkGroundTerm().getType() == listType);
+}
+
+TEST_F(TestUtilBlackDatatype, mutual_list_trees1)
+{
+  /* Create two mutual datatypes corresponding to this definition
+   * block:
+   *
+   *   DATATYPE
+   *     tree = node(left: tree, right: tree) | leaf(list),
+   *     list = cons(car: tree, cdr: list) | nil
+   *   END;
+   */
+  std::set<TypeNode> unresolvedTypes;
+  TypeNode unresList =
+      d_nodeManager->mkSort("list", NodeManager::SORT_FLAG_PLACEHOLDER);
+  unresolvedTypes.insert(unresList);
+  TypeNode unresTree =
+      d_nodeManager->mkSort("tree", NodeManager::SORT_FLAG_PLACEHOLDER);
+  unresolvedTypes.insert(unresTree);
+
+  DType tree("tree");
+  std::shared_ptr<DTypeConstructor> node =
+      std::make_shared<DTypeConstructor>("node");
+  node->addArgSelf("left");
+  node->addArgSelf("right");
+  tree.addConstructor(node);
+
+  std::shared_ptr<DTypeConstructor> leaf =
+      std::make_shared<DTypeConstructor>("leaf");
+  leaf->addArg("leaf", unresList);
+  tree.addConstructor(leaf);
+
+  Debug("datatypes") << tree << std::endl;
+
+  DType list("list");
+  std::shared_ptr<DTypeConstructor> cons =
+      std::make_shared<DTypeConstructor>("cons");
+  cons->addArg("car", unresTree);
+  cons->addArgSelf("cdr");
+  list.addConstructor(cons);
+
+  std::shared_ptr<DTypeConstructor> nil =
+      std::make_shared<DTypeConstructor>("nil");
+  list.addConstructor(nil);
+
+  Debug("datatypes") << list << std::endl;
+
+  ASSERT_FALSE(tree.isResolved());
+  ASSERT_FALSE(list.isResolved());
+
+  std::vector<DType> dts;
+  dts.push_back(tree);
+  dts.push_back(list);
+  std::vector<TypeNode> dtts =
+      d_nodeManager->mkMutualDatatypeTypes(dts, unresolvedTypes);
+
+  ASSERT_TRUE(dtts[0].getDType().isResolved());
+  ASSERT_TRUE(dtts[1].getDType().isResolved());
+
+  ASSERT_FALSE(dtts[0].getDType().isFinite());
+  ASSERT_TRUE(dtts[0].getDType().getCardinality().compare(Cardinality::INTEGERS)
+              == Cardinality::EQUAL);
+  ASSERT_TRUE(dtts[0].getDType().isWellFounded());
+  Debug("groundterms") << "ground term of " << dtts[0].getDType().getName()
+                       << std::endl
+                       << "  is " << dtts[0].mkGroundTerm() << std::endl;
+  ASSERT_TRUE(dtts[0].mkGroundTerm().getType() == dtts[0]);
+
+  ASSERT_FALSE(dtts[1].getDType().isFinite());
+  ASSERT_TRUE(dtts[1].getDType().getCardinality().compare(Cardinality::INTEGERS)
+              == Cardinality::EQUAL);
+  ASSERT_TRUE(dtts[1].getDType().isWellFounded());
+  Debug("groundterms") << "ground term of " << dtts[1].getDType().getName()
+                       << std::endl
+                       << "  is " << dtts[1].mkGroundTerm() << std::endl;
+  ASSERT_TRUE(dtts[1].mkGroundTerm().getType() == dtts[1]);
+}
+
+TEST_F(TestUtilBlackDatatype, mutual_list_trees2)
+{
+  std::set<TypeNode> unresolvedTypes;
+  TypeNode unresList =
+      d_nodeManager->mkSort("list", NodeManager::SORT_FLAG_PLACEHOLDER);
+  unresolvedTypes.insert(unresList);
+  TypeNode unresTree =
+      d_nodeManager->mkSort("tree", NodeManager::SORT_FLAG_PLACEHOLDER);
+  unresolvedTypes.insert(unresTree);
+
+  DType tree("tree");
+  std::shared_ptr<DTypeConstructor> node =
+      std::make_shared<DTypeConstructor>("node");
+  node->addArgSelf("left");
+  node->addArgSelf("right");
+  tree.addConstructor(node);
+
+  std::shared_ptr<DTypeConstructor> leaf =
+      std::make_shared<DTypeConstructor>("leaf");
+  leaf->addArg("leaf", unresList);
+  tree.addConstructor(leaf);
+
+  DType list("list");
+  std::shared_ptr<DTypeConstructor> cons =
+      std::make_shared<DTypeConstructor>("cons");
+  cons->addArg("car", unresTree);
+  cons->addArgSelf("cdr");
+  list.addConstructor(cons);
+
+  std::shared_ptr<DTypeConstructor> nil =
+      std::make_shared<DTypeConstructor>("nil");
+  list.addConstructor(nil);
+
+  // add another constructor to list datatype resulting in an
+  // "otherNil-list"
+  std::shared_ptr<DTypeConstructor> otherNil =
+      std::make_shared<DTypeConstructor>("otherNil");
+  list.addConstructor(otherNil);
+
+  std::vector<DType> dts;
+  dts.push_back(tree);
+  dts.push_back(list);
+  // remake the types
+  std::vector<TypeNode> dtts2 =
+      d_nodeManager->mkMutualDatatypeTypes(dts, unresolvedTypes);
+
+  ASSERT_FALSE(dtts2[0].getDType().isFinite());
+  ASSERT_TRUE(
+      dtts2[0].getDType().getCardinality().compare(Cardinality::INTEGERS)
+      == Cardinality::EQUAL);
+  ASSERT_TRUE(dtts2[0].getDType().isWellFounded());
+  Debug("groundterms") << "ground term of " << dtts2[0].getDType().getName()
+                       << std::endl
+                       << "  is " << dtts2[0].mkGroundTerm() << std::endl;
+  ASSERT_TRUE(dtts2[0].mkGroundTerm().getType() == dtts2[0]);
+
+  ASSERT_FALSE(dtts2[1].getDType().isParametric());
+  ASSERT_FALSE(dtts2[1].getDType().isFinite());
+  ASSERT_TRUE(
+      dtts2[1].getDType().getCardinality().compare(Cardinality::INTEGERS)
+      == Cardinality::EQUAL);
+  ASSERT_TRUE(dtts2[1].getDType().isWellFounded());
+  Debug("groundterms") << "ground term of " << dtts2[1].getDType().getName()
+                       << std::endl
+                       << "  is " << dtts2[1].mkGroundTerm() << std::endl;
+  ASSERT_TRUE(dtts2[1].mkGroundTerm().getType() == dtts2[1]);
+}
+
+TEST_F(TestUtilBlackDatatype, not_so_well_founded)
+{
+  DType tree("tree");
+
+  std::shared_ptr<DTypeConstructor> node =
+      std::make_shared<DTypeConstructor>("node");
+  node->addArgSelf("left");
+  node->addArgSelf("right");
+  tree.addConstructor(node);
+
+  Debug("datatypes") << tree << std::endl;
+  TypeNode treeType = d_nodeManager->mkDatatypeType(tree);
+  Debug("datatypes") << treeType << std::endl;
+
+  ASSERT_FALSE(treeType.getDType().isParametric());
+  ASSERT_FALSE(treeType.getDType().isFinite());
+  ASSERT_TRUE(
+      treeType.getDType().getCardinality().compare(Cardinality::INTEGERS)
+      == Cardinality::EQUAL);
+  ASSERT_FALSE(treeType.getDType().isWellFounded());
+  ASSERT_TRUE(treeType.mkGroundTerm().isNull());
+  ASSERT_TRUE(treeType.getDType().mkGroundTerm(treeType).isNull());
+}
+
+TEST_F(TestUtilBlackDatatype, parametric_DType)
+{
+  std::vector<TypeNode> v;
+  TypeNode t1, t2;
+  v.push_back(t1 = d_nodeManager->mkSort("T1"));
+  v.push_back(t2 = d_nodeManager->mkSort("T2"));
+  DType pair("pair", v);
+
+  std::shared_ptr<DTypeConstructor> mkpair =
+      std::make_shared<DTypeConstructor>("mk-pair");
+  mkpair->addArg("first", t1);
+  mkpair->addArg("second", t2);
+  pair.addConstructor(mkpair);
+  TypeNode pairType = d_nodeManager->mkDatatypeType(pair);
+
+  ASSERT_TRUE(pairType.getDType().isParametric());
+  v.clear();
+  v.push_back(d_nodeManager->integerType());
+  v.push_back(d_nodeManager->integerType());
+  TypeNode pairIntInt = pairType.getDType().getTypeNode(v);
+  v.clear();
+  v.push_back(d_nodeManager->realType());
+  v.push_back(d_nodeManager->realType());
+  TypeNode pairRealReal = pairType.getDType().getTypeNode(v);
+  v.clear();
+  v.push_back(d_nodeManager->realType());
+  v.push_back(d_nodeManager->integerType());
+  TypeNode pairRealInt = pairType.getDType().getTypeNode(v);
+  v.clear();
+  v.push_back(d_nodeManager->integerType());
+  v.push_back(d_nodeManager->realType());
+  TypeNode pairIntReal = pairType.getDType().getTypeNode(v);
+
+  ASSERT_NE(pairIntInt, pairRealReal);
+  ASSERT_NE(pairIntReal, pairRealReal);
+  ASSERT_NE(pairRealInt, pairRealReal);
+  ASSERT_NE(pairIntInt, pairIntReal);
+  ASSERT_NE(pairIntInt, pairRealInt);
+  ASSERT_NE(pairIntReal, pairRealInt);
+
+  ASSERT_TRUE(pairRealReal.isComparableTo(pairRealReal));
+  ASSERT_FALSE(pairIntReal.isComparableTo(pairRealReal));
+  ASSERT_FALSE(pairRealInt.isComparableTo(pairRealReal));
+  ASSERT_FALSE(pairIntInt.isComparableTo(pairRealReal));
+  ASSERT_FALSE(pairRealReal.isComparableTo(pairRealInt));
+  ASSERT_FALSE(pairIntReal.isComparableTo(pairRealInt));
+  ASSERT_TRUE(pairRealInt.isComparableTo(pairRealInt));
+  ASSERT_FALSE(pairIntInt.isComparableTo(pairRealInt));
+  ASSERT_FALSE(pairRealReal.isComparableTo(pairIntReal));
+  ASSERT_TRUE(pairIntReal.isComparableTo(pairIntReal));
+  ASSERT_FALSE(pairRealInt.isComparableTo(pairIntReal));
+  ASSERT_FALSE(pairIntInt.isComparableTo(pairIntReal));
+  ASSERT_FALSE(pairRealReal.isComparableTo(pairIntInt));
+  ASSERT_FALSE(pairIntReal.isComparableTo(pairIntInt));
+  ASSERT_FALSE(pairRealInt.isComparableTo(pairIntInt));
+  ASSERT_TRUE(pairIntInt.isComparableTo(pairIntInt));
+
+  ASSERT_TRUE(pairRealReal.isSubtypeOf(pairRealReal));
+  ASSERT_FALSE(pairIntReal.isSubtypeOf(pairRealReal));
+  ASSERT_FALSE(pairRealInt.isSubtypeOf(pairRealReal));
+  ASSERT_FALSE(pairIntInt.isSubtypeOf(pairRealReal));
+  ASSERT_FALSE(pairRealReal.isSubtypeOf(pairRealInt));
+  ASSERT_FALSE(pairIntReal.isSubtypeOf(pairRealInt));
+  ASSERT_TRUE(pairRealInt.isSubtypeOf(pairRealInt));
+  ASSERT_FALSE(pairIntInt.isSubtypeOf(pairRealInt));
+  ASSERT_FALSE(pairRealReal.isSubtypeOf(pairIntReal));
+  ASSERT_TRUE(pairIntReal.isSubtypeOf(pairIntReal));
+  ASSERT_FALSE(pairRealInt.isSubtypeOf(pairIntReal));
+  ASSERT_FALSE(pairIntInt.isSubtypeOf(pairIntReal));
+  ASSERT_FALSE(pairRealReal.isSubtypeOf(pairIntInt));
+  ASSERT_FALSE(pairIntReal.isSubtypeOf(pairIntInt));
+  ASSERT_FALSE(pairRealInt.isSubtypeOf(pairIntInt));
+  ASSERT_TRUE(pairIntInt.isSubtypeOf(pairIntInt));
+
+  ASSERT_EQ(TypeNode::leastCommonTypeNode(pairRealReal, pairRealReal),
+            pairRealReal);
+  ASSERT_TRUE(
+      TypeNode::leastCommonTypeNode(pairIntReal, pairRealReal).isNull());
+  ASSERT_TRUE(
+      TypeNode::leastCommonTypeNode(pairRealInt, pairRealReal).isNull());
+  ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntInt, pairRealReal).isNull());
+  ASSERT_TRUE(
+      TypeNode::leastCommonTypeNode(pairRealReal, pairRealInt).isNull());
+  ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntReal, pairRealInt).isNull());
+  ASSERT_EQ(TypeNode::leastCommonTypeNode(pairRealInt, pairRealInt),
+            pairRealInt);
+  ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntInt, pairRealInt).isNull());
+  ASSERT_TRUE(
+      TypeNode::leastCommonTypeNode(pairRealReal, pairIntReal).isNull());
+  ASSERT_EQ(TypeNode::leastCommonTypeNode(pairIntReal, pairIntReal),
+            pairIntReal);
+  ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairRealInt, pairIntReal).isNull());
+  ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntInt, pairIntReal).isNull());
+  ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairRealReal, pairIntInt).isNull());
+  ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntReal, pairIntInt).isNull());
+  ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairRealInt, pairIntInt).isNull());
+  ASSERT_EQ(TypeNode::leastCommonTypeNode(pairIntInt, pairIntInt), pairIntInt);
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
deleted file mode 100644
index 9909a8a7b..000000000
--- a/test/unit/util/datatype_black.h
+++ /dev/null
@@ -1,502 +0,0 @@
-/*********************                                                        */
-/*! \file datatype_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::DType
- **
- ** Black box testing of CVC4::DType.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <sstream>
-
-#include "api/cvc4cpp.h"
-#include "expr/dtype.h"
-#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;
-
-class DatatypeBlack : public CxxTest::TestSuite {
- public:
-  void setUp() override
-  {
-    d_slv = new api::Solver();
-    d_nm = d_slv->getNodeManager();
-    d_scope = new NodeManagerScope(d_nm);
-    Debug.on("datatypes");
-    Debug.on("groundterms");
-  }
-
-  void tearDown() override
-  {
-    delete d_scope;
-    delete d_slv;
-  }
-
-  void testEnumeration() {
-    DType colors("colors");
-
-    std::shared_ptr<DTypeConstructor> yellow =
-        std::make_shared<DTypeConstructor>("yellow");
-    std::shared_ptr<DTypeConstructor> blue =
-        std::make_shared<DTypeConstructor>("blue");
-    std::shared_ptr<DTypeConstructor> green =
-        std::make_shared<DTypeConstructor>("green");
-    std::shared_ptr<DTypeConstructor> red =
-        std::make_shared<DTypeConstructor>("red");
-
-    colors.addConstructor(yellow);
-    colors.addConstructor(blue);
-    colors.addConstructor(green);
-    colors.addConstructor(red);
-
-    Debug("datatypes") << colors << std::endl;
-    TypeNode colorsType = d_nm->mkDatatypeType(colors);
-    Debug("datatypes") << colorsType << std::endl;
-
-    Node ctor = colorsType.getDType()[1].getConstructor();
-    Node apply = d_nm->mkNode(kind::APPLY_CONSTRUCTOR, ctor);
-    Debug("datatypes") << apply << std::endl;
-
-    TS_ASSERT(!colorsType.getDType().isParametric());
-    TS_ASSERT(colorsType.getDType().isFinite());
-    TS_ASSERT(colorsType.getDType().getCardinality().compare(4)
-              == Cardinality::EQUAL);
-    TS_ASSERT(ctor.getType().getCardinality().compare(1) == Cardinality::EQUAL);
-    TS_ASSERT(colorsType.getDType().isWellFounded());
-    Debug("groundterms") << "ground term of " << colorsType.getDType().getName()
-                         << endl
-                         << "  is " << colorsType.mkGroundTerm() << endl;
-    TS_ASSERT(colorsType.mkGroundTerm().getType() == colorsType);
-  }
-
-  void testNat() {
-    DType nat("nat");
-
-    std::shared_ptr<DTypeConstructor> succ =
-        std::make_shared<DTypeConstructor>("succ");
-    succ->addArgSelf("pred");
-    nat.addConstructor(succ);
-
-    std::shared_ptr<DTypeConstructor> zero =
-        std::make_shared<DTypeConstructor>("zero");
-    nat.addConstructor(zero);
-
-    Debug("datatypes") << nat << std::endl;
-    TypeNode natType = d_nm->mkDatatypeType(nat);
-    Debug("datatypes") << natType << std::endl;
-
-    Node ctor = natType.getDType()[1].getConstructor();
-    Node apply = d_nm->mkNode(kind::APPLY_CONSTRUCTOR, ctor);
-    Debug("datatypes") << apply << std::endl;
-
-    TS_ASSERT(!natType.getDType().isParametric());
-    TS_ASSERT(!natType.getDType().isFinite());
-    TS_ASSERT(natType.getDType().getCardinality().compare(Cardinality::INTEGERS)
-              == Cardinality::EQUAL);
-    TS_ASSERT(natType.getDType().isWellFounded());
-    Debug("groundterms") << "ground term of " << natType.getDType().getName()
-                         << endl
-                         << "  is " << natType.mkGroundTerm() << endl;
-    TS_ASSERT(natType.mkGroundTerm().getType() == natType);
-  }
-
-  void testTree() {
-    DType tree("tree");
-    TypeNode integerType = d_nm->integerType();
-
-    std::shared_ptr<DTypeConstructor> node =
-        std::make_shared<DTypeConstructor>("node");
-    node->addArgSelf("left");
-    node->addArgSelf("right");
-    tree.addConstructor(node);
-
-    std::shared_ptr<DTypeConstructor> leaf =
-        std::make_shared<DTypeConstructor>("leaf");
-    leaf->addArg("leaf", integerType);
-    tree.addConstructor(leaf);
-
-    Debug("datatypes") << tree << std::endl;
-    TypeNode treeType = d_nm->mkDatatypeType(tree);
-    Debug("datatypes") << treeType << std::endl;
-
-    TS_ASSERT(!treeType.getDType().isParametric());
-    TS_ASSERT(!treeType.getDType().isFinite());
-    TS_ASSERT(
-        treeType.getDType().getCardinality().compare(Cardinality::INTEGERS)
-        == Cardinality::EQUAL);
-    TS_ASSERT(treeType.getDType().isWellFounded());
-    Debug("groundterms") << "ground term of " << treeType.getDType().getName()
-                         << endl
-                         << "  is " << treeType.mkGroundTerm() << endl;
-    TS_ASSERT(treeType.mkGroundTerm().getType() == treeType);
-  }
-
-  void testListInt() {
-    DType list("list");
-    TypeNode integerType = d_nm->integerType();
-
-    std::shared_ptr<DTypeConstructor> cons =
-        std::make_shared<DTypeConstructor>("cons");
-    cons->addArg("car", integerType);
-    cons->addArgSelf("cdr");
-    list.addConstructor(cons);
-
-    std::shared_ptr<DTypeConstructor> nil =
-        std::make_shared<DTypeConstructor>("nil");
-    list.addConstructor(nil);
-
-    Debug("datatypes") << list << std::endl;
-    TypeNode listType = d_nm->mkDatatypeType(list);
-    Debug("datatypes") << listType << std::endl;
-
-    TS_ASSERT(!listType.getDType().isParametric());
-    TS_ASSERT(!listType.getDType().isFinite());
-    TS_ASSERT(
-        listType.getDType().getCardinality().compare(Cardinality::INTEGERS)
-        == Cardinality::EQUAL);
-    TS_ASSERT(listType.getDType().isWellFounded());
-    Debug("groundterms") << "ground term of " << listType.getDType().getName()
-                         << endl
-                         << "  is " << listType.mkGroundTerm() << endl;
-    TS_ASSERT(listType.mkGroundTerm().getType() == listType);
-  }
-
-  void testListReal() {
-    DType list("list");
-    TypeNode realType = d_nm->realType();
-
-    std::shared_ptr<DTypeConstructor> cons =
-        std::make_shared<DTypeConstructor>("cons");
-    cons->addArg("car", realType);
-    cons->addArgSelf("cdr");
-    list.addConstructor(cons);
-
-    std::shared_ptr<DTypeConstructor> nil =
-        std::make_shared<DTypeConstructor>("nil");
-    list.addConstructor(nil);
-
-    Debug("datatypes") << list << std::endl;
-    TypeNode listType = d_nm->mkDatatypeType(list);
-    Debug("datatypes") << listType << std::endl;
-
-    TS_ASSERT(!listType.getDType().isParametric());
-    TS_ASSERT(!listType.getDType().isFinite());
-    TS_ASSERT(listType.getDType().getCardinality().compare(Cardinality::REALS)
-              == Cardinality::EQUAL);
-    TS_ASSERT(listType.getDType().isWellFounded());
-    Debug("groundterms") << "ground term of " << listType.getDType().getName()
-                         << endl
-                         << "  is " << listType.mkGroundTerm() << endl;
-    TS_ASSERT(listType.mkGroundTerm().getType() == listType);
-  }
-
-  void testListBoolean() {
-    DType list("list");
-    TypeNode booleanType = d_nm->booleanType();
-
-    std::shared_ptr<DTypeConstructor> cons =
-        std::make_shared<DTypeConstructor>("cons");
-    cons->addArg("car", booleanType);
-    cons->addArgSelf("cdr");
-    list.addConstructor(cons);
-
-    std::shared_ptr<DTypeConstructor> nil =
-        std::make_shared<DTypeConstructor>("nil");
-    list.addConstructor(nil);
-
-    Debug("datatypes") << list << std::endl;
-    TypeNode listType = d_nm->mkDatatypeType(list);
-    Debug("datatypes") << listType << std::endl;
-
-    TS_ASSERT(!listType.getDType().isFinite());
-    TS_ASSERT(
-        listType.getDType().getCardinality().compare(Cardinality::INTEGERS)
-        == Cardinality::EQUAL);
-    TS_ASSERT(listType.getDType().isWellFounded());
-    Debug("groundterms") << "ground term of " << listType.getDType().getName()
-                         << endl
-                         << "  is " << listType.mkGroundTerm() << endl;
-    TS_ASSERT(listType.mkGroundTerm().getType() == listType);
-  }
-
-  void testMutualListTrees() {
-    /* Create two mutual datatypes corresponding to this definition
-     * block:
-     *
-     *   DATATYPE
-     *     tree = node(left: tree, right: tree) | leaf(list),
-     *     list = cons(car: tree, cdr: list) | nil
-     *   END;
-     */
-    std::set<TypeNode> unresolvedTypes;
-    TypeNode unresList =
-        d_nm->mkSort("list", NodeManager::SORT_FLAG_PLACEHOLDER);
-    unresolvedTypes.insert(unresList);
-    TypeNode unresTree =
-        d_nm->mkSort("tree", NodeManager::SORT_FLAG_PLACEHOLDER);
-    unresolvedTypes.insert(unresTree);
-
-    DType tree("tree");
-    std::shared_ptr<DTypeConstructor> node =
-        std::make_shared<DTypeConstructor>("node");
-    node->addArgSelf("left");
-    node->addArgSelf("right");
-    tree.addConstructor(node);
-
-    std::shared_ptr<DTypeConstructor> leaf =
-        std::make_shared<DTypeConstructor>("leaf");
-    leaf->addArg("leaf", unresList);
-    tree.addConstructor(leaf);
-
-    Debug("datatypes") << tree << std::endl;
-
-    DType list("list");
-    std::shared_ptr<DTypeConstructor> cons =
-        std::make_shared<DTypeConstructor>("cons");
-    cons->addArg("car", unresTree);
-    cons->addArgSelf("cdr");
-    list.addConstructor(cons);
-
-    std::shared_ptr<DTypeConstructor> nil =
-        std::make_shared<DTypeConstructor>("nil");
-    list.addConstructor(nil);
-
-    Debug("datatypes") << list << std::endl;
-
-    TS_ASSERT(! tree.isResolved());
-    TS_ASSERT(! list.isResolved());
-
-    vector<DType> dts;
-    dts.push_back(tree);
-    dts.push_back(list);
-    vector<TypeNode> dtts = d_nm->mkMutualDatatypeTypes(dts, unresolvedTypes);
-
-    TS_ASSERT(dtts[0].getDType().isResolved());
-    TS_ASSERT(dtts[1].getDType().isResolved());
-
-    TS_ASSERT(!dtts[0].getDType().isFinite());
-    TS_ASSERT(dtts[0].getDType().getCardinality().compare(Cardinality::INTEGERS)
-              == Cardinality::EQUAL);
-    TS_ASSERT(dtts[0].getDType().isWellFounded());
-    Debug("groundterms") << "ground term of " << dtts[0].getDType().getName()
-                         << endl
-                         << "  is " << dtts[0].mkGroundTerm() << endl;
-    TS_ASSERT(dtts[0].mkGroundTerm().getType() == dtts[0]);
-
-    TS_ASSERT(!dtts[1].getDType().isFinite());
-    TS_ASSERT(dtts[1].getDType().getCardinality().compare(Cardinality::INTEGERS)
-              == Cardinality::EQUAL);
-    TS_ASSERT(dtts[1].getDType().isWellFounded());
-    Debug("groundterms") << "ground term of " << dtts[1].getDType().getName()
-                         << endl
-                         << "  is " << dtts[1].mkGroundTerm() << endl;
-    TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]);
-  }
-  void testMutualListTrees2()
-  {
-    std::set<TypeNode> unresolvedTypes;
-    TypeNode unresList =
-        d_nm->mkSort("list", NodeManager::SORT_FLAG_PLACEHOLDER);
-    unresolvedTypes.insert(unresList);
-    TypeNode unresTree =
-        d_nm->mkSort("tree", NodeManager::SORT_FLAG_PLACEHOLDER);
-    unresolvedTypes.insert(unresTree);
-
-    DType tree("tree");
-    std::shared_ptr<DTypeConstructor> node =
-        std::make_shared<DTypeConstructor>("node");
-    node->addArgSelf("left");
-    node->addArgSelf("right");
-    tree.addConstructor(node);
-
-    std::shared_ptr<DTypeConstructor> leaf =
-        std::make_shared<DTypeConstructor>("leaf");
-    leaf->addArg("leaf", unresList);
-    tree.addConstructor(leaf);
-
-    DType list("list");
-    std::shared_ptr<DTypeConstructor> cons =
-        std::make_shared<DTypeConstructor>("cons");
-    cons->addArg("car", unresTree);
-    cons->addArgSelf("cdr");
-    list.addConstructor(cons);
-
-    std::shared_ptr<DTypeConstructor> nil =
-        std::make_shared<DTypeConstructor>("nil");
-    list.addConstructor(nil);
-
-    // add another constructor to list datatype resulting in an
-    // "otherNil-list"
-    std::shared_ptr<DTypeConstructor> otherNil =
-        std::make_shared<DTypeConstructor>("otherNil");
-    list.addConstructor(otherNil);
-
-    vector<DType> dts;
-    dts.push_back(tree);
-    dts.push_back(list);
-    // remake the types
-    vector<TypeNode> dtts2 = d_nm->mkMutualDatatypeTypes(dts, unresolvedTypes);
-
-    TS_ASSERT(!dtts2[0].getDType().isFinite());
-    TS_ASSERT(
-        dtts2[0].getDType().getCardinality().compare(Cardinality::INTEGERS)
-        == Cardinality::EQUAL);
-    TS_ASSERT(dtts2[0].getDType().isWellFounded());
-    Debug("groundterms") << "ground term of " << dtts2[0].getDType().getName()
-                         << endl
-                         << "  is " << dtts2[0].mkGroundTerm() << endl;
-    TS_ASSERT(dtts2[0].mkGroundTerm().getType() == dtts2[0]);
-
-    TS_ASSERT(!dtts2[1].getDType().isParametric());
-    TS_ASSERT(!dtts2[1].getDType().isFinite());
-    TS_ASSERT(
-        dtts2[1].getDType().getCardinality().compare(Cardinality::INTEGERS)
-        == Cardinality::EQUAL);
-    TS_ASSERT(dtts2[1].getDType().isWellFounded());
-    Debug("groundterms") << "ground term of " << dtts2[1].getDType().getName()
-                         << endl
-                         << "  is " << dtts2[1].mkGroundTerm() << endl;
-    TS_ASSERT(dtts2[1].mkGroundTerm().getType() == dtts2[1]);
-  }
-
-  void testNotSoWellFounded() {
-    DType tree("tree");
-
-    std::shared_ptr<DTypeConstructor> node =
-        std::make_shared<DTypeConstructor>("node");
-    node->addArgSelf("left");
-    node->addArgSelf("right");
-    tree.addConstructor(node);
-
-    Debug("datatypes") << tree << std::endl;
-    TypeNode treeType = d_nm->mkDatatypeType(tree);
-    Debug("datatypes") << treeType << std::endl;
-
-    TS_ASSERT(!treeType.getDType().isParametric());
-    TS_ASSERT(!treeType.getDType().isFinite());
-    TS_ASSERT(
-        treeType.getDType().getCardinality().compare(Cardinality::INTEGERS)
-        == Cardinality::EQUAL);
-    TS_ASSERT(!treeType.getDType().isWellFounded());
-    TS_ASSERT(treeType.mkGroundTerm().isNull());
-    TS_ASSERT(treeType.getDType().mkGroundTerm(treeType).isNull());
-  }
-
-  void testParametricDType()
-  {
-    vector<TypeNode> v;
-    TypeNode t1, t2;
-    v.push_back(t1 = d_nm->mkSort("T1"));
-    v.push_back(t2 = d_nm->mkSort("T2"));
-    DType pair("pair", v);
-
-    std::shared_ptr<DTypeConstructor> mkpair =
-        std::make_shared<DTypeConstructor>("mk-pair");
-    mkpair->addArg("first", t1);
-    mkpair->addArg("second", t2);
-    pair.addConstructor(mkpair);
-    TypeNode pairType = d_nm->mkDatatypeType(pair);
-
-    TS_ASSERT(pairType.getDType().isParametric());
-    v.clear();
-    v.push_back(d_nm->integerType());
-    v.push_back(d_nm->integerType());
-    TypeNode pairIntInt = pairType.getDType().getTypeNode(v);
-    v.clear();
-    v.push_back(d_nm->realType());
-    v.push_back(d_nm->realType());
-    TypeNode pairRealReal = pairType.getDType().getTypeNode(v);
-    v.clear();
-    v.push_back(d_nm->realType());
-    v.push_back(d_nm->integerType());
-    TypeNode pairRealInt = pairType.getDType().getTypeNode(v);
-    v.clear();
-    v.push_back(d_nm->integerType());
-    v.push_back(d_nm->realType());
-    TypeNode pairIntReal = pairType.getDType().getTypeNode(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(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(pairRealReal, pairRealReal),
-                     pairRealReal);
-    TS_ASSERT(
-        TypeNode::leastCommonTypeNode(pairIntReal, pairRealReal).isNull());
-    TS_ASSERT(
-        TypeNode::leastCommonTypeNode(pairRealInt, pairRealReal).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairRealReal).isNull());
-    TS_ASSERT(
-        TypeNode::leastCommonTypeNode(pairRealReal, pairRealInt).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntReal, pairRealInt).isNull());
-    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairRealInt, pairRealInt),
-                     pairRealInt);
-    TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairRealInt).isNull());
-    TS_ASSERT(
-        TypeNode::leastCommonTypeNode(pairRealReal, pairIntReal).isNull());
-    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairIntReal, pairIntReal),
-                     pairIntReal);
-    TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealInt, pairIntReal).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairIntReal).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealReal, pairIntInt).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntReal, pairIntInt).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealInt, pairIntInt).isNull());
-    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairIntInt, pairIntInt),
-                     pairIntInt);
-  }
-
- private:
-  api::Solver* d_slv;
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-}; /* class DTypeBlack */