Uses of Class
org.smtlib.IParser.ParserException

Packages that use IParser.ParserException

Package	Description
org.smtlib	This package contains the main classes and abstract interfaces for this SMT-LIB tool; the tool provides a stand-alone SMT-LIB-compliant command-line application, an application that responds to SMT-LIB commands over a network port, and an SMT-LIB Java API.
org.smtlib.command	This package contains implementations of the SMT-LIB commands, implementing the interfaces defined in ICommand; these implementations are independent of the concrete syntax that might be used, except that each command object has methods that can parse or print representations of the command in the standard (or potentially other) concrete syntaxes.
org.smtlib.ext	This package contains commands that are extensions to SMT-LIB.
org.smtlib.impl	This package is an implementation of the interfaces defined in org.smtlib.
org.smtlib.sexpr	This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.

Uses of IParser.ParserException in org.smtlib

Subclasses of IParser.ParserException in org.smtlib

Modifier and Type	Class	Description
static class	IParser.SyntaxException	An exception to be thrown if there is an unrecoverable problem scanning the syntax

Methods in org.smtlib that throw IParser.ParserException

Modifier and Type	Method	Description
default void	IParser.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	IParser.isEOD()	Returns true if the parser is at the end of data
T	IParser.ElementParser.parse()
IExpr.IAttribute<?>	IParser.parseAttribute()	Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.
IAttributeValue	IParser.parseAttributeValue()	Parses a value for an attribute, returning null with error messages if an error occurs
IExpr.IBinaryLiteral	IParser.parseBinary()	Parse an SMT-LIB binary literal; return null and log an error response if there is no numeral
IExpr.IBinding	IParser.parseBinding()	Parses a binding "(id expression)", returning null with error messages if an error occurs
List<IExpr.IBinding>	IParser.parseBindings()	Parses a parenthesized sequence of let-bindings, returning null with error messages if an error occurs
ICommand	IParser.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	IParser.parseConstructor()	Parses a constructor declaration "(symbol selector*)"
ISort.IDatatype	IParser.parseDatatype()	Parses a datatype declaration
IExpr.IDecimal	IParser.parseDecimal()	Parse an SMT-LIB decimal literal; return null and log an error response if there is no numeral
IExpr.IDeclaration	IParser.parseDeclaration()	Parses a declaration "(id sort)", returning null with error messages if an error occurs
List<IExpr.IDeclaration>	IParser.parseDeclarations()	Parses a parenthesized sequence of IDeclaration items, returning null with error messages if an error occurs
IExpr	IParser.parseExpr()	Parses a term or formula; return null and log an error response if there is no term or formula
IExpr.IFunctionDeclaration	IParser.parseFunctionDeclaration()	Parses a function declaration "(symbol (sorted_var*) sort)" used in define-funs-rec
IExpr.IHexLiteral	IParser.parseHex()	Parse an SMT-LIB hex literal; return null and log an error response if there is no numeral
IExpr.IIdentifier	IParser.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	IParser.parseKeyword()	Parse an SMT-LIB keyword; return null and log an error response if there is no valid keyword
default List<ISort.IDatatype>	IParser.parseListDatatypes(Parser p)	Parses a parenthesized list of datatype declarations from the given parser.
default List<IExpr>	IParser.parseListTerms(Parser p)	Parses a parenthesized list of terms from the given parser.
IExpr.ILiteral	IParser.parseLiteral()	Parse an SMT-LIB literal of any kind; return null and log an error response if there is no literal
ILogic	IParser.parseLogic()	Parse an SMT-LIB logic; return null and log an error response if there is no valid logic definition
IExpr.INumeral	IParser.parseNumeral()	Parse an SMT-LIB numeral; return null and log an error response if there is no numeral
IExpr.IQualifiedIdentifier	IParser.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	IParser.parseScript()	Parses an SMT-LIB command script.
IExpr.ISelector	IParser.parseSelector()	Parses a selector declaration "(symbol sort)"
ISort	IParser.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	IParser.parseStringLiteral()	Parse an SMT-LIB string literal; return null and log an error response if there is no valid string literal
IExpr.ISymbol	IParser.parseSymbol()	Parse an SMT-LIB symbol; return null and log an error response if there is no symbol
ITheory	IParser.parseTheory()	Parse an SMT-LIB theory; return null and log an error response if there is no valid theory definition

