From 4a263c9db788017713a65989f99ca8d338f3f08d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 1 Mar 2021 05:42:33 -0800 Subject: [PATCH] google test: util: Migrate datatype_black. (#6019) --- test/unit/util/CMakeLists.txt | 2 +- test/unit/util/datatype_black.cpp | 499 +++++++++++++++++++++++++++++ test/unit/util/datatype_black.h | 502 ------------------------------ 3 files changed, 500 insertions(+), 503 deletions(-) create mode 100644 test/unit/util/datatype_black.cpp delete mode 100644 test/unit/util/datatype_black.h 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 + +#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 yellow = + std::make_shared("yellow"); + std::shared_ptr blue = + std::make_shared("blue"); + std::shared_ptr green = + std::make_shared("green"); + std::shared_ptr red = + std::make_shared("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 succ = + std::make_shared("succ"); + succ->addArgSelf("pred"); + nat.addConstructor(succ); + + std::shared_ptr zero = + std::make_shared("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 node = + std::make_shared("node"); + node->addArgSelf("left"); + node->addArgSelf("right"); + tree.addConstructor(node); + + std::shared_ptr leaf = + std::make_shared("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 cons = + std::make_shared("cons"); + cons->addArg("car", integerType); + cons->addArgSelf("cdr"); + list.addConstructor(cons); + + std::shared_ptr nil = + std::make_shared("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 cons = + std::make_shared("cons"); + cons->addArg("car", realType); + cons->addArgSelf("cdr"); + list.addConstructor(cons); + + std::shared_ptr nil = + std::make_shared("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 cons = + std::make_shared("cons"); + cons->addArg("car", booleanType); + cons->addArgSelf("cdr"); + list.addConstructor(cons); + + std::shared_ptr nil = + std::make_shared("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 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 node = + std::make_shared("node"); + node->addArgSelf("left"); + node->addArgSelf("right"); + tree.addConstructor(node); + + std::shared_ptr leaf = + std::make_shared("leaf"); + leaf->addArg("leaf", unresList); + tree.addConstructor(leaf); + + Debug("datatypes") << tree << std::endl; + + DType list("list"); + std::shared_ptr cons = + std::make_shared("cons"); + cons->addArg("car", unresTree); + cons->addArgSelf("cdr"); + list.addConstructor(cons); + + std::shared_ptr nil = + std::make_shared("nil"); + list.addConstructor(nil); + + Debug("datatypes") << list << std::endl; + + ASSERT_FALSE(tree.isResolved()); + ASSERT_FALSE(list.isResolved()); + + std::vector dts; + dts.push_back(tree); + dts.push_back(list); + std::vector 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 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 node = + std::make_shared("node"); + node->addArgSelf("left"); + node->addArgSelf("right"); + tree.addConstructor(node); + + std::shared_ptr leaf = + std::make_shared("leaf"); + leaf->addArg("leaf", unresList); + tree.addConstructor(leaf); + + DType list("list"); + std::shared_ptr cons = + std::make_shared("cons"); + cons->addArg("car", unresTree); + cons->addArgSelf("cdr"); + list.addConstructor(cons); + + std::shared_ptr nil = + std::make_shared("nil"); + list.addConstructor(nil); + + // add another constructor to list datatype resulting in an + // "otherNil-list" + std::shared_ptr otherNil = + std::make_shared("otherNil"); + list.addConstructor(otherNil); + + std::vector dts; + dts.push_back(tree); + dts.push_back(list); + // remake the types + std::vector 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 node = + std::make_shared("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 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 mkpair = + std::make_shared("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 - -#include - -#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 yellow = - std::make_shared("yellow"); - std::shared_ptr blue = - std::make_shared("blue"); - std::shared_ptr green = - std::make_shared("green"); - std::shared_ptr red = - std::make_shared("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 succ = - std::make_shared("succ"); - succ->addArgSelf("pred"); - nat.addConstructor(succ); - - std::shared_ptr zero = - std::make_shared("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 node = - std::make_shared("node"); - node->addArgSelf("left"); - node->addArgSelf("right"); - tree.addConstructor(node); - - std::shared_ptr leaf = - std::make_shared("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 cons = - std::make_shared("cons"); - cons->addArg("car", integerType); - cons->addArgSelf("cdr"); - list.addConstructor(cons); - - std::shared_ptr nil = - std::make_shared("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 cons = - std::make_shared("cons"); - cons->addArg("car", realType); - cons->addArgSelf("cdr"); - list.addConstructor(cons); - - std::shared_ptr nil = - std::make_shared("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 cons = - std::make_shared("cons"); - cons->addArg("car", booleanType); - cons->addArgSelf("cdr"); - list.addConstructor(cons); - - std::shared_ptr nil = - std::make_shared("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 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 node = - std::make_shared("node"); - node->addArgSelf("left"); - node->addArgSelf("right"); - tree.addConstructor(node); - - std::shared_ptr leaf = - std::make_shared("leaf"); - leaf->addArg("leaf", unresList); - tree.addConstructor(leaf); - - Debug("datatypes") << tree << std::endl; - - DType list("list"); - std::shared_ptr cons = - std::make_shared("cons"); - cons->addArg("car", unresTree); - cons->addArgSelf("cdr"); - list.addConstructor(cons); - - std::shared_ptr nil = - std::make_shared("nil"); - list.addConstructor(nil); - - Debug("datatypes") << list << std::endl; - - TS_ASSERT(! tree.isResolved()); - TS_ASSERT(! list.isResolved()); - - vector dts; - dts.push_back(tree); - dts.push_back(list); - vector 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 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 node = - std::make_shared("node"); - node->addArgSelf("left"); - node->addArgSelf("right"); - tree.addConstructor(node); - - std::shared_ptr leaf = - std::make_shared("leaf"); - leaf->addArg("leaf", unresList); - tree.addConstructor(leaf); - - DType list("list"); - std::shared_ptr cons = - std::make_shared("cons"); - cons->addArg("car", unresTree); - cons->addArgSelf("cdr"); - list.addConstructor(cons); - - std::shared_ptr nil = - std::make_shared("nil"); - list.addConstructor(nil); - - // add another constructor to list datatype resulting in an - // "otherNil-list" - std::shared_ptr otherNil = - std::make_shared("otherNil"); - list.addConstructor(otherNil); - - vector dts; - dts.push_back(tree); - dts.push_back(list); - // remake the types - vector 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 node = - std::make_shared("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 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 mkpair = - std::make_shared("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 */ -- 2.30.2