Get the name for a given command, e.g., “assert”.
@param cmd The command to invoke.
@return The name of the command.
@note The returned char* pointer is only valid until the next call to this
function.
Invoke a given command on the solver and symbol manager sm and return any
resulting output as a string.
@param cmd The command to invoke.
@param cvc5 The solver to invoke the command on.
@param sm The symbol manager to invoke the command on.
@return The output of invoking the command.
@note The returned char* pointer is only valid until the next call to this
function.
Get a string representation of this command.
@param cmd The command to invoke.
@return The string representation.
@note The returned char* pointer is only valid until the next call to this
function.
Append string to the input being parsed by this parser. Should be
called after calling cvc5_parser_set_inc_str_input().
@param parser The input parser instance.
@param input The input string.
Construct a new instance of a cvc5 input parser.
@param cvc5 The associated solver instance.
@param sm The associated symbol manager instance, contains a symbol table
that maps symbols to terms and sorts. Must have a logic that is
compatible with the solver. May be NULL to start with and
initially empty symbol manager.
@return The cvc5 symbol manager instance.
Parse and return the next command. Will initialize the logic to “ALL”
or the forced logic if no logic is set prior to this point and a command
is read that requires initializing the logic.
Parse and return the next term. Requires setting the logic prior
to this point.
@param parser The input parser instance.
@param error_msg Output parameter for the error message in case of a parse
error, NULL if no error occurred.
@return The parsed term. NULL if no term was read.
Configure given file as input to a given input parser.
@param parser The input parser instance.
@param lang the input language (e.g., #CVC5_INPUT_LANGUAGE_SMT_LIB_2_6)
@param filename The name of the file to configure.
Configure that we will be feeding strings to a given input parser via
cvc5_parser_append_inc_str_input() below.
@param parser The input parser instance.
@param lang The input language of the input string.
@param name The name to use as input stream name for error messages.
Configure a given concrete input string as the input to a given input parser.
@param parser The input parser instance.
@param lang The input language of the input string.
@param input The input string.
@param name The name to use as input stream name for error messages.
Get the list of sorts that have been declared via declare-sort commands.
These are the sorts that are printed as part of a response to a
get-model command.
Get the list of terms that have been declared via declare-fun and
declare-const. These are the terms that are printed in response to a
get-model command.
Get the logic configured for a given symbol manager.
@note Asserts cvc5_sm_is_logic_set().
@param sm The symbol manager instance.
@return The configured logic.
@note The returned char* pointer is only valid until the next call to this
function.