1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_run.ML
2 Author: Fabian Immler, TU Muenchen
4 Author: Jasmin Blanchette, TU Muenchen
9 signature SLEDGEHAMMER_RUN =
11 type relevance_override = Sledgehammer_Filter.relevance_override
12 type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
13 type params = Sledgehammer_Provers.params
14 type prover = Sledgehammer_Provers.prover
16 val auto_minimize_min_facts : int Unsynchronized.ref
17 val get_minimizing_prover : Proof.context -> bool -> string -> prover
18 val run_sledgehammer :
19 params -> bool -> int -> relevance_override -> (string -> minimize_command)
20 -> Proof.state -> bool * Proof.state
23 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
26 open Sledgehammer_Util
27 open Sledgehammer_Filter
28 open Sledgehammer_ATP_Translate
29 open Sledgehammer_Provers
30 open Sledgehammer_Minimize
32 fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
36 " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
39 " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
43 "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
45 val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
47 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...})
49 (problem as {state, subgoal, subgoal_count, facts, ...}) =
50 get_prover ctxt auto name params minimize_command problem
51 |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
52 if is_some outcome then
56 val (used_facts, message) =
57 if length used_facts >= !auto_minimize_min_facts then
58 minimize_facts name params (not verbose) subgoal subgoal_count
60 (filter_used_facts used_facts
61 (map (apsnd single o untranslated_fact) facts))
62 |>> Option.map (map fst)
64 (SOME used_facts, message)
68 (if debug andalso not (null used_facts) then
69 facts ~~ (0 upto length facts - 1)
70 |> map (fn (fact, j) =>
71 fact |> untranslated_fact |> apsnd (K j))
72 |> filter_used_facts used_facts
73 |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
75 |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^
76 quote name ^ " proof (of " ^
77 string_of_int (length facts) ^ "): ") "."
78 |> Output.urgent_message
81 {outcome = NONE, used_facts = used_facts,
82 run_time_in_msecs = run_time_in_msecs, message = message})
87 (params as {debug, blocking, max_relevant, timeout, expect, ...})
88 auto minimize_command only
89 {state, goal, subgoal, subgoal_count, facts, smt_head} name =
91 val ctxt = Proof.context_of state
92 val birth_time = Time.now ()
93 val death_time = Time.+ (birth_time, timeout)
95 the_default (default_max_relevant_for_prover ctxt name) max_relevant
96 val num_facts = length facts |> not only ? Integer.min max_relevant
98 prover_description ctxt params name num_facts subgoal subgoal_count goal
100 {state = state, goal = goal, subgoal = subgoal,
101 subgoal_count = subgoal_count, facts = take num_facts facts,
105 |> get_minimizing_prover ctxt auto name params (minimize_command name)
106 |> (fn {outcome, message, ...} =>
107 (if is_some outcome then "none" else "some" (* sic *), message))
110 val (outcome_code, message) =
115 handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
117 if Exn.is_interrupt exn then
120 ("unknown", "Internal error:\n" ^
121 ML_Compiler.exn_message exn ^ "\n"))
123 (* The "expect" argument is deliberately ignored if the prover is
124 missing so that the "Metis_Examples" can be processed on any
126 if expect = "" orelse outcome_code = expect orelse
127 not (is_prover_installed ctxt name) then
129 else if blocking then
130 error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
132 warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
133 in (outcome_code = "some", message) end
136 let val (success, message) = TimeLimit.timeLimit timeout go () in
137 (success, state |> success ? Proof.goal_message (fn () =>
138 Pretty.chunks [Pretty.str "",
139 Pretty.mark Markup.hilite (Pretty.str message)]))
141 else if blocking then
142 let val (success, message) = TimeLimit.timeLimit timeout go () in
143 List.app Output.urgent_message
144 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
148 (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
152 fun class_of_smt_solver ctxt name =
153 ctxt |> select_smt_solver name
154 |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
156 (* Makes backtraces more transparent and might be more efficient as well. *)
157 fun smart_par_list_map _ [] = []
158 | smart_par_list_map f [x] = [f x]
159 | smart_par_list_map f xs = Par_List.map f xs
161 fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
162 | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
165 val auto_max_relevant_divisor = 2
167 fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
168 relevance_thresholds, max_relevant, ...})
169 auto i (relevance_override as {only, ...}) minimize_command
172 error "No prover is set."
173 else case subgoal_count state of
174 0 => (Output.urgent_message "No subgoal!"; (false, state))
177 val _ = Proof.assert_backward state
179 state |> Proof.map_context (Config.put SMT_Config.verbose debug)
180 val ctxt = Proof.context_of state
181 val thy = ProofContext.theory_of ctxt
182 val {facts = chained_ths, goal, ...} = Proof.goal state
183 val (_, hyp_ts, concl_t) = strip_subgoal goal i
184 val no_dangerous_types = types_dangerous_types type_sys
185 val _ = () |> not blocking ? kill_provers
186 val _ = case find_first (not o is_prover_available ctxt) provers of
187 SOME name => error ("No such prover: " ^ name ^ ".")
189 val _ = if auto then () else Output.urgent_message "Sledgehammering..."
190 val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
191 fun launch_provers state get_facts translate maybe_smt_head provers =
193 val facts = get_facts ()
194 val num_facts = length facts
195 val facts = facts ~~ (0 upto num_facts - 1)
196 |> map (translate num_facts)
198 {state = state, goal = goal, subgoal = i, subgoal_count = n,
200 smt_head = maybe_smt_head
201 (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
202 val launch = launch_prover params auto minimize_command only
205 fold (fn prover => fn (true, state) => (true, state)
206 | (false, _) => launch problem prover)
207 provers (false, state)
210 |> (if blocking then smart_par_list_map else map) (launch problem)
211 |> exists fst |> rpair state
213 fun get_facts label no_dangerous_types relevance_fudge provers =
215 val max_max_relevant =
219 0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
221 |> auto ? (fn n => n div auto_max_relevant_divisor)
222 val is_built_in_const =
223 is_built_in_const_for_prover ctxt (hd provers)
225 relevant_facts ctxt no_dangerous_types relevance_thresholds
226 max_max_relevant is_built_in_const relevance_fudge
227 relevance_override chained_ths hyp_ts concl_t
230 label ^ plural_s (length provers) ^ ": " ^
232 "Found no relevant facts."
234 "Including (up to) " ^ string_of_int (length facts) ^
235 " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
236 (facts |> map (fst o fst) |> space_implode " ") ^ ".")
237 |> Output.urgent_message
241 fun launch_atps (accum as (success, _)) =
242 if success orelse null atps then
246 (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
247 (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
249 fun launch_smts (accum as (success, _)) =
250 if success orelse null smts then
254 val facts = get_facts "SMT solver" true smt_relevance_fudge smts
255 val weight = SMT_Weighted_Fact oo weight_smt_fact thy
257 (if debug then curry (op o) SOME else try)
258 (SMT_Solver.smt_filter_head state (facts ()))
260 smts |> map (`(class_of_smt_solver ctxt))
261 |> AList.group (op =)
262 |> map (launch_provers state (K facts) weight smt_head o snd)
263 |> exists fst |> rpair state
265 fun launch_atps_and_smt_solvers () =
266 [launch_atps, launch_smts]
267 |> smart_par_list_map (fn f => f (false, state) |> K ())
268 handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
271 |> (if blocking then launch_atps #> not auto ? launch_smts
272 else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))