From 538eea94a5861a6eb300c0cb2da381d217e6e73b Mon Sep 17 00:00:00 2001 From: yoni206 Date: Sat, 16 Oct 2021 02:09:02 +0300 Subject: [PATCH] Python api documentation: Op, Grammar, Result, Enums (#7095) This PR adds documentation to the python class Op, Grammar, Result, and for API enums. Additionally, documentation for isNull functions in the datatype classes is added for the python API, and a small change in the cpp API documentation is introduced. --- docs/api/cpp/cpp.rst | 1 + docs/api/cpp/unknownexplanation.rst | 6 + docs/api/python/grammar.rst | 6 + docs/api/python/op.rst | 6 + docs/api/python/python.rst | 5 + docs/api/python/result.rst | 6 + docs/api/python/roundingmode.rst | 6 + docs/api/python/unknownexplanation.rst | 6 + src/api/cpp/cvc5.h | 2 +- src/api/python/cvc5.pxi | 146 ++++++++++++++++++++++--- 10 files changed, 173 insertions(+), 17 deletions(-) create mode 100644 docs/api/cpp/unknownexplanation.rst create mode 100644 docs/api/python/grammar.rst create mode 100644 docs/api/python/op.rst create mode 100644 docs/api/python/result.rst create mode 100644 docs/api/python/roundingmode.rst create mode 100644 docs/api/python/unknownexplanation.rst diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index c10ae7517..04f731203 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -30,5 +30,6 @@ C++ API Documentation sort statistics term + unknownexplanation diff --git a/docs/api/cpp/unknownexplanation.rst b/docs/api/cpp/unknownexplanation.rst new file mode 100644 index 000000000..9a64ec4aa --- /dev/null +++ b/docs/api/cpp/unknownexplanation.rst @@ -0,0 +1,6 @@ +UnknownExplanation +============ + +.. doxygenenum:: cvc5::api::Result::UnknownExplanation + :project: cvc5 + diff --git a/docs/api/python/grammar.rst b/docs/api/python/grammar.rst new file mode 100644 index 000000000..a2059fa93 --- /dev/null +++ b/docs/api/python/grammar.rst @@ -0,0 +1,6 @@ +Grammar +================ + +.. autoclass:: pycvc5.Grammar + :members: + :undoc-members: diff --git a/docs/api/python/op.rst b/docs/api/python/op.rst new file mode 100644 index 000000000..7769b33f0 --- /dev/null +++ b/docs/api/python/op.rst @@ -0,0 +1,6 @@ +Op +================ + +.. autoclass:: pycvc5.Op + :members: + :undoc-members: diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index d815f837a..a6aca2cf9 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -19,3 +19,8 @@ Python API Documentation datatypeconstructordecl datatypedecl datatypeselector + grammar + op + result + roundingmode + unknownexplanation diff --git a/docs/api/python/result.rst b/docs/api/python/result.rst new file mode 100644 index 000000000..9edb12b92 --- /dev/null +++ b/docs/api/python/result.rst @@ -0,0 +1,6 @@ +Result +================ + +.. autoclass:: pycvc5.Result + :members: + :undoc-members: diff --git a/docs/api/python/roundingmode.rst b/docs/api/python/roundingmode.rst new file mode 100644 index 000000000..0c226082e --- /dev/null +++ b/docs/api/python/roundingmode.rst @@ -0,0 +1,6 @@ +RoundingMode +================ + +.. autoclass:: pycvc5.RoundingMode + :members: + :undoc-members: diff --git a/docs/api/python/unknownexplanation.rst b/docs/api/python/unknownexplanation.rst new file mode 100644 index 000000000..54c37665b --- /dev/null +++ b/docs/api/python/unknownexplanation.rst @@ -0,0 +1,6 @@ +UnknownExplanation +================ + +.. autoclass:: pycvc5.UnknownExplanation + :members: + :undoc-members: diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3db581db6..5e0f0d834 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2464,7 +2464,7 @@ class CVC5_EXPORT Grammar /** * Allow \p ntSymbol to be any input variable to corresponding * synth-fun/synth-inv with the same sort as \p ntSymbol. - * @param ntSymbol the non-terminal allowed to be any input constant + * @param ntSymbol the non-terminal allowed to be any input variable */ void addAnyVariable(const Term& ntSymbol); diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index e45f0206e..2a35363ea 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -95,7 +95,10 @@ cdef c_hash[c_Term] ctermhash = c_hash[c_Term]() cdef class Datatype: - """Wrapper class for :cpp:class:`cvc5::api::Datatype`.""" + """ + A cvc5 datatype. + Wrapper class for :cpp:class:`cvc5::api::Datatype`. + """ cdef c_Datatype cd cdef Solver solver def __cinit__(self, Solver solver): @@ -114,7 +117,7 @@ cdef class Datatype: def getConstructor(self, str name): """ :param name: the name of the constructor. - :return: a constructor by name. + :return: a constructor by name. """ cdef DatatypeConstructor dc = DatatypeConstructor(self.solver) dc.cdc = self.cd.getConstructor(name.encode()) @@ -151,34 +154,35 @@ cdef class Datatype: return self.cd.getNumConstructors() def isParametric(self): - """:return: whether this datatype is parametric.""" + """:return: True if this datatype is parametric.""" return self.cd.isParametric() def isCodatatype(self): - """:return: whether this datatype corresponds to a co-datatype.""" + """:return: True if this datatype corresponds to a co-datatype.""" return self.cd.isCodatatype() def isTuple(self): - """:return: whether this datatype corresponds to a tuple.""" + """:return: True if this datatype corresponds to a tuple.""" return self.cd.isTuple() def isRecord(self): - """:return: whether this datatype corresponds to a record.""" + """:return: True if this datatype corresponds to a record.""" return self.cd.isRecord() def isFinite(self): - """:return: whether this datatype is finite.""" + """:return: True if this datatype is finite.""" return self.cd.isFinite() def isWellFounded(self): - """:return: whether this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() `).""" + """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() `).""" return self.cd.isWellFounded() def hasNestedRecursion(self): - """:return: whether this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() `).""" + """:return: True if this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() `).""" return self.cd.hasNestedRecursion() def isNull(self): + """:return: True if this Datatype is a null object.""" return self.cd.isNull() def __str__(self): @@ -195,7 +199,10 @@ cdef class Datatype: cdef class DatatypeConstructor: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`.""" + """ + A cvc5 datatype constructor. + Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`. + """ cdef c_DatatypeConstructor cdc cdef Solver solver def __cinit__(self, Solver solver): @@ -270,6 +277,7 @@ cdef class DatatypeConstructor: return term def isNull(self): + """:return: True if this DatatypeConstructor is a null object.""" return self.cdc.isNull() def __str__(self): @@ -286,7 +294,10 @@ cdef class DatatypeConstructor: cdef class DatatypeConstructorDecl: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`.""" + """ + A cvc5 datatype constructor declaration. + Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`. + """ cdef c_DatatypeConstructorDecl cddc cdef Solver solver @@ -311,6 +322,7 @@ cdef class DatatypeConstructorDecl: self.cddc.addSelectorSelf(name.encode()) def isNull(self): + """:return: True if this DatatypeConstructorDecl is a null object.""" return self.cddc.isNull() def __str__(self): @@ -321,7 +333,10 @@ cdef class DatatypeConstructorDecl: cdef class DatatypeDecl: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`.""" + """ + A cvc5 datatype declaration. + Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`. + """ cdef c_DatatypeDecl cdd cdef Solver solver def __cinit__(self, Solver solver): @@ -354,6 +369,7 @@ cdef class DatatypeDecl: return self.cdd.getName().decode() def isNull(self): + """:return: True if this DatatypeDecl is a null object.""" return self.cdd.isNull() def __str__(self): @@ -364,7 +380,10 @@ cdef class DatatypeDecl: cdef class DatatypeSelector: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`.""" + """ + A cvc5 datatype selector. + Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`. + """ cdef c_DatatypeSelector cds cdef Solver solver def __cinit__(self, Solver solver): @@ -402,6 +421,7 @@ cdef class DatatypeSelector: return sort def isNull(self): + """:return: True if this DatatypeSelector is a null object.""" return self.cds.isNull() def __str__(self): @@ -412,6 +432,13 @@ cdef class DatatypeSelector: cdef class Op: + """ + A cvc5 operator. + An operator is a term that represents certain operators, + instantiated with its required parameters, e.g., + a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`. + Wrapper class for :cpp:class:`cvc5::api::Op`. + """ cdef c_Op cop cdef Solver solver def __cinit__(self, Solver solver): @@ -434,18 +461,33 @@ cdef class Op: return cophash(self.cop) def getKind(self): + """ + :return: the kind of this operator. + """ return kind( self.cop.getKind()) def isIndexed(self): + """ + :return: True iff this operator is indexed. + """ return self.cop.isIndexed() def isNull(self): + """ + :return: True iff this operator is a null term. + """ return self.cop.isNull() def getNumIndices(self): + """ + :return: number of indices of this op. + """ return self.cop.getNumIndices() def getIndices(self): + """ + :return: the indices used to create this Op (see :cpp:func:`Op::getIndices() `). + """ indices = None try: indices = self.cop.getIndices[string]().decode() @@ -468,6 +510,10 @@ cdef class Op: return indices cdef class Grammar: + """ + A Sygus Grammar. + Wrapper class for :cpp:class:`cvc5::api::Grammar`. + """ cdef c_Grammar cgrammar cdef Solver solver def __cinit__(self, Solver solver): @@ -475,46 +521,100 @@ cdef class Grammar: self.cgrammar = c_Grammar() def addRule(self, Term ntSymbol, Term rule): + """ + Add ``rule`` to the set of rules corresponding to ``ntSymbol``. + + :param ntSymbol: the non-terminal to which the rule is added. + :param rule: the rule to add. + """ self.cgrammar.addRule(ntSymbol.cterm, rule.cterm) def addAnyConstant(self, Term ntSymbol): + """ + Allow ``ntSymbol`` to be an arbitrary constant. + + :param ntSymbol: the non-terminal allowed to be constant. + """ self.cgrammar.addAnyConstant(ntSymbol.cterm) def addAnyVariable(self, Term ntSymbol): + """ + Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``. + + :param ntSymbol: the non-terminal allowed to be any input variable. + """ self.cgrammar.addAnyVariable(ntSymbol.cterm) def addRules(self, Term ntSymbol, rules): + """ + Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``. + + :param ntSymbol: the non-terminal to which the rules are added. + :param rules: the rules to add. + """ cdef vector[c_Term] crules for r in rules: crules.push_back(( r).cterm) self.cgrammar.addRules(ntSymbol.cterm, crules) cdef class Result: + """ + Encapsulation of a three-valued solver result, with explanations. + Wrapper class for :cpp:class:`cvc5::api::Result`. + """ cdef c_Result cr def __cinit__(self): # gets populated by solver self.cr = c_Result() def isNull(self): + """ + :return: True if Result is empty, i.e., a nullary Result, + and not an actual result returned from a :cpp:func:`Solver::checkSat() ` (and friends) query. + """ return self.cr.isNull() def isSat(self): + """ + :return: True if query was a satisfiable :cpp:func:`Solver::checkSat() ` or :cpp:func:`Solver::checkSatAssuming() ` query. + """ return self.cr.isSat() def isUnsat(self): + """ + :return: True if query was an usatisfiable :cpp:func:`Solver::checkSat() ` or :cpp:func:`Solver::checkSatAssuming() ` query. + """ return self.cr.isUnsat() def isSatUnknown(self): + """ + :return: True if query was a :cpp:func:`Solver::checkSat() ` or :cpp:func:`Solver::checkSatAssuming() ` query and cvc5 was not able to determine (un)satisfiability. + """ return self.cr.isSatUnknown() def isEntailed(self): + """ + :return: True if corresponding query was an entailed :cpp:func:`Solver::checkEntailed() ` query. + """ return self.cr.isEntailed() def isNotEntailed(self): + """ + :return: True if corresponding query was a :cpp:func:`Solver::checkEntailed() ` query that is not entailed. + """ return self.cr.isNotEntailed() def isEntailmentUnknown(self): + """ + :return: True if query was a :cpp:func:`Solver::checkEntailed() ` query query and cvc5 was not able to determine if it is entailed. + """ return self.cr.isEntailmentUnknown() + + def getUnknownExplanation(self): + """ + :return: an explanation for an unknown query result. + """ + return UnknownExplanation( self.cr.getUnknownExplanation()) def __eq__(self, Result other): return self.cr == other.cr @@ -522,9 +622,6 @@ cdef class Result: def __ne__(self, Result other): return self.cr != other.cr - def getUnknownExplanation(self): - return UnknownExplanation( self.cr.getUnknownExplanation()) - def __str__(self): return self.cr.toString().decode() @@ -533,6 +630,20 @@ cdef class Result: cdef class RoundingMode: + """ + Rounding modes for floating-point numbers. + + For many floating-point operations, infinitely precise results may not be + representable with the number of available bits. Thus, the results are + rounded in a certain way to one of the representable floating-point numbers. + + These rounding modes directly follow the SMT-LIB theory for floating-point + arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`. + The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE + Standard 754. + + Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`. + """ cdef c_RoundingMode crm cdef str name def __cinit__(self, int rm): @@ -557,6 +668,9 @@ cdef class RoundingMode: cdef class UnknownExplanation: + """ + Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`. + """ cdef c_UnknownExplanation cue cdef str name def __cinit__(self, int ue): -- 2.30.2