From c69b57edf5ed63b5d6ad65e5ab7936a6e830099a Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 16 Dec 2021 21:20:49 -0800 Subject: [PATCH] api: Rename DatatypeSelector::getRangeSort() to getCodomainSort(). (#7831) --- src/api/cpp/cvc5.cpp | 4 ++-- src/api/cpp/cvc5.h | 13 +++++++------ src/api/java/io/github/cvc5/api/Datatype.java | 4 ++-- .../io/github/cvc5/api/DatatypeConstructorDecl.java | 5 +++-- .../java/io/github/cvc5/api/DatatypeSelector.java | 8 ++++---- src/api/java/jni/datatype_selector.cpp | 10 ++++++---- src/api/python/cvc5.pxd | 2 +- src/api/python/cvc5.pxi | 12 +++++++----- test/unit/api/cpp/datatype_api_black.cpp | 13 +++++++------ test/unit/api/java/DatatypeTest.java | 10 +++++----- test/unit/api/python/test_datatype_api.py | 10 +++++----- 11 files changed, 49 insertions(+), 42 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 024fa8239..71ce432fe 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3528,7 +3528,7 @@ void DatatypeConstructorDecl::addSelector(const std::string& name, CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK_SORT(sort); CVC5_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) - << "non-null range sort for selector"; + << "non-null codomain sort for selector"; //////// all checks before this line d_ctor->addArg(name, *sort.d_type); //////// @@ -3747,7 +3747,7 @@ Term DatatypeSelector::getUpdaterTerm() const CVC5_API_TRY_CATCH_END; } -Sort DatatypeSelector::getRangeSort() const +Sort DatatypeSelector::getCodomainSort() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 726e74363..3904a553c 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1722,11 +1722,12 @@ class CVC5_EXPORT DatatypeConstructorDecl /** * Add datatype selector declaration. * @param name the name of the datatype selector declaration to add - * @param sort the range sort of the datatype selector declaration to add + * @param sort the codomain sort of the datatype selector declaration to add */ void addSelector(const std::string& name, const Sort& sort); /** - * Add datatype selector declaration whose range type is the datatype itself. + * Add datatype selector declaration whose codomain type is the datatype + * itself. * @param name the name of the datatype selector declaration to add */ void addSelectorSelf(const std::string& name); @@ -1917,8 +1918,8 @@ class CVC5_EXPORT DatatypeSelector */ Term getUpdaterTerm() const; - /** @return the range sort of this selector. */ - Sort getRangeSort() const; + /** @return the codomain sort of this selector. */ + Sort getCodomainSort() const; /** * @return true if this DatatypeSelector is a null object @@ -2307,8 +2308,8 @@ class CVC5_EXPORT Datatype * Does this datatype have nested recursion? This method returns false if a * value of this datatype includes a subterm of its type that is nested * beneath a non-datatype type constructor. For example, a datatype - * T containing a constructor having a selector with range type (Set T) has - * nested recursion. + * T containing a constructor having a selector with codomain type (Set T) + * has nested recursion. * * @return true if this datatype has nested recursion */ diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java index 39ea2bb19..b96781fd5 100644 --- a/src/api/java/io/github/cvc5/api/Datatype.java +++ b/src/api/java/io/github/cvc5/api/Datatype.java @@ -178,8 +178,8 @@ public class Datatype extends AbstractPointer implements IterablegetRangeSort()); + Sort* retPointer = new Sort(current->getCodomainSort()); return (jlong)retPointer; CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index cc1bad1cd..e283fb7b6 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -115,7 +115,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": string getName() except + Term getSelectorTerm() except + Term getUpdaterTerm() except + - Sort getRangeSort() except + + Sort getCodomainSort() except + bint isNull() except + string toString() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 9c4f59c35..88d69c26a 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -323,13 +323,15 @@ cdef class DatatypeConstructorDecl: Add datatype selector declaration. :param name: the name of the datatype selector declaration to add. - :param sort: the range sort of the datatype selector declaration to add. + :param sort: the codomain sort of the datatype selector declaration + to add. """ self.cddc.addSelector(name.encode(), sort.csort) def addSelectorSelf(self, str name): """ - Add datatype selector declaration whose range sort is the datatype itself. + Add datatype selector declaration whose codomain sort is the + datatype itself. :param name: the name of the datatype selector declaration to add. """ @@ -426,12 +428,12 @@ cdef class DatatypeSelector: term.cterm = self.cds.getUpdaterTerm() return term - def getRangeSort(self): + def getCodomainSort(self): """ - :return: the range sort of this selector. + :return: the codomain sort of this selector. """ cdef Sort sort = Sort(self.solver) - sort.csort = self.cds.getRangeSort() + sort.csort = self.cds.getCodomainSort() return sort def isNull(self): diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index a4f6bc722..bf4a2cd11 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -131,8 +131,8 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSorts) DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; ASSERT_EQ(dtsTreeNodeLeft.getName(), "left"); // argument type should have resolved to be recursive - ASSERT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype()); - ASSERT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]); + ASSERT_TRUE(dtsTreeNodeLeft.getCodomainSort().isDatatype()); + ASSERT_EQ(dtsTreeNodeLeft.getCodomainSort(), dtsorts[0]); // fails due to empty datatype std::vector dtdeclsBad; @@ -247,7 +247,7 @@ TEST_F(TestApiBlackDatatype, datatypeNames) // get selector DatatypeSelector dselTail = dcons[1]; ASSERT_EQ(dselTail.getName(), std::string("tail")); - ASSERT_EQ(dselTail.getRangeSort(), dtypeSort); + ASSERT_EQ(dselTail.getCodomainSort(), dtypeSort); // get selector from datatype ASSERT_NO_THROW(dt.getSelector("head")); @@ -417,9 +417,10 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) // this is not well-founded due to non-simple recursion ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); ASSERT_EQ(dtsorts.size(), 1); - ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()); - ASSERT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(), - dtsorts[0]); + ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getCodomainSort().isArray()); + ASSERT_EQ( + dtsorts[0].getDatatype()[0][0].getCodomainSort().getArrayElementSort(), + dtsorts[0]); ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded()); ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index 002a08ff1..afca8a92f 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -112,8 +112,8 @@ class DatatypeTest DatatypeSelector dtsTreeNodeLeft = dtcTreeNode.getSelector(0); assertEquals(dtsTreeNodeLeft.getName(), "left"); // argument type should have resolved to be recursive - assertTrue(dtsTreeNodeLeft.getRangeSort().isDatatype()); - assertEquals(dtsTreeNodeLeft.getRangeSort(), dtsorts.get(0)); + assertTrue(dtsTreeNodeLeft.getCodomainSort().isDatatype()); + assertEquals(dtsTreeNodeLeft.getCodomainSort(), dtsorts.get(0)); // fails due to empty datatype List dtdeclsBad = new ArrayList<>(); @@ -225,7 +225,7 @@ class DatatypeTest // get selector DatatypeSelector dselTail = dcons.getSelector(1); assertEquals(dselTail.getName(), "tail"); - assertEquals(dselTail.getRangeSort(), dtypeSort); + assertEquals(dselTail.getCodomainSort(), dtypeSort); // possible to construct null datatype declarations if not using solver assertThrows(CVC5ApiException.class, () -> d_solver.getNullDatatypeDecl().getName()); @@ -391,12 +391,12 @@ class DatatypeTest dtsorts = atomic.get(); assertEquals(dtsorts.size(), 1); assertTrue( - dtsorts.get(0).getDatatype().getConstructor(0).getSelector(0).getRangeSort().isArray()); + dtsorts.get(0).getDatatype().getConstructor(0).getSelector(0).getCodomainSort().isArray()); assertEquals(dtsorts.get(0) .getDatatype() .getConstructor(0) .getSelector(0) - .getRangeSort() + .getCodomainSort() .getArrayElementSort(), dtsorts.get(0)); assertTrue(dtsorts.get(0).getDatatype().isWellFounded()); diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index 2d7e1c8d9..a883596de 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -127,8 +127,8 @@ def test_mk_datatype_sorts(solver): dtsTreeNodeLeft = dtcTreeNode[0] assert dtsTreeNodeLeft.getName() == "left" # argument type should have resolved to be recursive - assert dtsTreeNodeLeft.getRangeSort().isDatatype() - assert dtsTreeNodeLeft.getRangeSort() == dtsorts[0] + assert dtsTreeNodeLeft.getCodomainSort().isDatatype() + assert dtsTreeNodeLeft.getCodomainSort() == dtsorts[0] # fails due to empty datatype dtdeclsBad = [] @@ -245,7 +245,7 @@ def test_datatype_names(solver): # get selector dselTail = dcons[1] assert dselTail.getName() == "tail" - assert dselTail.getRangeSort() == dtypeSort + assert dselTail.getCodomainSort() == dtypeSort # get selector from datatype dt.getSelector("head") @@ -408,8 +408,8 @@ def test_datatype_simply_rec(solver): # this is not well-founded due to non-simple recursion dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) assert len(dtsorts) == 1 - assert dtsorts[0].getDatatype()[0][0].getRangeSort().isArray() - assert dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort() \ + assert dtsorts[0].getDatatype()[0][0].getCodomainSort().isArray() + assert dtsorts[0].getDatatype()[0][0].getCodomainSort().getArrayElementSort() \ == dtsorts[0] assert dtsorts[0].getDatatype().isWellFounded() assert dtsorts[0].getDatatype().hasNestedRecursion() -- 2.30.2