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.