api: Add Sort::getInstantiatedParameters(). (cvc5#8445)

This adds a function to retrieve the sort arguments an instantiated
sort has been instantiated with. It further deletes
Sort::getDatatypeParamSorts() and
Sort::getUninterpretedSortParamSorts().

Author: aniemetz

src/api/cpp/cvc5.cpp

@@ -1445,6 +1445,18 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   CVC5_API_TRY_CATCH_END;
 }
 
+std::vector<Sort> Sort::getInstantiatedParameters() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
+  CVC5_API_CHECK(d_type->isInstantiated())
+      << "Expected instantiated parametric sort";
+  //////// all checks before this line
+  return typeNodeVectorToSorts(d_solver, d_type->getInstantiatedParamTypes());
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Sort Sort::substitute(const Sort& sort, const Sort& replacement) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -1672,27 +1684,6 @@ Sort Sort::getSequenceElementSort() const
   CVC5_API_TRY_CATCH_END;
 }
 
-/* Uninterpreted sort -------------------------------------------------- */
-
-std::vector<Sort> Sort::getUninterpretedSortParamSorts() const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
-  //////// all checks before this line
-
-  /* This method is not implemented in the NodeManager, since whether a
-   * uninterpreted sort is parameterized is irrelevant for solving. */
-  std::vector<TypeNode> params;
-  for (size_t i = 0, nchildren = d_type->getNumChildren(); i < nchildren; i++)
-  {
-    params.push_back((*d_type)[i]);
-  }
-  return typeNodeVectorToSorts(d_solver, params);
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 /* Sort constructor sort ----------------------------------------------- */
 
 size_t Sort::getUninterpretedSortConstructorArity() const
@@ -1745,18 +1736,6 @@ uint32_t Sort::getFloatingPointSignificandSize() const
 
 /* Datatype sort ------------------------------------------------------- */
 
