Package org.sosy_lab.java_smt.basicimpl

Class Tokenizer

  • public final class Tokenizer
extends Object
    Helper class for splitting up an SMT-LIB2 file into a string of commands.

    • Method Detail

      • tokenize

        public static List<String> tokenize​(String input)
        Split up a sequence of lisp expressions.

        This is used by AbstractFormulaManager.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))"]

      • isSetLogicToken

        public static boolean isSetLogicToken​(String token)
        Check if the token is (set-logic ..).

        Use tokenize(String) to turn an SMT-LIB2 script into a string of input tokens.

      • isDeclarationToken

        public static boolean isDeclarationToken​(String token)
        Check if the token is a function or variable declaration.

        Use tokenize(String) to turn an SMT-LIB2 script into a string of input tokens.

      • isDefinitionToken

        public static boolean isDefinitionToken​(String token)
        Check if the token is a function definition.

        Use tokenize(String) to turn an SMT-LIB2 script into a string of input tokens.

      • isAssertToken

        public static boolean isAssertToken​(String token)
        Check if the token is an (assert ...).

        Use tokenize(String) to turn an SMT-LIB2 script into a string of input tokens.

      • isPushToken

        public static boolean isPushToken​(String token)
        Check if the token is an (push ...).

        Use tokenize(String) to turn an SMT-LIB2 script into a string of input tokens.

      • isPopToken

        public static boolean isPopToken​(String token)
        Check if the token is an (pop ...).

        Use tokenize(String) to turn an SMT-LIB2 script into a string of input tokens.

      • isResetAssertionsToken

        public static boolean isResetAssertionsToken​(String token)
        Check if the token is an (reset-assertions ...).

        Use tokenize(String) to turn an SMT-LIB2 script into a string of input tokens.

      • isResetToken

        public static boolean isResetToken​(String token)
        Check if the token is an (reset).

        Use tokenize(String) to turn an SMT-LIB2 script into a string of input tokens.

      • isExitToken

        public static boolean isExitToken​(String token)
        Check if the token is (exit).

        Use tokenize(String) to turn an SMT-LIB2 script into a string of input tokens.

      • 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 tokenize(String) to turn an SMT-LIB2 script into a string of input tokens.