# HG changeset patch # User fleury # Date 1406721793 -7200 # Node ID 9e4d2f7ad0a07c9e9c444f8f7f1c31b5ad76a146 # Parent 3c4e6bc7455f891eb3302276e8a2445f9a74d1ce Whitespace and indentation correction. diff -r 3c4e6bc7455f -r 9e4d2f7ad0a0 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jul 30 14:03:13 2014 +0200 @@ -239,13 +239,13 @@ in if textual then (case ts of - [fst, lst] => - if loose_aconv (fst, lst) then + [t1, t2] => + if loose_aconv (t1, t2) then @{const True} - else if Term.aconv_untyped (lst, @{const True}) then - fst - else if Term.aconv_untyped (fst, @{const True}) then - lst + else if Term.aconv_untyped (t2, @{const True}) then + t1 + else if Term.aconv_untyped (t1, @{const True}) then + t2 else equal_term ts | _ => equal_term ts) diff -r 3c4e6bc7455f -r 9e4d2f7ad0a0 src/HOL/Tools/SMT2/verit_proof.ML --- a/src/HOL/Tools/SMT2/verit_proof.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/SMT2/verit_proof.ML Wed Jul 30 14:03:13 2014 +0200 @@ -39,7 +39,6 @@ fun mk_node id rule prems concl bounds = VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds} -(*two structures needed*) datatype veriT_step = VeriT_Step of { id: string, rule: string, @@ -54,8 +53,8 @@ val veriT_input_rule = "input" val veriT_rewrite_rule = "__rewrite" (*arbitrary*) val veriT_tmp_ite_elim_rule = "tmp_ite_elim" -val veriT_tmp_skolemize = "tmp_skolemize" -val veriT_alpha_conv = "tmp_alphaconv" +val veriT_tmp_skolemize_rule = "tmp_skolemize" +val veriT_alpha_conv_rule = "tmp_alphaconv" (* proof parser *) @@ -102,7 +101,7 @@ fun update_step_and_cx (st as VeriT_Node {id, rule, prems, concl, bounds}) cx = if rule = veriT_tmp_ite_elim_rule then (mk_node id rule prems concl bounds, add_bound_variables_to_ctxt cx bounds concl) - else if rule = veriT_tmp_skolemize then + else if rule = veriT_tmp_skolemize_rule then let val concl' = replace_bound_var_by_free_var concl bounds in @@ -159,7 +158,6 @@ fun rotate_pair (a, (b, c)) = ((a, b), c) fun get_id (SMTLIB2.S [SMTLIB2.Sym "set", SMTLIB2.Sym id, SMTLIB2.S l]) = (id, l) | get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t) - fun unprefix_id x = (*unprefix veriT_step_prefix*) x fun parse_rule (SMTLIB2.Sym rule :: l) = (rule, l) fun parse_source (SMTLIB2.Key "clauses" :: SMTLIB2.S source ::l) = (SOME (map (fn (SMTLIB2.Sym id) => id) source), l) @@ -177,10 +175,9 @@ (HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1, perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l fun to_node (((((id, rule), prems), concl), bounds), cx) = (mk_node id rule - (the_default [] prems) concl bounds, cx) + (the_default [] prems) concl bounds, cx) in get_id - #>> unprefix_id ##> parse_rule #> rotate_pair ##> parse_source @@ -217,7 +214,7 @@ if m + n = 0 then [actual_lines ^ line] :: seperate l "" 0 else seperate l (actual_lines ^ line) (m + n) - end + end | seperate [] _ 0 = [] in seperate lines "" 0 @@ -296,7 +293,7 @@ let val concl' = replace_bound_var_by_free_var concl bounds in - mk_node id veriT_tmp_skolemize prems concl' [] + mk_node id veriT_tmp_skolemize_rule prems concl' [] end else st @@ -309,7 +306,7 @@ map (fn x => perhaps (Symtab.lookup replace_table) x) prems fun find_predecessor prem = perhaps (Symtab.lookup replace_table) prem in - if rule = veriT_alpha_conv then + if rule = veriT_alpha_conv_rule then remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems)) replace_table) steps else diff -r 3c4e6bc7455f -r 9e4d2f7ad0a0 src/HOL/Tools/SMT2/verit_proof_parse.ML --- a/src/HOL/Tools/SMT2/verit_proof_parse.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/SMT2/verit_proof_parse.ML Wed Jul 30 14:03:13 2014 +0200 @@ -39,9 +39,9 @@ NONE => let val id' = if th = ll_offset then 0 else id - ll_offset (* 0: for the conjecture*) - val ((prems, iidths), (id'', replaced')) = prems_to_theorem_number ths - (if th <> ll_offset then id + 1 else id) - ((x, string_of_int id') :: replaced) + val ((prems, iidths), (id'', replaced')) = + prems_to_theorem_number ths (if th <> ll_offset then id + 1 else id) + ((x, string_of_int id') :: replaced) in ((string_of_int id' :: prems, (th, (id', th - ll_offset)) :: iidths), (id'', replaced')) diff -r 3c4e6bc7455f -r 9e4d2f7ad0a0 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:13 2014 +0200 @@ -61,9 +61,9 @@ val zipperposition_cnf_rule = "cnf" val skolemize_rules = - [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule, -zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_tmp_skolemize_rule, -satallax_skolemize_rule] + [e_skolemize_rule, leo2_extcnf_combined_rule, satallax_skolemize_rule, spass_skolemize_rule, + vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule, + zipperposition_cnf_rule] val is_skolemize_rule = member (op =) skolemize_rules val is_arith_rule = (String.isPrefix z3_th_lemma_rule) orf (member (op =) veriT_arith_rules) diff -r 3c4e6bc7455f -r 9e4d2f7ad0a0 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jul 30 14:03:13 2014 +0200 @@ -258,7 +258,6 @@ val canonical_isar_supported_prover = eN val z3N = "z3" -val veriT_newN = "veriT" fun isar_supported_prover_of thy name = if is_atp thy name orelse name = z3N then name