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.