From 3c18371323bafb8f06c36de39aad100772ec6729 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Fri, 1 Apr 2022 22:12:10 +0200
Subject: [PATCH] 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.
---
 docs/api/python/base/datatype.rst            |  1 +
 docs/api/python/base/datatypeconstructor.rst |  1 +
 docs/api/python/base/op.rst                  |  1 +
 docs/api/python/base/term.rst                |  1 +
 src/api/python/cvc5.pxi                      | 31 +++++++++++++++++++-
 5 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/docs/api/python/base/datatype.rst b/docs/api/python/base/datatype.rst
index 7ab75ea61..0adc54f0d 100644
--- 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 c09a500f3..821e49ea4 100644
--- 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 548291d80..1381fc223 100644
--- 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 f692b931f..8137721af 100644
--- 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 1197e0b00..62b45de73 100644
--- 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
-- 
2.30.2