aboutsummaryrefslogtreecommitdiffstats
path: root/src/smtlib2
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2019-07-15 18:52:18 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2019-07-15 18:52:18 +0200
commit9b80b60bbf8bc7ec0ce8985b66399a179126882d (patch)
tree5e5fcf64b916317425226edf2456dfed5ffd8c5e /src/smtlib2
parentc2f860da64b15ef094d2905330e74658934f9cc2 (diff)
downloadsmtcoq-9b80b60bbf8bc7ec0ce8985b66399a179126882d.tar.gz
smtcoq-9b80b60bbf8bc7ec0ce8985b66399a179126882d.zip
3rdparty
Diffstat (limited to 'src/smtlib2')
-rw-r--r--src/smtlib2/smtlib2_ast.ml253
-rw-r--r--src/smtlib2/smtlib2_ast.mli97
-rw-r--r--src/smtlib2/smtlib2_lex.mll89
-rw-r--r--src/smtlib2/smtlib2_parse.mly302
-rw-r--r--src/smtlib2/smtlib2_util.ml30
-rw-r--r--src/smtlib2/smtlib2_util.mli26
6 files changed, 0 insertions, 797 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 *)
-
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 <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/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