Document special member functions in python API (#8513)

This PR documents relevant special member functions __getitem__ and __iter__ for some classes in the base python API.

diff --git a/docs/api/python/base/datatype.rst b/docs/api/python/base/datatype.rst
index 7ab75ea61daf0e82ffb4891b16ac24a5bc064928..0adc54f0d362b9dd42e4fd91012e38b46c288877 100644 (file)
--- a/docs/api/python/base/datatype.rst
+++ b/docs/api/python/base/datatype.rst
@@ -3,4 +3,5 @@ Datatype
 
 .. autoclass:: cvc5.Datatype
     :members:
+    :special-members: __getitem__, __iter__
     :undoc-members:

diff --git a/docs/api/python/base/datatypeconstructor.rst b/docs/api/python/base/datatypeconstructor.rst
index c09a500f39634ab9ead463353395d88304390efa..821e49ea46122f234abb01d4be9a653553b38e96 100644 (file)
--- a/docs/api/python/base/datatypeconstructor.rst
+++ b/docs/api/python/base/datatypeconstructor.rst
@@ -3,4 +3,5 @@ DatatypeConstructor
 
 .. autoclass:: cvc5.DatatypeConstructor
     :members:
+    :special-members: __getitem__, __iter__
     :undoc-members:

diff --git a/docs/api/python/base/op.rst b/docs/api/python/base/op.rst
index 548291d802c5d2eed8f05ba5ed59ce7310500c6d..1381fc2238a090115810b9b7e329ad85b8ca9ca0 100644 (file)
--- a/docs/api/python/base/op.rst
+++ b/docs/api/python/base/op.rst
@@ -3,4 +3,5 @@ Op
 
 .. autoclass:: cvc5.Op
     :members:
+    :special-members: __getitem__
     :undoc-members:

diff --git a/docs/api/python/base/term.rst b/docs/api/python/base/term.rst
index f692b931fec33f9b1d8a3f359610ac2f7bb3dc6c..8137721af911cf55a2c67bd30f0b5a4d2d4fe7de 100644 (file)
--- a/docs/api/python/base/term.rst
+++ b/docs/api/python/base/term.rst
@@ -3,4 +3,5 @@ Term
 
 .. autoclass:: cvc5.Term
     :members:
+    :special-members: __getitem__, __iter__
     :undoc-members:

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 1197e0b00397e44db7580d6764703cd5899c591c..62b45de7397360e179f8154f232f0741202599df 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -92,6 +92,16 @@ cdef class Datatype:
         self.solver = solver
 
     def __getitem__(self, index):
+        """
+            Get the datatype constructor with the given index, where index can
+            be either a numeric id starting with zero, or the name of the
+            constructor. In the latter case, this is a linear search through the
+            constructors, so in case of multiple, similarly-named constructors,
+            the first is returned.
+
+            :param index: The id or name of the datatype constructor.
+            :return: The matching datatype constructor.
+        """
         cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
         if isinstance(index, int) and index >= 0:
             dc.cdc = self.cd[(<int?> index)]
@@ -211,6 +221,7 @@ cdef class Datatype:
         return self.cd.toString().decode()
 
     def __iter__(self):
+        """Iterate over all constructors."""
         for ci in self.cd:
             dc = DatatypeConstructor(self.solver)
             dc.cdc = ci
@@ -230,6 +241,16 @@ cdef class DatatypeConstructor:
         self.solver = solver
 
     def __getitem__(self, index):
+        """
+            Get the datatype selector with the given index, where index can be
+            either a numeric id starting with zero, or the name of the selector.
+            In the latter case, this is a linear search through the selectors,
+            so in case of multiple, similarly-named selectors, the first is
+            returned.
+
+            :param index: The id or name of the datatype selector.
+            :return: The matching datatype selector.
+        """
         cdef DatatypeSelector ds = DatatypeSelector(self.solver)
         if isinstance(index, int) and index >= 0:
             ds.cds = self.cdc[(<int?> index)]
@@ -345,6 +366,7 @@ cdef class DatatypeConstructor:
         return self.cdc.toString().decode()
 
     def __iter__(self):
+        """Iterate over all datatype selectors."""
         for ci in self.cdc:
             ds = DatatypeSelector(self.solver)
             ds.cds = ci
@@ -556,7 +578,7 @@ cdef class Op:
         """
         return self.cop.getNumIndices()
 
-    def __getitem__(self, i):
+    def __getitem__(self, int i):
         """
             Get the index at position ``i``.
 
@@ -3506,6 +3528,12 @@ cdef class Term:
         return self.cterm >= other.cterm
 
     def __getitem__(self, int index):
+        """
+            Get the child term at a given index.
+
+            :param index: The index of the child term to return.
+            :return: The child term with the given index.
+        """
         cdef Term term = Term(self.solver)
         if index >= 0:
             term.cterm = self.cterm[index]
@@ -3520,6 +3548,7 @@ cdef class Term:
         return self.cterm.toString().decode()
 
     def __iter__(self):
+        """Iterate over all child terms."""
         for ci in self.cterm:
             term = Term(self.solver)
             term.cterm = ci