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