1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200
1.3 @@ -99,6 +99,7 @@
1.4 val kill_provers : unit -> unit
1.5 val running_provers : unit -> unit
1.6 val messages : int option -> unit
1.7 + val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
1.8 val get_prover : Proof.context -> mode -> string -> prover
1.9 end;
1.10
1.11 @@ -306,6 +307,7 @@
1.12
1.13 type prover = params -> minimize_command -> prover_problem -> prover_result
1.14
1.15 +
1.16 (* configuration attributes *)
1.17
1.18 val dest_dir =
1.19 @@ -318,20 +320,6 @@
1.20 val measure_run_time =
1.21 Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
1.22
1.23 -fun with_path cleanup after f path =
1.24 - Exn.capture f path
1.25 - |> tap (fn _ => cleanup path)
1.26 - |> Exn.release
1.27 - |> tap (after path)
1.28 -
1.29 -fun proof_banner mode blocking name =
1.30 - case mode of
1.31 - Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
1.32 - | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
1.33 - | Normal => if blocking then quote name ^ " found a proof"
1.34 - else "Try this"
1.35 - | Minimize => "Try this"
1.36 -
1.37 val smt_triggers =
1.38 Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
1.39 val smt_weights =
1.40 @@ -379,6 +367,41 @@
1.41 fun overlord_file_location_for_prover prover =
1.42 (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
1.43
1.44 +fun with_path cleanup after f path =
1.45 + Exn.capture f path
1.46 + |> tap (fn _ => cleanup path)
1.47 + |> Exn.release
1.48 + |> tap (after path)
1.49 +
1.50 +fun proof_banner mode blocking name =
1.51 + case mode of
1.52 + Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
1.53 + | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
1.54 + | Normal => if blocking then quote name ^ " found a proof"
1.55 + else "Try this"
1.56 + | Minimize => "Try this"
1.57 +
1.58 +(* based on "Mirabelle.can_apply" and generalized *)
1.59 +fun try_apply timeout tac state i =
1.60 + let
1.61 + val {context = ctxt, facts, goal} = Proof.goal state
1.62 + val full_tac = Method.insert_tac facts i THEN tac ctxt i
1.63 + in try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal end
1.64 +
1.65 +fun try_metis debug timeout ths =
1.66 + try_apply timeout (Config.put Metis_Tactics.verbose debug
1.67 + #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths))
1.68 +
1.69 +fun filter_used_facts used = filter (member (op =) used o fst)
1.70 +
1.71 +fun preplay_one_line_proof debug reconstructor_guess timeout ths state i =
1.72 + let val timer = Timer.startRealTimer () in
1.73 + case try_metis debug timeout ths state i of
1.74 + SOME (SOME _) => Preplayed (Metis, Timer.checkRealTimer timer)
1.75 + | SOME NONE => Preplay_Failed
1.76 + | NONE => Trust_Playable (reconstructor_guess, SOME timeout)
1.77 + end
1.78 +
1.79
1.80 (* generic TPTP-based ATPs *)
1.81
1.82 @@ -485,7 +508,7 @@
1.83 conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
1.84 ({debug, verbose, overlord, blocking, type_sys, max_relevant,
1.85 max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof,
1.86 - isar_shrink_factor, slicing, timeout, ...} : params)
1.87 + isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
1.88 minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
1.89 let
1.90 val thy = Proof.theory_of state
1.91 @@ -708,7 +731,7 @@
1.92 extract_important_message output
1.93 else
1.94 ""
1.95 - fun append_to_message message =
1.96 + fun complete_message message =
1.97 message ^
1.98 (if verbose then
1.99 "\nATP real CPU time: " ^
1.100 @@ -719,21 +742,34 @@
1.101 "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
1.102 else
1.103 "")
1.104 - val isar_params =
1.105 - (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
1.106 - val metis_params =
1.107 - (proof_banner mode blocking name, minimize_command, type_sys, atp_proof,
1.108 - facts_offset, fact_names, typed_helpers, goal, subgoal)
1.109 val (outcome, (message, used_facts)) =
1.110 case outcome of
1.111 NONE =>
1.112 - (NONE, proof_text ctxt isar_proof isar_params metis_params
1.113 - |>> append_to_message)
1.114 - | SOME failure =>
1.115 - if failure = ProofMissing orelse failure = ProofIncomplete then
1.116 - (NONE, metis_proof_text ctxt metis_params |>> append_to_message)
1.117 - else
1.118 - (outcome, (string_for_failure failure, []))
1.119 + let
1.120 + val used_facts =
1.121 + used_facts_in_atp_proof ctxt type_sys facts_offset fact_names
1.122 + atp_proof
1.123 + val reconstructor_guess =
1.124 + if uses_typed_helpers typed_helpers atp_proof then MetisFT
1.125 + else Metis
1.126 + val ths = facts |> map untranslated_fact
1.127 + |> filter_used_facts used_facts
1.128 + |> map snd
1.129 + val preplay =
1.130 + preplay_one_line_proof debug reconstructor_guess preplay_timeout ths
1.131 + state subgoal
1.132 + val full_types = uses_typed_helpers typed_helpers atp_proof
1.133 + val isar_params =
1.134 + (debug, full_types, isar_shrink_factor, type_sys, pool,
1.135 + conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof)
1.136 + val one_line_params =
1.137 + (preplay, proof_banner mode blocking name, used_facts,
1.138 + minimize_command, goal, subgoal)
1.139 + in
1.140 + (NONE, (proof_text ctxt isar_proof isar_params one_line_params
1.141 + |> complete_message, used_facts))
1.142 + end
1.143 + | SOME failure => (outcome, (string_for_failure failure, []))
1.144 in
1.145 {outcome = outcome, message = message, used_facts = used_facts,
1.146 run_time_in_msecs = msecs}
1.147 @@ -877,30 +913,6 @@
1.148 end
1.149 in do_slice timeout 1 NONE Time.zeroTime end
1.150
1.151 -(* based on "Mirabelle.can_apply" and generalized *)
1.152 -fun try_apply timeout tac state i =
1.153 - let
1.154 - val {context = ctxt, facts, goal} = Proof.goal state
1.155 - val full_tac = Method.insert_tac facts i THEN tac ctxt i
1.156 - in try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal end
1.157 -
1.158 -fun try_metis debug timeout ths =
1.159 - try_apply timeout (Config.put Metis_Tactics.verbose debug
1.160 - #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths))
1.161 -
1.162 -datatype metis_try =
1.163 - Preplayed of string * Time.time |
1.164 - Preplay_Timed_Out |
1.165 - Preplay_Failed
1.166 -
1.167 -fun preplay debug timeout ths state i =
1.168 - let val timer = Timer.startRealTimer () in
1.169 - case try_metis debug timeout ths state i of
1.170 - SOME (SOME _) => Preplayed ("metis", Timer.checkRealTimer timer)
1.171 - | SOME NONE => Preplay_Failed
1.172 - | NONE => Preplay_Timed_Out
1.173 - end
1.174 -
1.175 fun run_smt_solver mode name
1.176 (params as {debug, verbose, blocking, preplay_timeout, ...})
1.177 minimize_command
1.178 @@ -920,14 +932,15 @@
1.179 NONE =>
1.180 let
1.181 val (settings, method, time) =
1.182 - case preplay debug preplay_timeout (map snd used_facts) state
1.183 - subgoal of
1.184 - Preplayed (method, time) => (method, "", SOME time)
1.185 + case preplay_one_line_proof debug Metis preplay_timeout
1.186 + (map snd used_facts) state subgoal of
1.187 + Preplayed (method, time) =>
1.188 + ("", reconstructor_name method, SOME (false, time))
1.189 | _ => (if name = SMT_Solver.solver_name_of ctxt then ""
1.190 else "smt_solver = " ^ maybe_quote name,
1.191 "smt", NONE)
1.192 in
1.193 - try_command_line (proof_banner mode blocking name)
1.194 + try_command_line (proof_banner mode blocking name) time
1.195 (apply_on_subgoal settings subgoal subgoal_count ^
1.196 command_call method (map fst other_lemmas)) ^
1.197 minimize_line minimize_command