Op ¶

class 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 hash < cvc5 :: Op > ¶

Hash function for Ops.

Public Functions

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