From 11bc0e4c3147b0fce3033b6a4290d8730aa401ad Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 17 Nov 2019 20:19:24 -0600 Subject: [PATCH] Updates to the unit tests, api, and examples for datatypes (#3459) * Updates to the unit tests, api, and examples for datatypes * Format --- examples/api/datatypes-new.cpp | 12 +++++++++--- examples/api/datatypes.cpp | 2 +- src/api/cvc4cpp.cpp | 10 +++++----- src/api/cvc4cpp.h | 8 ++++---- test/unit/api/solver_black.h | 18 +++++++++++------- test/unit/util/datatype_black.h | 32 +++++++++++++++++++++++++------- 6 files changed, 55 insertions(+), 27 deletions(-) diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index 8c625772521..efbd33645b1 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -27,7 +27,7 @@ void test(Solver& slv, Sort& consListSort) // the complete spec for the datatype from the DatatypeSort, and // this Datatype object has constructor symbols (and others) filled in. - Datatype consList = consListSort.getDatatype(); + const Datatype& consList = consListSort.getDatatype(); // t = cons 0 nil // @@ -103,7 +103,7 @@ void test(Solver& slv, Sort& consListSort) Sort paramConsIntListSort = paramConsListSort.instantiate(std::vector{slv.getIntegerSort()}); - Datatype paramConsList = paramConsListSort.getDatatype(); + const Datatype& paramConsList = paramConsListSort.getDatatype(); std::cout << "parameterized datatype sort is " << std::endl; for (const DatatypeConstructor& ctor : paramConsList) @@ -169,7 +169,13 @@ int main() << ">>> Alternatively, use declareDatatype" << std::endl; std::cout << std::endl; - std::vector ctors = {cons, nil}; + DatatypeConstructorDecl cons2("cons"); + DatatypeSelectorDecl head2("head", slv.getIntegerSort()); + DatatypeSelectorDecl tail2("tail", DatatypeDeclSelfSort()); + cons2.addSelector(head2); + cons2.addSelector(tail2); + DatatypeConstructorDecl nil2("nil"); + std::vector ctors = {cons2, nil2}; Sort consListSort2 = slv.declareDatatype("list2", ctors); test(slv, consListSort2); diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index dabc1228f1a..34d440e3ea4 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -114,7 +114,7 @@ int main() { DatatypeType paramConsListType = em.mkDatatypeType(paramConsListSpec); Type paramConsIntListType = paramConsListType.instantiate(std::vector{em.integerType()}); - Datatype paramConsList = paramConsListType.getDatatype(); + const Datatype& paramConsList = paramConsListType.getDatatype(); std::cout << "parameterized datatype sort is " << std::endl; for (const DatatypeConstructor& ctor : paramConsList) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index b6bd4777a82..4bb772e9df9 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1542,8 +1542,8 @@ std::string DatatypeConstructorDecl::toString() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::DatatypeConstructor DatatypeConstructorDecl::getDatatypeConstructor( - void) const +const CVC4::DatatypeConstructor& +DatatypeConstructorDecl::getDatatypeConstructor(void) const { return *d_ctor; } @@ -1613,7 +1613,7 @@ std::string DatatypeDecl::toString() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::Datatype DatatypeDecl::getDatatype(void) const { return *d_dtype; } +const CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; } std::ostream& operator<<(std::ostream& out, const DatatypeSelectorDecl& stordecl) @@ -1782,7 +1782,7 @@ std::string DatatypeConstructor::toString() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::DatatypeConstructor DatatypeConstructor::getDatatypeConstructor( +const CVC4::DatatypeConstructor& DatatypeConstructor::getDatatypeConstructor( void) const { return *d_ctor; @@ -1850,7 +1850,7 @@ Datatype::const_iterator Datatype::end() const // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -CVC4::Datatype Datatype::getDatatype(void) const { return *d_dtype; } +const CVC4::Datatype& Datatype::getDatatype(void) const { return *d_dtype; } Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype, bool begin) diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 49c283b757f..ad923f866ae 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1022,7 +1022,7 @@ class CVC4_PUBLIC DatatypeConstructorDecl // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! - CVC4::DatatypeConstructor getDatatypeConstructor(void) const; + const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const; private: /** @@ -1095,7 +1095,7 @@ class CVC4_PUBLIC DatatypeDecl // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! - CVC4::Datatype getDatatype(void) const; + const CVC4::Datatype& getDatatype(void) const; private: /* The internal (intermediate) datatype wrapped by this datatype @@ -1309,7 +1309,7 @@ class CVC4_PUBLIC DatatypeConstructor // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! - CVC4::DatatypeConstructor getDatatypeConstructor(void) const; + const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const; private: /** @@ -1461,7 +1461,7 @@ class CVC4_PUBLIC Datatype // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! - CVC4::Datatype getDatatype(void) const; + const CVC4::Datatype& getDatatype(void) const; private: /** diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 41c4a86dd12..374a3ff2afb 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -624,6 +624,7 @@ void SolverBlack::testMkTermFromOpTerm() OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1); OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL); // list datatype + Sort sort = d_solver->mkParamSort("T"); DatatypeDecl listDecl("paramlist", sort); DatatypeConstructorDecl cons("cons"); @@ -776,17 +777,21 @@ void SolverBlack::testMkConstArray() void SolverBlack::testDeclareDatatype() { - DatatypeConstructorDecl cons("cons"); DatatypeConstructorDecl nil("nil"); std::vector ctors1 = {nil}; - std::vector ctors2 = {cons, nil}; - std::vector ctors3; TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1)); + DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl nil2("nil"); + std::vector ctors2 = {cons, nil2}; TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2)); - TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors2)); - TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors3), + DatatypeConstructorDecl cons2("cons"); + DatatypeConstructorDecl nil3("nil"); + std::vector ctors3 = {cons2, nil3}; + TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors3)); + std::vector ctors4; + TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors4), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors3), + TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors4), CVC4ApiException&); } @@ -983,7 +988,6 @@ void SolverBlack::testSimplify() Sort uSort = d_solver->mkUninterpretedSort("u"); Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort()); - DatatypeDecl consListSpec("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index e48d04a7f41..6df18fd44c4 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -277,21 +277,39 @@ class DatatypeBlack : public CxxTest::TestSuite { Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl << " is " << dtts[1].mkGroundTerm() << endl; TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]); + } + void testMutualListTrees2() + { + Datatype tree("tree"); + DatatypeConstructor node("node", "is_node"); + node.addArg("left", DatatypeSelfType()); + node.addArg("right", DatatypeSelfType()); + tree.addConstructor(node); + + DatatypeConstructor leaf("leaf", "is_leaf"); + leaf.addArg("leaf", DatatypeUnresolvedType("list")); + tree.addConstructor(leaf); + + Datatype list("list"); + DatatypeConstructor cons("cons", "is_cons"); + cons.addArg("car", DatatypeUnresolvedType("tree")); + cons.addArg("cdr", DatatypeSelfType()); + list.addConstructor(cons); + + DatatypeConstructor nil("nil", "is_nil"); + list.addConstructor(nil); // add another constructor to list datatype resulting in an // "otherNil-list" DatatypeConstructor otherNil("otherNil", "is_otherNil"); - dts[1].addConstructor(otherNil); + list.addConstructor(otherNil); + vector dts; + dts.push_back(tree); + dts.push_back(list); // remake the types vector dtts2 = d_em->mkMutualDatatypeTypes(dts); - TS_ASSERT_DIFFERS(dtts, dtts2); - TS_ASSERT_DIFFERS(dtts[1], dtts2[1]); - - // tree is also different because it's a tree of otherNil-lists - TS_ASSERT_DIFFERS(dtts[0], dtts2[0]); - TS_ASSERT(! dtts2[0].getDatatype().isFinite()); TS_ASSERT(dtts2[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(dtts2[0].getDatatype().isWellFounded());