Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
smtlib_syntax.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198
(******************************************************************************) (* *) (* An SMT-LIB 2 for the Alt-Ergo Theorem Prover *) (* *) (******************************************************************************) type 'a data = { p : (Lexing.position * Lexing.position) option ; c : 'a ; ty : Smtlib_ty.ty; mutable is_quantif : bool} type constant = | Const_Dec of string | Const_Num of string | Const_Str of string | Const_Hex of string | Const_Bin of string 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_aux = | Diagnooutputchan | Globaldeclarations | Interactive | Printsucces | Produceassertions | Produceassignement | Producemodels | Produceproofs | Produceunsatassumptions | Produceunsatcores | Randomseed | Regularoutputchan | Verbosity | Ressourcelimit and key_option = key_option_aux data and option_aux = | Option_key of key_option * index | Option_attribute of attribute 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_aux = | Pattern of term list | Named of symbol and key_term = key_term_aux data (* attributes *) and sexpr_aux = | SexprSpecConst of constant | SexprSymbol of symbol | SexprKeyword of keyword | SexprInParen of sexpr list and sexpr = sexpr_aux data and attribute_value_aux = | AttributeValSpecConst of constant | AttributeValSymbol of symbol | AttributeValSexpr of sexpr list | NoAttributeValue and attribute_value = attribute_value_aux data and attribute_aux = | AttributeKey of key_info | AttributeKeyValue of key_info * attribute_value and attribute = attribute_aux data (* index *) and index_aux = | IndexSymbol of symbol | IndexNumeral of string and index = index_aux data (* identifiers *) and identifier_aux = | IdSymbol of symbol | IdUnderscoreSymNum of symbol * index list and identifier = identifier_aux data and prop_literal_aux = | PropLit of symbol | PropLitNot of symbol and prop_literal = prop_literal_aux data (* sorts and polymorphism *) and sort_aux = | SortIdentifier of identifier | SortIdMulti of identifier * sort list and sort = sort_aux data (* typed variable *) and sorted_var = symbol * sort (* qualidentifiers *) and qualidentifier_aux = | QualIdentifierId of identifier | QualIdentifierAs of identifier * sort and qualidentifier = qualidentifier_aux data (* valued variable *) and varbinding = symbol * term (* pattern *) and pattern_aux = | MatchPattern of (symbol * symbol list) | MatchUnderscore and pattern = pattern_aux data (* terms *) 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 term = term_aux data (* datatypes *) and sort_dec = symbol * string and selector_dec = symbol * sort and constructor_dec = symbol * selector_dec list (* script commands *) type command_aux = | Cmd_Assert of (symbol list * term) | Cmd_CheckSat | 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 type command = command_aux data type commands = command list (*******************************************************************)