python docs for Datatype-related classes (#7058)

1 files changed, 67 insertions, 0 deletions

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 68998d521..865e51cb1 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -193,6 +193,7 @@ cdef class Datatype:
 
 
 cdef class DatatypeConstructor:
+    """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`."""
     cdef c_DatatypeConstructor cdc
     cdef Solver solver
     def __cinit__(self, Solver solver):
@@ -210,32 +211,58 @@ cdef class DatatypeConstructor:
         return ds
 
     def getName(self):
+        """
+            :return: the name of the constructor.
+        """
         return self.cdc.getName().decode()
 
     def getConstructorTerm(self):
+        """
+            :return: the constructor operator as a term.
+        """
         cdef Term term = Term(self.solver)
         term.cterm = self.cdc.getConstructorTerm()
         return term
 
     def getSpecializedConstructorTerm(self, Sort retSort):
+        """
+            Specialized method for parametric datatypes (see :cpp:func:`DatatypeConstructor::getSpecializedConstructorTerm() <cvc5::api::DatatypeConstructor::getSpecializedConstructorTerm>`).
+
+            :param retSort: the desired return sort of the constructor
+            :return: the constructor operator as a term.
+        """
         cdef Term term = Term(self.solver)
         term.cterm = self.cdc.getSpecializedConstructorTerm(retSort.csort)
         return term
 
     def getTesterTerm(self):
+        """
+            :return: the tester operator that is related to this constructor, as a term.
+        """
         cdef Term term = Term(self.solver)
         term.cterm = self.cdc.getTesterTerm()
         return term
 
     def getNumSelectors(self):
+        """
+            :return: the number of selecters (so far) of this Datatype constructor.
+        """
         return self.cdc.getNumSelectors()
 
     def getSelector(self, str name):
+        """
+            :param name: the name of the datatype selector.
+            :return: the first datatype selector with the given name
+        """
         cdef DatatypeSelector ds = DatatypeSelector(self.solver)
         ds.cds = self.cdc.getSelector(name.encode())
         return ds
 
     def getSelectorTerm(self, str name):
+        """
+            :param name: the name of the datatype selector.
+            :return: a term representing the firstdatatype selector with the given name.
+        """
         cdef Term term = Term(self.solver)
         term.cterm = self.cdc.getSelectorTerm(name.encode())
         return term
@@ -257,6 +284,7 @@ cdef class DatatypeConstructor:
 
 
 cdef class DatatypeConstructorDecl:
+    """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`."""
     cdef c_DatatypeConstructorDecl cddc
     cdef Solver solver
 
@@ -264,9 +292,20 @@ cdef class DatatypeConstructorDecl:
         self.solver = solver
 
     def addSelector(self, str name, Sort sort):
+        """
+            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.
+        """
         self.cddc.addSelector(name.encode(), sort.csort)
 
     def addSelectorSelf(self, str name):
+        """
+            Add datatype selector declaration whose range sort is the datatype itself.
+
+            :param name: the name of the datatype selector declaration to add.
+        """
         self.cddc.addSelectorSelf(name.encode())
 
     def isNull(self):
@@ -280,21 +319,36 @@ cdef class DatatypeConstructorDecl:
 
 
 cdef class DatatypeDecl:
+    """Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`."""
     cdef c_DatatypeDecl cdd
     cdef Solver solver
     def __cinit__(self, Solver solver):
         self.solver = solver
 
     def addConstructor(self, DatatypeConstructorDecl ctor):
+        """
+            Add a datatype constructor declaration.
+
+            :param ctor: the datatype constructor declaration to add.
+        """
         self.cdd.addConstructor(ctor.cddc)
 
     def getNumConstructors(self):
+        """
+            :return: number of constructors (so far) for this datatype declaration.
+        """
         return self.cdd.getNumConstructors()
 
     def isParametric(self):
+        """
+            :return: is this datatype declaration parametric?
+        """
         return self.cdd.isParametric()
 
     def getName(self):
+        """
+            :return: the name of this datatype declaration.
+        """
         return self.cdd.getName().decode()
 
     def isNull(self):
@@ -308,6 +362,7 @@ cdef class DatatypeDecl:
 
 
 cdef class DatatypeSelector:
+    """Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`."""
     cdef c_DatatypeSelector cds
     cdef Solver solver
     def __cinit__(self, Solver solver):
@@ -315,19 +370,31 @@ cdef class DatatypeSelector:
         self.solver = solver
 
     def getName(self):
+        """
+            :return: the name of this datatype selector.
+        """
         return self.cds.getName().decode()
 
     def getSelectorTerm(self):
+        """
+            :return: the selector opeartor of this datatype selector as a term.
+        """
         cdef Term term = Term(self.solver)
         term.cterm = self.cds.getSelectorTerm()
         return term
 
     def getUpdaterTerm(self):
+        """
+            :return: the updater opeartor of this datatype selector as a term.
+        """
         cdef Term term = Term(self.solver)
         term.cterm = self.cds.getUpdaterTerm()
         return term
 
     def getRangeSort(self):
+        """
+            :return: the range sort of this selector.
+        """
         cdef Sort sort = Sort(self.solver)
         sort.csort = self.cds.getRangeSort()
         return sort