From be403c18c6291e1cf15cdbe46489e65d9323e1b6 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 30 Aug 2021 22:32:24 +0300 Subject: python docs for Datatype-related classes (#7058) --- src/api/python/cvc5.pxi | 67 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) (limited to 'src/api/python') 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 -- cgit v1.2.3