309 | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0) |
309 | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0) |
310 |
310 |
311 in |
311 in |
312 |
312 |
313 fun run_sledgehammer (params as {provers, ...}) output_dir e_selection_heuristic term_order |
313 fun run_sledgehammer (params as {provers, ...}) output_dir e_selection_heuristic term_order |
314 force_sos keep_probs keep_proofs proof_method_from_msg thy_index trivial proof_method named_thms |
314 force_sos keep_probs keep_proofs proof_method_from_msg thy_index trivial pos st = |
315 pos st = |
|
316 let |
315 let |
317 val thy = Proof.theory_of st |
316 val thy = Proof.theory_of st |
318 val thy_name = Context.theory_name thy |
317 val thy_name = Context.theory_name thy |
319 val triv_str = if trivial then "[T] " else "" |
318 val triv_str = if trivial then "[T] " else "" |
320 val keep = |
319 val keep = |
328 else |
327 else |
329 NONE |
328 NONE |
330 val prover_name = hd provers |
329 val prover_name = hd provers |
331 val (sledgehamer_outcome, msg, cpu_time) = |
330 val (sledgehamer_outcome, msg, cpu_time) = |
332 run_sh params e_selection_heuristic term_order force_sos keep pos st |
331 run_sh params e_selection_heuristic term_order force_sos keep pos st |
333 val (outcome_msg, change_data) = |
332 val (outcome_msg, change_data, proof_method_and_used_thms) = |
334 (case sledgehamer_outcome of |
333 (case sledgehamer_outcome of |
335 Sledgehammer.SH_Some {used_facts, run_time, ...} => |
334 Sledgehammer.SH_Some {used_facts, run_time, ...} => |
336 let |
335 let |
337 val num_used_facts = length used_facts |
336 val num_used_facts = length used_facts |
338 val time_prover = Time.toMilliseconds run_time |
337 val time_prover = Time.toMilliseconds run_time |
348 #> not trivial ? inc_sh_nontriv_success |
347 #> not trivial ? inc_sh_nontriv_success |
349 #> inc_sh_lemmas num_used_facts |
348 #> inc_sh_lemmas num_used_facts |
350 #> inc_sh_max_lems num_used_facts |
349 #> inc_sh_max_lems num_used_facts |
351 #> inc_sh_time_prover time_prover |
350 #> inc_sh_time_prover time_prover |
352 in |
351 in |
353 proof_method := proof_method_from_msg msg; |
352 (outcome_msg, change_data, |
354 named_thms := SOME (map_filter get_thms used_facts); |
353 SOME (proof_method_from_msg msg, map_filter get_thms used_facts)) |
355 (outcome_msg, change_data) |
|
356 end |
354 end |
357 | _ => ("", I)) |
355 | _ => ("", I, NONE)) |
358 in |
356 in |
359 (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg, change_data #> inc_sh_time_isa cpu_time) |
357 (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg, change_data #> inc_sh_time_isa cpu_time, |
|
358 proof_method_and_used_thms) |
360 end |
359 end |
361 |
360 |
362 end |
361 end |
363 |
362 |
364 fun override_params prover type_enc timeout = |
363 fun override_params prover type_enc timeout = |
383 timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal |
382 timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal |
384 fun sledge_tac time_slice prover type_enc = |
383 fun sledge_tac time_slice prover type_enc = |
385 Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
384 Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
386 (override_params prover type_enc (my_timeout time_slice)) fact_override [] |
385 (override_params prover type_enc (my_timeout time_slice)) fact_override [] |
387 in |
386 in |
388 if !meth = "sledgehammer_tac" then |
387 if meth = "sledgehammer_tac" then |
389 sledge_tac 0.2 ATP_Proof.vampireN "mono_native" |
388 sledge_tac 0.2 ATP_Proof.vampireN "mono_native" |
390 ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" |
389 ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" |
391 ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" |
390 ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" |
392 ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" |
391 ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" |
393 ORELSE' SMT_Solver.smt_tac ctxt thms |
392 ORELSE' SMT_Solver.smt_tac ctxt thms |
394 else if !meth = "smt" then |
393 else if meth = "smt" then |
395 SMT_Solver.smt_tac ctxt thms |
394 SMT_Solver.smt_tac ctxt thms |
396 else if full then |
395 else if full then |
397 Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] |
396 Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] |
398 ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms |
397 ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms |
399 else if String.isPrefix "metis (" (!meth) then |
398 else if String.isPrefix "metis (" meth then |
400 let |
399 let |
401 val (type_encs, lam_trans) = |
400 val (type_encs, lam_trans) = |
402 !meth |
401 meth |
403 |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start |
402 |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start |
404 |> filter Token.is_proper |> tl |
403 |> filter Token.is_proper |> tl |
405 |> Metis_Tactic.parse_metis_options |> fst |
404 |> Metis_Tactic.parse_metis_options |> fst |
406 |>> the_default [ATP_Proof_Reconstruct.partial_typesN] |
405 |>> the_default [ATP_Proof_Reconstruct.partial_typesN] |
407 ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans |
406 ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans |
408 in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end |
407 in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end |
409 else if !meth = "metis" then |
408 else if meth = "metis" then |
410 Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms |
409 Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms |
411 else if !meth = "none" then |
410 else if meth = "none" then |
412 K all_tac |
411 K all_tac |
413 else if !meth = "fail" then |
412 else if meth = "fail" then |
414 K no_tac |
413 K no_tac |
415 else |
414 else |
416 (warning ("Unknown method " ^ quote (!meth)); K no_tac) |
415 (warning ("Unknown method " ^ quote meth); K no_tac) |
417 end |
416 end |
418 fun apply_method named_thms = |
417 fun apply_method named_thms = |
419 Mirabelle.can_apply timeout (do_method named_thms) st |
418 Mirabelle.can_apply timeout (do_method named_thms) st |
420 |
419 |
421 fun with_time (false, t) = ("failed (" ^ string_of_int t ^ ")", I) |
420 fun with_time (false, t) = ("failed (" ^ string_of_int t ^ ")", I) |
468 let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in |
467 let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in |
469 if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then |
468 if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then |
470 "" |
469 "" |
471 else |
470 else |
472 let |
471 let |
473 val meth = Unsynchronized.ref "" |
|
474 val named_thms = |
|
475 Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) |
|
476 val trivial = |
472 val trivial = |
477 check_trivial andalso Try0.try0 (SOME try_timeout) ([], [], [], []) pre |
473 check_trivial andalso Try0.try0 (SOME try_timeout) ([], [], [], []) pre |
478 handle Timeout.TIMEOUT _ => false |
474 handle Timeout.TIMEOUT _ => false |
479 val (outcome, log1, change_data1) = |
475 val (outcome, log1, change_data1, proof_method_and_used_thms) = |
480 run_sledgehammer params output_dir e_selection_heuristic term_order |
476 run_sledgehammer params output_dir e_selection_heuristic term_order |
481 force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial meth |
477 force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial pos pre |
482 named_thms pos pre |
|
483 val (log2, change_data2) = |
478 val (log2, change_data2) = |
484 (case !named_thms of |
479 (case proof_method_and_used_thms of |
485 SOME thms => |
480 SOME (proof_method, used_thms) => |
486 run_proof_method trivial false name meth thms timeout pos pre |
481 run_proof_method trivial false name proof_method used_thms timeout pos pre |
487 |> apfst (prefix (!meth ^ " (sledgehammer): ")) |
482 |> apfst (prefix (proof_method ^ " (sledgehammer): ")) |
488 | NONE => ("", I)) |
483 | NONE => ("", I)) |
489 val () = Synchronized.change data |
484 val () = Synchronized.change data |
490 (change_data1 #> change_data2 #> inc_sh_calls #> not trivial ? inc_sh_nontriv_calls) |
485 (change_data1 #> change_data2 #> inc_sh_calls #> not trivial ? inc_sh_nontriv_calls) |
491 in |
486 in |
492 log1 ^ "\n" ^ log2 |
487 log1 ^ "\n" ^ log2 |