From e47fa1305536d0e2d3c16ef2225d2b8534d5aa39 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Mar 2020 16:05:59 -0500 Subject: [PATCH] Add missing datatype functions to new API (#3930) This is in preparation for migrating the parser to use the Term-level API for datatypes. Notably, this adds the function mkDatatypeSorts for making mutually recursive datatypes. I've added a unit test that demonstrates this method (which mirrors the Expr-level datatype API). --- src/api/cvc4cpp.cpp | 53 +++++++++++++++++++- src/api/cvc4cpp.h | 49 ++++++++++++++++++- test/unit/api/datatype_api_black.h | 78 ++++++++++++++++++++++++++++++ 3 files changed, 178 insertions(+), 2 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 3b28e2f5c..ff25bbabb 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1878,11 +1878,17 @@ std::string DatatypeDecl::toString() const return ss.str(); } +std::string DatatypeDecl::getName() const +{ + CVC4_API_CHECK_NOT_NULL; + return d_dtype->getName(); +} + bool DatatypeDecl::isNull() const { return isNullHelper(); } // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! -const CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; } +CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; } std::ostream& operator<<(std::ostream& out, const DatatypeSelectorDecl& stordecl) @@ -1911,6 +1917,11 @@ Term DatatypeSelector::getSelectorTerm() const return sel; } +Sort DatatypeSelector::getRangeSort() const +{ + return Sort(d_stor->getRangeType()); +} + std::string DatatypeSelector::toString() const { std::stringstream ss; @@ -2458,6 +2469,33 @@ Term Solver::mkTermInternal(Kind kind, const std::vector& children) const CVC4_API_SOLVER_TRY_CATCH_END; } +std::vector Solver::mkDatatypeSortsInternal( + std::vector& dtypedecls, + std::set& unresolvedSorts) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + + std::vector datatypes; + for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; i++) + { + CVC4_API_ARG_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0, + dtypedecls[i]) + << "a datatype declaration with at least one constructor"; + datatypes.push_back(dtypedecls[i].getDatatype()); + } + std::set utypes = sortSetToTypes(unresolvedSorts); + std::vector dtypes = + d_exprMgr->mkMutualDatatypeTypes(datatypes, utypes); + std::vector retTypes; + for (CVC4::DatatypeType t : dtypes) + { + retTypes.push_back(Sort(t)); + } + return retTypes; + + CVC4_API_SOLVER_TRY_CATCH_END; +} + /* Helpers for converting vectors. */ /* .......................................................................... */ @@ -2604,6 +2642,19 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const CVC4_API_SOLVER_TRY_CATCH_END; } +std::vector Solver::mkDatatypeSorts( + std::vector& dtypedecls) const +{ + std::set unresolvedSorts; + return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); +} + +std::vector Solver::mkDatatypeSorts(std::vector& dtypedecls, + std::set& unresolvedSorts) const +{ + return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); +} + Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index db29359c5..dcf787b8e 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1260,9 +1260,12 @@ class CVC4_PUBLIC DatatypeDecl */ std::string toString() const; + /** @return the name of this datatype declaration. */ + std::string getName() const; + // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! - const CVC4::Datatype& getDatatype(void) const; + CVC4::Datatype& getDatatype(void) const; private: /** @@ -1350,6 +1353,9 @@ class CVC4_PUBLIC DatatypeSelector */ Term getSelectorTerm() const; + /** @return the range sort of this argument. */ + Sort getRangeSort() const; + /** * @return a string representation of this datatype selector */ @@ -1920,6 +1926,37 @@ class CVC4_PUBLIC Solver */ Sort mkDatatypeSort(DatatypeDecl dtypedecl) const; + /** + * Create a vector of datatype sorts. The names of the datatype declarations + * must be distinct. + * + * @param dtypedecls the datatype declarations from which the sort is created + * @return the datatype sorts + */ + std::vector mkDatatypeSorts( + std::vector& dtypedecls) const; + + /** + * Create a vector of datatype sorts using unresolved sorts. The names of + * the datatype declarations in dtypedecls must be distinct. + * + * This method is called when the DatatypeDecl objects dtypedecls have been + * built using "unresolved" sorts. + * + * We associate each sort in unresolvedSorts with exacly one datatype from + * dtypedecls. In particular, it must have the same name as exactly one + * datatype declaration in dtypedecls. + * + * When constructing datatypes, unresolved sorts are replaced by the datatype + * sort constructed for the datatype declaration it is associated with. + * + * @param dtypedecls the datatype declarations from which the sort is created + * @param unresolvedSorts the list of unresolved sorts + * @return the datatype sorts + */ + std::vector mkDatatypeSorts(std::vector& dtypedecls, + std::set& unresolvedSorts) const; + /** * Create function sort. * @param domain the sort of the fuction argument @@ -2867,6 +2904,16 @@ class CVC4_PUBLIC Solver */ Term mkTermInternal(Kind kind, const std::vector& children) const; + /** + * Create a vector of datatype sorts, using unresolved sorts. + * @param dtypedecls the datatype declarations from which the sort is created + * @param unresolvedSorts the list of unresolved sorts + * @return the datatype sorts + */ + std::vector mkDatatypeSortsInternal( + std::vector& dtypedecls, + std::set& unresolvedSorts) const; + /* The expression manager of this solver. */ std::unique_ptr d_exprMgr; /* The SMT engine of this solver. */ diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h index dcccd2628..f25282624 100644 --- a/test/unit/api/datatype_api_black.h +++ b/test/unit/api/datatype_api_black.h @@ -27,6 +27,7 @@ class DatatypeBlack : public CxxTest::TestSuite void tearDown() override; void testMkDatatypeSort(); + void testMkDatatypeSorts(); void testDatatypeStructs(); void testDatatypeNames(); @@ -57,6 +58,77 @@ void DatatypeBlack::testMkDatatypeSort() TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm()); } +void DatatypeBlack::testMkDatatypeSorts() +{ + /* Create two mutual datatypes corresponding to this definition + * block: + * + * DATATYPE + * tree = node(left: tree, right: tree) | leaf(data: list), + * list = cons(car: tree, cdr: list) | nil + * END; + */ + // Make unresolved types as placeholders + std::set unresTypes; + Sort unresTree = d_solver.mkUninterpretedSort("tree"); + Sort unresList = d_solver.mkUninterpretedSort("list"); + unresTypes.insert(unresTree); + unresTypes.insert(unresList); + + DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); + DatatypeConstructorDecl node("node"); + DatatypeSelectorDecl left("left", unresTree); + node.addSelector(left); + DatatypeSelectorDecl right("right", unresTree); + node.addSelector(right); + tree.addConstructor(node); + + DatatypeConstructorDecl leaf("leaf"); + DatatypeSelectorDecl data("data", unresList); + leaf.addSelector(data); + tree.addConstructor(leaf); + + DatatypeDecl list = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl car("car", unresTree); + cons.addSelector(car); + DatatypeSelectorDecl cdr("cdr", unresTree); + cons.addSelector(cdr); + list.addConstructor(cons); + + DatatypeConstructorDecl nil("nil"); + list.addConstructor(nil); + + std::vector dtdecls; + dtdecls.push_back(tree); + dtdecls.push_back(list); + std::vector dtsorts; + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == dtdecls.size()); + for (unsigned i = 0, ndecl = dtdecls.size(); i < ndecl; i++) + { + TS_ASSERT(dtsorts[i].isDatatype()); + TS_ASSERT(!dtsorts[i].getDatatype().isFinite()); + TS_ASSERT(dtsorts[i].getDatatype().getName() == dtdecls[i].getName()); + } + // verify the resolution was correct + Datatype dtTree = dtsorts[0].getDatatype(); + DatatypeConstructor dtcTreeNode = dtTree[0]; + TS_ASSERT(dtcTreeNode.getName() == "node"); + DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; + TS_ASSERT(dtsTreeNodeLeft.getName() == "left"); + // argument type should have resolved to be recursive + TS_ASSERT(dtsTreeNodeLeft.getRangeSort().isDatatype()); + TS_ASSERT(dtsTreeNodeLeft.getRangeSort() == dtsorts[0]); + + // fails due to empty datatype + std::vector dtdeclsBad; + DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD"); + dtdeclsBad.push_back(emptyD); + TS_ASSERT_THROWS(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException&); +} + void DatatypeBlack::testDatatypeStructs() { Sort intSort = d_solver.getIntegerSort(); @@ -138,6 +210,8 @@ void DatatypeBlack::testDatatypeNames() // create datatype sort to test DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName()); + TS_ASSERT(dtypeSpec.getName() == std::string("list")); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", intSort); cons.addSelector(head); @@ -163,4 +237,8 @@ void DatatypeBlack::testDatatypeNames() // get selector DatatypeSelector dselTail = dcons[1]; TS_ASSERT(dselTail.getName() == std::string("tail")); + TS_ASSERT(dselTail.getRangeSort() == dtypeSort); + + // possible to construct null datatype declarations if not using solver + TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&); } -- 2.30.2