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

Show Fun_symbol_decl

data Par_fun_symbol_decl Source

Constructors

Par_fun_symbol_decl Fun_symbol_decl
Par_fun_symbol_decl_symbols [Symbol] Identifier [Sort] [Attribute]

Instances

Show Par_fun_symbol_decl

data Theory_decl Source

Constructors

Theory_decl Symbol [Theory_attribute]

Instances

Show Theory_decl

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

Show Logic_attribute

data Logic Source

Constructors

Logic Symbol [Logic_attribute]

Instances

Show Logic

data Info_flag Source

Constructors

Error_behavior
Name
Authors
Version
Status
Reason_unknown
Info_flag Keyword
All_statistics

Instances

Show Info_flag

data Script Source

Constructors

Script [Command]

Instances

Show Script

data Gen_response Source

Constructors

Unsupported
Success
Error String

Instances

Show Gen_response

data Error_behavior Source

Constructors

Immediate_exit
Continued_execution

Instances

Show Error_behavior

data Reason_unknown Source

Constructors

Timeout
Memout
Incomplete

Instances

Show Reason_unknown

data Status Source

Constructors

Sat
Unsat
Unknown

Instances

Show Status

data Info_response Source

Constructors

Info_response_error_behavior Error_behavior
Info_response_name String
Info_response_authors String
Info_response_version String
Info_response_status Status
Info_response_reason_unknown Reason_unknown
Info_response_attribute Attribute

Instances

Show Info_response

type Proof = S_expr Source

type Valuation_pair = (Term, Term)Source

type T_valuation_pair = (Symbol, Bool)Source

data Command_response Source

Constructors

Gen_response Gen_response
Info_response Info_response
Gi_response [Info_response]
Cs_response Status
Ga_response [Term]
Gp_response Proof
Guc_response [Symbol]
Gv_response [Valuation_pair]
Gta_response [T_valuation_pair]

Instances

Show Command_response

Parsing

parseScript :: String -> Script Source

Lazily parses an SMT-LIB command script.

parseResponses :: String -> [Command_response]Source

Lazily parses an SMT-LIB command responses.

parseTheory :: String -> Theory_decl Source

Lazily parses an SMT-LIB theory declaration.

parseLogic :: String -> Logic Source

Lazily parses an SMT-LIB logic.

Parsing Verification

checkScript :: FilePath -> IO Bool Source

Checks the parsing of a command script.

checkResponses :: FilePath -> IO Bool Source

Checks the parsing of command responses.

checkParser :: IO ()Source

Recursively searches current directory for *.smt2 files to test the parser.

Term_spec_constant Spec_constant
Term_qual_identifier Qual_identifier
Term_qual_identifier_ Qual_identifier [Term]
Term_distinct Term [Term]
Term_let [Var_binding] Term
Term_forall [Sorted_var] Term
Term_exists [Sorted_var] Term
Term_attributes Term [Attribute]

Theory_attribute_sorts [Sort_symbol_decl]
Theory_attribute_funs [Par_fun_symbol_decl]
Theory_attribute_sorts_desc String
Theory_attribute_funs_desc String
Theory_attribute_definition String
Theory_attribute_values String
Theory_attribute_notes String
Theory_attribute Attribute

Print_success Bool
Expand_definitions Bool
Interactive_mode Bool
Produce_proofs Bool
Produce_unsat_cores Bool
Produce_models Bool
Produce_assignments Bool
Regular_output_channel String
Diagnostic_output_channel String
Random_seed Int
Verbosity Int
Option_attribute Attribute

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