Package org.smtlib.sexpr

Class Lexer

java.lang.Object

org.smtlib.sexpr.Lexer

Direct Known Subclasses:

Parser

public class Lexer
extends Object

Converts character sequences (from ISource) into tokens, presuming the standard SMT-LIBv2 concrete syntax. It is intended to be used as a base class for a parser, but could also be used by inclusion.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static interface	Lexer.IPLexToken	An interface used for punctuation tokens that can be retrieved from the parser input.
protected class	Lexer.LexToken	A lexical token class for single punctuation characters.

Field Summary

Fields

Modifier and Type	Field	Description
protected IPos	badWhitespace	The position of a vertical tab or form feed, outside a comment, in the white space before the token last scanned, or null: \p{Space} reads them as white space, which SMT-LIB's white space is not; the Parser reports them (the Lexer reports nothing itself, #148)
static final Pattern	combined	This composite regular expression matches tokens in the SMTLIB input.
protected final CharSequence	csr	The CharSequence corresponding to the source object
protected final Matcher	matcher	The Matcher used to do lexical scanning
int	prefixCommentEnd	The character range prefixCommentText was captured from (before the one leading newline stripping below, if any, is applied to prefixCommentText itself) -- lets a caller that turns a comment into its own node (see command/C_comment.java) give that node an accurate pos().
int	prefixCommentStart	The character range prefixCommentText was captured from (before the one leading newline stripping below, if any, is applied to prefixCommentText itself) -- lets a caller that turns a comment into its own node (see command/C_comment.java) give that node an accurate pos().
String	prefixCommentText	Any comment text found before the current token, starting from the first line terminator onward -- i.e.
int	sameLineTrailingEnd
int	sameLineTrailingStart
String	sameLineTrailingText	Whitespace/comment text, if any, found between the previous token and the first line terminator after it -- i.e.
static final Pattern	skipThroughEndOfLine	A pattern to skip up to the end of the line

Constructor Summary

Constructors

Constructor	Description
Lexer(SMT.Configuration smtConfig, ISource src)	Creates a Lexer using an SMT configuration object and a source for characters

Method Summary

Modifier and Type	Method	Description
void	abortLine()	Skips the rest of the current line, including a token already looked ahead at, resetting the matcher to point to the line termination character
int	currentPos()	Returns the position of the next character to be read
Lexer.LexToken	EOD(int cpos)	Creates a lexical token for a end-of-data at the given position
ILexToken	getToken()	Returns the next lexical token, advancing the scanner.
ILexToken	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	getToken(String text)	Returns the first token found in the given text
protected ILexToken	getToken(Matcher matcher)	Returns the next token found in the given matcher, advancing the matcher
boolean	isEOD()	Returns true if the next token is the end-of-data
boolean	isLP()	Returns true if the next token is a left parenthesis (without consuming it)
boolean	isRP()	Returns true if the next token is a right parenthesis (without consuming it)
Lexer.LexToken	LP(int cpos)	Creates a lexical token for a left parenthesis at the given position
ILexToken	peekToken()	Returns the next lexical token without consuming it; a subsequent call to getToken will return the same token.
IPos	pos(int start, int end)	Creates an IPos object with the given start and end and the source for this Lexer
Lexer.LexToken	RP(int cpos)	Creates a lexical token for a right parenthesis at the given position
protected static <T extends IPos.IPosable> T	setPos(T t, IPos pos)	A static helper method that sets the position of an AST node, but returns the same type
IPos	skipThruRP()	Reads and discards tokens until an unmatched right parenthesis or end-of-data is read
final ISource	source()	The source of input used in this lexer; typically a different lexer object will be used for each source (e.g.

Methods inherited from class java.lang.Object

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

Field Details

matcher

protected final Matcher matcher

The Matcher used to do lexical scanning

prefixCommentText

public String prefixCommentText

Any comment text found before the current token, starting from the first line terminator onward -- i.e. excluding whatever is captured separately in sameLineTrailingText below. This is what becomes a standalone C_comment node (see command/C_comment.java): text that occupies its own line(s), not sharing a line with whatever token preceded it.

prefixCommentStart

public int prefixCommentStart

The character range prefixCommentText was captured from (before the one leading newline stripping below, if any, is applied to prefixCommentText itself) -- lets a caller that turns a comment into its own node (see command/C_comment.java) give that node an accurate pos().

prefixCommentEnd

public int prefixCommentEnd

The character range prefixCommentText was captured from (before the one leading newline stripping below, if any, is applied to prefixCommentText itself) -- lets a caller that turns a comment into its own node (see command/C_comment.java) give that node an accurate pos().

sameLineTrailingText

public String sameLineTrailingText

Whitespace/comment text, if any, found between the previous token and the first line terminator after it -- i.e. sharing a physical line with whatever token preceded it (typically a trailing "; comment" right after a command's closing parenthesis). Null unless that same-line span actually contains a comment (plain trailing whitespace doesn't count). Kept separate from prefixCommentText so a caller can attach it to the command that precedes it (see Parser.parseCommand()) rather than folding it into the next command's leading comment -- the two are semantically different: this is "trailing decoration of a real source line," not "a comment line of its own." A same-line span can contain at most one comment, since a comment consumes to end of line by construction, so nothing else can follow it before the line terminator.

sameLineTrailingStart

public int sameLineTrailingStart

sameLineTrailingEnd

public int sameLineTrailingEnd

badWhitespace

protected IPos badWhitespace

The position of a vertical tab or form feed, outside a comment, in the white space before the token last scanned, or null: \p{Space} reads them as white space, which SMT-LIB's white space is not; the Parser reports them (the Lexer reports nothing itself, #148)

csr

protected final CharSequence csr

The CharSequence corresponding to the source object

combined

public static final Pattern combined

This composite regular expression matches tokens in the SMTLIB input. It first gobbles up any whitespace and comments, and then gets one instance of a token. For the most part, the fact the + and * are greedy ensures that tokens are not prematurely ended. But, there are three items to note: 1) when scanning for Numerals and Decimals, the scanner has to be sure that the token is followed by whitespace, parentheses or a comment. It is not allowed to have other characters immediately after a numeral. But the characters that follow are not part of the Numeral or Decimal and have to be rescanned. 2) It appears that in interpreting the regular expression, if two alternatives match, it is the textually earlier one in the regex that is reported as matching via matcher.group(int). Thus we include a catch-all error token as the last element of the set of alternatives, so that there is always something that matches. 3) The regex for a SMT-LIB string literal (rgxStringLiteral) is accurate, but causes stack overflow on long (>~1000 characters) strings. One would not think that there was a recursive call for each character, but it appears that there is. It may be that a redesign of the regex would help, but instead, I just changed the regex to match the opening quote - then we scan the string by hand and adjust the matcher position afterwards (see the matcher.group(k=7) case in getToken(Matcher)).

