1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
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:
|
