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.