Package org.sosy_lab.java_smt.basicimpl

Class SMTLibTokenizer

java.lang.Object

org.sosy_lab.java_smt.basicimpl.SMTLibTokenizer

All Implemented Interfaces:

Iterable<String>

public final class SMTLibTokenizer
extends Object
implements Iterable<String>

Helper class for splitting up an SMT-LIB2 file into a string of commands.

This is not a full SMTLIB parser, but only provides basic support for SMTLIB commands.

Use this class as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static final class	SMTLibTokenizer.TokenizerIterator

Method Summary

Modifier and Type	Method	Description
static String	dequoteSMTLib(String s)	Variable names (symbols) can be wrapped with "|".
static boolean	isAssertToken(String token)	Check if the token is an (assert ...).
static boolean	isDeclarationToken(String token)	Check if the token is a function or variable declaration.
static boolean	isDefinitionToken(String token)	Check if the token is a function definition.
static boolean	isExitToken(String token)	Check if the token is (exit).
static boolean	isForbiddenToken(String token)	Check if this is a forbidden token.
static boolean	isPopToken(String token)	Check if the token is an (pop ...).
static boolean	isPushToken(String token)	Check if the token is an (push ...).
static boolean	isResetAssertionsToken(String token)	Check if the token is an (reset-assertions ...).
static boolean	isResetToken(String token)	Check if the token is an (reset).
static boolean	isSetInfoToken(String token)	Check if the token is (set-info ..).
static boolean	isSetLogicToken(String token)	Check if the token is (set-logic ..).
Iterator<String>	iterator()
static SMTLibTokenizer	of(String inputToTokenize)	Creates a new SMTLibTokenizer from the input String.
ImmutableList<String>	toImmutableList()	Split up a sequence of lisp expressions into a list of nen-empty tokens.

Methods inherited from class java.lang.Object

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

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Method Details

of

public static SMTLibTokenizer of(String inputToTokenize)

Creates a new SMTLibTokenizer from the input String. The resulting SMTLibTokenizer is an Iterable for the SMTLIB tokens. A new Iterator on the input can be created with iterator(). A ImmutableList of all tokens can be created via toImmutableList(). Tokenized input is returned sanitized from unnecessary characters, and checked for basic (but not full) syntactic validity (e.g. that every opened bracket is also closed in a valid way).

Parameters:

inputToTokenize - SMTLIB input String that may be empty, but not null.

dequoteSMTLib

public static String dequoteSMTLib(String s)

Variable names (symbols) can be wrapped with "|". This function removes those chars.

toImmutableList

public ImmutableList<String> toImmutableList()

Split up a sequence of lisp expressions into a list of nen-empty tokens. This method simply uses the SMTLibTokenizer.TokenizerIterator and creates a list out of all tokens. Repeated calls to this method are inefficient, as a new List is created every time it is called.

This is used by FormulaManager.parse(String) as part of the preprocessing before the input is passed on to the solver. SMT-LIB2 scripts are sequences of commands that are just r-expression. We split them up and then return the list.

As an example tokenize("(define-const a Int)(assert (= a 0)") will return the sequence ["(define-const a Int)", "(assert (= a 0))"]

iterator

public Iterator<String> iterator()

Specified by:

iterator in interface Iterable<String>

isSetLogicToken

public static boolean isSetLogicToken(String token)

Check if the token is (set-logic ..).

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

isSetInfoToken

public static boolean isSetInfoToken(String token)

Check if the token is (set-info ..).

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

isDeclarationToken

public static boolean isDeclarationToken(String token)

Check if the token is a function or variable declaration.

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

isDefinitionToken

public static boolean isDefinitionToken(String token)

Check if the token is a function definition.

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

isAssertToken

public static boolean isAssertToken(String token)

Check if the token is an (assert ...).

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

isPushToken

public static boolean isPushToken(String token)

Check if the token is an (push ...).

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

isPopToken

public static boolean isPopToken(String token)

Check if the token is an (pop ...).

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

isResetAssertionsToken

public static boolean isResetAssertionsToken(String token)

Check if the token is an (reset-assertions ...).

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

isResetToken

public static boolean isResetToken(String token)

Check if the token is an (reset).

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

isExitToken

public static boolean isExitToken(String token)

Check if the token is (exit).

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().

isForbiddenToken

public static boolean isForbiddenToken(String token)

Check if this is a forbidden token.

The list of forbidden tokens contains:

• push
• pop
• reset-assertions
• reset

Forbidden tokens manipulate the stack and are not supported while parsing SMT-lIB2 string. When a forbidden token is found parsing should be aborted by throwing an IllegalArgumentException exception.

Use SMTLibTokenizer as an Iterable, or the Iterator with iterator() to turn an SMT-LIB2 script into a string of input tokens efficiently. Alternatively, a ImmutableList of all tokens can be created with toImmutableList().