diff options
Diffstat (limited to 'src/smtlib2/smtlib2_ast.mli')
| -rw-r--r-- | src/smtlib2/smtlib2_ast.mli | 97 |
1 files changed, 0 insertions, 97 deletions
diff --git a/src/smtlib2/smtlib2_ast.mli b/src/smtlib2/smtlib2_ast.mli deleted file mode 100644 index 3d3f126..0000000 --- a/src/smtlib2/smtlib2_ast.mli +++ /dev/null @@ -1,97 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq, originally belong to The Alt-ergo theorem prover *) -(* Copyright (C) 2006-2010 *) -(* *) -(* Sylvain Conchon *) -(* Evelyne Contejean *) -(* Stephane Lescuyer *) -(* Mohamed Iguernelala *) -(* Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -type loc = Lexing.position * Lexing.position -type specconstant = - SpecConstsDec of loc * string - | SpecConstNum of loc * string - | SpecConstString of loc * string - | SpecConstsHex of loc * string - | SpecConstsBinary of loc * string -type symbol = Symbol of loc * string | SymbolWithOr of loc * string -type sexpr = - SexprSpecConst of loc * specconstant - | SexprSymbol of loc * symbol - | SexprKeyword of loc * string - | SexprInParen of loc * (loc * sexpr list) -type attributevalue = - AttributeValSpecConst of loc * specconstant - | AttributeValSymbol of loc * symbol - | AttributeValSexpr of loc * (loc * sexpr list) -type attribute = - AttributeKeyword of loc * string - | AttributeKeywordValue of loc * string * attributevalue -type an_option = AnOptionAttribute of loc * attribute -type infoflag = InfoFlagKeyword of loc * string -type identifier = - IdSymbol of loc * symbol - | IdUnderscoreSymNum of loc * symbol * (loc * string list) -type sort = - SortIdentifier of loc * identifier - | SortIdSortMulti of loc * identifier * (loc * sort list) -type qualidentifier = - QualIdentifierId of loc * identifier - | QualIdentifierAs of loc * identifier * sort -type sortedvar = SortedVarSymSort of loc * symbol * sort -type varbinding = VarBindingSymTerm of loc * symbol * term -and term = - TermSpecConst of loc * specconstant - | TermQualIdentifier of loc * qualidentifier - | TermQualIdTerm of loc * qualidentifier * (loc * term list) - | TermLetTerm of loc * (loc * varbinding list) * term - | TermForAllTerm of loc * (loc * sortedvar list) * term - | TermExistsTerm of loc * (loc * sortedvar list) * term - | TermExclimationPt of loc * term * (loc * attribute list) -type command = - CSetLogic of loc * symbol - | CSetOption of loc * an_option - | CSetInfo of loc * attribute - | CDeclareSort of loc * symbol * string - | CDefineSort of loc * symbol * (loc * symbol list) * sort - | CDeclareFun of loc * symbol * (loc * sort list) * sort - | CDefineFun of loc * symbol * (loc * sortedvar list) * sort * term - | CPush of loc * string - | CPop of loc * string - | CAssert of loc * term - | CCheckSat of loc - | CGetAssert of loc - | CGetProof of loc - | CGetUnsatCore of loc - | CGetValue of loc * (loc * term list) - | CGetAssign of loc - | CGetOption of loc * string - | CGetInfo of loc * infoflag - | CExit of loc -type commands = Commands of loc * (loc * command list) -val loc_an_option : an_option -> loc -val loc_attribute : attribute -> loc -val loc_attributevalue : attributevalue -> loc -val loc_command : command -> loc -val loc_commands : commands -> loc -val loc_identifier : identifier -> loc -val loc_infoflag : infoflag -> loc -val loc_qualidentifier : qualidentifier -> loc -val loc_sexpr : sexpr -> loc -val loc_sort : sort -> loc -val loc_sortedvar : sortedvar -> loc -val loc_specconstant : specconstant -> loc -val loc_symbol : symbol -> loc -val loc_term : term -> loc -val loc_varbinding : varbinding -> loc -val loc_couple : 'a * 'b -> 'a -val loc_of : commands -> loc |