-std::vector<Sort> Sort::getDatatypeParamSorts() const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK_NOT_NULL;
-  CVC5_API_CHECK(d_type->isParametricDatatype())
-      << "Not a parametric datatype sort.";
-  //////// all checks before this line
-  return typeNodeVectorToSorts(d_solver, d_type->getDType().getParameters());
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 size_t Sort::getDatatypeArity() const
 {
   CVC5_API_TRY_CATCH_BEGIN;

src/api/cpp/cvc5.h

@@ -615,14 +615,25 @@ class CVC5_EXPORT Sort
    * Instantiate a parameterized datatype sort or uninterpreted sort
    * constructor sort.
    *
-   * Create sorts parameter with Solver::mkParamSort().
+   * Create sort parameters with Solver::mkParamSort().
    *
    * @warning This method is experimental and may change in future versions.
    *
    * @param params the list of sort parameters to instantiate with
+   * @return the instantiated sort
    */
   Sort instantiate(const std::vector<Sort>& params) const;
 
+  /**
+   * Get the sorts used to instantiate the sort parameters of a parametric
+   * sort (parametric datatype or uninterpreted sort constructor sort,
+   * see Sort::instantiate(const std::vector<Sort>& const)).
+   *
+   * @return the sorts used to instantiate the sort parameters of a
+   *         parametric sort
+   */
+  std::vector<Sort> getInstantiatedParameters() const;
+
   /**
    * Substitution of Sorts.
    *
@@ -768,11 +779,6 @@ class CVC5_EXPORT Sort
    */
   bool isUninterpretedSortParameterized() const;
 
-  /**
-   * @return the parameter sorts of an uninterpreted sort
-   */
-  std::vector<Sort> getUninterpretedSortParamSorts() const;
-
   /* Sort constructor sort ----------------------------------------------- */
 
   /**
@@ -801,18 +807,6 @@ class CVC5_EXPORT Sort
 
   /* Datatype sort ------------------------------------------------------- */
 
-  /**
-   *
-   * Return the parameters of a parametric datatype sort. If this sort is a
-   * non-instantiated parametric datatype, this returns the parameter sorts of
-   * the underlying datatype. If this sort is an instantiated parametric
-   * datatype, then this returns the sort parameters that were used to
-   * construct the sort via Sort::instantiate().
-   *
-   * @return the parameter sorts of a parametric datatype sort.
-   */
-  std::vector<Sort> getDatatypeParamSorts() const;
-
   /**
    * @return the arity of a datatype sort
    */

src/api/java/io/github/cvc5/api/Sort.java

@@ -399,6 +399,7 @@ public Datatype getDatatype()
    * @apiNote This method is experimental and may change in future versions.
    *
    * @param params the list of sort parameters to instantiate with
+   * @return the instantiated sort
    */
   public Sort instantiate(List<Sort> params)
   {
@@ -424,6 +425,22 @@ public Sort instantiate(Sort[] params)
 
   private native long instantiate(long pointer, long[] paramsPointers);
 
+  /**
+   * Get the sorts used to instantiate the sort parameters of a parametric
+   * sort (parametric datatype or uninterpreted sort constructor sort,
+   * see Sort.instantiate()).
+   *
+   * @return the sorts used to instantiate the sort parameters of a
+   *         parametric sort
+   */
+  public Sort[] getInstantiatedParameters()
+  {
+    long[] pointers = getInstantiatedParameters(pointer);
+    return Utils.getSorts(solver, pointers);
+  }
+
+  private native long[] getInstantiatedParameters(long pointer);
+
   /**
    * Substitution of Sorts.
    *
@@ -661,19 +678,6 @@ public Sort getSequenceElementSort()
 
   private native long getSequenceElementSort(long pointer);
 
-  /* Uninterpreted sort -------------------------------------------------- */
-
-  /**
-   * @return the parameter sorts of an uninterpreted sort
-   */
-  public Sort[] getUninterpretedSortParamSorts()
-  {
-    long[] pointers = getUninterpretedSortParamSorts(pointer);
-    return Utils.getSorts(solver, pointers);
-  }
-
-  private native long[] getUninterpretedSortParamSorts(long pointer);
-
   /* Sort constructor sort ----------------------------------------------- */
 
   /**
@@ -722,23 +726,6 @@ public int getFloatingPointSignificandSize()
 
   /* Datatype sort ------------------------------------------------------- */
 
-  /**
-   * Return the parameters of a parametric datatype sort. If this sort is a
-   * non-instantiated parametric datatype, this returns the parameter sorts of
-   * the underlying datatype. If this sort is an instantiated parametric
-   * datatype, then this returns the sort parameters that were used to
-   * construct the sort via Sort.instantiate().
-   *
-   * @return the parameter sorts of a datatype sort
-   */
-  public Sort[] getDatatypeParamSorts()
-  {
-    long[] pointers = getDatatypeParamSorts(pointer);
-    return Utils.getSorts(solver, pointers);
-  }
-
-  private native long[] getDatatypeParamSorts(long pointer);
-
   /**
    * @return the arity of a datatype sort
    */

src/api/java/jni/sort.cpp

@@ -468,6 +468,30 @@ Java_io_github_cvc5_api_Sort_isInstantiated(JNIEnv* env, jobject, jlong pointer)
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
+/*
+ * Class:     io_github_cvc5_api_Sort
+ * Method:    getInstantiatedParameters
+ * Signature: (J)[J
+ */
+JNIEXPORT jlongArray JNICALL
+Java_io_github_cvc5_api_Sort_getInstantiatedParameters(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Sort* current = reinterpret_cast<Sort*>(pointer);
+  std::vector<Sort> sorts = current->getInstantiatedParameters();
+  std::vector<jlong> sortPointers(sorts.size());
+  for (size_t i = 0; i < sorts.size(); i++)
+  {
+    sortPointers[i] = reinterpret_cast<jlong>(new Sort(sorts[i]));
+  }
+  jlongArray ret = env->NewLongArray(sorts.size());
+  env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data());
+  return ret;
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
+}
+
 /*
  * Class:     io_github_cvc5_api_Sort
  * Method:    getDatatype
@@ -840,30 +864,6 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getSequenceElementSort(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
-/*
- * Class:     io_github_cvc5_api_Sort
- * Method:    getUninterpretedSortParamSorts
- * Signature: (J)[J
- */
-JNIEXPORT jlongArray JNICALL
-Java_io_github_cvc5_api_Sort_getUninterpretedSortParamSorts(JNIEnv* env,
-                                                            jobject,
-                                                            jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Sort* current = reinterpret_cast<Sort*>(pointer);
-  std::vector<Sort> sorts = current->getUninterpretedSortParamSorts();
-  std::vector<jlong> sortPointers(sorts.size());
-  for (size_t i = 0; i < sorts.size(); i++)
-  {
-    sortPointers[i] = reinterpret_cast<jlong>(new Sort(sorts[i]));
-  }
-  jlongArray ret = env->NewLongArray(sorts.size());
-  env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data());
-  return ret;
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
 /*
  * Class:     io_github_cvc5_api_Sort
  * Method:    getUninterpretedSortConstructorArity
@@ -926,28 +926,6 @@ Java_io_github_cvc5_api_Sort_getFloatingPointSignificandSize(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
-/*
- * Class:     io_github_cvc5_api_Sort
- * Method:    getDatatypeParamSorts
- * Signature: (J)[J
- */
-JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Sort_getDatatypeParamSorts(
-    JNIEnv* env, jobject, jlong pointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Sort* current = reinterpret_cast<Sort*>(pointer);
-  std::vector<Sort> sorts = current->getDatatypeParamSorts();
-  std::vector<jlong> sortPointers(sorts.size());
-  for (size_t i = 0; i < sorts.size(); i++)
-  {
-    sortPointers[i] = reinterpret_cast<jlong>(new Sort(sorts[i]));
-  }
-  jlongArray ret = env->NewLongArray(sorts.size());
-  env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data());
-  return ret;
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
-}
-
 /*
  * Class:     io_github_cvc5_api_Sort
  * Method:    getDatatypeArity

src/api/python/cvc5.pxd

@@ -400,6 +400,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isInstantiated() except +
         Datatype getDatatype() except +
         Sort instantiate(const vector[Sort]& params) except +
+        vector[Sort] getInstantiatedParameters() except +
         Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except +
         size_t getConstructorArity() except +
         vector[Sort] getConstructorDomainSorts() except +
@@ -416,12 +417,10 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Sort getSetElementSort() except +
         Sort getBagElementSort() except +
         Sort getSequenceElementSort() except +
-        vector[Sort] getUninterpretedSortParamSorts() except +
         size_t getUninterpretedSortConstructorArity() except +
         uint32_t getBitVectorSize() except +
         uint32_t getFloatingPointExponentSize() except +
         uint32_t getFloatingPointSignificandSize() except +
-        vector[Sort] getDatatypeParamSorts() except +
         size_t getDatatypeArity() except +
         size_t getTupleLength() except +
         vector[Sort] getTupleSorts() except +

src/api/python/cvc5.pxi

@@ -2837,6 +2837,7 @@ cdef class Sort:
                          versions.
 
             :param params: the list of sort parameters to instantiate with
+            :return: the instantiated sort
         """
         cdef Sort sort = Sort(self.solver)
         cdef vector[c_Sort] v
@@ -2845,6 +2846,22 @@ cdef class Sort:
         sort.csort = self.csort.instantiate(v)
         return sort
 
+    def getInstantiatedParameters(self):
+        """
+            Get the sorts used to instantiate the sort parameters of a
+            parametric sort (parametric datatype or uninterpreted sort
+            constructor sort, see Sort.instantiate()).
+
+            :return the sorts used to instantiate the sort parameters of a
+                    parametric sort
+        """
+        instantiated_sorts = []
+        for s in self.csort.getInstantiatedParameters():
+            sort = Sort(self.solver)
+            sort.csort = s
+            instantiated_sorts.append(sort)
+        return instantiated_sorts
+
     def substitute(self, sort_or_list_1, sort_or_list_2):
         """
         Substitution of Sorts.
@@ -3017,17 +3034,6 @@ cdef class Sort:
         sort.csort = self.csort.getSequenceElementSort()
         return sort
 
-    def getUninterpretedSortParamSorts(self):
-        """
-            :return: the parameter sorts of an uninterpreted sort
-        """
-        param_sorts = []
-        for s in self.csort.getUninterpretedSortParamSorts():
-            sort = Sort(self.solver)
-            sort.csort = s
-            param_sorts.append(sort)
-        return param_sorts
-
     def getUninterpretedSortConstructorArity(self):
         """
             :return: the arity of a sort constructor sort
@@ -3052,24 +3058,6 @@ cdef class Sort:
         """
         return self.csort.getFloatingPointSignificandSize()
 
-    def getDatatypeParamSorts(self):
-        """
-             Return the parameters of a parametric datatype sort. If this sort
-             is a non-instantiated parametric datatype, this returns the
-             parameter sorts of the underlying datatype. If this sort is an
-             instantiated parametric datatype, then this returns the sort
-             parameters that were used to construct the sort via
-             :py:meth:`instantiate()`.
-
-             :return: the parameter sorts of a parametric datatype sort
-        """
-        param_sorts = []
-        for s in self.csort.getDatatypeParamSorts():
-            sort = Sort(self.solver)
-            sort.csort = s
-            param_sorts.append(sort)
-        return param_sorts
-
     def getDatatypeArity(self):
         """
             :return: the arity of a datatype sort

src/expr/type_node.cpp

@@ -364,7 +364,9 @@ std::vector<TypeNode> TypeNode::getInstantiatedParamTypes() const
 {
   Assert(isInstantiated());
   vector<TypeNode> params;
-  for (uint32_t i = 1, i_end = getNumChildren(); i < i_end; ++i)
+  for (uint32_t i = isInstantiatedDatatype() ? 1 : 0, i_end = getNumChildren();
+       i < i_end;
+       ++i)
   {
     params.push_back((*this)[i]);
   }