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 Gi_response = [Info_response]Source

type Cs_response = Status Source

type Ga_response = [Term]Source

type Proof = S_expr Source

type Gp_response = Proof Source

type Guc_response = [Symbol]Source

type Valuation_pair = (Term, Term)Source

type Gv_response = [Valuation_pair]Source

type T_valuation_pair = (Symbol, Bool)Source

type Gta_response = [T_valuation_pair]Source

Parsing

parseScript :: String -> Script Source

Parses an SMT-LIB command script.

Parsing Verification

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