skipThroughEndOfLine

public static final Pattern skipThroughEndOfLine

A pattern to skip up to the end of the line

Constructor Details

Lexer

public Lexer(SMT.Configuration smtConfig,
 ISource src)

Creates a Lexer using an SMT configuration object and a source for characters

Method Details

abortLine

public void abortLine()

Skips the rest of the current line, including a token already looked ahead at, resetting the matcher to point to the line termination character

LP

public Lexer.LexToken LP(int cpos)

Creates a lexical token for a left parenthesis at the given position

RP

public Lexer.LexToken RP(int cpos)

Creates a lexical token for a right parenthesis at the given position

EOD

public Lexer.LexToken EOD(int cpos)

Creates a lexical token for a end-of-data at the given position

source

public final ISource source()

The source of input used in this lexer; typically a different lexer object will be used for each source (e.g. different file, string, port, etc.) of input data.

setPos

protected static <T extends IPos.IPosable> T setPos(T t,
 IPos pos)

A static helper method that sets the position of an AST node, but returns the same type

peekToken

public ILexToken peekToken()
                    throws IParser.ParserException

Returns the next lexical token without consuming it; a subsequent call to getToken will return the same token.

Throws:

IParser.ParserException - if something bad or an intentional abort happens

getToken

public ILexToken getToken(Class<?> clazz)
                   throws IParser.ParserException

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.

Throws:

IParser.ParserException - if something bad or an intentional abort happens

currentPos

public int currentPos()

Returns the position of the next character to be read

isEOD

public boolean isEOD()
              throws IParser.ParserException

Returns true if the next token is the end-of-data

Throws:

IParser.ParserException

skipThruRP

public IPos skipThruRP()
                throws IParser.ParserException

Reads and discards tokens until an unmatched right parenthesis or end-of-data is read

Returns:

the position of the right parenthesis or end-of-data

Throws:

IParser.ParserException

isLP

public boolean isLP()
             throws IParser.ParserException

Returns true if the next token is a left parenthesis (without consuming it)

Throws:

IParser.ParserException

isRP

public boolean isRP()
             throws IParser.ParserException

Returns true if the next token is a right parenthesis (without consuming it)

Throws:

IParser.ParserException

pos

public IPos pos(int start,
 int end)

Creates an IPos object with the given start and end and the source for this Lexer

getToken

public ILexToken getToken(String text)
                   throws IParser.ParserException

Returns the first token found in the given text

Throws:

IParser.ParserException

getToken

public ILexToken getToken()
                   throws IParser.ParserException

Returns the next lexical token, advancing the scanner.

Throws:

IParser.ParserException - if something bad or an intentional abort happens

getToken

protected ILexToken getToken(Matcher matcher)
                      throws IParser.ParserException

Returns the next token found in the given matcher, advancing the matcher

Throws:

IParser.ParserException