From: yoni206 Date: Tue, 23 Nov 2021 17:34:14 +0000 (+0200) Subject: Python API documentation: terms (#7659) X-Git-Tag: cvc5-1.0.0~784 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=feae0b304028c3cb95ae239b9aa072398dfa890e;p=cvc5.git Python API documentation: terms (#7659) This PR adds documentation for the Terms class in the python API. Co-authored-by: Gereon Kremer gereon.kremer@cs.rwth-aachen.de --- diff --git a/docs/api/python/regular/python.rst b/docs/api/python/regular/python.rst index 0cf78d0ce..2e50f2d68 100644 --- a/docs/api/python/regular/python.rst +++ b/docs/api/python/regular/python.rst @@ -22,4 +22,5 @@ Python API Documentation roundingmode solver sort + term unknownexplanation diff --git a/docs/api/python/regular/term.rst b/docs/api/python/regular/term.rst new file mode 100644 index 000000000..00992209d --- /dev/null +++ b/docs/api/python/regular/term.rst @@ -0,0 +1,6 @@ +Term +================ + +.. autoclass:: pycvc5.Term + :members: + :undoc-members: diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 3d24b5dbd..aa207cd40 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1107,8 +1107,8 @@ cdef class Solver: def mkReal(self, val, den=None): """Create a real constant. - :param: `val` the value of the term. Can be an integer, float, or string. It will be formatted as a string before the term is built. - :param: `den` if not None, the value is `val`/`den` + :param val: the value of the term. Can be an integer, float, or string. It will be formatted as a string before the term is built. + :param den: if not None, the value is `val`/`den` :return: a real term with literal value Can be used in various forms: @@ -1245,9 +1245,9 @@ cdef class Solver: - ``Term mkBitVector(int size, string val, int base)`` :return: a bit-vector literal term - :param: `size` an integer size. - :param: `val` an integer representating the value, in the first form. In the second form, a string representing the value. - :param: `base` the base of the string representation (second form only) + :param size: an integer size. + :param val: an integer representating the value, in the first form. In the second form, a string representing the value. + :param base: the base of the string representation (second form only) """ cdef Term term = Term(self) if len(args) == 0: @@ -1453,7 +1453,7 @@ cdef class Solver: def mkDatatypeConstructorDecl(self, str name): """ :return: a datatype constructor declaration - :param: `name` the constructor's name + :param name: the constructor's name """ cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self) ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode()) @@ -2740,6 +2740,10 @@ cdef class Sort: cdef class Term: + """ + A cvc5 Term. + Wrapper class for :cpp:class:`cvc5::api::Term`. + """ cdef c_Term cterm cdef Solver solver def __cinit__(self, Solver solver): @@ -2788,20 +2792,27 @@ cdef class Term: return ctermhash(self.cterm) def getNumChildren(self): + """:return: the number of children of this term.""" return self.cterm.getNumChildren() def getId(self): + """:return: the id of this term.""" return self.cterm.getId() def getKind(self): + """:return: the :py:class:`pycvc5.Kind` of this term.""" return kind( self.cterm.getKind()) def getSort(self): + """:return: the :py:class:`pycvc5.Sort` of this term.""" cdef Sort sort = Sort(self.solver) sort.csort = self.cterm.getSort() return sort def substitute(self, term_or_list_1, term_or_list_2): + """ + :return: the result of simultaneously replacing the term(s) stored in ``term_or_list_1`` by the term(s) stored in ``term_or_list_2`` in this term. + """ # The resulting term after substitution cdef Term term = Term(self.solver) # lists for substitutions @@ -2832,115 +2843,237 @@ cdef class Term: return term def hasOp(self): + """:return: True iff this term has an operator.""" return self.cterm.hasOp() def getOp(self): + """ + Note: This is safe to call when :py:meth:`hasOp()` returns True. + + :return: the :py:class:`pycvc5.Op` used to create this Term. + """ cdef Op op = Op(self.solver) op.cop = self.cterm.getOp() return op def hasSymbol(self): + """:return: True iff this term has a symbol.""" return self.cterm.hasSymbol() def getSymbol(self): + """ + Asserts :py:meth:`hasSymbol()`. + + :return: the raw symbol of the term. + """ return self.cterm.getSymbol().decode() def isNull(self): + """:return: True iff this term is a null term.""" return self.cterm.isNull() def notTerm(self): + """ + Boolean negation. + + :return: the Boolean negation of this term. + """ cdef Term term = Term(self.solver) term.cterm = self.cterm.notTerm() return term def andTerm(self, Term t): + """ + Boolean and. + + :param t: a Boolean term + :return: the conjunction of this term and the given term + """ cdef Term term = Term(self.solver) term.cterm = self.cterm.andTerm(( t).cterm) return term def orTerm(self, Term t): + """ + Boolean or. + + :param t: a Boolean term + :return: the disjunction of this term and the given term + """ cdef Term term = Term(self.solver) term.cterm = self.cterm.orTerm(t.cterm) return term def xorTerm(self, Term t): + """ + Boolean exclusive or. + + :param t: a Boolean term + :return: the exclusive disjunction of this term and the given term + """ cdef Term term = Term(self.solver) term.cterm = self.cterm.xorTerm(t.cterm) return term def eqTerm(self, Term t): + """ + Equality + + :param t: a Boolean term + :return: the Boolean equivalence of this term and the given term + """ cdef Term term = Term(self.solver) term.cterm = self.cterm.eqTerm(t.cterm) return term def impTerm(self, Term t): + """ + Boolean Implication. + + :param t: a Boolean term + :return: the implication of this term and the given term + """ cdef Term term = Term(self.solver) term.cterm = self.cterm.impTerm(t.cterm) return term def iteTerm(self, Term then_t, Term else_t): + """ + If-then-else with this term as the Boolean condition. + + :param then_t: the `then` term + :param else_t: the `else` term + :return: the if-then-else term with this term as the Boolean condition + """ cdef Term term = Term(self.solver) term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm) return term def isConstArray(self): + """:return: True iff this term is a constant array.""" return self.cterm.isConstArray() def getConstArrayBase(self): + """ + Asserts :py:meth:`isConstArray()`. + + :return: the base (element stored at all indicies) of this constant array + """ cdef Term term = Term(self.solver) term.cterm = self.cterm.getConstArrayBase() return term def isBooleanValue(self): + """:return: True iff this term is a Boolean value.""" return self.cterm.isBooleanValue() def getBooleanValue(self): + """ + Asserts :py:meth:`isBooleanValue()` + + :return: the representation of a Boolean value as a native Boolean value. + """ return self.cterm.getBooleanValue() def isStringValue(self): + """:return: True iff this term is a string value.""" return self.cterm.isStringValue() def getStringValue(self): + """ + Note: This method is not to be confused with :py:meth:`__str__()` which + returns the term in some string representation, whatever data it + may hold. + Asserts :py:meth:`isStringValue()`. + + :return: the string term as a native string value. + """ cdef Py_ssize_t size cdef c_wstring s = self.cterm.getStringValue() return PyUnicode_FromWideChar(s.data(), s.size()) def isIntegerValue(self): + """:return: True iff this term is an integer value.""" return self.cterm.isIntegerValue() + + def getIntegerValue(self): + """ + Asserts :py:meth:`isIntegerValue()`. + + :return: the integer term as a native python integer. + """ + return int(self.cterm.getIntegerValue().decode()) + def isAbstractValue(self): + """:return: True iff this term is an abstract value.""" return self.cterm.isAbstractValue() def getAbstractValue(self): + """ + Asserts :py:meth:`isAbstractValue()`. + + :return: the representation of an abstract value as a string. + """ return self.cterm.getAbstractValue().decode() def isFloatingPointPosZero(self): + """:return: True iff the term is the floating-point value for positive zero.""" return self.cterm.isFloatingPointPosZero() def isFloatingPointNegZero(self): + """:return: True iff the term is the floating-point value for negative zero.""" return self.cterm.isFloatingPointNegZero() def isFloatingPointPosInf(self): + """:return: True iff the term is the floating-point value for positive infinity.""" return self.cterm.isFloatingPointPosInf() def isFloatingPointNegInf(self): + """:return: True iff the term is the floating-point value for negative infinity.""" return self.cterm.isFloatingPointNegInf() def isFloatingPointNaN(self): + """:return: True iff the term is the floating-point value for not a number.""" return self.cterm.isFloatingPointNaN() def isFloatingPointValue(self): + """:return: True iff this term is a floating-point value.""" return self.cterm.isFloatingPointValue() def getFloatingPointValue(self): + """ + Asserts :py:meth:`isFloatingPointValue()`. + + :return: the representation of a floating-point value as a tuple of the exponent width, the significand width and a bit-vector value. + """ cdef c_tuple[uint32_t, uint32_t, c_Term] t = self.cterm.getFloatingPointValue() cdef Term term = Term(self.solver) term.cterm = get2(t) return (get0(t), get1(t), term) def isSetValue(self): + """ + A term is a set value if it is considered to be a (canonical) constant set + value. A canonical set value is one whose AST is: + + (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) + + where ``c1 ... cn`` are values ordered by id such that ``c1 > ... > cn`` (see + also :cpp:func:`cvc5::api::Term::operator>()`). + + Note that a universe set term ``(kind SET_UNIVERSE)`` is not considered to be + a set value. + + :return: True if the term is a set value. + """ return self.cterm.isSetValue() def getSetValue(self): + """ + Asserts :py:meth:`isSetValue()`. + + :return: the representation of a set value as a set of terms. + """ elems = set() for e in self.cterm.getSetValue(): term = Term(self.solver) @@ -2949,9 +3082,19 @@ cdef class Term: return elems def isSequenceValue(self): + """:return: True iff this term is a sequence value.""" return self.cterm.isSequenceValue() def getSequenceValue(self): + """ + Asserts :py:meth:`isSequenceValue()`. + + Note that it is usually necessary for sequences to call + :py:meth:`Solver.simplify()` to turn a sequence that is constructed by, e.g., + concatenation of unit sequences, into a sequence value. + + :return: the representation of a sequence value as a vector of terms. + """ elems = [] for e in self.cterm.getSequenceValue(): term = Term(self.solver) @@ -2960,9 +3103,15 @@ cdef class Term: return elems def isUninterpretedValue(self): + """:return: True iff this term is a value from an uninterpreted sort.""" return self.cterm.isUninterpretedValue() def getUninterpretedValue(self): + """ + Asserts :py:meth:`isUninterpretedValue()`. + + :return: the representation of an uninterpreted value as a pair of its sort and its index. + """ cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue() cdef Sort sort = Sort(self.solver) sort.csort = p.first @@ -2970,9 +3119,15 @@ cdef class Term: return (sort, i) def isTupleValue(self): + """:return: True iff this term is a tuple value.""" return self.cterm.isTupleValue() def getTupleValue(self): + """ + Asserts :py:meth:`isTupleValue()`. + + :return: the representation of a tuple value as a vector of terms. + """ elems = [] for e in self.cterm.getTupleValue(): term = Term(self.solver) @@ -2980,21 +3135,33 @@ cdef class Term: elems.append(term) return elems - def getIntegerValue(self): - return int(self.cterm.getIntegerValue().decode()) - def isRealValue(self): + """ + Note that a term of kind PI is not considered to be a real value. + + :return: True iff this term is a rational value. + """ return self.cterm.isRealValue() def getRealValue(self): - """Returns the value of a real term as a Fraction""" + """ + Asserts :py:meth:`isRealValue()`. + + :return: the representation of a rational value as a python Fraction. + """ return Fraction(self.cterm.getRealValue().decode()) def isBitVectorValue(self): + """:return: True iff this term is a bit-vector value.""" return self.cterm.isBitVectorValue() def getBitVectorValue(self, base = 2): - """Returns the value of a bit-vector term as a 0/1 string""" + """ + Asserts :py:meth:`isBitVectorValue()`. + Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexdecimal string). + + :return: the representation of a bit-vector value in string representation. + """ return self.cterm.getBitVectorValue(base).decode() def toPythonObj(self): @@ -3002,13 +3169,14 @@ cdef class Term: Converts a constant value Term to a Python object. Currently supports: - Boolean -- returns a Python bool - Int -- returns a Python int - Real -- returns a Python Fraction - BV -- returns a Python int (treats BV as unsigned) - String -- returns a Python Unicode string - Array -- returns a Python dict mapping indices to values - -- the constant base is returned as the default value + + - Boolean -- returns a Python bool + - Int -- returns a Python int + - Real -- returns a Python Fraction + - BV -- returns a Python int (treats BV as unsigned) + - String -- returns a Python Unicode string + - Array -- returns a Python dict mapping indices to values. the constant base is returned as the default value + """ if self.isBooleanValue():