diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-02 13:38:21 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-02 13:38:21 +0100 |
commit | 607c758e0220d8ba91eaf0e9e96b5ea71c5c6fd2 (patch) | |
tree | 9333c12809138a6bbaeeb137e81a4fc6c4d34ef9 /src/verit | |
parent | e3ff85dccf62b497cd017d2b55e08e7f49ebd80f (diff) | |
download | smtcoq-607c758e0220d8ba91eaf0e9e96b5ea71c5c6fd2.tar.gz smtcoq-607c758e0220d8ba91eaf0e9e96b5ea71c5c6fd2.zip |
Separate verit input (smtlib2) from output
Diffstat (limited to 'src/verit')
-rw-r--r-- | src/verit/smtlib2_ast.ml | 189 | ||||
-rw-r--r-- | src/verit/smtlib2_genConstr.ml | 226 | ||||
-rw-r--r-- | src/verit/smtlib2_lex.mll | 88 | ||||
-rw-r--r-- | src/verit/smtlib2_parse.mly | 299 | ||||
-rw-r--r-- | src/verit/smtlib2_util.ml | 29 |
5 files changed, 0 insertions, 831 deletions
diff --git a/src/verit/smtlib2_ast.ml b/src/verit/smtlib2_ast.ml deleted file mode 100644 index cce4625..0000000 --- a/src/verit/smtlib2_ast.ml +++ /dev/null @@ -1,189 +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_util - -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;; diff --git a/src/verit/smtlib2_genConstr.ml b/src/verit/smtlib2_genConstr.ml deleted file mode 100644 index f11d650..0000000 --- a/src/verit/smtlib2_genConstr.ml +++ /dev/null @@ -1,226 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2015 *) -(* *) -(* Michaël Armand *) -(* Benjamin Grégoire *) -(* Chantal Keller *) -(* *) -(* Inria - École Polytechnique - MSR-Inria Joint Lab *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - -open Smtlib2_ast -open SmtAtom -open SmtForm -open SmtMisc -open CoqTerms - - -(* For debugging *) - -let pp_symbol s = - let pp_position p = "{pos_fname = "^p.Lexing.pos_fname^"; pos_lnum = "^(string_of_int p.Lexing.pos_lnum)^"; pos_bol = "^(string_of_int p.Lexing.pos_bol)^"; pos_cnum = "^(string_of_int p.Lexing.pos_cnum)^"}" in - - let pp_loc (p1,p2) = "("^(pp_position p1)^", "^(pp_position p2)^")" in - - match s with - | Symbol (l,s) -> "Symbol ("^(pp_loc l)^", "^s^")" - | SymbolWithOr (l,s) -> "SymbolWithOr ("^(pp_loc l)^", "^s^")" - - -(* Main functions *) - -let string_of_symbol = function | Symbol (_,s) | SymbolWithOr (_,s) -> s - - -let identifier_of_qualidentifier = function - | QualIdentifierId (_,id) | QualIdentifierAs (_,id,_) -> id - - -let string_type s = match s with - | "Bool" -> Tbool - | "Int" -> TZ - | _ -> VeritSyntax.get_btype s - - -let sort_of_string s = (string_type s, []) - - -let sort_of_symbol s = sort_of_string (string_of_symbol s) - - -let string_of_identifier = function - | IdSymbol (_,s) -> (string_of_symbol s) - | IdUnderscoreSymNum (_,s,(_,l)) -> - List.fold_left (fun c c' -> c^"_"^c') (string_of_symbol s) l - - -let string_of_qualidentifier id = string_of_identifier (identifier_of_qualidentifier id) - - -let rec sort_of_sort = function - | SortIdentifier (_,id) -> sort_of_string (string_of_identifier id) - | SortIdSortMulti (_,id,(_,l)) -> - (string_type (string_of_identifier id), List.map sort_of_sort l) - - -let declare_sort rt sym = - let s = string_of_symbol sym in - let cons_t = declare_new_type (Names.id_of_string ("Smt_sort_"^s)) in - let eq_t = declare_new_variable (Names.id_of_string ("eq_"^s)) (Term.mkArrow cons_t (Term.mkArrow cons_t (Lazy.force cbool))) in - let x = mkName "x" in - let y = mkName "y" in - let rx = Term.mkRel 2 in - let ry = Term.mkRel 1 in - let eq_refl = Term.mkProd (x,cons_t,Term.mkProd (y,cons_t,mklApp creflect [|mklApp ceq [|cons_t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in - let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl_"^s)) eq_refl in - let ce = mklApp cTyp_eqb [|cons_t;eq_t;eq_refl_v|] in - let res = Btype.declare rt cons_t ce in - VeritSyntax.add_btype s res; - res - - -let declare_fun rt ro sym arg cod = - let s = string_of_symbol sym in - let tyl = List.map sort_of_sort arg in - let ty = sort_of_sort cod in - - let coqTy = List.fold_right (fun typ c -> Term.mkArrow (Btype.interp_to_coq rt (fst typ)) c) tyl (Btype.interp_to_coq rt (fst ty)) in - let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in - - let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) in - VeritSyntax.add_fun s op; - op - - -let make_root_specconstant ra = function - | SpecConstsDec _ -> failwith "Smtlib2_genConstr.make_root_specconstant: decimals not implemented yet" - | SpecConstNum (_,s) -> - (try - let i = int_of_string s in - Atom.hatom_Z_of_int ra i - with - | Failure _ -> - let i = Big_int.big_int_of_string s in - Atom.hatom_Z_of_bigint ra i) - | SpecConstString _ -> failwith "Smtlib2_genConstr.make_root_specconstant: strings not implemented yet" - | SpecConstsHex _ -> failwith "Smtlib2_genConstr.make_root_specconstant: hexadecimals not implemented yet" - | SpecConstsBinary _ -> failwith "Smtlib2_genConstr.make_root_specconstant: binaries not implemented yet" - - -type atom_form = | Atom of SmtAtom.Atom.t | Form of SmtAtom.Form.t - - -let make_root ra rf t = - - let hlets = Hashtbl.create 17 in - - let rec make_root_term = function - | TermSpecConst (_,c) -> Atom (make_root_specconstant ra c) - | TermQualIdentifier (_,id) -> - let v = string_of_qualidentifier id in - (try Hashtbl.find hlets v with - | Not_found -> - make_root_app v []) - | TermQualIdTerm (_,id,(_,l)) -> - let v = string_of_qualidentifier id in - make_root_app v l - | TermLetTerm (_,(_,l),t) -> - List.iter (fun (VarBindingSymTerm (_, sym, u)) -> - let u' = make_root_term u in - let s' = string_of_symbol sym in - Hashtbl.add hlets s' u') l; - make_root_term t - | TermForAllTerm _ -> failwith "Smtlib2_genConstr.make_root_term: ForAll not implemented yet" - | TermExistsTerm _ -> failwith "Smtlib2_genConstr.make_root_term: Exists not implemented yet" - | TermExclimationPt (_,t,_) -> make_root_term t - - and make_root_app v l = - match (v,l) with - | "=", [a;b] -> - (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> - (match Atom.type_of a' with - | Tbool -> Form (Form.get rf (Fapp (Fiff, [|Form.get rf (Fatom a'); Form.get rf (Fatom b')|]))) - | ty -> Atom (Atom.mk_eq ra ty a' b')) - | _, _ -> assert false) - | "<", [a;b] -> - (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_lt ra a' b') - | _, _ -> assert false) - | "<=", [a;b] -> - (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_le ra a' b') - | _, _ -> assert false) - | ">", [a;b] -> - (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_gt ra a' b') - | _, _ -> assert false) - | ">=", [a;b] -> - (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_ge ra a' b') - | _, _ -> assert false) - | "+", [a;b] -> - (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_plus ra a' b') - | _, _ -> assert false) - | "-", [a;b] -> - (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_minus ra a' b') - | _, _ -> assert false) - | "*", [a;b] -> - (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_mult ra a' b') - | _, _ -> assert false) - | "-", [a] -> - (match make_root_term a with - | Atom a' -> Atom (Atom.mk_opp ra a') - | _ -> assert false) - | "distinct", _ -> - let make_h h = - match make_root_term h with - | Atom h' -> h' - | _ -> assert false in - let a = Array.make (List.length l) (make_h (List.hd l)) in - let i = ref (-1) in - List.iter (fun h -> - incr i; - a.(!i) <- make_h h) l; - Atom (Atom.mk_distinct ra (Atom.type_of a.(0)) a) - | "true", _ -> Form (Form.get rf Form.pform_true) - | "false", _ -> Form (Form.get rf Form.pform_false) - | "and", _ -> - Form (Form.get rf (Fapp (Fand, Array.of_list (List.map make_root l)))) - | "or", _ -> - Form (Form.get rf (Fapp (For, Array.of_list (List.map make_root l)))) - | "xor", _ -> - Form (Form.get rf (Fapp (Fxor, Array.of_list (List.map make_root l)))) - | "=>", _ -> - Form (Form.get rf (Fapp (Fimp, Array.of_list (List.map make_root l)))) - | "ite", _ -> - Form (Form.get rf (Fapp (Fite, Array.of_list (List.map make_root l)))) - | "not", [a] -> Form (Form.neg (make_root a)) - | _, _ -> - let op = VeritSyntax.get_fun v in - let l' = List.map (fun t -> match make_root_term t with - | Atom h -> h | Form _ -> assert false) l in - Atom (Atom.get ra (Aapp (op, Array.of_list l'))) - - and make_root t = - match make_root_term t with - | Atom h -> Form.get rf (Fatom h) - | Form f -> f in - - make_root t - - -let declare_commands rt ro ra rf acc = function - | CDeclareSort (_,sym,_) -> let _ = declare_sort rt sym in acc - | CDeclareFun (_,sym, (_, arg), cod) -> - let _ = declare_fun rt ro sym arg cod in acc - | CAssert (_, t) -> (make_root ra rf t)::acc - | _ -> acc diff --git a/src/verit/smtlib2_lex.mll b/src/verit/smtlib2_lex.mll deleted file mode 100644 index f235403..0000000 --- a/src/verit/smtlib2_lex.mll +++ /dev/null @@ -1,88 +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/verit/smtlib2_parse.mly b/src/verit/smtlib2_parse.mly deleted file mode 100644 index b4e02a7..0000000 --- a/src/verit/smtlib2_parse.mly +++ /dev/null @@ -1,299 +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 - -/* 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/verit/smtlib2_util.ml b/src/verit/smtlib2_util.ml deleted file mode 100644 index 1ce5e46..0000000 --- a/src/verit/smtlib2_util.ml +++ /dev/null @@ -1,29 +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;; |