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::Solver::mkOp(Kind kind, const std::vector<uint32_t> args) and cvc5::Solver::mkTerm(const Op& op, const std::vector<Term>& children) .

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 ) const

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