api: Rename DatatypeSelector::getRangeSort() to getCodomainSort(). (#7831)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 024fa82393a209a9d7a57fac07845839ac26289b..71ce432fe729731cf1a4f91a929560faadb42ad8 100644 (file)
--- 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 726e74363e6f0c7e4f6b78b8dcebb050759d1574..3904a553ca379353dcb39932aa456d2831d46870 100644 (file)
--- 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 39ea2bb193ee20257612e119755a3e72118dd069..b96781fd59957426129c031998969e013b597a7b 100644 (file)
--- 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 Iterable<DatatypeConstr
    * 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/DatatypeConstructorDecl.java b/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java
index e1f5ca74682055b8563310a3fbc9f8bd6377f050..5cff1e09bbadb43265d0a95b3ca57163228e4e4c 100644 (file)
--- a/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java
+++ b/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java
@@ -35,7 +35,7 @@ public class DatatypeConstructorDecl extends AbstractPointer
   /**
    * 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
    */
   public void addSelector(String name, Sort sort)
   {
@@ -45,7 +45,8 @@ public class DatatypeConstructorDecl extends AbstractPointer
   private native void addSelector(long pointer, String name, long sortPointer);
 
   /**
-   * 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
    */
   public void addSelectorSelf(String name)

diff --git a/src/api/java/io/github/cvc5/api/DatatypeSelector.java b/src/api/java/io/github/cvc5/api/DatatypeSelector.java
index d388e7f2b8fc1f0763eea7d396907aaf6295a670..5f8aaabc633da4ddc9479aa4550e0a95533390b3 100644 (file)
--- a/src/api/java/io/github/cvc5/api/DatatypeSelector.java
+++ b/src/api/java/io/github/cvc5/api/DatatypeSelector.java
@@ -64,14 +64,14 @@ public class DatatypeSelector extends AbstractPointer
 
   private native long getUpdaterTerm(long pointer);
 
-  /** @return the range sort of this selector. */
-  public Sort getRangeSort()
+  /** @return the codomain sort of this selector. */
+  public Sort getCodomainSort()
   {
-    long sortPointer = getRangeSort(pointer);
+    long sortPointer = getCodomainSort(pointer);
     return new Sort(solver, sortPointer);
   }
 
-  private native long getRangeSort(long pointer);
+  private native long getCodomainSort(long pointer);
 
   /**
    * @return true if this DatatypeSelector is a null object

diff --git a/src/api/java/jni/datatype_selector.cpp b/src/api/java/jni/datatype_selector.cpp
index 4a33585139050c16ca3b5630a90c098b5d4381fe..c001d10c7b3688b30411d3c555243dc0688a395c 100644 (file)
--- a/src/api/java/jni/datatype_selector.cpp
+++ b/src/api/java/jni/datatype_selector.cpp
@@ -78,15 +78,17 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_DatatypeSelector_getUpdaterTerm(
 
 /*
  * Class:     io_github_cvc5_api_DatatypeSelector
- * Method:    getRangeSort
+ * Method:    getCodomainSort
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_DatatypeSelector_getRangeSort(
-    JNIEnv* env, jobject, jlong pointer)
+JNIEXPORT jlong JNICALL
+Java_io_github_cvc5_api_DatatypeSelector_getCodomainSort(JNIEnv* env,
+                                                         jobject,
+                                                         jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   DatatypeSelector* current = (DatatypeSelector*)pointer;
-  Sort* retPointer = new Sort(current->getRangeSort());
+  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 cc1bad1cdb6a477efd2a922c4828311e48ef17ce..e283fb7b65fa7a6161747ce6994932b252ba1fcd 100644 (file)
--- 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 9c4f59c35c89aa406fe967af32fab468271e1a24..88d69c26adc2349b55fb3e955a702da21879a976 100644 (file)
--- 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 a4f6bc7221bedcbccb140f9e711ed047cff9ae09..bf4a2cd118f43ea5c62c30237620941db1f722ca 100644 (file)
--- 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<DatatypeDecl> 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 002a08ff1b4409724d784be61db4118c7d03d117..afca8a92f0a77d47a8c99776fa3b8e1ccd2973fa 100644 (file)
--- 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<DatatypeDecl> 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 2d7e1c8d9928250af649ed73c9bb1c26316ac4ac..a883596deda054d2ce671b086f9abbc78a63253c 100644 (file)
--- 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()