Op
This class encapsulates a cvc5 operator. A
cvc5.Op
is a term that
represents an operator, instantiated with the parameters it requires (if any).
A
cvc5.Term
of operator kind that does not require additional
parameters, e.g.,
cvc5.Kind.ADD
, is usually constructed via
cvc5.Solver.mkTerm(Kind
kind,
const
std.vector<Term>&
children)
.
Alternatively, any
cvc5.Term
can be constructed via first
instantiating a corresponding
cvc5.Op
, even if the operator does
not require additional parameters.
Terms with operators that require additional parameters, e.g.,
cvc5.Kind.BITVECTOR_EXTRACT
, must be created via
cvc5.TermManager.mkOp()
and
cvc5.TermManager.mkTerm()
.
- class cvc5. Op
-
A cvc5 operator.
An operator is a term that represents certain operators, instantiated with its required parameters, e.g., a term of kind
BITVECTOR_EXTRACT
.Wrapper class for
cvc5::Op
.- __getitem__ ( )
-
Get the index at position
i
.- Parameters :
-
i – The position of the index to return.
- Returns :
-
The index at position
i
.
- getKind ( )
-
- Returns :
-
The kind of this operator.
- getNumIndices ( )
-
- Returns :
-
The number of indices of this op.
- isIndexed ( )
-
- Returns :
-
True iff this operator is indexed.
- isNull ( )
-
- Returns :
-
True iff this operator is a null term.