Python api documentation for sorts (#7440)

This PR adds documentation for the Sort python API.

5 files changed, 313 insertions, 15 deletions

diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst
index a6aca2cf9..f6258af2d 100644
--- a/docs/api/python/python.rst
+++ b/docs/api/python/python.rst
@@ -13,7 +13,6 @@ Python API Documentation
     :maxdepth: 1
 
     quickstart
-    solver
     datatype
     datatypeconstructor
     datatypeconstructordecl
@@ -23,4 +22,6 @@ Python API Documentation
     op
     result
     roundingmode
+    solver
+    sort
     unknownexplanation
diff --git a/docs/api/python/sort.rst b/docs/api/python/sort.rst
new file mode 100644
index 000000000..270113e0c
--- /dev/null
+++ b/docs/api/python/sort.rst
@@ -0,0 +1,6 @@
+Sort
+================
+
+.. autoclass:: pycvc5.Sort
+    :members:
+    :undoc-members:
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index c618106a6..f0a36b792 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -354,19 +354,19 @@ class CVC5_EXPORT Sort
 
   /**
    * Is this a Boolean sort?
-   * @return true if the sort is a Boolean sort
+   * @return true if the sort is the Boolean sort
    */
   bool isBoolean() const;
 
   /**
    * Is this a integer sort?
-   * @return true if the sort is a integer sort
+   * @return true if the sort is the integer sort
    */
   bool isInteger() const;
 
   /**
    * Is this a real sort?
-   * @return true if the sort is a real sort
+   * @return true if the sort is the real sort
    */
   bool isReal() const;
 
@@ -462,7 +462,7 @@ class CVC5_EXPORT Sort
 
   /**
    * Is this an array sort?
-   * @return true if the sort is a array sort
+   * @return true if the sort is an array sort
    */
   bool isArray() const;
 
@@ -485,8 +485,8 @@ class CVC5_EXPORT Sort
   bool isSequence() const;
 
   /**
-   * Is this a sort kind?
-   * @return true if this is a sort kind
+   * Is this an uninterpreted sort?
+   * @return true if this is an uninterpreted sort
    */
   bool isUninterpretedSort() const;
 
@@ -499,9 +499,9 @@ class CVC5_EXPORT Sort
   /**
    * Is this a first-class sort?
    * First-class sorts are sorts for which:
-   * (1) we handle equalities between terms of that type, and
-   * (2) they are allowed to be parameters of parametric sorts (e.g. index or
-   *     element sorts of arrays).
+   * 1. we handle equalities between terms of that type, and
+   * 2. they are allowed to be parameters of parametric sorts (e.g. index or
+   * element sorts of arrays).
    *
    * Examples of sorts that are not first-class include sort constructor sorts
    * and regular expression sorts.
@@ -641,7 +641,7 @@ class CVC5_EXPORT Sort
   Sort getArrayIndexSort() const;
 
   /**
-   * @return the array element sort of an array element sort
+   * @return the array element sort of an array sort
    */
   Sort getArrayElementSort() const;
 
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index cf405b519..42aee08b0 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -341,6 +341,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isComparableTo(Sort s) except +
         Datatype getDatatype() except +
         Sort instantiate(const vector[Sort]& params) except +
+        Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except +
         size_t getConstructorArity() except +
         vector[Sort] getConstructorDomainSorts() except +
         Sort getConstructorCodomainSort() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 9391dbdd1..9a7358bbf 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -609,7 +609,7 @@ cdef class Result:
             :return: True if query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query  query and cvc5 was not able to determine if it is entailed.
         """
         return self.cr.isEntailmentUnknown()
-    
+
     def getUnknownExplanation(self):
         """
             :return: an explanation for an unknown query result.
@@ -641,7 +641,7 @@ cdef class RoundingMode:
         arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
         The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
         Standard 754.
-        
+
         Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`.
     """
     cdef c_RoundingMode crm
@@ -1041,7 +1041,7 @@ cdef class Solver:
                         raise ValueError("Argument {} must fit in a uint32_t".format(a))
 
                     v.push_back((<uint32_t?> a))
-                op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v)   
+                op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v)
             else:
                 raise ValueError("Unsupported signature"
                                  " mkOp: {}".format(" X ".join([str(k), str(args[0])])))
@@ -1347,7 +1347,7 @@ cdef class Solver:
 
     def mkRoundingMode(self, RoundingMode rm):
         """Create a roundingmode constant.
-        
+
         :param rm: the floating point rounding mode this constant represents
         """
         cdef Term term = Term(self)
@@ -2191,6 +2191,9 @@ cdef class Solver:
 
 
 cdef class Sort:
+    """
+    The sort of a cvc5 term.
+    """
     cdef c_Sort csort
     cdef Solver solver
     def __cinit__(self, Solver solver):
@@ -2225,98 +2228,266 @@ cdef class Sort:
         return csorthash(self.csort)
 
     def isNull(self):
+        """:return: True if this Sort is a null sort."""
         return self.csort.isNull()
 
     def isBoolean(self):
+        """
+            Is this a Boolean sort?
+
+            :return: True if the sort is the Boolean sort.
+        """
         return self.csort.isBoolean()
 
     def isInteger(self):
+        """
+            Is this an integer sort?
+
+            :return: True if the sort is the integer sort.
+        """
         return self.csort.isInteger()
 
     def isReal(self):
+        """
+            Is this a real sort?
+
+            :return: True if the sort is the real sort.
+        """
         return self.csort.isReal()
 
     def isString(self):
+        """
+            Is this a string sort?
+
+            :return: True if the sort is the string sort.
+        """
         return self.csort.isString()
 
     def isRegExp(self):
+        """
+            Is this a regexp sort?
+
+            :return: True if the sort is the regexp sort.
+        """
         return self.csort.isRegExp()
 
     def isRoundingMode(self):
+        """
+            Is this a rounding mode sort?
+
+            :return: True if the sort is the rounding mode sort.
+        """
         return self.csort.isRoundingMode()
 
     def isBitVector(self):
+        """
+            Is this a bit-vector sort?
+
+            :return: True if the sort is a bit-vector sort.
+        """
         return self.csort.isBitVector()
 
     def isFloatingPoint(self):
+        """
+            Is this a floating-point sort?
+
+            :return: True if the sort is a bit-vector sort.
+        """
         return self.csort.isFloatingPoint()
 
     def isDatatype(self):
+        """
+            Is this a datatype sort?
+
+            :return: True if the sort is a datatype sort.
+        """
         return self.csort.isDatatype()
 
     def isParametricDatatype(self):
+        """
+            Is this a parametric datatype sort?
+
+            :return: True if the sort is a parametric datatype sort.
+        """
         return self.csort.isParametricDatatype()
 
     def isConstructor(self):
+        """
+            Is this a constructor sort?
+
+            :return: True if the sort is a constructor sort.
+        """
         return self.csort.isConstructor()
 
     def isSelector(self):
+        """
+            Is this a selector sort?
+
+            :return: True if the sort is a selector sort.
+        """
         return self.csort.isSelector()
 
     def isTester(self):
+        """
+            Is this a tester sort?
+
+            :return: True if the sort is a selector sort.
+        """
         return self.csort.isTester()
 
     def isUpdater(self):
+        """
+            Is this a datatype updater sort?
+
+            :return: True if the sort is a datatype updater sort.
+        """
         return self.csort.isUpdater()
 
     def isFunction(self):
+        """
+            Is this a function sort?
+
+            :return: True if the sort is a function sort.
+        """
         return self.csort.isFunction()
 
     def isPredicate(self):
+        """
+            Is this a predicate sort?
+            That is, is this a function sort mapping to Boolean? All predicate
+            sorts are also function sorts.
+
+            :return: True if the sort is a predicate sort.
+        """
         return self.csort.isPredicate()
 
     def isTuple(self):
+        """
+            Is this a tuple sort?
+
+            :return: True if the sort is a tuple sort.
+        """
         return self.csort.isTuple()
 
     def isRecord(self):
+        """
+            Is this a record sort?
+
+            :return: True if the sort is a record sort.
+        """
         return self.csort.isRecord()
 
     def isArray(self):
+        """
+            Is this an array sort?
+
+            :return: True if the sort is an array sort.
+        """
         return self.csort.isArray()
 
     def isSet(self):
+        """
+            Is this a set sort?
+
+            :return: True if the sort is a set sort.
+        """
         return self.csort.isSet()
 
     def isBag(self):
+        """
+            Is this a bag sort?
+
+            :return: True if the sort is a bag sort.
+        """
         return self.csort.isBag()
 
     def isSequence(self):
+        """
+            Is this a sequence sort?
+
+            :return: True if the sort is a sequence sort.
+        """
         return self.csort.isSequence()
 
     def isUninterpretedSort(self):
+        """
+            Is this a sort uninterpreted?
+
+            :return: True if the sort is uninterpreted.
+        """
         return self.csort.isUninterpretedSort()
 
     def isSortConstructor(self):
+        """
+            Is this a sort constructor kind?
+
+            :return: True if this a sort constructor kind.
+        """
         return self.csort.isSortConstructor()
 
     def isFirstClass(self):
+        """
+            Is this a first-class sort?
+            First-class sorts are sorts for which:
+
+            1. we handle equalities between terms of that type, and
+            2. they are allowed to be parameters of parametric sorts
+               (e.g. index or element sorts of arrays).
+
+            Examples of sorts that are not first-class include sort constructor
+            sorts and regular expression sorts.
+
+            :return: True if the sort is a first-class sort.
+        """
         return self.csort.isFirstClass()
 
     def isFunctionLike(self):
+        """
+            Is this a function-LIKE sort?
+
+            Anything function-like except arrays (e.g., datatype selectors) is
+            considered a function here. Function-like terms can not be the argument
+            or return value for any term that is function-like.
+            This is mainly to avoid higher order.
+
+            Note that arrays are explicitly not considered function-like here.
+
+            :return: True if this is a function-like sort
+        """
         return self.csort.isFunctionLike()
 
     def isSubsortOf(self, Sort sort):
+        """
+            Is this sort a subsort of the given sort?
+
+	    :return: True if this sort is a subsort of s
+        """
         return self.csort.isSubsortOf(sort.csort)
 
     def isComparableTo(self, Sort sort):
+        """
+            Is this sort comparable to the given sort
+            (i.e., do they share a common ancestor in the subsort tree)?
+
+            :return: True if this sort is comparable to s
+        """
         return self.csort.isComparableTo(sort.csort)
 
     def getDatatype(self):
+        """
+            :return: the underlying datatype of a datatype sort
+        """
         cdef Datatype d = Datatype(self.solver)
         d.cd = self.csort.getDatatype()
         return d
 
     def instantiate(self, params):
+        """
+            Instantiate a parameterized datatype/sort sort.
+            Create sorts parameter with :py:meth:`Solver.mkParamSort()`
+
+            :param params: the list of sort parameters to instantiate with
+        """
         cdef Sort sort = Sort(self.solver)
         cdef vector[c_Sort] v
         for s in params:
@@ -2324,10 +2495,54 @@ cdef class Sort:
         sort.csort = self.csort.instantiate(v)
         return sort
 
+    def substitute(self, sort_or_list_1, sort_or_list_2):
+        """
+            Substitution of Sorts.
+
+	    :param sort_or_list_1: the subsort or subsorts to be substituted within this sort.
+            :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort.
+        """
+
+        # The resulting sort after substitution
+        cdef Sort sort = Sort(self.solver)
+        # lists for substitutions
+        cdef vector[c_Sort] ces
+        cdef vector[c_Sort] creplacements
+
+        # normalize the input parameters to be lists
+        if isinstance(sort_or_list_1, list):
+            assert isinstance(sort_or_list_2, list)
+            es = sort_or_list_1
+            replacements = sort_or_list_2
+            if len(es) != len(replacements):
+                raise RuntimeError("Expecting list inputs to substitute to "
+                                   "have the same length but got: "
+                                   "{} and {}".format(len(es), len(replacements)))
+
+            for e, r in zip(es, replacements):
+                ces.push_back((<Sort?> e).csort)
+                creplacements.push_back((<Sort?> r).csort)
+
+        else:
+            # add the single elements to the vectors
+            ces.push_back((<Sort?> sort_or_list_1).csort)
+            creplacements.push_back((<Sort?> sort_or_list_2).csort)
+
+        # call the API substitute method with lists
+        sort.csort = self.csort.substitute(ces, creplacements)
+        return sort
+
+
     def getConstructorArity(self):
+        """
+            :return: the arity of a constructor sort.
+        """
         return self.csort.getConstructorArity()
 
     def getConstructorDomainSorts(self):
+        """
+            :return: the domain sorts of a constructor sort
+        """
         domain_sorts = []
         for s in self.csort.getConstructorDomainSorts():
             sort = Sort(self.solver)
@@ -2336,34 +2551,55 @@ cdef class Sort:
         return domain_sorts
 
     def getConstructorCodomainSort(self):
+        """
+            :return: the codomain sort of a constructor sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getConstructorCodomainSort()
         return sort
 
     def getSelectorDomainSort(self):
+        """
+            :return: the domain sort of a selector sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getSelectorDomainSort()
         return sort
 
     def getSelectorCodomainSort(self):
+        """
+            :return: the codomain sort of a selector sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getSelectorCodomainSort()
         return sort
 
     def getTesterDomainSort(self):
+        """
+            :return: the domain sort of a tester sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getTesterDomainSort()
         return sort
 
     def getTesterCodomainSort(self):
+        """
+            :return: the codomain sort of a tester sort, which is the Boolean sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getTesterCodomainSort()
         return sort
 
     def getFunctionArity(self):
+        """
+            :return: the arity of a function sort
+        """
         return self.csort.getFunctionArity()
 
     def getFunctionDomainSorts(self):
+        """
+            :return: the domain sorts of a function sort
+        """
         domain_sorts = []
         for s in self.csort.getFunctionDomainSorts():
             sort = Sort(self.solver)
@@ -2372,42 +2608,69 @@ cdef class Sort:
         return domain_sorts
 
     def getFunctionCodomainSort(self):
+        """
+            :return: the codomain sort of a function sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getFunctionCodomainSort()
         return sort
 
     def getArrayIndexSort(self):
+        """
+            :return: the array index sort of an array sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getArrayIndexSort()
         return sort
 
     def getArrayElementSort(self):
+        """
+            :return: the array element sort of an array sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getArrayElementSort()
         return sort
 
     def getSetElementSort(self):
+        """
+            :return: the element sort of a set sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getSetElementSort()
         return sort
 
     def getBagElementSort(self):
+        """
+            :return: the element sort of a bag sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getBagElementSort()
         return sort
 
     def getSequenceElementSort(self):
+        """
+            :return: the element sort of a sequence sort
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.csort.getSequenceElementSort()
         return sort
 
     def getUninterpretedSortName(self):
+        """
+            :return: the name of an uninterpreted sort
+        """
         return self.csort.getUninterpretedSortName().decode()
 
     def isUninterpretedSortParameterized(self):
+        """
+            :return: True if an uninterpreted sort is parameterized
+        """
         return self.csort.isUninterpretedSortParameterized()
 
     def getUninterpretedSortParamSorts(self):
+        """
+            :return: the parameter sorts of an uninterpreted sort
+        """
         param_sorts = []
         for s in self.csort.getUninterpretedSortParamSorts():
             sort = Sort(self.solver)
@@ -2416,21 +2679,39 @@ cdef class Sort:
         return param_sorts
 
     def getSortConstructorName(self):
+        """
+            :return: the name of a sort constructor sort
+        """
         return self.csort.getSortConstructorName().decode()
 
     def getSortConstructorArity(self):
+        """
+            :return: the arity of a sort constructor sort
+        """
         return self.csort.getSortConstructorArity()
 
     def getBitVectorSize(self):
+        """
+            :return: the bit-width of the bit-vector sort
+        """
         return self.csort.getBitVectorSize()
 
     def getFloatingPointExponentSize(self):
+        """
+            :return: the bit-width of the exponent of the floating-point sort
+        """
         return self.csort.getFloatingPointExponentSize()
 
     def getFloatingPointSignificandSize(self):
+        """
+            :return: the width of the significand of the floating-point sort
+        """
         return self.csort.getFloatingPointSignificandSize()
 
     def getDatatypeParamSorts(self):
+        """
+            :return: the parameter sorts of a datatype sort
+        """
         param_sorts = []
         for s in self.csort.getDatatypeParamSorts():
             sort = Sort(self.solver)
@@ -2439,12 +2720,21 @@ cdef class Sort:
         return param_sorts
 
     def getDatatypeArity(self):
+        """
+            :return: the arity of a datatype sort
+        """
         return self.csort.getDatatypeArity()
 
     def getTupleLength(self):
+        """
+            :return: the length of a tuple sort
+        """
         return self.csort.getTupleLength()
 
     def getTupleSorts(self):
+        """
+            :return: the element sorts of a tuple sort
+        """
         tuple_sorts = []
         for s in self.csort.getTupleSorts():
             sort = Sort(self.solver)