# HG changeset patch # User blanchet # Date 1280333245 -7200 # Node ID 1745685335932821056e9cbbd3d74fae4fa76565 # Parent e2d546a07fa2dfe5e72c06e91178ef5e77d3a786 fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses diff -r e2d546a07fa2 -r 174568533593 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 17:38:40 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 18:07:25 2010 +0200 @@ -41,7 +41,7 @@ output: string, proof: string, internal_thm_names: string Vector.vector, - conjecture_shape: int list, + conjecture_shape: int list list, filtered_clauses: (string * thm) list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result @@ -112,7 +112,7 @@ output: string, proof: string, internal_thm_names: string Vector.vector, - conjecture_shape: int list, + conjecture_shape: int list list, filtered_clauses: (string * thm) list} type prover = @@ -681,15 +681,14 @@ clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part of this hack. *) let - val j0 = hd conjecture_shape + val j0 = hd (hd conjecture_shape) val seq = extract_clause_sequence output val name_map = extract_clause_formula_relation output fun renumber_conjecture j = AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0)) - |> the_single - |> (fn s => find_index (curry (op =) s) seq + 1) + |> map (fn s => find_index (curry (op =) s) seq + 1) in - (conjecture_shape |> map renumber_conjecture, + (conjecture_shape |> map (maps renumber_conjecture), seq |> map (the o AList.lookup (op =) name_map) |> map (fn s => case try (unprefix axiom_prefix) s of SOME s' => undo_ascii_of s' @@ -800,6 +799,7 @@ explicit_apply probfile clauses val conjecture_shape = conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 + |> map single val result = do_run false |> (fn (_, msecs0, _, SOME _) => diff -r e2d546a07fa2 -r 174568533593 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 28 17:38:40 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 28 18:07:25 2010 +0200 @@ -19,11 +19,11 @@ bool * minimize_command * string * string vector * thm * int -> string * string list val isar_proof_text: - string Symtab.table * bool * int * Proof.context * int list + string Symtab.table * bool * int * Proof.context * int list list -> bool * minimize_command * string * string vector * thm * int -> string * string list val proof_text: - bool -> string Symtab.table * bool * int * Proof.context * int list + bool -> string Symtab.table * bool * int * Proof.context * int list list -> bool * minimize_command * string * string vector * thm * int -> string * string list end; @@ -66,7 +66,8 @@ | mk_anot phi = AConn (ANot, [phi]) fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2]) -val index_in_shape : int -> int list -> int = find_index o curry (op =) +val index_in_shape : int -> int list list -> int = + find_index o exists o curry (op =) fun is_axiom_clause_number thm_names num = num > 0 andalso num <= Vector.length thm_names andalso Vector.sub (thm_names, num - 1) <> "" @@ -745,27 +746,33 @@ nth hyp_ts (index_in_shape num conjecture_shape) handle Subscript => raise Fail ("Cannot find hypothesis " ^ Int.toString num) - val concl_l = (raw_prefix, List.last conjecture_shape) - fun first_pass ([], contra) = ([], contra) - | first_pass ((step as Fix _) :: proof, contra) = - first_pass (proof, contra) |>> cons step - | first_pass ((step as Let _) :: proof, contra) = - first_pass (proof, contra) |>> cons step - | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) = - if l = concl_l then - first_pass (proof, contra ||> l = concl_l ? cons step) - else - first_pass (proof, contra) |>> cons (Assume (l, find_hyp num)) - | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = - let val step = Have (qs, l, t, ByMetis (ls, ss)) in - if exists (member (op =) (fst contra)) ls then - first_pass (proof, contra |>> cons l ||> cons step) - else - first_pass (proof, contra) |>> cons step - end - | first_pass _ = raise Fail "malformed proof" + val concl_ls = map (pair raw_prefix) (List.last conjecture_shape) + val canonicalize_labels = + map (fn l => if member (op =) concl_ls l then hd concl_ls else l) + #> distinct (op =) + fun first_pass ([], contra) = ([], contra) + | first_pass ((step as Fix _) :: proof, contra) = + first_pass (proof, contra) |>> cons step + | first_pass ((step as Let _) :: proof, contra) = + first_pass (proof, contra) |>> cons step + | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) = + if member (op =) concl_ls l then + first_pass (proof, contra ||> l = hd concl_ls ? cons step) + else + first_pass (proof, contra) |>> cons (Assume (l, find_hyp num)) + | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = + let + val ls = canonicalize_labels ls + val step = Have (qs, l, t, ByMetis (ls, ss)) + in + if exists (member (op =) (fst contra)) ls then + first_pass (proof, contra |>> cons l ||> cons step) + else + first_pass (proof, contra) |>> cons step + end + | first_pass _ = raise Fail "malformed proof" val (proof_top, (contra_ls, contra_proof)) = - first_pass (proof, ([concl_l], [])) + first_pass (proof, (concl_ls, [])) val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst fun backpatch_labels patches ls = fold merge_fact_sets (map (backpatch_label patches) ls) ([], []) @@ -800,7 +807,7 @@ val proofs = map_filter (fn l => - if l = concl_l then + if member (op =) concl_ls l then NONE else let