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.