Op 

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 .

Public Functions

Op ( ) 

Constructor.

~Op ( ) 

Destructor.

bool operator == ( const Op & t ) const 

Syntactic equality operator.

Note

Both operators must belong to the same solver object.

Parameters

t – The operator to compare to for equality.

Returns

True if both operators are syntactically identical.

bool operator != ( const Op & t ) const 

Syntactic disequality operator.

Note

Both terms must belong to the same solver object.

Parameters

t – The operator to compare to for disequality.

Returns

True if operators differ syntactically.

Kind getKind ( ) const 

Returns

The kind of this operator.

bool isNull ( ) const 

Returns

True if this operator is a null term.

bool isIndexed ( ) const 

Returns

True iff this operator is indexed.

size_t getNumIndices ( ) const 

Returns

The number of indices of this op.

Term operator [] ( size_t i ) const 

Get the index at position i .

Parameters

i – The position of the index to return.

Returns

The index at position i.

std :: string toString ( ) const 

Returns

A string representation of this operator.

template < >
struct std :: hash < cvc5 :: Op > 

Hash function for Ops.

Public Functions

size_t operator () ( const cvc5 :: Op & t ) const 