PAKCS
Exported names: Imported modules:

Module Language.SMTLIB.Scanner

This module provides a simple scanner for the SMT-LIB language (v2.6).

Author: Jan Tikovsky

Version: October 2017

Summary of exported operations:

scan :: String -> [Token]   

Exported datatypes:

Token

Constructors:

  • LParen :: Token
  • RParen :: Token
  • Semi :: Token
  • Bang :: Token
  • Underscore :: Token
  • Colon :: Token
  • Comma :: Token
  • DQuote :: Token
  • KW_as :: Token
  • KW_BINARY :: Token
  • KW_DECIMAL :: Token
  • KW_error :: Token
  • KW_exists :: Token
  • KW_HEXADEC :: Token
  • KW_forall :: Token
  • KW_let :: Token
  • KW_model :: Token
  • KW_NUMERAL :: Token
  • KW_par :: Token
  • KW_sat :: Token
  • KW_STRING :: Token
  • KW_success :: Token
  • KW_unknown :: Token
  • KW_unsat :: Token
  • KW_unsupported :: Token
  • KW_assert :: Token
  • KW_check_sat :: Token
  • KW_check_sat_assuming :: Token
  • KW_decl_const :: Token
  • KW_decl_datatypes :: Token
  • KW_decl_fun :: Token
  • KW_decl_sort :: Token
  • KW_def_fun :: Token
  • KW_def_fun_rec :: Token
  • KW_def_funs_rec :: Token
  • KW_def_sort :: Token
  • KW_echo :: Token
  • KW_exit :: Token
  • KW_get_assertions :: Token
  • KW_get_assignment :: Token
  • KW_get_info :: Token
  • KW_get_model :: Token
  • KW_get_option :: Token
  • KW_get_proof :: Token
  • KW_get_unsat_assumptions :: Token
  • KW_get_unsat_core :: Token
  • KW_get_value :: Token
  • KW_pop :: Token
  • KW_push :: Token
  • KW_reset :: Token
  • KW_reset_assertions :: Token
  • KW_set_info :: Token
  • KW_set_logic :: Token
  • KW_set_option :: Token
  • KW_assertion_stack_levels :: Token
  • KW_authors :: Token
  • KW_error_behavior :: Token
  • KW_name :: Token
  • KW_reason_unknown :: Token
  • KW_version :: Token
  • KW_immediate_exit :: Token
  • KW_continued_execution :: Token
  • KW_memout :: Token
  • KW_incomplete :: Token
  • Id :: String -> Token
  • Num :: Int -> Token
  • BVal :: Bool -> Token

Exported operations:

scan :: String -> [Token]