Initial setup for docs of python API (#6445)

This PR adds the basic setup for including the python API in our sphinx documentation and shows how it works using the Datatype class as an example. In detail
- it enables sphinx.ext.autodoc and makes sure the generated pycvc5 is in the search path
- adds a index page for the python API
- adds a page for the Datatype class
- adds docstrings for the Datatype class
- does some finetuning (remove source locations, but adds signature information)

diff --git a/cmake/UseCython.cmake b/cmake/UseCython.cmake
index 7ff4a276bd802a4be691e04ecab44f4d6e132256..c79e43f0164cd13acb1cfc9b4d775d443857761d 100644 (file)
--- a/cmake/UseCython.cmake
+++ b/cmake/UseCython.cmake
@@ -350,7 +350,6 @@ function(add_cython_target _name)
   if(CMAKE_BUILD_TYPE STREQUAL "Debug" OR
      CMAKE_BUILD_TYPE STREQUAL "RelWithDebInfo")
     set(cython_debug_arg "--gdb")
-    set(embed_pos_arg "--embed-positions")
     set(line_directives_arg "--line-directives")
   endif()
 

diff --git a/docs/conf.py.in b/docs/conf.py.in
index 12bfa9ed0d920fb4d6c2dd8e780ee1babe0454e1..28e8fa04cc0e276afbe54c2cb6b5c5e908e46f8e 100644 (file)
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -15,6 +15,9 @@ import sys
 # add path to enable extensions
 sys.path.insert(0, '${CMAKE_CURRENT_SOURCE_DIR}/ext/')
 
+# path to python api
+sys.path.insert(0, '${CMAKE_BINARY_DIR}/src/api/python')
+
 
 # -- Project information -----------------------------------------------------
 
@@ -30,6 +33,7 @@ author = 'The Authors of cvc5'
 # ones.
 extensions = [
         'breathe',
+        'sphinx.ext.autodoc',
         'sphinx.ext.autosectionlabel',
         'sphinxcontrib.bibtex',
         'sphinx_tabs.tabs',

diff --git a/docs/index.rst b/docs/index.rst
index 71fed0356ce3073230ca47d6423c2fe5c1f5d30e..14adad0fc6f088c3eb4a86f0ce66bef7d267292b 100644 (file)
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -13,8 +13,9 @@ cvc5 API Documentation
 ---------------
 
 .. toctree::
-   :maxdepth: 2
+   :maxdepth: 1
 
    cpp/cpp
+   python/python
    references
    examples/examples

diff --git a/docs/python/datatype.rst b/docs/python/datatype.rst
new file mode 100644 (file)
index 0000000..89f1487
--- /dev/null
+++ b/docs/python/datatype.rst
@@ -0,0 +1,7 @@
+Datatype
+========
+
+.. autoclass:: pycvc5.Datatype
+    :members:
+    :undoc-members:
+    :special-members: __getitem__

diff --git a/docs/python/python.rst b/docs/python/python.rst
new file mode 100644 (file)
index 0000000..6d09448
--- /dev/null
+++ b/docs/python/python.rst
@@ -0,0 +1,7 @@
+Python API Documentation
+========================
+
+.. toctree::
+    :maxdepth: 2
+
+    datatype

diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt
index 02405a0ccd5faf6b7a8c236c6b76706f8c1b7654..227872aa7424268b22b2c9bc772e14a932ec1155 100644 (file)
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -22,6 +22,8 @@ endif()
 find_package(PythonExtensions REQUIRED)
 find_package(Cython 0.29 REQUIRED)
 
+set(CYTHON_FLAGS "-X embedsignature=True")
+
 # Generate cvc5kinds.{pxd,pyx}
 configure_file(genkinds.py.in genkinds.py)
 set(GENERATED_FILES

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index fb3a6b37772d6e96c2540cd8cd1c265bd9f397f8..73dd7baee1c03bb0d15485484155460853814a82 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -80,12 +80,14 @@ cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
 
 
 cdef class Datatype:
+    """Wrapper class for :cpp:class:`cvc5::api::Datatype`."""
     cdef c_Datatype cd
     cdef Solver solver
     def __cinit__(self, Solver solver):
         self.solver = solver
 
     def __getitem__(self, index):
+        """Return a constructor by index or by name."""
         cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
         if isinstance(index, int) and index >= 0:
             dc.cdc = self.cd[(<int?> index)]
@@ -96,37 +98,47 @@ cdef class Datatype:
         return dc
 
     def getConstructor(self, str name):
+        """Return a constructor by name."""
         cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
         dc.cdc = self.cd.getConstructor(name.encode())
         return dc
 
     def getConstructorTerm(self, str name):
+        """:return: the term representing the datatype constructor with the given name (see :cpp:func:`Datatype::getConstructorTerm() <cvc5::api::Datatype::getConstructorTerm>`)."""
         cdef Term term = Term(self.solver)
         term.cterm = self.cd.getConstructorTerm(name.encode())
         return term
 
     def getNumConstructors(self):
+        """:return: number of constructors."""
         return self.cd.getNumConstructors()
 
     def isParametric(self):
+        """:return: whether this datatype is parametric."""
         return self.cd.isParametric()
 
     def isCodatatype(self):
+        """:return: whether this datatype corresponds to a co-datatype."""
         return self.cd.isCodatatype()
 
     def isTuple(self):
+        """:return: whether this datatype corresponds to a tuple."""
         return self.cd.isTuple()
 
     def isRecord(self):
+        """:return: whether this datatype corresponds to a record."""
         return self.cd.isRecord()
 
     def isFinite(self):
+        """:return: whether this datatype is finite."""
         return self.cd.isFinite()
 
     def isWellFounded(self):
+        """:return: whether this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
         return self.cd.isWellFounded()
 
     def hasNestedRecursion(self):
+        """:return: whether this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`)."""
         return self.cd.hasNestedRecursion()
 
     def __str__(self):