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.