Package org.smtlib

Interface IParser

All Known Implementing Classes:

Parser

public interface IParser

This is the interface to a parser for SMT-LIB. The interface is independent of the concrete syntax being used; a specific implementation of this interface will implement a specific concrete syntax for the SMT-LIB abstract syntax.

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static class	IParser.AbortInputException	An exception to be thrown if parsing is to be intentionally aborted (and restarted, ignoring any tokens since the last successful call to the parser.
static interface	IParser.ElementParser<T>	Functional interface for a lambda that parses one element from a Parser.
static interface	IParser.IFactory	The interface for the parser/printer factory
static class	IParser.ParserException	An exception thrown if parsing is to be aborted.
static class	IParser.SyntaxException	An exception to be thrown if there is an unrecoverable problem scanning the syntax

Method Summary

Modifier and Type	Method	Description
void	abortLine()	Skips remainder of current line
default void	checkUserId(IExpr.ISymbol id)	Checks that a user-defined symbol does not begin with the reserved characters @ or .; throws a ParserException if the check fails.
boolean	commandHasError()	Returns true if the command most recently returned by parseCommand() had a syntax error that parsing recovered from; such a command is not sent to a solver
boolean	commandHasLexicalError()	Returns true if one of the errors commandHasError() reports was an invalid character
boolean	isEOD()	Returns true if the parser is at the end of data
IResponse.IError	lastError()	Returns the most recent error, or null
IExpr.IAttribute<?>	parseAttribute()	Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.
IAttributeValue	parseAttributeValue()	Parses a value for an attribute, returning null with error messages if an error occurs
IExpr.IBinaryLiteral	parseBinary()	Parse an SMT-LIB binary literal; return null and log an error response if there is no numeral
IExpr.IBinding	parseBinding()	Parses a binding "(id expression)", returning null with error messages if an error occurs
List<IExpr.IBinding>	parseBindings()	Parses a parenthesized sequence of let-bindings, returning null with error messages if an error occurs
ICommand	parseCommand()	Parses an SMT-LIB command, if the parser is looking at text representing a valid SMT-LIB command; returns null and logs errors if the text is not a valid command.
IExpr.IConstructor	parseConstructor()	Parses a constructor declaration "(symbol selector*)"
ISort.IDatatype	parseDatatype()	Parses a datatype declaration
IExpr.IDecimal	parseDecimal()	Parse an SMT-LIB decimal literal; return null and log an error response if there is no numeral
IExpr.IDeclaration	parseDeclaration()	Parses a declaration "(id sort)", returning null with error messages if an error occurs
List<IExpr.IDeclaration>	parseDeclarations()	Parses a parenthesized sequence of IDeclaration items, returning null with error messages if an error occurs
IExpr	parseExpr()	Parses a term or formula; return null and log an error response if there is no term or formula
IExpr.IFunctionDeclaration	parseFunctionDeclaration()	Parses a function declaration "(symbol (sorted_var*) sort)" used in define-funs-rec
IExpr.IHexLiteral	parseHex()	Parse an SMT-LIB hex literal; return null and log an error response if there is no numeral
IExpr.IIdentifier	parseIdentifier()	Parses an identifier (either a symbol or a parameterized identifier) from the token stream, returning null (with logged error messages) if there is not one.
IExpr.IKeyword	parseKeyword()	Parse an SMT-LIB keyword; return null and log an error response if there is no valid keyword
default List<ISort.IDatatype>	parseListDatatypes(Parser p)	Parses a parenthesized list of datatype declarations from the given parser.
default List<IExpr>	parseListTerms(Parser p)	Parses a parenthesized list of terms from the given parser.
IExpr.ILiteral	parseLiteral()	Parse an SMT-LIB literal of any kind; return null and log an error response if there is no literal
ILogic	parseLogic()	Parse an SMT-LIB logic; return null and log an error response if there is no valid logic definition
IExpr.INumeral	parseNumeral()	Parse an SMT-LIB numeral; return null and log an error response if there is no numeral
IExpr.IQualifiedIdentifier	parseQualifiedIdentifier()	Parses a qualified identifier (either a symbol, a parameterized identifier, or an as identifier) from the token stream, returning null (with logged error messages) if there is not one.
ICommand.IScript	parseScript()	Parses an SMT-LIB command script.
IExpr.ISelector	parseSelector()	Parses a selector declaration "(symbol sort)"
ISort	parseSort(List<ISort.IParameter> parameters)	Parses a sort, returning null with error messages if a valid sort is not in the next parser tokens.
IExpr.IStringLiteral	parseStringLiteral()	Parse an SMT-LIB string literal; return null and log an error response if there is no valid string literal
IExpr.ISymbol	parseSymbol()	Parse an SMT-LIB symbol; return null and log an error response if there is no symbol
ITheory	parseTheory()	Parse an SMT-LIB theory; return null and log an error response if there is no valid theory definition
SMT.Configuration	smt()	Returns the configuration with which the parser was instantiated.

Method Details

smt

SMT.Configuration smt()

Returns the configuration with which the parser was instantiated.

isEOD

boolean isEOD()
       throws IOException,
IParser.ParserException

Returns true if the parser is at the end of data

Throws:

IOException

IParser.ParserException

lastError

IResponse.IError lastError()

Returns the most recent error, or null

commandHasError

boolean commandHasError()

Returns true if the command most recently returned by parseCommand() had a syntax error that parsing recovered from; such a command is not sent to a solver

commandHasLexicalError

boolean commandHasLexicalError()

Returns true if one of the errors commandHasError() reports was an invalid character

abortLine

void abortLine()

Skips remainder of current line

parseAttribute

IExpr.IAttribute<?> parseAttribute()
                            throws IParser.ParserException

Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.

Throws:

IParser.ParserException

parseAttributeValue

IAttributeValue parseAttributeValue()
                             throws IParser.ParserException

Parses a value for an attribute, returning null with error messages if an error occurs

Throws:

IParser.ParserException

parseCommand

ICommand parseCommand()
               throws IOException,
IParser.ParserException

Parses an SMT-LIB command, if the parser is looking at text representing a valid SMT-LIB command; returns null and logs errors if the text is not a valid command.

Returns:

the command or null

Throws:

IOException - if an IO problem happened during parsing

IParser.ParserException

parseScript

ICommand.IScript parseScript()
                      throws IOException,
IParser.ParserException

Parses an SMT-LIB command script. The result is either a string literal or a parenthesized list of commands (which are parenthesized themselves); the string literal denotes the name of a file from which the commands are read when the command is executed; if the script is included directly, it is parsed, but typechecking is performed in context upon execution. If any errors occur, messages are logged and null is returned, with the parser advancing through a matching right parenthesis.

Returns:

the parsed script

Throws:

IOException - if an IO error occurs in reading input

IParser.ParserException - if an unrecoverable error occurs in parsing tokens

parseExpr

IExpr parseExpr()
         throws IParser.ParserException

Parses a term or formula; return null and log an error response if there is no term or formula

Throws:

IParser.ParserException

parseSymbol

IExpr.ISymbol parseSymbol()
                   throws IParser.ParserException

Parse an SMT-LIB symbol; return null and log an error response if there is no symbol

Throws:

IParser.ParserException

parseLiteral

IExpr.ILiteral parseLiteral()
                     throws IParser.ParserException

Parse an SMT-LIB literal of any kind; return null and log an error response if there is no literal

Throws:

IParser.ParserException

parseNumeral

IExpr.INumeral parseNumeral()
                     throws IParser.ParserException

Parse an SMT-LIB numeral; return null and log an error response if there is no numeral

Throws:

IParser.ParserException

parseDecimal

IExpr.IDecimal parseDecimal()
                     throws IParser.ParserException

Parse an SMT-LIB decimal literal; return null and log an error response if there is no numeral

Throws:

IParser.ParserException

parseBinary

IExpr.IBinaryLiteral parseBinary()
                          throws IParser.ParserException

Parse an SMT-LIB binary literal; return null and log an error response if there is no numeral

Throws:

IParser.ParserException

parseHex

IExpr.IHexLiteral parseHex()
                    throws IParser.ParserException

Parse an SMT-LIB hex literal; return null and log an error response if there is no numeral

Throws:

IParser.ParserException

parseStringLiteral

IExpr.IStringLiteral parseStringLiteral()
                                 throws IParser.ParserException

Parse an SMT-LIB string literal; return null and log an error response if there is no valid string literal

Throws:

IParser.ParserException

parseKeyword

IExpr.IKeyword parseKeyword()
                     throws IParser.ParserException

Parse an SMT-LIB keyword; return null and log an error response if there is no valid keyword

Throws:

IParser.ParserException

parseQualifiedIdentifier

IExpr.IQualifiedIdentifier parseQualifiedIdentifier()
                                             throws IParser.ParserException

Parses a qualified identifier (either a symbol, a parameterized identifier, or an as identifier) from the token stream, returning null (with logged error messages) if there is not one.

Throws:

IParser.ParserException

parseIdentifier

IExpr.IIdentifier parseIdentifier()
                           throws IParser.ParserException

Parses an identifier (either a symbol or a parameterized identifier) from the token stream, returning null (with logged error messages) if there is not one.

Throws:

IParser.ParserException

parseSort

ISort parseSort(List<ISort.IParameter> parameters)
         throws IParser.ParserException

Parses a sort, returning null with error messages if a valid sort is not in the next parser tokens.

Throws:

IParser.ParserException

parseLogic

ILogic parseLogic()
           throws IParser.ParserException

Parse an SMT-LIB logic; return null and log an error response if there is no valid logic definition

Throws:

IParser.ParserException

parseTheory

ITheory parseTheory()
             throws IParser.ParserException

Parse an SMT-LIB theory; return null and log an error response if there is no valid theory definition

Throws:

IParser.ParserException

parseBinding

IExpr.IBinding parseBinding()
                     throws IOException,
IParser.ParserException

Parses a binding "(id expression)", returning null with error messages if an error occurs

Throws:

IOException

IParser.ParserException

parseDatatype

ISort.IDatatype parseDatatype()
                       throws IOException,
IParser.ParserException

Parses a datatype declaration

Throws:

IOException

IParser.ParserException

parseSelector

IExpr.ISelector parseSelector()
                       throws IParser.ParserException

Parses a selector declaration "(symbol sort)"

Throws:

IParser.ParserException

parseConstructor

IExpr.IConstructor parseConstructor()
                             throws IParser.ParserException

Parses a constructor declaration "(symbol selector*)"

Throws:

IParser.ParserException

parseFunctionDeclaration

IExpr.IFunctionDeclaration parseFunctionDeclaration()
                                             throws IParser.ParserException

Parses a function declaration "(symbol (sorted_var*) sort)" used in define-funs-rec

Throws:

IParser.ParserException

parseDeclaration

IExpr.IDeclaration parseDeclaration()
                             throws IOException,
IParser.ParserException

Parses a declaration "(id sort)", returning null with error messages if an error occurs

Throws:

IOException

IParser.ParserException

parseBindings

List<IExpr.IBinding> parseBindings()
                            throws IOException,
IParser.ParserException

Parses a parenthesized sequence of let-bindings, returning null with error messages if an error occurs

Throws:

IOException

IParser.ParserException

parseDeclarations

List<IExpr.IDeclaration> parseDeclarations()
                                    throws IOException,
IParser.ParserException

Parses a parenthesized sequence of IDeclaration items, returning null with error messages if an error occurs

Throws:

IOException

IParser.ParserException

parseListTerms

default List<IExpr> parseListTerms(Parser p)
                            throws IParser.ParserException

Parses a parenthesized list of terms from the given parser.

Throws:

IParser.ParserException

parseListDatatypes

default List<ISort.IDatatype> parseListDatatypes(Parser p)
                                          throws IParser.ParserException

Parses a parenthesized list of datatype declarations from the given parser.

Throws:

IParser.ParserException

checkUserId

default void checkUserId(IExpr.ISymbol id)
                  throws IParser.ParserException

Checks that a user-defined symbol does not begin with the reserved characters @ or .; throws a ParserException if the check fails.

Throws:

IParser.ParserException