Uses of IParser.ParserException in org.smtlib.command

Methods in org.smtlib.command that throw IParser.ParserException

Modifier and Type	Method	Description
static C_assert	C_assert.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_check_sat_assuming	C_check_sat_assuming.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_declare_const	C_declare_const.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_declare_datatype	C_declare_datatype.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_declare_datatypes	C_declare_datatypes.parse(Parser p)	Parses the arguments: ( (symbol numeral)+ ) ( datatype_dec+ )
static C_declare_fun	C_declare_fun.parse(Parser p)	Parses the arguments of the command, producing a new command instance.
static C_declare_sort_parameter	C_declare_sort_parameter.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_declare_sort	C_declare_sort.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_define_const	C_define_const.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_define_fun_rec	C_define_fun_rec.parse(Parser p)	Parses the command arguments and creates a command instance
static C_define_fun	C_define_fun.parse(Parser p)	Parses the command arguments and creates a command instance
static C_define_funs_rec	C_define_funs_rec.parse(Parser p)	Parses the command arguments and creates a command instance
static C_define_sort	C_define_sort.parse(Parser p)	Parses the command arguments and creates a command instance
static C_echo	C_echo.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_exit	C_exit.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_get_assertions	C_get_assertions.parse(Parser p)	Parses the command, producing a new command instance
static C_get_assignment	C_get_assignment.parse(Parser p)	Parses the command, producing a new command instance
static C_get_info	C_get_info.parse(Parser p)	Creates a command instance by parsing the concrete S-expression syntax
static C_get_model	C_get_model.parse(Parser p)	Parses the command, producing a new command instance
static C_get_option	C_get_option.parse(Parser p)	Creates a command instance by parsing the concrete S-expression syntax
static C_get_proof	C_get_proof.parse(Parser p)	Parses the command, producing a new command instance
static C_get_unsat_assumptions	C_get_unsat_assumptions.parse(Parser p)	Parses the command, producing a new command instance
static C_get_unsat_core	C_get_unsat_core.parse(Parser p)	Parses the command, producing a new command instance
static C_get_value	C_get_value.parse(Parser p)	Parses the command, producing a new command instance
static C_pop	C_pop.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_push	C_push.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_reset_assertions	C_reset_assertions.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_reset	C_reset.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_set_info	C_set_info.parse(Parser p)	Creates a command instance by parsing the concrete S-expression syntax
static C_set_logic	C_set_logic.parse(Parser p)	Creates a command instance by parsing the S-expression concrete syntax
static C_set_option	C_set_option.parse(Parser p)	Creates a command instance by parsing the concrete S-expression syntax

Uses of IParser.ParserException in org.smtlib.ext

Methods in org.smtlib.ext that throw IParser.ParserException

Modifier and Type	Method	Description
static C_exec	C_exec.parse(Parser p)	Parses the arguments of the command, producing a new command instance
static C_what	C_what.parse(Parser p)	Parses the input concrete S-expression syntax to produce a command instance

Uses of IParser.ParserException in org.smtlib.impl

Methods in org.smtlib.impl that return IParser.ParserException

Modifier and Type	Method	Description
static IParser.ParserException	Command.error(SMT.Configuration smt, String msg, IPos pos)	Creates a ParserException with the given message and position.

Uses of IParser.ParserException in org.smtlib.sexpr

Methods in org.smtlib.sexpr that return IParser.ParserException

Modifier and Type	Method	Description
IParser.ParserException	Parser.error(String msg, IPos pos)	Creates a ParserException with the given message and position; callers should throw the result.
IParser.ParserException	Parser.error(String msg, ILexToken token)	Creates a ParserException from the given message and token; callers should throw the result.

