From 642c8b738e6681fe511dfb3610d896d3b67bbd7d Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 27 Apr 2021 15:29:19 +0200 Subject: [PATCH] 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) --- cmake/UseCython.cmake | 1 - docs/conf.py.in | 4 ++++ docs/index.rst | 3 ++- docs/python/datatype.rst | 7 +++++++ docs/python/python.rst | 7 +++++++ src/api/python/CMakeLists.txt | 2 ++ src/api/python/cvc5.pxi | 12 ++++++++++++ 7 files changed, 34 insertions(+), 2 deletions(-) create mode 100644 docs/python/datatype.rst create mode 100644 docs/python/python.rst diff --git a/cmake/UseCython.cmake b/cmake/UseCython.cmake index 7ff4a276b..c79e43f01 100644 --- 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 12bfa9ed0..28e8fa04c 100644 --- 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 71fed0356..14adad0fc 100644 --- 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 index 000000000..89f14877f --- /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 index 000000000..6d094488f --- /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 02405a0cc..227872aa7 100644 --- 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 fb3a6b377..73dd7baee 100644 --- 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[( 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() `).""" 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() `).""" return self.cd.isWellFounded() def hasNestedRecursion(self): + """:return: whether this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() `).""" return self.cd.hasNestedRecursion() def __str__(self): -- 2.30.2