aboutsummaryrefslogtreecommitdiffstats
path: root/src/smtlib2/smtlib2_ast.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/smtlib2/smtlib2_ast.ml')
-rw-r--r--src/smtlib2/smtlib2_ast.ml253
1 files changed, 0 insertions, 253 deletions
diff --git a/src/smtlib2/smtlib2_ast.ml b/src/smtlib2/smtlib2_ast.ml
deleted file mode 100644
index 65dc3e3..0000000
--- a/src/smtlib2/smtlib2_ast.ml
+++ /dev/null
@@ -1,253 +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)
-
-
-(* 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 *)
-
generated by cgit (git 2.34.1) at 2024-06-26 16:17:06 +0000