From a8e45781feeb2d3fe9556de69e25c190f0030501 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 7 Dec 2021 19:51:47 -0800
Subject: [PATCH] api: Improve documentation for getDatatypeParamSorts().
 (#7763)

---
 src/api/cpp/cvc5.h                        | 9 ++++++++-
 src/api/java/io/github/cvc5/api/Sort.java | 6 ++++++
 src/api/python/cvc5.pxi                   | 9 ++++++++-
 3 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 61c7bb284..e40a4f721 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -743,7 +743,14 @@ class CVC5_EXPORT Sort
   /* Datatype sort ------------------------------------------------------- */
 
   /**
-   * @return the parameter sorts of a 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;
 
diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java
index 440b1ba59..26a963a56 100644
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -752,6 +752,12 @@ public class Sort extends AbstractPointer implements Comparable<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 datatype sort
    */
   public Sort[] getDatatypeParamSorts()
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index aa207cd40..d3e47e3d9 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2706,7 +2706,14 @@ cdef class Sort:
 
     def getDatatypeParamSorts(self):
         """
-            :return: the parameter sorts of a 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
+             :py:meth:`instantiate()`.
+
+             :return: the parameter sorts of a parametric datatype sort
         """
         param_sorts = []
         for s in self.csort.getDatatypeParamSorts():
-- 
2.30.2