Language.SMTLIB
Contents
Description
Parsing and printing SMT-LIB.
- type Numeral = Integer
- type Symbol = String
- type Keyword = String
- data Spec_constant
- data S_expr
- data Identifier
- = Identifier Symbol
- | Identifier_ Symbol [Numeral]
- data Sort
- data Attribute_value
- data Attribute
- data Qual_identifier
- data Var_binding = Var_binding Symbol Term
- data Sorted_var = Sorted_var Symbol Sort
- data Term
- data Sort_symbol_decl = Sort_symbol_decl Identifier Numeral [Attribute]
- data Meta_spec_constant
- data Fun_symbol_decl
- data Par_fun_symbol_decl
- data Theory_attribute
- data Theory_decl = Theory_decl Symbol [Theory_attribute]
- data Logic_attribute
- data Logic = Logic Symbol [Logic_attribute]
- data Option
- data Info_flag
- = Error_behavior
- | Name
- | Authors
- | Version
- | Status
- | Reason_unknown
- | Info_flag Keyword
- | All_statistics
- data Command
- = Set_logic Symbol
- | Set_option Option
- | Set_info Attribute
- | Declare_sort Symbol Numeral
- | Define_sort Symbol [Symbol] Sort
- | Declare_fun Symbol [Sort] Sort
- | Define_fun Symbol [Sorted_var] Sort Term
- | Push Int
- | Pop Int
- | Assert Term
- | Check_sat
- | Get_assertions
- | Get_proof
- | Get_unsat_core
- | Get_value [Term]
- | Get_assignment
- | Get_option Keyword
- | Get_info Info_flag
- | Exit
- data Script = Script [Command]
- data Gen_response
- = Unsupported
- | Success
- | Error String
- data Error_behavior
- data Reason_unknown
- = Timeout
- | Memout
- | Incomplete
- data Status
- data Info_response
- type Proof = S_expr
- type Valuation_pair = (Term, Term)
- type T_valuation_pair = (Symbol, Bool)
- data Command_response
- parseScript :: String -> Script
- parseResponses :: String -> [Command_response]
- parseTheory :: String -> Theory_decl
- parseLogic :: String -> Logic
- checkScript :: FilePath -> IO Bool
- checkResponses :: FilePath -> IO Bool
- checkParser :: IO ()
Syntax
data Spec_constant Source
Constructors
Spec_constant_numeral Numeral | |
Spec_constant_decimal Rational | |
Spec_constant_hexadecimal String | |
Spec_constant_binary [Bool] | |
Spec_constant_string String |
Instances
Constructors
S_expr_constant Spec_constant | |
S_expr_symbol Symbol | |
S_expr_keyword Keyword | |
S_exprs [S_expr] |
Constructors
Sort_bool | |
Sort_identifier Identifier | |
Sort_identifiers Identifier [Sort] |
data Attribute_value Source
Constructors
Attribute_value_spec_constant Spec_constant | |
Attribute_value_symbol Symbol | |
Attribute_value_s_expr [S_expr] |
Instances
Constructors
Attribute Keyword | |
Attribute_s_expr Keyword S_expr |
data Qual_identifier Source
Constructors
Qual_identifier Identifier | |
Qual_identifier_sort Identifier Sort |
Instances
data Meta_spec_constant Source
Instances
data Fun_symbol_decl Source
Constructors
Fun_symbol_decl_spec_constant Spec_constant Sort [Attribute] | |
Fun_symbol_decl_meta_spec_constant Meta_spec_constant Sort [Attribute] | |
Fun_symbol_decl Identifier [Sort] [Attribute] |
Instances
data Par_fun_symbol_decl Source
Constructors
Par_fun_symbol_decl Fun_symbol_decl | |
Par_fun_symbol_decl_symbols [Symbol] Identifier [Sort] [Attribute] |
Instances
data Theory_attribute Source
Constructors
Instances
data Logic_attribute Source
Constructors
Logic_attribute_theories [Symbol] | |
Logic_attribute_language String | |
Logic_attribute_extensions String | |
Logic_attribute_values String | |
Logic_attribute_notes String | |
Logic_attribute Attribute |
Instances
Constructors
data Info_response Source
Constructors
Instances
type Valuation_pair = (Term, Term)Source
type T_valuation_pair = (Symbol, Bool)Source
data Command_response Source
Constructors
Instances
Parsing
parseScript :: String -> ScriptSource
Lazily parses an SMT-LIB command script.
parseResponses :: String -> [Command_response]Source
Lazily parses an SMT-LIB command responses.
parseTheory :: String -> Theory_declSource
Lazily parses an SMT-LIB theory declaration.
parseLogic :: String -> LogicSource
Lazily parses an SMT-LIB logic.
Parsing Verification
checkScript :: FilePath -> IO BoolSource
Checks the parsing of a command script.
checkResponses :: FilePath -> IO BoolSource
Checks the parsing of command responses.
Recursively searches current directory for *.smt2 files to test the parser.