# HG changeset patch # User blanchet # Date 1400729030 -7200 # Node ID 8b2283566f6e4df0d5d464f135d5bc6a6e60f355 # Parent df3a26987a8dbf6b8dbb8a31a029696f928cc1a8 properly reconstruct helpers in Z3 proofs diff -r df3a26987a8d -r 8b2283566f6e src/HOL/Tools/SMT2/z3_new_isar.ML --- a/src/HOL/Tools/SMT2/z3_new_isar.ML Thu May 22 04:12:06 2014 +0200 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Thu May 22 05:23:50 2014 +0200 @@ -84,8 +84,8 @@ Term.map_abs_vars (perhaps (try Name.dest_skolem)) #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T)))) -fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_ts prem_ids conjecture_id fact_ids - proof = +fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids conjecture_id + fact_helper_ids proof = let val thy = Proof_Context.theory_of ctxt @@ -108,12 +108,12 @@ (case rule of Z3_New_Proof.Asserted => let - val ss = the_list (AList.lookup (op =) fact_ids id) + val ss = the_list (AList.lookup (op =) fact_helper_ids id) val name0 = (sid ^ "a", ss) val (role0, concl0) = (case ss of - [s] => (Axiom, the (AList.lookup (op =) fact_ts s)) + [s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s)) | _ => if id = conjecture_id then (Conjecture, concl_t) diff -r df3a26987a8d -r 8b2283566f6e src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu May 22 04:12:06 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu May 22 05:23:50 2014 +0200 @@ -129,8 +129,7 @@ ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => print_used_facts used_facts used_from | _ => ()) - |> spy - ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) + |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) |> (fn {outcome, preplay, message, message_tail, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN @@ -143,13 +142,12 @@ really_go () else (really_go () - handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") - | exn => - if Exn.is_interrupt exn then - reraise exn - else - (unknownN, fn () => "Internal error:\n" ^ - Runtime.exn_message exn ^ "\n")) + handle + ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") + | exn => + if Exn.is_interrupt exn then reraise exn + else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) + val _ = (* The "expect" argument is deliberately ignored if the prover is missing so that the "Metis_Examples" can be processed on any @@ -175,9 +173,7 @@ let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () val outcome = - if outcome_code = someN orelse mode = Normal then - quote name ^ ": " ^ message () - else "" + if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else "" val _ = if outcome <> "" andalso is_some output_result then the output_result outcome @@ -274,9 +270,8 @@ if mode = Auto_Try then (unknownN, state) |> fold (fn prover => fn accum as (outcome_code, _) => - if outcome_code = someN then accum - else launch problem prover) - provers + if outcome_code = someN then accum else launch problem prover) + provers else provers |> (if blocking then Par_List.map else map) (launch problem #> fst) diff -r df3a26987a8d -r 8b2283566f6e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 22 04:12:06 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 22 05:23:50 2014 +0200 @@ -73,16 +73,11 @@ fun add_line_pass1 (line as (name, role, t, rule, [])) lines = (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or definitions. *) - if role = Conjecture orelse role = Negated_Conjecture then - line :: lines - else if is_True_prop t then - map (replace_dependencies_in_line (name, [])) lines - else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then - line :: lines - else if role = Axiom then - lines (* axioms (facts) need no proof lines *) - else - map (replace_dependencies_in_line (name, [])) lines + if role = Conjecture orelse role = Negated_Conjecture then line :: lines + else if is_True_prop t then map (replace_dependencies_in_line (name, [])) lines + else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines + else if role = Axiom then lines (* axioms (facts) need no proof lines *) + else map (replace_dependencies_in_line (name, [])) lines | add_line_pass1 line lines = line :: lines fun add_lines_pass2 res _ [] = rev res @@ -364,7 +359,9 @@ SOME s => s | NONE => if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "") - in one_line_proof ^ isar_proof end + in + one_line_proof ^ isar_proof + end fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = (case play of diff -r df3a26987a8d -r 8b2283566f6e src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu May 22 04:12:06 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu May 22 05:23:50 2014 +0200 @@ -63,8 +63,8 @@ message_tail : string} type prover = - params -> ((string * string list) list -> string -> minimize_command) - -> prover_problem -> prover_result + params -> ((string * string list) list -> string -> minimize_command) -> prover_problem -> + prover_result val SledgehammerN : string val str_of_mode : mode -> string @@ -76,8 +76,7 @@ val is_atp : theory -> string -> bool val bunch_of_proof_methods : bool -> bool -> string -> proof_method list val is_fact_chained : (('a * stature) * 'b) -> bool - val filter_used_facts : - bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> + val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list val play_one_line_proof : mode -> bool -> Time.time -> ((string * 'a) * thm) list -> Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome @@ -294,8 +293,7 @@ sort_strings (SMT2_Config.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) in - Output.urgent_message ("Supported provers: " ^ - commas (local_provers @ remote_provers) ^ ".") + Output.urgent_message ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".") end fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover" diff -r df3a26987a8d -r 8b2283566f6e src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 04:12:06 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 05:23:50 2014 +0200 @@ -242,15 +242,22 @@ SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)), fn preplay => let - val fact_ids = - map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @ - map (fn (id, ((name, _), _)) => (id, name)) fact_ids - val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t - (map (fn ((s, _), th) => (s, prop_of th)) used_named_facts) prem_ids conjecture_id - fact_ids z3_proof - val isar_params = - K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar, + fun isar_params () = + let + val fact_helper_ts = + map (fn (_, th) => (short_thm_name ctxt th, prop_of th)) helper_ids @ + map (fn ((s, _), th) => (s, prop_of th)) used_named_facts + val fact_helper_ids = + map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @ + map (fn (id, ((name, _), _)) => (id, name)) fact_ids + + val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts + concl_t fact_helper_ts prem_ids conjecture_id fact_helper_ids z3_proof + in + (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar, minimize <> SOME false, atp_proof, goal) + end + val one_line_params = (preplay, proof_banner mode name, used_facts, choose_minimize_command thy params minimize_command name preplay, subgoal,