From 9b80b60bbf8bc7ec0ce8985b66399a179126882d Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 15 Jul 2019 18:52:18 +0200 Subject: 3rdparty --- src/smtlib2/smtlib2_ast.ml | 253 ----------------------------------- src/smtlib2/smtlib2_ast.mli | 97 -------------- src/smtlib2/smtlib2_lex.mll | 89 ------------- src/smtlib2/smtlib2_parse.mly | 302 ------------------------------------------ src/smtlib2/smtlib2_util.ml | 30 ----- src/smtlib2/smtlib2_util.mli | 26 ---- 6 files changed, 797 deletions(-) delete mode 100644 src/smtlib2/smtlib2_ast.ml delete mode 100644 src/smtlib2/smtlib2_ast.mli delete mode 100644 src/smtlib2/smtlib2_lex.mll delete mode 100644 src/smtlib2/smtlib2_parse.mly delete mode 100644 src/smtlib2/smtlib2_util.ml delete mode 100644 src/smtlib2/smtlib2_util.mli (limited to 'src/smtlib2') 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 *) - 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 diff --git a/src/smtlib2/smtlib2_lex.mll b/src/smtlib2/smtlib2_lex.mll deleted file mode 100644 index 2b965af..0000000 --- a/src/smtlib2/smtlib2_lex.mll +++ /dev/null @@ -1,89 +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 *) -(* *) -(**************************************************************************) - - -{ -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/src/smtlib2/smtlib2_parse.mly b/src/smtlib2/smtlib2_parse.mly deleted file mode 100644 index d618a1a..0000000 --- a/src/smtlib2/smtlib2_parse.mly +++ /dev/null @@ -1,302 +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 */ -/* */ -/**************************************************************************/ - - -%{ - 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) } -; diff --git a/src/smtlib2/smtlib2_util.ml b/src/smtlib2/smtlib2_util.ml deleted file mode 100644 index d503145..0000000 --- a/src/smtlib2/smtlib2_util.ml +++ /dev/null @@ -1,30 +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 *) -(* *) -(**************************************************************************) - - -(* 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/src/smtlib2/smtlib2_util.mli b/src/smtlib2/smtlib2_util.mli deleted file mode 100644 index b4e8916..0000000 --- a/src/smtlib2/smtlib2_util.mli +++ /dev/null @@ -1,26 +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 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 -- cgit