Package org.sosy_lab.java_smt.basicimpl

Class Tokenizer

java.lang.Object
org.sosy_lab.java_smt.basicimpl.Tokenizer
public final class Tokenizer extends Object
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.

  • Method Details

    • dequote

      public static String dequote(String s)
      Variable names (symbols) can be wrapped with "|". This function removes those chars.

    • tokenize

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

      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))"]

    • 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.