diff options
| -rw-r--r-- | cmake/UseCython.cmake | 1 | ||||
| -rw-r--r-- | docs/conf.py.in | 4 | ||||
| -rw-r--r-- | docs/index.rst | 3 | ||||
| -rw-r--r-- | docs/python/datatype.rst | 7 | ||||
| -rw-r--r-- | docs/python/python.rst | 7 | ||||
| -rw-r--r-- | src/api/python/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/api/python/cvc5.pxi | 12 |
7 files changed, 34 insertions, 2 deletions
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[(<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): |