Methods in org.smtlib.sexpr that throw IParser.ParserException

Modifier and Type	Method	Description
ILexToken	Lexer.getToken()	Returns the next lexical token, advancing the scanner.
ILexToken	Lexer.getToken(Class<?> clazz)	Returns the next lexical token; if the token returned matches the given class (or is a subclass), then the scanner is advanced; if the token does not match, the scanner is not advanced.
ILexToken	Lexer.getToken(String text)	Returns the first token found in the given text
protected ILexToken	Lexer.getToken(Matcher matcher)	Returns the next token found in the given matcher, advancing the matcher
protected ILexToken	Parser.getToken(Matcher m)	Reports a vertical tab or form feed between tokens (except with --relax), which is then read as white space, and a keyword that is not a colon followed by a simple symbol (#185)
boolean	Lexer.isEOD()	Returns true if the next token is the end-of-data
boolean	Lexer.isLP()	Returns true if the next token is a left parenthesis (without consuming it)
boolean	Lexer.isRP()	Returns true if the next token is a right parenthesis (without consuming it)
List<IExpr>	Parser.parseAssertionList()	Parses a parenthesized list of terms, as returned by a get-assertions response.
List<IResponse.IPair<IExpr.ISymbol,Boolean>>	Parser.parseAssignmentList()	Parses a parenthesized list of (symbol bool) pairs, as returned by a get-assignment response.
IResponse.IPair<IExpr.ISymbol,Boolean>	Parser.parseAssignmentPair()	Parses one (symbol bool) pair, as found in a get-assignment response.
IExpr.IAttribute<?>	Parser.parseAttribute()	Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.
protected IExpr.IAttribute<?>	Parser.parseAttributeRest(IExpr.IKeyword keyword)	Parses the (optional) value of an attribute whose keyword has already been parsed.
List<IExpr.IAttribute<?>>	Parser.parseAttributeSequence()	Parse a sequence of attributes (keyword with optional value) terminated by a right parenthesis, returning null with error messages if an error occurs.
IAttributeValue	Parser.parseAttributeValue()	Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.
IExpr.IBinaryLiteral	Parser.parseBinary()	Parses a binary literal, returning null with the given message if an error occurs; if the next token is not a binary literal, the token is not consumed,
IExpr.IBinding	Parser.parseBinding()	Parses a binding "(id expression)", returning null with error messages if an error occurs
List<IExpr.IBinding>	Parser.parseBindings()	Parses a parenthesized sequence of let-bindings
IExpr.IConstructor	Parser.parseConstructor()	Parses a constructor declaration "(symbol selector*)"
ISort.IDatatype	Parser.parseDatatype()	Parses a datatype declaration: "( constructor+ )" or "( par ( symbol+ ) ( constructor+ ) )"
IExpr.IDecimal	Parser.parseDecimal()	Parses a decimal, returning null with the given message if an error occurs; if the next token is not a decimal, the token is not consumed,
IExpr.IDeclaration	Parser.parseDeclaration()	Parses a declaration "(id sort)", returning null with error messages if an error occurs
List<IExpr.IDeclaration>	Parser.parseDeclarations()	Parses a parenthesized sequence of IDeclaration items
IExpr	Parser.parseExpr()	Parses an expression, returning null with error messages if there is not a valid expression in the token stream.
IExpr.IFunctionDeclaration	Parser.parseFunctionDeclaration()	Parses a function declaration "( symbol ( sorted_var* ) sort )" used in define-funs-rec
IExpr.IHexLiteral	Parser.parseHex()	Parses a hex literal, returning null with the given message if an error occurs; if the next token is not a hex literal, the token is not consumed,
IExpr.IIdentifier	Parser.parseIdentifier()	Parses an identifier (either symbol or parameterized identifier) from the token stream, returning null with logged error messages if there is not one.
SMTExpr.Keyword	Parser.parseKeyword()	Parses a keyword, returning null with an error message if an error occurs; if the next token is not a keyword, the token is not consumed.
<T> List<T>	Parser.parseList(IParser.ElementParser<T> elementParser, String kind, boolean allowEmpty)	Parses a parenthesized list of elements using the given element parser.
IExpr.ILiteral	Parser.parseLiteral()	Parses a literal, returning null with error messages if an error occurs.
ILogic	Parser.parseLogic()	Parses a logic definition (including beginning and ending parentheses, returning null with error messages if it fails; only part of the checking of the contents is performed in this call (the rest is done in loadLogic).
ILexToken	Parser.parseLP()	Parses a left parenthesis, returning null and emitting an error message if there isn't one (and the next token is not consumed)
IExpr.IMatchCase	Parser.parseMatchCase()	Parses a single match case: "(pattern term)"
IExpr.INumeral	Parser.parseNumeral()	Parses a numeral, returning null with error messages if an error occurs; if the next token is not a numeral, the token is not consumed,
IExpr.IPattern	Parser.parsePattern()	Parses a match pattern: either a bare symbol (or wildcard _) or "(symbol symbol*)" where params may include _
IExpr.IQualifiedIdentifier	Parser.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.
IResponse	Parser.parseResponse(String response)
ILexToken	Parser.parseRP()	Parses a right parenthesis, returning null and emitting an error message if there isn't one (and the next token is not consumed)
IExpr.ISelector	Parser.parseSelector()	Parses a selector declaration "(symbol sort)"
Sexpr.Seq	Parser.parseSeq(ILexToken lp)	Parses and adds Sexpr to a list until parseSexpr returns null (indicating a RightParen has been seen or end of input or an error)
ISexpr	Parser.parseSexpr()	Parses an Sexpr
Sort	Parser.parseSort(List<ISort.IParameter> parameters)	Parses a sort, returning null with error messages if a valid sort is not in the next parser tokens.
List<ISort>	Parser.parseSortList(List<ISort.IParameter> parameters)	Parses sequence of sorts up to a right-parenthesis, returning null with error messages if an error occurs.
SMTExpr.StringLiteral	Parser.parseStringLiteral()	Parses a string literal, returning null with an error message if an error occurs; if the next token is not a string literal, the token is not consumed,
SMTExpr.Symbol	Parser.parseSymbol()	Parses a symbol, returning null with messages and not advancing the parser if an error occurs
SMTExpr.Symbol	Parser.parseSymbol(String msg)	Parses a symbol (but not a reserved word unless the configuration field 'relax' is true), returning null with messages if an error occurs; the parser is advanced only if an actual symbol is parsed.
List<IExpr.ISymbol>	Parser.parseSymbolList()	Parses a parenthesized list of names, as returned by a get-unsat-core response.
SMTExpr.Symbol	Parser.parseSymbolOrReservedWord(String msg)	Parses a symbol or a reserved word, returning null with messages if an error occurs.
List<IExpr.IAttribute<?>>	Parser.parseTermAttributeSequence()	Parses the attributes of an annotated term (! t attr+) up to the right parenthesis.
List<IExpr>	Parser.parseTermList()	Parses a parenthesized list of terms, as returned by a get-unsat-assumptions response.
ITheory	Parser.parseTheory()	Parses a theory definition (including beginning and ending parentheses, returning null with error messages if it fails; only part of the checking of the contents is performed in this call (the rest is done in loadTheory).
List<IResponse.IPair<IExpr,IExpr>>	Parser.parseValueList()	Parses a parenthesized list of (term value) pairs, as returned by a get-value response.
IResponse.IPair<IExpr,IExpr>	Parser.parseValuePair()	Parses one (term value) pair, as found in a get-value response.
ILexToken	Lexer.peekToken()	Returns the next lexical token without consuming it; a subsequent call to getToken will return the same token.
IPos	Lexer.skipThruRP()	Reads and discards tokens until an unmatched right parenthesis or end-of-data is read