From 9b80b60bbf8bc7ec0ce8985b66399a179126882d Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 15 Jul 2019 18:52:18 +0200 Subject: 3rdparty --- 3rdparty/alt-ergo/smtlib2_parse.mly | 302 ++++++++++++++++++++++++++++++++++++ 1 file changed, 302 insertions(+) create mode 100644 3rdparty/alt-ergo/smtlib2_parse.mly (limited to '3rdparty/alt-ergo/smtlib2_parse.mly') 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 NUMERAL +%token DECIMAL +%token HEXADECIMAL +%token BINARY +%token STRINGLIT +%token ASCIIWOR +%token KEYWORD +%token SYMBOL + + +%type main +%type an_option +%type attribute +%type attributevalue +%type command +%type commands +%type identifier +%type infoflag +%type qualidentifier +%type sexpr +%type sort +%type sortedvar +%type specconstant +%type symbol +%type term +%type varbinding + +/* %type attributevalsexpr_attributevalue_sexpr5 */ +/* %type commanddeclarefun_command_sort13 */ +/* %type commanddefinefun_command_sortedvar15 */ +/* %type commanddefinesort_command_symbol11 */ +/* %type commandgetvalue_command_term24 */ +/* %type commands_commands_command30 */ +/* %type sexprinparen_sexpr_sexpr41 */ +/* %type sortidsortmulti_sort_sort44 */ +/* %type termexclimationpt_term_attribute64 */ +/* %type termexiststerm_term_sortedvar62 */ +/* %type termforallterm_term_sortedvar60 */ +/* %type termletterm_term_varbinding58 */ +/* %type termqualidterm_term_term56 */ +/* %type 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) } +; -- cgit