Cvc5InputParser

This struct is the main interface for retrieving commands and expressions from an input.

typedef struct Cvc5InputParser Cvc5InputParser

This struct is the main interface for retrieving commands and expressions from an input using a parser.

After construction, it is expected that an input is first configure via, e.g., cvc5_parser_set_file_input(), cvc5_parser_set_str_input() or cvc5_parser_set_inc_str_input() and cvc5_parser_append_inc_str_input(). Then, functions cvc5_parser_next_command() and cvc5_parser_next_term() can be invoked to parse the input.

The input parser interacts with a symbol manager, which determines which symbols are defined in the current context, based on the background logic and user-defined symbols. If no symbol manager is provided, then the input parser will construct (an initially empty) one.

If provided, the symbol manager must have a logic that is compatible with the provided solver. That is, if both the solver and symbol manager have their logics set (cvc5_sm_is_logic_set() and cvc5_is_logic_set()), then their logics must be the same.

Upon setting an input source, if either the solver (resp. symbol manager) has its logic set, then the symbol manager (resp. solver) is set to use that logic, if its logic is not already set.

Cvc5InputParser *cvc5_parser_new(Cvc5 *cvc5, Cvc5SymbolManager *sm)

Construct a new instance of a cvc5 input parser.

Parameters:

  • cvc5 – The associated solver instance.

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

Returns:

The cvc5 symbol manager instance.

void cvc5_parser_delete(Cvc5InputParser *parser)

Delete a cvc5 input parser instance.

Parameters:

parser – The input parser instance.

void cvc5_parser_release(Cvc5InputParser *parser)

Release all objects managed by the parser.

This will free all memory used by any managed objects allocated by the parser.

Note

This invalidates all managed objects created by the parser.

Parameters:

parser – The parser instance.

Cvc5 *cvc5_parser_get_solver(Cvc5InputParser *parser)

Get the associated solver instance of a given parser.

Parameters:

parser – The parser instance.

Returns:

The solver.

Cvc5SymbolManager *cvc5_parser_get_sm(Cvc5InputParser *parser)

Get the associated symbol manager of a given parser.

Parameters:

parser – The parser instance.

Returns:

The symbol manager.

void cvc5_parser_set_file_input(Cvc5InputParser *parser, Cvc5InputLanguage lang, const char *filename)

Configure given file as input to a given input parser.

Parameters:

  • parser – The input parser instance.

  • lang – the input language (e.g., #CVC5_INPUT_LANGUAGESMT_LIB_2_6)

  • filename – The name of the file to configure.

void cvc5_parser_set_str_input(Cvc5InputParser *parser, Cvc5InputLanguage lang, const char *input, const char *name)

Configure a given concrete input string as the input to a given input parser.

Parameters:

  • parser – The input parser instance.

  • lang – The input language of the input string.

  • input – The input string.

  • name – The name to use as input stream name for error messages.

void cvc5_parser_set_inc_str_input(Cvc5InputParser *parser, Cvc5InputLanguage lang, const char *name)

Configure that we will be feeding strings to a given input parser via cvc5_parser_append_inc_str_input() below.

Parameters:

  • parser – The input parser instance.

  • lang – The input language of the input string.

  • name – The name to use as input stream name for error messages.

void cvc5_parser_append_inc_str_input(Cvc5InputParser *parser, const char *input)

Append string to the input being parsed by this parser. Should be called after calling cvc5_parser_set_inc_str_input().

Parameters:

  • parser – The input parser instance.

  • input – The input string.

Cvc5Command cvc5_parser_next_command(Cvc5InputParser *parser, const char **error_msg)

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.

Parameters:

  • parser – The input parser instance.

  • error_msg – Output parameter for the error message in case of a parse error, NULL if no error occurred.

Returns:

The parsed command. NULL if no command was read.

Cvc5Term cvc5_parser_next_term(Cvc5InputParser *parser, const char **error_msg)

Parse and return the next term. Requires setting the logic prior to this point.

Parameters:

  • parser – The input parser instance.

  • error_msg – Output parameter for the error message in case of a parse error, NULL if no error occurred.

Returns:

The parsed term. NULL if no term was read.

bool cvc5_parser_done(Cvc5InputParser *parser)

Is this parser done reading input?

Parameters:

parser – The input parser instance.

Returns:

True if parser is done reading input.