diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2019-07-15 18:52:18 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2019-07-15 18:52:18 +0200 |
commit | 9b80b60bbf8bc7ec0ce8985b66399a179126882d (patch) | |
tree | 5e5fcf64b916317425226edf2456dfed5ffd8c5e /3rdparty | |
parent | c2f860da64b15ef094d2905330e74658934f9cc2 (diff) | |
download | smtcoq-9b80b60bbf8bc7ec0ce8985b66399a179126882d.tar.gz smtcoq-9b80b60bbf8bc7ec0ce8985b66399a179126882d.zip |
3rdparty
Diffstat (limited to '3rdparty')
-rw-r--r-- | 3rdparty/alt-ergo/smtlib2_ast.ml | 253 | ||||
-rw-r--r-- | 3rdparty/alt-ergo/smtlib2_ast.mli | 97 | ||||
-rw-r--r-- | 3rdparty/alt-ergo/smtlib2_lex.mll | 89 | ||||
-rw-r--r-- | 3rdparty/alt-ergo/smtlib2_parse.mly | 302 | ||||
-rw-r--r-- | 3rdparty/alt-ergo/smtlib2_util.ml | 30 | ||||
-rw-r--r-- | 3rdparty/alt-ergo/smtlib2_util.mli | 26 |
6 files changed, 797 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 *) + diff --git a/3rdparty/alt-ergo/smtlib2_ast.mli b/3rdparty/alt-ergo/smtlib2_ast.mli new file mode 100644 index 0000000..3d3f126 --- /dev/null +++ b/3rdparty/alt-ergo/smtlib2_ast.mli @@ -0,0 +1,97 @@ +(**************************************************************************) +(* *) +(* 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 diff --git a/3rdparty/alt-ergo/smtlib2_lex.mll b/3rdparty/alt-ergo/smtlib2_lex.mll new file mode 100644 index 0000000..2b965af --- /dev/null +++ b/3rdparty/alt-ergo/smtlib2_lex.mll @@ -0,0 +1,89 @@ +(**************************************************************************) +(* *) +(* 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 *) +(* *) +(**************************************************************************) + + +{ +open Lexing +open Smtlib2_parse + + +let newline lexbuf = + let pos = lexbuf.lex_curr_p in + lexbuf.lex_curr_p <- + { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum; + pos_cnum=0 } + +} + +rule token = parse +| ['\t' ' ' ]+ + { token lexbuf } +| ';' (_ # '\n')* + { token lexbuf } +| ['\n']+ as str + { newline lexbuf; + Smtlib2_util.line := (!Smtlib2_util.line + (String.length str)); + token lexbuf } +| "_" { UNDERSCORE } +| "(" { LPAREN } +| ")" { RPAREN } +| "as" { AS } +| "let" { LET } +| "forall" { FORALL } +| "exists" { EXISTS } +| "!" { EXCLIMATIONPT } +| "set-logic" { SETLOGIC } +| "set-option" { SETOPTION } +| "set-info" { SETINFO } +| "declare-sort" { DECLARESORT } +| "define-sort" { DEFINESORT } +| "declare-fun" { DECLAREFUN } +| "define-fun" { DEFINEFUN } +| "push" { PUSH } +| "pop" { POP } +| "assert" { ASSERT } +| "check-sat" { CHECKSAT } +| "get-assertions" { GETASSERT } +| "get-proof" { GETPROOF } +| "get-unsat-core" { GETUNSATCORE } +| "get-value" { GETVALUE } +| "get-assignment" { GETASSIGN } +| "get-option" { GETOPTION } +| "get-info" { GETINFO } +| "exit" { EXIT } +| '#' 'x' ['0'-'9' 'A'-'F' 'a'-'f']+ as str + { HEXADECIMAL(str) } +| '#' 'b' ['0'-'1']+ as str + { BINARY(str) } +| '|' ([ '!'-'~' ' ' '\n' '\t' '\r'] # ['\\' '|'])* '|' as str + { ASCIIWOR(str) } +| ':' ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=' '%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']+ as str + { KEYWORD(str) } +| ['a'-'z' 'A'-'Z' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@'] ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']* as str + { SYMBOL(str) } +| '"' (([ '!'-'~' ' ' '\n' '\t' '\r' ] # ['\\' '"']) | ('\\' ['!'-'~' ' ' '\n' '\t' '\r'] ))* '"' as str + { STRINGLIT(str) } +| ( '0' | ['1'-'9'] ['0'-'9']* ) as str + { NUMERAL(str) } +| ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str + { DECIMAL(str) } +| eof + { EOF } +| _ + {failwith( + (Lexing.lexeme lexbuf) ^ + ": lexing error on line "^(string_of_int !Smtlib2_util.line))}{} diff --git a/3rdparty/alt-ergo/smtlib2_parse.mly b/3rdparty/alt-ergo/smtlib2_parse.mly new file mode 100644 index 0000000..d618a1a --- /dev/null +++ b/3rdparty/alt-ergo/smtlib2_parse.mly @@ -0,0 +1,302 @@ +/**************************************************************************/ +/* */ +/* 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 */ +/* */ +/**************************************************************************/ + + +%{ + open Smtlib2_ast + + let loc () = symbol_start_pos (), symbol_end_pos () + +%} + +%start main +%start term +%start sort + +/* general */ +%token EXCLIMATIONPT +%token UNDERSCORE +%token AS +%token EXISTS +%token FORALL +%token LET + +/* commands */ +%token SETLOGIC +%token SETOPTION +%token SETINFO +%token DECLARESORT +%token DEFINESORT +%token DECLAREFUN +%token DEFINEFUN +%token PUSH +%token POP +%token ASSERT +%token CHECKSAT +%token GETASSERT +%token GETPROOF +%token GETUNSATCORE +%token GETVALUE +%token GETASSIGN +%token GETOPTION +%token GETINFO +%token EXIT + +/* Other tokens */ +%token LPAREN +%token RPAREN +%token EOF + +%token <string> NUMERAL +%token <string> DECIMAL +%token <string> HEXADECIMAL +%token <string> BINARY +%token <string> STRINGLIT +%token <string> ASCIIWOR +%token <string> KEYWORD +%token <string> SYMBOL + + +%type <Smtlib2_ast.commands option> main +%type <Smtlib2_ast.an_option> an_option +%type <Smtlib2_ast.attribute> attribute +%type <Smtlib2_ast.attributevalue> attributevalue +%type <Smtlib2_ast.command> command +%type <Smtlib2_ast.commands> commands +%type <Smtlib2_ast.identifier> identifier +%type <Smtlib2_ast.infoflag> infoflag +%type <Smtlib2_ast.qualidentifier> qualidentifier +%type <Smtlib2_ast.sexpr> sexpr +%type <Smtlib2_ast.sort> sort +%type <Smtlib2_ast.sortedvar> sortedvar +%type <Smtlib2_ast.specconstant> specconstant +%type <Smtlib2_ast.symbol> symbol +%type <Smtlib2_ast.term> term +%type <Smtlib2_ast.varbinding> varbinding + +/* %type <Smtlib2_ast.attributevalsexpr_attributevalue_sexpr5> attributevalsexpr_attributevalue_sexpr5 */ +/* %type <Smtlib2_ast.commanddeclarefun_command_sort13> commanddeclarefun_command_sort13 */ +/* %type <Smtlib2_ast.commanddefinefun_command_sortedvar15> commanddefinefun_command_sortedvar15 */ +/* %type <Smtlib2_ast.commanddefinesort_command_symbol11> commanddefinesort_command_symbol11 */ +/* %type <Smtlib2_ast.commandgetvalue_command_term24> commandgetvalue_command_term24 */ +/* %type <Smtlib2_ast.commands_commands_command30> commands_commands_command30 */ +/* %type <Smtlib2_ast.sexprinparen_sexpr_sexpr41> sexprinparen_sexpr_sexpr41 */ +/* %type <Smtlib2_ast.sortidsortmulti_sort_sort44> sortidsortmulti_sort_sort44 */ +/* %type <Smtlib2_ast.termexclimationpt_term_attribute64> termexclimationpt_term_attribute64 */ +/* %type <Smtlib2_ast.termexiststerm_term_sortedvar62> termexiststerm_term_sortedvar62 */ +/* %type <Smtlib2_ast.termforallterm_term_sortedvar60> termforallterm_term_sortedvar60 */ +/* %type <Smtlib2_ast.termletterm_term_varbinding58> termletterm_term_varbinding58 */ +/* %type <Smtlib2_ast.termqualidterm_term_term56> termqualidterm_term_term56 */ +/* %type <Smtlib2_ast.idunderscoresymnum_identifier_numeral33> idunderscoresymnum_identifier_numeral33 */ +%% + +main: +| commands { Some($1) } +| EOF { None } +; + +an_option: +| attribute { AnOptionAttribute(loc_attribute $1, $1) } +; + +attribute: +| KEYWORD { AttributeKeyword(loc (), $1) } +| KEYWORD attributevalue { AttributeKeywordValue(loc (), $1, $2) } +; + +sexpr_list: +/*sexprinparen_sexpr_sexpr41:*/ +/*attributevalsexpr_attributevalue_sexpr5:*/ +| { (loc (), []) } +| sexpr sexpr_list { let (_, l1) = $2 in (loc_sexpr $1, ($1)::(l1)) } +; + +attributevalue: +| specconstant { AttributeValSpecConst(loc_specconstant $1, $1) } +| symbol { AttributeValSymbol(loc_symbol $1, $1) } +| LPAREN sexpr_list RPAREN { AttributeValSexpr(loc (), $2) } +; + +symbol_list: /*commanddefinesort_command_symbol11:*/ +| { (loc (), []) } +| symbol symbol_list { let (_, l1) = $2 in (loc_symbol $1, ($1)::(l1)) } +; + +sort_list0: /*commanddeclarefun_command_sort13:*/ +| { (loc (), []) } +| sort sort_list0 { let (_, l1) = $2 in (loc_sort $1, ($1)::(l1)) } +; + +sortedvar_list: /*commanddefinefun_command_sortedvar15:*/ +| { (loc (), []) } +| sortedvar sortedvar_list + { let (_, l1) = $2 in (loc_sortedvar $1, ($1)::(l1)) } +; + +command: +| LPAREN SETLOGIC symbol RPAREN + { CSetLogic(loc (), $3) } +| LPAREN SETOPTION an_option RPAREN + { CSetOption(loc (), $3) } +| LPAREN SETINFO attribute RPAREN + { CSetInfo(loc (), $3) } +| LPAREN DECLARESORT symbol NUMERAL RPAREN + { CDeclareSort(loc (), $3, $4) } +| LPAREN DEFINESORT symbol LPAREN symbol_list RPAREN sort RPAREN + { CDefineSort(loc (), $3, $5, $7) } +| LPAREN DECLAREFUN symbol LPAREN sort_list0 RPAREN sort RPAREN + { CDeclareFun(loc (), $3, $5, $7) } +| LPAREN DEFINEFUN symbol LPAREN sortedvar_list RPAREN sort term RPAREN + { CDefineFun(loc (), $3, $5, $7, $8) } +| LPAREN PUSH NUMERAL RPAREN + { CPush(loc (), $3) } +| LPAREN POP NUMERAL RPAREN + { CPop(loc (), $3) } +| LPAREN ASSERT term RPAREN + { CAssert(loc (), $3) } +| LPAREN CHECKSAT RPAREN + { CCheckSat(loc ()) } +| LPAREN GETASSERT RPAREN + { CGetAssert(loc ()) } +| LPAREN GETPROOF RPAREN + { CGetProof(loc ()) } +| LPAREN GETUNSATCORE RPAREN + { CGetUnsatCore(loc ()) } +| LPAREN GETVALUE LPAREN term_list1 RPAREN RPAREN + { CGetValue(loc (), $4) } +| LPAREN GETASSIGN RPAREN + { CGetAssign(loc ()) } +| LPAREN GETOPTION KEYWORD RPAREN + { CGetOption(loc (), $3) } +| LPAREN GETINFO infoflag RPAREN + { CGetInfo(loc (), $3) } +| LPAREN EXIT RPAREN + { CExit(loc ()) } +; + + +command_list: /*commands_commands_command30:*/ +| { (loc (), []) } +| command command_list { let (_, l1) = $2 in (loc_command $1, ($1)::(l1)) } +; + +commands: +| command_list { Commands(loc_couple $1, $1) } +; + +numeral_list: /*idunderscoresymnum_identifier_numeral33:*/ +| NUMERAL { (loc (), ($1)::[]) } +| NUMERAL numeral_list { let (_, l1) = $2 in (loc (), ($1)::(l1)) } +; + +identifier: +| symbol { IdSymbol(loc_symbol $1, $1) } +| LPAREN UNDERSCORE symbol numeral_list RPAREN + { IdUnderscoreSymNum(loc (), $3, $4) } +; + +infoflag: +| KEYWORD { InfoFlagKeyword(loc (), $1) } +; + +qualidentifier: +| identifier { QualIdentifierId(loc_identifier $1, $1) } +| LPAREN AS identifier sort RPAREN { QualIdentifierAs(loc (), $3, $4) } +; + +sexpr: +| specconstant { SexprSpecConst(loc_specconstant $1, $1) } +| symbol { SexprSymbol(loc_symbol $1, $1) } +| KEYWORD { SexprKeyword(loc (), $1) } +| LPAREN sexpr_list RPAREN { SexprInParen(loc (), $2) } +; + + +sort_list1: /*sortidsortmulti_sort_sort44:*/ +| sort { (loc_sort $1, ($1)::[]) } +| sort sort_list1 { let (_, l1) = $2 in (loc_sort $1, ($1)::(l1)) } +; + +sort: +| identifier { SortIdentifier(loc_identifier $1, $1) } +| LPAREN identifier sort_list1 RPAREN { SortIdSortMulti(loc (), $2, $3) } +; + +sortedvar: +| LPAREN symbol sort RPAREN { SortedVarSymSort(loc (), $2, $3) } +; + +specconstant: +| DECIMAL { SpecConstsDec(loc (), $1) } +| NUMERAL { SpecConstNum(loc (), $1) } +| STRINGLIT { SpecConstString(loc (), $1) } +| HEXADECIMAL { SpecConstsHex(loc (), $1) } +| BINARY { SpecConstsBinary(loc (), $1) } +; + +symbol: +| SYMBOL { Symbol(loc (), $1) } +| ASCIIWOR { SymbolWithOr(loc (), $1) } +; + +term_list1: +/*termqualidterm_term_term56:*/ +/*commandgetvalue_command_term24:*/ +| term { (loc_term $1, ($1)::[]) } +| term term_list1 { let (_, l1) = $2 in (loc_term $1, ($1)::(l1)) } +; + +varbinding_list1: /*termletterm_term_varbinding58:*/ +| varbinding { (loc_varbinding $1, ($1)::[]) } +| varbinding varbinding_list1 + { let (_, l1) = $2 in (loc_varbinding $1, ($1)::(l1)) } +; + +sortedvar_list1: +/*termforallterm_term_sortedvar60:*/ +/*termexiststerm_term_sortedvar62:*/ +| sortedvar { (loc_sortedvar $1, ($1)::[]) } +| sortedvar sortedvar_list1 + { let (_, l1) = $2 in (loc_sortedvar $1, ($1)::(l1)) } +; + +attribute_list1: /*termexclimationpt_term_attribute64:*/ +| attribute { (loc_attribute $1, ($1)::[]) } +| attribute attribute_list1 + { let (_, l1) = $2 in (loc_attribute $1, ($1)::(l1)) } +; + +term: +| specconstant + { TermSpecConst(loc_specconstant $1, $1) } +| qualidentifier + { TermQualIdentifier(loc_qualidentifier $1, $1) } +| LPAREN qualidentifier term_list1 RPAREN + { TermQualIdTerm(loc (), $2, $3) } +| LPAREN LET LPAREN varbinding_list1 RPAREN term RPAREN + { TermLetTerm(loc (), $4, $6) } +| LPAREN FORALL LPAREN sortedvar_list1 RPAREN term RPAREN + { TermForAllTerm(loc (), $4, $6) } +| LPAREN EXISTS LPAREN sortedvar_list1 RPAREN term RPAREN + { TermExistsTerm(loc (), $4, $6) } +| LPAREN EXCLIMATIONPT term attribute_list1 RPAREN + { TermExclimationPt(loc (), $3, $4) } +; + +varbinding: +| LPAREN symbol term RPAREN { VarBindingSymTerm(loc (), $2, $3) } +; diff --git a/3rdparty/alt-ergo/smtlib2_util.ml b/3rdparty/alt-ergo/smtlib2_util.ml new file mode 100644 index 0000000..d503145 --- /dev/null +++ b/3rdparty/alt-ergo/smtlib2_util.ml @@ -0,0 +1,30 @@ +(**************************************************************************) +(* *) +(* 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 *) +(* *) +(**************************************************************************) + + +(* auto-generated by gt *) + +(* no extra data from grammar file. *) +type extradata = unit;; +let initial_data() = ();; + +let file = ref "stdin";; +let line = ref 1;; +type pos = int;; +let string_of_pos p = "line "^(string_of_int p);; +let cur_pd() = (!line, initial_data());; (* "pd": pos + extradata *) +type pd = pos * extradata;; diff --git a/3rdparty/alt-ergo/smtlib2_util.mli b/3rdparty/alt-ergo/smtlib2_util.mli new file mode 100644 index 0000000..b4e8916 --- /dev/null +++ b/3rdparty/alt-ergo/smtlib2_util.mli @@ -0,0 +1,26 @@ +(**************************************************************************) +(* *) +(* 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 extradata = unit +val initial_data : unit -> unit +val file : string ref +val line : int ref +type pos = int +val string_of_pos : int -> string +val cur_pd : unit -> int * unit +type pd = pos * extradata |