Psmt2Frontend.Smtlib_syntax
type 'a data = {
p : (Stdlib.Lexing.position * Stdlib.Lexing.position) option; |
c : 'a; |
ty : Smtlib_ty.ty; |
mutable is_quantif : bool; |
}
type symbol = string data
type keyword_aux =
| Category |
| Smtlibversion |
| Source |
| Statuts of symbol |
| License |
| Notes |
| Axioms |
| Definitio |
| Extensions |
| Funs |
| FunsDescript |
| Language |
| Sorts |
| SortsDescr |
| Theories |
| Values |
and keyword = keyword_aux data
and key_option = key_option_aux data
and option = option_aux data
and key_info_aux =
| Allstats |
| Assertionstacklvl |
| Authors |
| Difficulty |
| Errorbehav |
| Incremental |
| Instance |
| Name |
| Reasonunknown |
| Series |
| Version |
| Key_info of keyword |
and key_info = key_info_aux data
and key_term = key_term_aux data
and attribute_value = attribute_value_aux data
and attribute = attribute_aux data
and identifier = identifier_aux data
and prop_literal = prop_literal_aux data
and qualidentifier = qualidentifier_aux data
and pattern = pattern_aux data
and term_aux =
| TermSpecConst of constant |
| TermQualIdentifier of qualidentifier |
| TermQualIdTerm of qualidentifier * term list |
| TermLetTerm of varbinding list * term |
| TermForAllTerm of sorted_var list * term |
| TermExistsTerm of sorted_var list * term |
| TermExclimationPt of term * key_term list |
| TermMatch of term * (pattern * term) list |
and sort_dec = symbol * string
and constructor_dec = symbol * selector_dec list
type command_aux =
| Cmd_Assert of symbol list * term |
| Cmd_CheckSat |
| Cmd_CheckAllSat of symbol list |
| Cmd_CheckSatAssum of prop_literal list |
| Cmd_CheckEntailment of symbol list * term |
| Cmd_DeclareConst of symbol * symbol list * sort |
| Cmd_DeclareDataType of symbol * symbol list * constructor_dec list |
| Cmd_DeclareDataTypes of sort_dec list * (symbol list * constructor_dec list) list |
| Cmd_DeclareFun of symbol * symbol list * sort list * sort |
| Cmd_DeclareSort of symbol * string |
| Cmd_DefineFun of symbol * symbol list * sorted_var list * sort * term |
| Cmd_DefineFunRec of symbol * symbol list * sorted_var list * sort * term |
| Cmd_DefineFunsRec of (symbol * symbol list * sorted_var list * sort) list * term list |
| Cmd_DefineSort of symbol * symbol list * sort |
| Cmd_Echo of symbol |
| Cmd_GetAssert |
| Cmd_GetProof |
| Cmd_GetUnsatCore |
| Cmd_GetValue of term list |
| Cmd_GetAssign |
| Cmd_GetOption of keyword |
| Cmd_GetInfo of key_info |
| Cmd_GetModel |
| Cmd_GetUnsatAssumptions |
| Cmd_Reset |
| Cmd_ResetAssert |
| Cmd_SetLogic of symbol |
| Cmd_SetOption of option |
| Cmd_SetInfo of attribute |
| Cmd_Push of string |
| Cmd_Pop of string |
| Cmd_Exit |
| Cmd_Maximize of term |
| Cmd_Minimize of term |
type command = command_aux data
type commands = command list