Cvc5Command 

Encapsulation of a command. Commands are constructed by the input parser and can be invoked on the solver and symbol manager .

typedef struct cvc5_cmd_t * Cvc5Command 

Encapsulation of a command.

Commands are constructed by the input parser and can be invoked on the solver and symbol manager.

const char * cvc5_cmd_invoke ( Cvc5Command cmd , Cvc5 * cvc5 , Cvc5SymbolManager * sm ) 

Invoke a given command on the solver and symbol manager sm and return any resulting output as a string.

Note

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

Parameters :

• cmd – The command to invoke.

• cvc5 – The solver to invoke the command on.

• sm – The symbol manager to invoke the command on.

Returns :

The output of invoking the command.

const char * cvc5_cmd_to_string ( const Cvc5Command cmd ) 

Get a string representation of this command.

Note

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

Parameters :

cmd – The command to invoke.

Returns :

The string representation.

const char * cvc5_cmd_get_name ( const Cvc5Command cmd ) 

Get the name for a given command, e.g., “assert”.

Note

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

Parameters :

cmd – The command to invoke.

Returns :

The name of the command.

Cvc5Command cvc5_cmd_copy ( Cvc5Command cmd ) 

Make copy of command, increases reference counter of cmd .

Note

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

Parameters :

cmd – The command to copy.

Returns :

The same command with its reference count increased by one.

void cvc5_cmd_release ( Cvc5Command cmd ) 

Release copy of command, decrements reference counter of cmd .

Note

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

Parameters :

cmd – The command to release.