io.github.cvc5

Class InputParser

java.lang.Object

io.github.cvc5.InputParser

public class InputParser
extends java.lang.Object

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 set via setFileInput(InputLanguage, String), setStringInput(InputLanguage, String, String), or setIncrementalStringInput(InputLanguage, String) and appendIncrementalStringInput(String). Then, the methods nextCommand() and nextTerm() 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.

Field Summary

Fields

Modifier and Type	Field and Description
protected long	pointer

Constructor Summary

Constructors

Constructor and Description
InputParser(Solver solver) Construct an input parser with an initially empty symbol manager.
InputParser(Solver solver, SymbolManager sm) Construct an input parser

Method Summary

Modifier and Type	Method and Description
void	appendIncrementalStringInput(java.lang.String input) Append string to the input being parsed by this parser.
void	deletePointer()
protected void	deletePointer(long pointer)
boolean	done()
long	getPointer()
Solver	getSolver()
SymbolManager	getSymbolManager()
Command	nextCommand() Parse and return the next command.
Term	nextTerm() Parse and return the next term.
void	setFileInput(InputLanguage lang, java.lang.String fileName) Set the input for the given file.
void	setIncrementalStringInput(InputLanguage lang, java.lang.String name) Set that we will be feeding strings to this parser via appendIncrementalStringInput below.
void	setStringInput(InputLanguage lang, java.lang.String input, java.lang.String name) Set the input to the given concrete input string.
java.lang.String	toString()
protected java.lang.String	toString(long pointer)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

pointer

protected long pointer

Constructor Detail

InputParser

public 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

public InputParser(Solver solver)

Construct an input parser with an initially empty symbol manager.

Parameters:

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

Method Detail

deletePointer

protected void deletePointer(long pointer)

toString

protected java.lang.String toString(long pointer)

getSolver

public Solver getSolver()

Returns:

The underlying solver of this input parser

getSymbolManager

public SymbolManager getSymbolManager()

Returns:

The underlying symbol manager of this input parser.

setFileInput

public void setFileInput(InputLanguage lang,
                         java.lang.String fileName)

Set the input for the given file.

Parameters:

lang - the input language (e.g. InputLanguage.SMT_LIB_2_6).

fileName - the input file name.

setStringInput

public void setStringInput(InputLanguage lang,
                           java.lang.String input,
                           java.lang.String name)

Set the input to the given concrete input string.

Parameters:

lang - The input language.

input - The input string.

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

setIncrementalStringInput

public void setIncrementalStringInput(InputLanguage lang,
                                      java.lang.String name)

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

appendIncrementalStringInput

public void appendIncrementalStringInput(java.lang.String input)

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

Parameters:

input - The input string.

nextCommand

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

nextTerm

public Term nextTerm()

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

Returns:

The parsed term.

done

public boolean done()

Returns:

True if this parser done reading input.

getPointer

public long getPointer()

deletePointer

public void deletePointer()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object