3rdparty

1 files changed, 253 insertions, 0 deletions

diff --git a/3rdparty/alt-ergo/smtlib2_ast.ml b/3rdparty/alt-ergo/smtlib2_ast.ml
new file mode 100644
index 0000000..65dc3e3
--- /dev/null
+++ b/3rdparty/alt-ergo/smtlib2_ast.ml
@@ -0,0 +1,253 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     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)
+
+
+(* loc stands for pos (position) and extradata *)
+
+let loc_an_option = function
+  | AnOptionAttribute(d,_) -> d
+
+let loc_attribute = function
+  | AttributeKeyword(d,_) -> d
+  | AttributeKeywordValue(d,_,_) -> d
+
+let loc_attributevalue = function
+  | AttributeValSpecConst(d,_) -> d
+  | AttributeValSymbol(d,_) -> d
+  | AttributeValSexpr(d,_) -> d
+
+let loc_command = function
+  | CSetLogic(d,_) -> d
+  | CSetOption(d,_) -> d
+  | CSetInfo(d,_) -> d
+  | CDeclareSort(d,_,_) -> d
+  | CDefineSort(d,_,_,_) -> d
+  | CDeclareFun(d,_,_,_) -> d
+  | CDefineFun(d,_,_,_,_) -> d
+  | CPush(d,_) -> d
+  | CPop(d,_) -> d
+  | CAssert(d,_) -> d
+  | CCheckSat(d) -> d
+  | CGetAssert(d) -> d
+  | CGetProof(d) -> d
+  | CGetUnsatCore(d) -> d
+  | CGetValue(d,_) -> d
+  | CGetAssign(d) -> d
+  | CGetOption(d,_) -> d
+  | CGetInfo(d,_) -> d
+  | CExit(d) -> d
+
+let loc_commands = function
+  | Commands(d,_) -> d
+
+let loc_identifier = function
+  | IdSymbol(d,_) -> d
+  | IdUnderscoreSymNum(d,_,_) -> d
+
+let loc_infoflag = function
+  | InfoFlagKeyword(d,_) -> d
+
+let loc_qualidentifier = function
+  | QualIdentifierId(d,_) -> d
+  | QualIdentifierAs(d,_,_) -> d
+
+let loc_sexpr = function
+  | SexprSpecConst(d,_) -> d
+  | SexprSymbol(d,_) -> d
+  | SexprKeyword(d,_) -> d
+  | SexprInParen(d,_) -> d
+
+let loc_sort = function
+  | SortIdentifier(d,_) -> d
+  | SortIdSortMulti(d,_,_) -> d
+
+let loc_sortedvar = function
+  | SortedVarSymSort(d,_,_) -> d
+
+let loc_specconstant = function
+  | SpecConstsDec(d,_) -> d
+  | SpecConstNum(d,_) -> d
+  | SpecConstString(d,_) -> d
+  | SpecConstsHex(d,_) -> d
+  | SpecConstsBinary(d,_) -> d
+
+let loc_symbol = function
+  | Symbol(d,_) -> d
+  | SymbolWithOr(d,_) -> d
+
+let loc_term = function
+  | TermSpecConst(d,_) -> d
+  | TermQualIdentifier(d,_) -> d
+  | TermQualIdTerm(d,_,_) -> d
+  | TermLetTerm(d,_,_) -> d
+  | TermForAllTerm(d,_,_) -> d
+  | TermExistsTerm(d,_,_) -> d
+  | TermExclimationPt(d,_,_) -> d
+
+let loc_varbinding = function
+  | VarBindingSymTerm(d,_,_) -> d
+
+let loc_couple = fst
+
+let loc_of e = loc_commands e;;
+
+
+
+(* let print_specconstant fmt = function
+ *   | SpecConstsDec (_, s)
+ *   | SpecConstNum (_, s)
+ *   | SpecConstString (_, s)
+ *   | SpecConstsHex (_, s)
+ *   | SpecConstsBinary (_, s) -> Format.pp_print_string fmt s *)
+
+
+(* let print_symbol fmt = function
+ *   | Symbol (_, s)
+ *   | SymbolWithOr (_, s) -> Format.pp_print_string fmt s *)
+
+
+(* let print_identifier fmt = function
+ *   | IdSymbol (_, s) -> print_symbol fmt s
+ *   | IdUnderscoreSymNum (_, s, (_, l)) ->
+ *     Format.fprintf fmt "(_ %a" print_symbol s;
+ *     List.iter (Format.fprintf fmt " %s") l;
+ *     Format.fprintf fmt ")" *)
+
+(* let rec print_sort fmt = function
+ *   | SortIdentifier (_, i) -> print_identifier fmt i
+ *   | SortIdSortMulti (_, i, (_, ls)) ->
+ *     Format.fprintf fmt "(%a" print_identifier i;
+ *     List.iter (Format.fprintf fmt " %a" print_sort) ls;
+ *     Format.fprintf fmt ")" *)
+
+(* let print_qualidentifier fmt = function
+ *   | QualIdentifierId (_, i) -> print_identifier fmt i
+ *   | QualIdentifierAs (_, i, s) ->
+ *     Format.fprintf fmt "(%a as %a)"
+ *       print_identifier i print_sort s *)
+
+(* let print_sortedvar fmt = function
+ *   | SortedVarSymSort (_, v, s) ->
+ *     Format.fprintf fmt "(%a %a)" print_symbol v print_sort s *)
+
+(* let rec print_varbinding fmt = function
+ *   | VarBindingSymTerm (_, s, t) ->
+ *     Format.fprintf fmt "(%a %a)" print_symbol s print_term t *)
+
+(* and print_term fmt = function
+ *   | TermSpecConst (_, c) -> print_specconstant fmt c
+ *   | TermQualIdentifier (_, i) -> print_qualidentifier fmt i
+ *   | TermQualIdTerm (_, i, (_, tl)) ->
+ *     Format.fprintf fmt "(%a" print_qualidentifier i;
+ *     List.iter (Format.fprintf fmt " %a" print_term) tl;
+ *     Format.fprintf fmt ")"
+ *   | TermLetTerm (_, (_, vb), t) ->
+ *     Format.fprintf fmt "(let (";
+ *     List.iter (Format.fprintf fmt " %a" print_varbinding) vb;
+ *     Format.fprintf fmt ") %a)" print_term t
+ *   | TermForAllTerm (_, (_, sv), t) ->
+ *     Format.fprintf fmt "(forall (";
+ *     List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
+ *     Format.fprintf fmt ") %a)" print_term t
+ *   | TermExistsTerm (_, (_, sv), t) ->
+ *     Format.fprintf fmt "(exists (";
+ *     List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
+ *     Format.fprintf fmt ") %a)" print_term t
+ *   | TermExclimationPt (_, t, _) -> print_term fmt t *)
+