diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2021-08-30 22:32:24 +0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-30 12:32:24 -0700 |
commit | be403c18c6291e1cf15cdbe46489e65d9323e1b6 (patch) | |
tree | f8cd1335c2bde78ff0a202dd6ced34a36f7777ad /src/api | |
parent | 9b89eb1c0a7c2e9b5be9b9a80e9e24473454ce52 (diff) |
python docs for Datatype-related classes (#7058)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cpp/cvc5.h | 2 | ||||
-rw-r--r-- | src/api/python/cvc5.pxi | 67 |
2 files changed, 68 insertions, 1 deletions
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() <cvc5::api::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 |