From: yoni206 Date: Mon, 30 Aug 2021 19:32:24 +0000 (+0300) Subject: python docs for Datatype-related classes (#7058) X-Git-Tag: cvc5-1.0.0~1322 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be403c18c6291e1cf15cdbe46489e65d9323e1b6;p=cvc5.git python docs for Datatype-related classes (#7058) --- diff --git a/docs/api/python/datatype.rst b/docs/api/python/datatype.rst index 89f14877f..a6052b1f5 100644 --- a/docs/api/python/datatype.rst +++ b/docs/api/python/datatype.rst @@ -4,4 +4,3 @@ Datatype .. autoclass:: pycvc5.Datatype :members: :undoc-members: - :special-members: __getitem__ diff --git a/docs/api/python/datatypeconstructor.rst b/docs/api/python/datatypeconstructor.rst new file mode 100644 index 000000000..ed457562b --- /dev/null +++ b/docs/api/python/datatypeconstructor.rst @@ -0,0 +1,6 @@ +DatatypeConstructor +=================== + +.. autoclass:: pycvc5.DatatypeConstructor + :members: + :undoc-members: diff --git a/docs/api/python/datatypeconstructordecl.rst b/docs/api/python/datatypeconstructordecl.rst new file mode 100644 index 000000000..77b1ea3f3 --- /dev/null +++ b/docs/api/python/datatypeconstructordecl.rst @@ -0,0 +1,6 @@ +DatatypeConstructorDecl +======================= + +.. autoclass:: pycvc5.DatatypeConstructorDecl + :members: + :undoc-members: diff --git a/docs/api/python/datatypedecl.rst b/docs/api/python/datatypedecl.rst new file mode 100644 index 000000000..0f61471f4 --- /dev/null +++ b/docs/api/python/datatypedecl.rst @@ -0,0 +1,6 @@ +DatatypeDecl +============ + +.. autoclass:: pycvc5.DatatypeDecl + :members: + :undoc-members: diff --git a/docs/api/python/datatypeselector.rst b/docs/api/python/datatypeselector.rst new file mode 100644 index 000000000..9c2ae22fe --- /dev/null +++ b/docs/api/python/datatypeselector.rst @@ -0,0 +1,6 @@ +DatatypeSelector +================ + +.. autoclass:: pycvc5.DatatypeSelector + :members: + :undoc-members: diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index 28443a7d6..3944d60ea 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -12,5 +12,9 @@ Python API Documentation .. toctree:: :maxdepth: 1 - datatype quickstart + datatype + datatypeconstructor + datatypeconstructordecl + datatypedecl + datatypeselector diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index d86fed14a..7a33210ed 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1809,7 +1809,7 @@ class CVC5_EXPORT DatatypeSelector */ Term getUpdaterTerm() const; - /** @return the range sort of this argument. */ + /** @return the range sort of this selector. */ Sort getRangeSort() const; /** diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 68998d521..865e51cb1 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -193,6 +193,7 @@ cdef class Datatype: cdef class DatatypeConstructor: + """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`.""" cdef c_DatatypeConstructor cdc cdef Solver solver def __cinit__(self, Solver solver): @@ -210,32 +211,58 @@ cdef class DatatypeConstructor: return ds def getName(self): + """ + :return: the name of the constructor. + """ return self.cdc.getName().decode() def getConstructorTerm(self): + """ + :return: the constructor operator as a term. + """ cdef Term term = Term(self.solver) term.cterm = self.cdc.getConstructorTerm() return term def getSpecializedConstructorTerm(self, Sort retSort): + """ + Specialized method for parametric datatypes (see :cpp:func:`DatatypeConstructor::getSpecializedConstructorTerm() `). + + :param retSort: the desired return sort of the constructor + :return: the constructor operator as a term. + """ cdef Term term = Term(self.solver) term.cterm = self.cdc.getSpecializedConstructorTerm(retSort.csort) return term def getTesterTerm(self): + """ + :return: the tester operator that is related to this constructor, as a term. + """ cdef Term term = Term(self.solver) term.cterm = self.cdc.getTesterTerm() return term def getNumSelectors(self): + """ + :return: the number of selecters (so far) of this Datatype constructor. + """ return self.cdc.getNumSelectors() def getSelector(self, str name): + """ + :param name: the name of the datatype selector. + :return: the first datatype selector with the given name + """ cdef DatatypeSelector ds = DatatypeSelector(self.solver) ds.cds = self.cdc.getSelector(name.encode()) return ds def getSelectorTerm(self, str name): + """ + :param name: the name of the datatype selector. + :return: a term representing the firstdatatype selector with the given name. + """ cdef Term term = Term(self.solver) term.cterm = self.cdc.getSelectorTerm(name.encode()) return term @@ -257,6 +284,7 @@ cdef class DatatypeConstructor: cdef class DatatypeConstructorDecl: + """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`.""" cdef c_DatatypeConstructorDecl cddc cdef Solver solver @@ -264,9 +292,20 @@ cdef class DatatypeConstructorDecl: self.solver = solver def addSelector(self, str name, Sort sort): + """ + Add datatype selector declaration. + + :param name: the name of the datatype selector declaration to add. + :param sort: the range sort of the datatype selector declaration to add. + """ self.cddc.addSelector(name.encode(), sort.csort) def addSelectorSelf(self, str name): + """ + Add datatype selector declaration whose range sort is the datatype itself. + + :param name: the name of the datatype selector declaration to add. + """ self.cddc.addSelectorSelf(name.encode()) def isNull(self): @@ -280,21 +319,36 @@ cdef class DatatypeConstructorDecl: cdef class DatatypeDecl: + """Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`.""" cdef c_DatatypeDecl cdd cdef Solver solver def __cinit__(self, Solver solver): self.solver = solver def addConstructor(self, DatatypeConstructorDecl ctor): + """ + Add a datatype constructor declaration. + + :param ctor: the datatype constructor declaration to add. + """ self.cdd.addConstructor(ctor.cddc) def getNumConstructors(self): + """ + :return: number of constructors (so far) for this datatype declaration. + """ return self.cdd.getNumConstructors() def isParametric(self): + """ + :return: is this datatype declaration parametric? + """ return self.cdd.isParametric() def getName(self): + """ + :return: the name of this datatype declaration. + """ return self.cdd.getName().decode() def isNull(self): @@ -308,6 +362,7 @@ cdef class DatatypeDecl: cdef class DatatypeSelector: + """Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`.""" cdef c_DatatypeSelector cds cdef Solver solver def __cinit__(self, Solver solver): @@ -315,19 +370,31 @@ cdef class DatatypeSelector: self.solver = solver def getName(self): + """ + :return: the name of this datatype selector. + """ return self.cds.getName().decode() def getSelectorTerm(self): + """ + :return: the selector opeartor of this datatype selector as a term. + """ cdef Term term = Term(self.solver) term.cterm = self.cds.getSelectorTerm() return term def getUpdaterTerm(self): + """ + :return: the updater opeartor of this datatype selector as a term. + """ cdef Term term = Term(self.solver) term.cterm = self.cds.getUpdaterTerm() return term def getRangeSort(self): + """ + :return: the range sort of this selector. + """ cdef Sort sort = Sort(self.solver) sort.csort = self.cds.getRangeSort() return sort