InputParser

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

class InputParser

This class 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 configured via, e.g., InputParser::setFileInput(), InputParser::setStreamInput(), InputParser::setStringInput() or InputParser::setIncrementalStringInput() and InputParser::appendIncrementalStringInput(). Then, functions InputParser::nextCommand() and InputParser::nextExpression() 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 (SymbolManager::isLogicSet() and Solver::isLogicSet()), 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.

Public Functions

InputParser(Solver *solver, SymbolManager *sm)

Construct an input parser

Parameters:

  • solver – The solver (e.g. for constructing terms and sorts)

  • sm – The symbol manager, which contains a symbol table that maps symbols to terms and sorts. Must have a logic that is compatible with the solver.

InputParser(Solver *solver)

Construct an input parser with an initially empty symbol manager.

Parameters:

solver – The solver (e.g. for constructing terms and sorts)

Solver *getSolver()

Get the associated solver instance of this input parser.

Returns:

The solver instance.

SymbolManager *getSymbolManager()

Get the associated symbol manager of this input parser.

Returns:

The associated symbol manager.

void setFileInput(modes::InputLanguage lang, const std::string &filename)

Configure given file as input.

Parameters:

  • lang – The input language (e.g., modes::InputLanguage::SMT_LIB_2_6).

  • filename – The name of the file to configure.

void setStreamInput(modes::InputLanguage lang, std::istream &input, const std::string &name)

Configure given stream as input.

Parameters:

  • lang – The input language.

  • input – The input stream.

  • name – The name of the stream, for use in error messages.

void setStringInput(modes::InputLanguage lang, const std::string &input, const std::string &name)

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

Parameters:

  • 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 setIncrementalStringInput(modes::InputLanguage lang, const std::string &name)

Configure that we will be feeding strings to this parser via appendIncrementalStringInput() below.

Parameters:

  • lang – the input language

  • name – the name of the stream, for use in error messages

void appendIncrementalStringInput(const std::string &input)

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

Parameters:

input – The input string

Command nextCommand()

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.

Returns:

The parsed command. This is the null command if no command was read.

Term nextTerm()

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

Returns:

The parsed term.

bool done() const

Is this parser done reading input?

Returns:

True if parser is done reading input.

Friends

friend class internal::InteractiveShell