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.

• solver – 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.

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.

Returns :

The name of the command.