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
data Attribute_value Source
data Qual_identifier Source
data Meta_spec_constant Source
data Fun_symbol_decl Source
data Theory_attribute Source
data Logic_attribute Source
data Info_response Source
type Valuation_pair = (Term, Term)Source
type T_valuation_pair = (Symbol, Bool)Source
data Command_response Source
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.