# HG changeset patch # User blanchet # Date 1297268338 -3600 # Node ID 11e862c68b40e8fd2eca504e1c0523f6a2501451 # Parent 839d1488045f1967746d536bb382fdf9324e2837 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices) diff -r 839d1488045f -r 11e862c68b40 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Feb 09 17:18:58 2011 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Feb 09 17:18:58 2011 +0100 @@ -475,14 +475,14 @@ AList.lookup (op =) args minimize_timeoutK |> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *) |> the_default 5 - val params = Sledgehammer_Isar.default_params ctxt + val params as {explicit_apply, ...} = Sledgehammer_Isar.default_params ctxt [("provers", prover_name), ("verbose", "true"), ("type_sys", type_sys), ("timeout", string_of_int timeout)] val minimize = - Sledgehammer_Minimize.minimize_facts prover_name params true 1 - (Sledgehammer_Util.subgoal_count st) + Sledgehammer_Minimize.minimize_facts prover_name params + (SOME explicit_apply) true 1 (Sledgehammer_Util.subgoal_count st) val _ = log separator in case minimize st (these (!named_thms)) of diff -r 839d1488045f -r 11e862c68b40 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 09 17:18:58 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 09 17:18:58 2011 +0100 @@ -241,7 +241,8 @@ has_incomplete_mode = false, proof_delims = [], known_failures = - [(IncompleteUnprovable, "\nsat"), + [(Unprovable, "\nsat"), + (IncompleteUnprovable, "\nunknown"), (ProofMissing, "\nunsat")], default_max_relevant = 250 (* FUDGE *), explicit_forall = true, diff -r 839d1488045f -r 11e862c68b40 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed Feb 09 17:18:58 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Wed Feb 09 17:18:58 2011 +0100 @@ -28,6 +28,7 @@ val split_used_facts : (string * locality) list -> (string * locality) list * (string * locality) list + val metis_proof_text : metis_params -> text_result val isar_proof_text : isar_params -> metis_params -> text_result val proof_text : bool -> isar_params -> metis_params -> text_result end; @@ -165,9 +166,13 @@ append (resolve_fact fact_names name) | add_fact _ _ = I -fun used_facts_in_tstplike_proof fact_names = - atp_proof_from_tstplike_string false - #> rpair [] #-> fold (add_fact fact_names) +fun used_facts_in_tstplike_proof fact_names tstplike_proof = + if tstplike_proof = "" then + Vector.foldl (op @) [] fact_names + else + tstplike_proof + |> atp_proof_from_tstplike_string false + |> rpair [] |-> fold (add_fact fact_names) val split_used_facts = List.partition (curry (op =) Chained o snd) diff -r 839d1488045f -r 11e862c68b40 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 09 17:18:58 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 09 17:18:58 2011 +0100 @@ -13,7 +13,7 @@ val binary_min_facts : int Unsynchronized.ref val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list val minimize_facts : - string -> params -> bool -> int -> int -> Proof.state + string -> params -> bool option -> bool -> int -> int -> Proof.state -> ((string * locality) * thm list) list -> ((string * locality) * thm list) list option * string val run_minimize : @@ -48,14 +48,24 @@ fun print silent f = if silent then () else Output.urgent_message (f ()) fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof, - isar_shrink_factor, ...} : params) silent (prover : prover) - explicit_apply timeout i n state facts = + isar_shrink_factor, ...} : params) + explicit_apply_opt silent (prover : prover) timeout i n state facts = let + val thy = Proof.theory_of state val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ (if verbose then " (timeout: " ^ string_from_time timeout ^ ")" else "") ^ "...") + val {goal, ...} = Proof.goal state + val explicit_apply = + case explicit_apply_opt of + SOME explicit_apply => explicit_apply + | NONE => + let val (_, hyp_ts, concl_t) = strip_subgoal goal i in + not (forall (Meson.is_fol_term thy) + (concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) + end val params = {debug = debug, verbose = false, overlord = overlord, blocking = true, provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, @@ -64,7 +74,6 @@ timeout = timeout, expect = ""} val facts = facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) - val {goal, ...} = Proof.goal state val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, facts = facts, smt_filter = NONE} @@ -129,8 +138,8 @@ part of the timeout. *) val slack_msecs = 200 -fun minimize_facts prover_name (params as {timeout, ...}) silent i n state - facts = +fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt + silent i n state facts = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -139,12 +148,8 @@ val _ = print silent (fn () => "Sledgehammer minimize: " ^ quote prover_name ^ ".") val {goal, ...} = Proof.goal state - val (_, hyp_ts, concl_t) = strip_subgoal goal i - val explicit_apply = - not (forall (Meson.is_fol_term thy) - (concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) fun do_test timeout = - test_facts params silent prover explicit_apply timeout i n state + test_facts params explicit_apply_opt silent prover timeout i n state val timer = Timer.startRealTimer () in (case do_test timeout facts of @@ -196,7 +201,7 @@ [] => error "No prover is set." | prover :: _ => (kill_provers (); - minimize_facts prover params false i n state facts + minimize_facts prover params NONE false i n state facts |> #2 |> Output.urgent_message) end diff -r 839d1488045f -r 11e862c68b40 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Feb 09 17:18:58 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Feb 09 17:18:58 2011 +0100 @@ -445,26 +445,29 @@ extract_important_message output else "" - val (message, used_facts) = + fun append_to_message message = + message ^ + (if verbose then + "\nATP real CPU time: " ^ + string_from_time (Time.fromMilliseconds (the msecs)) ^ "." + else + "") ^ + (if important_message <> "" then + "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message + else + "") + val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) + val metis_params = + (proof_banner auto, type_sys, minimize_command, tstplike_proof, + fact_names, goal, subgoal) + val (outcome, (message, used_facts)) = case outcome of NONE => - proof_text isar_proof - (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (proof_banner auto, type_sys, minimize_command, tstplike_proof, - fact_names, goal, subgoal) - |>> (fn message => - message ^ - (if verbose then - "\nATP real CPU time: " ^ - string_from_time (Time.fromMilliseconds (the msecs)) ^ "." - else - "") ^ - (if important_message <> "" then - "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ - important_message - else - "")) - | SOME failure => (string_for_failure "ATP" failure, []) + (NONE, proof_text isar_proof isar_params metis_params + |>> append_to_message) + | SOME ProofMissing => + (NONE, metis_proof_text metis_params |>> append_to_message) + | SOME failure => (outcome, (string_for_failure "ATP" failure, [])) in {outcome = outcome, message = message, used_facts = used_facts, run_time_in_msecs = msecs} diff -r 839d1488045f -r 11e862c68b40 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Feb 09 17:18:58 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Feb 09 17:18:58 2011 +0100 @@ -44,8 +44,8 @@ val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts) -fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...}) - minimize_command +fun get_minimizing_prover ctxt auto name + (params as {debug, verbose, explicit_apply, ...}) minimize_command (problem as {state, subgoal, subgoal_count, facts, ...}) = get_prover ctxt auto name params minimize_command problem |> (fn result as {outcome, used_facts, run_time_in_msecs, message} => @@ -55,8 +55,8 @@ let val (used_facts, message) = if length used_facts >= !auto_minimize_min_facts then - minimize_facts name params (not verbose) subgoal subgoal_count - state + minimize_facts name params (SOME explicit_apply) (not verbose) + subgoal subgoal_count state (filter_used_facts used_facts (map (apsnd single o untranslated_fact) facts)) |>> Option.map (map fst)