diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-12-07 19:51:47 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-08 03:51:47 +0000 |
| commit | a8e45781feeb2d3fe9556de69e25c190f0030501 (patch) | |
| tree | 0b7f87be7b683b4b2c3c4d69c13a7392b5f75c28 | |
| parent | fd127d90b9cf4c769c1fe1a9b16b811847a0eed9 (diff) | |
api: Improve documentation for getDatatypeParamSorts(). (#7763)
| -rw-r--r-- | src/api/cpp/cvc5.h | 9 | ||||
| -rw-r--r-- | src/api/java/io/github/cvc5/api/Sort.java | 6 | ||||
| -rw-r--r-- | 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(): |