docs/api/python/base/op.rst

Op
================

This class encapsulates a cvc5 operator. A :py:obj:`cvc5.Op` is a term that
represents an operator, instantiated with the parameters it requires (if any).

A :py:obj:`cvc5.Term` of operator kind that does not require additional
parameters, e.g., :py:obj:`cvc5.Kind.ADD`, is usually constructed via
:py:func:`cvc5.Solver.mkTerm(Kind kind, const std.vector\<Term>& children) <Term cvc5.Solver.mkTerm(Kind kind, const std.vector\<Term>& children) const>`.
Alternatively, any :py:obj:`cvc5.Term` can be constructed via first
instantiating a corresponding :py:obj:`cvc5.Op`, even if the operator does
not require additional parameters.
Terms with operators that require additional parameters, e.g.,
:py:obj:`cvc5.Kind.BITVECTOR_EXTRACT`, must be created via
:py:func:`cvc5.TermManager.mkOp()` and :py:func:`cvc5.TermManager.mkTerm()`.

----

.. autoclass:: cvc5.Op
    :members:
    :special-members: __getitem__
    :undoc-members:
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. 2021-10-16 02:09:02 +03:00			`Op`
			`================`

docs: python: Add missing docs text for pages. (#11057) 2024-08-05 11:47:34 -07:00			This class encapsulates a cvc5 operator. A :py:obj:`cvc5.Op` is a term that
			`represents an operator, instantiated with the parameters it requires (if any).`

			A :py:obj:`cvc5.Term` of operator kind that does not require additional
			parameters, e.g., :py:obj:`cvc5.Kind.ADD`, is usually constructed via
			:py:func:`cvc5.Solver.mkTerm(Kind kind, const std.vector\<Term>& children) <Term cvc5.Solver.mkTerm(Kind kind, const std.vector\<Term>& children) const>`.
			Alternatively, any :py:obj:`cvc5.Term` can be constructed via first
			instantiating a corresponding :py:obj:`cvc5.Op`, even if the operator does
			`not require additional parameters.`
			`Terms with operators that require additional parameters, e.g.,`
			:py:obj:`cvc5.Kind.BITVECTOR_EXTRACT`, must be created via
			:py:func:`cvc5.TermManager.mkOp()` and :py:func:`cvc5.TermManager.mkTerm()`.

			`----`

Change name of Python API's package from pycvc5 to cvc5. (#7953) In the process, I changed a CMake target name from pycvc5 to cvc5_base_py_api. I could not change the target to cvc5, because that name is taken. 2022-02-02 15:45:42 -08:00			`.. autoclass:: cvc5.Op`
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. 2021-10-16 02:09:02 +03:00			`:members:`
Document special member functions in python API (#8513) This PR documents relevant special member functions __getitem__ and __iter__ for some classes in the base python API. 2022-04-01 22:12:10 +02:00			`:special-members: __getitem__`
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. 2021-10-16 02:09:02 +03:00			`:undoc-members:`