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(const Op& op, const std::vector<Term>& children) .

• class cvc5::Op

• std::ostream& cvc5::operator<< (std::ostream& out, const Op& op)

• std::hash<cvc5::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.

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.

Parameters :

t – The operator to compare to for disequality.

Returns :

True if operators differ syntactically.

Kind getKind ( ) const 

Get the kind of this operator.

Returns :

The kind of this operator.

bool isNull ( ) const 

Determine if this operator is nullary.

Returns :

True if this operator is a nullary operator.

bool isIndexed ( ) const 

Determine if this operator is indexed.

Returns :

True iff this operator is indexed.

size_t getNumIndices ( ) const 

Get the number of indices of this operator.

Returns :

The number of indices of this operator.

Term operator [] ( size_t i ) 

Get the index at position i of an indexed operator.

Parameters :

i – The position of the index to return.

Returns :

The index at position i.

std :: string toString ( ) const 

Get the string representation of this operator.

Returns :

A string representation of this operator.

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const Op & op ) 

Serialize an operator to given stream.

Parameters :

• out – The output stream.

• op – The operator to be serialized to the given output stream.

Returns :

The output stream.

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

Hash function for Ops.

Public Functions

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