diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-04-27 15:29:19 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-27 15:29:19 +0200 |
commit | 642c8b738e6681fe511dfb3610d896d3b67bbd7d (patch) | |
tree | 26660ce4359f6104bd392cfac1ca46ae75d02ef9 /src | |
parent | 20820daece2eaf340a944ff386ffbafed1b79b75 (diff) |
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)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/python/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/api/python/cvc5.pxi | 12 |
2 files changed, 14 insertions, 0 deletions
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[(<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): |