Cvc5Op

The Cvc5Op struct represents a cvc5 operator, instantiated with the parameters it requires (if any).

A Cvc5Term of operator kind that does not require additional parameters, e.g., CVC5_KIND_ADD, is usually constructed via Cvc5Term cvc5_mk_term(Cvc5TermManager* tm, Cvc5Kind kind, size_t size, const Cvc5Term args[])(). Alternatively, any Cvc5Term can be constructed via first instantiating a corresponding Cvc5Op, 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_mk_op() (or cvc5_mk_op_from_str()) and cvc5_mk_term_from_op().

typedef struct cvc5_op_t *Cvc5Op

A cvc5 operator.

An operator is a term that represents certain operators, instantiated with its required parameters, e.g., a Term of kind CVC5_KIND_BITVECTOR_EXTRACT.

Cvc5Op cvc5_op_copy(Cvc5Op op)

Make copy of operator, increases reference counter of op.

Note

This step is optional and allows users to manage resources in a more fine-grained manner.

Parameters:

op – The op to copy.

Returns:

The same op with its reference count increased by one.

void cvc5_op_release(Cvc5Op op)

Release copy of operator, decrements reference counter of op.

Note

This step is optional and allows users to release resources in a more fine-grained manner. Further, any API function that returns a Cvc5Op returns a copy that is owned by the callee of the function and thus, can be released.

Parameters:

op – The op to release.

bool cvc5_op_is_equal(Cvc5Op a, Cvc5Op b)

Compare two operators for syntactic equality.

Parameters:

• a – The first operator.

• b – The second operator.

Returns:

True if both operators are syntactically identical.

bool cvc5_op_is_disequal(Cvc5Op a, Cvc5Op b)

Compare two operators for syntactic disequality.

Parameters:

• a – The first operator.

• b – The second operator.

Returns:

True if both operators are syntactically disequal.

Cvc5Kind cvc5_op_get_kind(Cvc5Op op)

Get the kind of a given operator.

Parameters:

op – The operator.

Returns:

The kind of the operator.

bool cvc5_op_is_indexed(Cvc5Op op)

Determine if a given operator is indexed.

Parameters:

op – The operator.

Returns:

True iff the operator is indexed.

size_t cvc5_op_get_num_indices(Cvc5Op op)

Get the number of indices of a given operator.

Parameters:

op – The operator.

Returns:

The number of indices of the operator.

Cvc5Term cvc5_op_get_index(Cvc5Op op, size_t i)

Get the index at position i of an indexed operator.

Parameters:

• op – The operator.

• i – The position of the index to return.

Returns:

The index at position i.

const char *cvc5_op_to_string(Cvc5Op op)

Get a string representation of a given operator.

Note

The returned char* pointer is only valid until the next call to this function.

Parameters:

op – The operator.

Returns:

A string representation of the operator.

size_t cvc5_op_hash(Cvc5Op op)

Compute the hash value of an operator.

Parameters:

op – The operator.

Returns:

The hash value of the operator.