python docs for Datatype-related classes (#7058)

diff --git a/docs/api/python/datatype.rst b/docs/api/python/datatype.rst
index 89f14877f15c3366bf4467be801cf2cb84ca1677..a6052b1f55083b99810f39893ee226c17e7bef99 100644 (file)
--- a/docs/api/python/datatype.rst
+++ b/docs/api/python/datatype.rst
@@ -4,4 +4,3 @@ Datatype
 .. autoclass:: pycvc5.Datatype
     :members:
     :undoc-members:
-    :special-members: __getitem__

diff --git a/docs/api/python/datatypeconstructor.rst b/docs/api/python/datatypeconstructor.rst
new file mode 100644 (file)
index 0000000..ed45756
--- /dev/null
+++ b/docs/api/python/datatypeconstructor.rst
@@ -0,0 +1,6 @@
+DatatypeConstructor
+===================
+
+.. autoclass:: pycvc5.DatatypeConstructor
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/datatypeconstructordecl.rst b/docs/api/python/datatypeconstructordecl.rst
new file mode 100644 (file)
index 0000000..77b1ea3
--- /dev/null
+++ b/docs/api/python/datatypeconstructordecl.rst
@@ -0,0 +1,6 @@
+DatatypeConstructorDecl
+=======================
+
+.. autoclass:: pycvc5.DatatypeConstructorDecl
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/datatypedecl.rst b/docs/api/python/datatypedecl.rst
new file mode 100644 (file)
index 0000000..0f61471
--- /dev/null
+++ b/docs/api/python/datatypedecl.rst
@@ -0,0 +1,6 @@
+DatatypeDecl
+============
+
+.. autoclass:: pycvc5.DatatypeDecl
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/datatypeselector.rst b/docs/api/python/datatypeselector.rst
new file mode 100644 (file)
index 0000000..9c2ae22
--- /dev/null
+++ b/docs/api/python/datatypeselector.rst
@@ -0,0 +1,6 @@
+DatatypeSelector
+================
+
+.. autoclass:: pycvc5.DatatypeSelector
+    :members:
+    :undoc-members:

diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst
index 28443a7d6a38280cafc4c3b17997a7ba846187bc..3944d60ea92f75adef61ce7241f047a59468a0c4 100644 (file)
--- a/docs/api/python/python.rst
+++ b/docs/api/python/python.rst
@@ -12,5 +12,9 @@ Python API Documentation
 .. toctree::
     :maxdepth: 1
 
-    datatype
     quickstart
+    datatype
+    datatypeconstructor
+    datatypeconstructordecl
+    datatypedecl
+    datatypeselector

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index d86fed14aba8ed05c372ace8833838ee243247ee..7a33210ed0b49f891bbe7ce7f8ce54e6d03a01c6 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1809,7 +1809,7 @@ class CVC5_EXPORT DatatypeSelector
    */
   Term getUpdaterTerm() const;
 
-  /** @return the range sort of this argument. */
+  /** @return the range sort of this selector. */
   Sort getRangeSort() const;
 
   /**

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 68998d521c1b5f43237a4fe7b3d7ca90a4c2547a..865e51cb1142cf5ae958aaed464c16d5d55d115e 100644 (file)
--- 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