Package org.smtlib.sexpr

Class Utils

java.lang.Object

org.smtlib.sexpr.Utils

public class Utils
extends Object

Constants and reserved-word sets specific to the S-expression concrete syntax.

Field Summary

Fields

Modifier and Type	Field	Description
static final String	AS
static final String	ATTRIBUTE	Concrete syntax for the token that starts an attributed expression
static final String	BINARY	Concrete syntax for the special BINARY token
static final String	DECIMAL	Concrete syntax for the special DECIMAL token
static final String	EXISTS
static final String	FORALL
static final String	HEXADECIMAL	Concrete syntax for the special HEXADECIMAL token
static final String	LAMBDA	Concrete syntax for the lambda token (SMT-LIB 2.7ff, HO-Core theory)
static final String	LET
static final String	LOGIC
static final String	MATCH	Concrete syntax for the match token
static final String	NUMERAL	Concrete syntax for the special NUMERAL token
static final String	PAR
static final String	PARAM	Concrete syntax for the token that starts a parameterized identifier
static final String	PATTERN	The keyword for a quantifier trigger pattern attribute
static final Map<String,SMT.Configuration.SMTLIB>	reservedSince	The SMT-LIB version in which a reserved word became reserved, for those not reserved in V2.0
static final Set<String>	reservedWords	All reserved words (reserved-non-commands plus command names)
static final Set<String>	reservedWordsNotCommands	Reserved words that are not commands (e.g.
static final String	STRING	Concrete syntax for the special STRING token
static final String	THEORY
static final String	WILDCARD	The _ wildcard in match patterns

Method Summary

Methods inherited from class java.lang.Object

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

Field Details

MATCH

public static final String MATCH

Concrete syntax for the match token

See Also:

• Constant Field Values

LAMBDA

public static final String LAMBDA

Concrete syntax for the lambda token (SMT-LIB 2.7ff, HO-Core theory)

See Also:

• Constant Field Values

NUMERAL

public static final String NUMERAL

Concrete syntax for the special NUMERAL token

See Also:

• Constant Field Values

DECIMAL

public static final String DECIMAL

Concrete syntax for the special DECIMAL token

See Also:

• Constant Field Values

STRING

public static final String STRING

Concrete syntax for the special STRING token

See Also:

• Constant Field Values

BINARY

public static final String BINARY

Concrete syntax for the special BINARY token

See Also:

• Constant Field Values

HEXADECIMAL

public static final String HEXADECIMAL

Concrete syntax for the special HEXADECIMAL token

See Also:

• Constant Field Values

PARAM

public static final String PARAM

Concrete syntax for the token that starts a parameterized identifier

See Also:

• Constant Field Values

WILDCARD

public static final String WILDCARD

The _ wildcard in match patterns

See Also:

• Constant Field Values

ATTRIBUTE

public static final String ATTRIBUTE

Concrete syntax for the token that starts an attributed expression

See Also:

• Constant Field Values

PATTERN

public static final String PATTERN

The keyword for a quantifier trigger pattern attribute

See Also:

• Constant Field Values

AS

public static final String AS

See Also:

• Constant Field Values

EXISTS

public static final String EXISTS

See Also:

• Constant Field Values

FORALL

public static final String FORALL

See Also:

• Constant Field Values

LET

public static final String LET

See Also:

• Constant Field Values

LOGIC

public static final String LOGIC

See Also:

• Constant Field Values

PAR

public static final String PAR

See Also:

• Constant Field Values

THEORY

public static final String THEORY

See Also:

• Constant Field Values

reservedWordsNotCommands

public static final Set<String> reservedWordsNotCommands

Reserved words that are not commands (e.g. keywords, built-in tokens)

reservedWords

public static final Set<String> reservedWords

All reserved words (reserved-non-commands plus command names)

reservedSince

public static final Map<String,SMT.Configuration.SMTLIB> reservedSince

The SMT-LIB version in which a reserved word became reserved, for those not reserved in V2.0