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
- = 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 Integer
- | Verbosity Integer
- | Option_attribute Attribute
- 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
- type Script = [Command]
- data Gen_response
- = Unsupported
- | Success
- | Error String
- data Error_behavior
- data Reason_unknown
- = Timeout
- | Memout
- | Incomplete
- data Status
- data Info_response
- type Gi_response = [Info_response]
- type Cs_response = Status
- type Ga_response = [Term]
- type Proof = S_expr
- type Gp_response = Proof
- type Guc_response = [Symbol]
- type Valuation_pair = (Term, Term)
- type Gv_response = [Valuation_pair]
- type T_valuation_pair = (Symbol, Bool)
- type Gta_response = [T_valuation_pair]
AST
data Spec_constant Source
Constructors
| Spec_constant_numeral Numeral | |
| Spec_constant_decimal Rational | |
| Spec_constant_hexadecimal Integer | |
| 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
data Theory_attribute Source
data Theory_decl Source
Constructors
| Theory_decl Symbol [Theory_attribute] |
data Logic_attribute Source
Constructors
| Logic Symbol [Logic_attribute] |
Constructors
data Gen_response Source
Constructors
| Unsupported | |
| Success | |
| Error String |
data Error_behavior Source
Constructors
| Immediate_exit | |
| Continued_execution |
data Reason_unknown Source
Constructors
| Timeout | |
| Memout | |
| Incomplete |
data Info_response Source
type Gi_response = [Info_response]Source
type Cs_response = StatusSource
type Ga_response = [Term]Source
type Gp_response = ProofSource
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