18 val max_callsK = "max_calls" |
18 val max_callsK = "max_calls" |
19 val minimizeK = "minimize" |
19 val minimizeK = "minimize" |
20 val minimize_timeoutK = "minimize_timeout" |
20 val minimize_timeoutK = "minimize_timeout" |
21 val metis_ftK = "metis_ft" |
21 val metis_ftK = "metis_ft" |
22 val reconstructorK = "reconstructor" |
22 val reconstructorK = "reconstructor" |
|
23 |
|
24 val preplay_timeout = "4" |
23 |
25 |
24 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " |
26 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " |
25 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " |
27 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " |
26 fun reconstructor_tag reconstructor id = |
28 fun reconstructor_tag reconstructor id = |
27 "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): " |
29 "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): " |
382 val params as {relevance_thresholds, max_relevant, slicing, ...} = |
384 val params as {relevance_thresholds, max_relevant, slicing, ...} = |
383 Sledgehammer_Isar.default_params ctxt |
385 Sledgehammer_Isar.default_params ctxt |
384 [("verbose", "true"), |
386 [("verbose", "true"), |
385 ("type_enc", type_enc), |
387 ("type_enc", type_enc), |
386 ("sound", sound), |
388 ("sound", sound), |
|
389 ("preplay_timeout", preplay_timeout), |
387 ("max_relevant", max_relevant), |
390 ("max_relevant", max_relevant), |
388 ("slicing", slicing), |
391 ("slicing", slicing), |
389 ("timeout", string_of_int timeout)] |
392 ("timeout", string_of_int timeout), |
|
393 ("preplay_timeout", preplay_timeout)] |
390 val default_max_relevant = |
394 val default_max_relevant = |
391 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing |
395 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing |
392 prover_name |
396 prover_name |
393 val is_appropriate_prop = |
397 val is_appropriate_prop = |
394 Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name |
398 Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name |
520 val params = Sledgehammer_Isar.default_params ctxt |
524 val params = Sledgehammer_Isar.default_params ctxt |
521 [("provers", prover_name), |
525 [("provers", prover_name), |
522 ("verbose", "true"), |
526 ("verbose", "true"), |
523 ("type_enc", type_enc), |
527 ("type_enc", type_enc), |
524 ("sound", sound), |
528 ("sound", sound), |
525 ("timeout", string_of_int timeout)] |
529 ("timeout", string_of_int timeout), |
|
530 ("preplay_timeout", preplay_timeout)] |
526 val minimize = |
531 val minimize = |
527 Sledgehammer_Minimize.minimize_facts prover_name params |
532 Sledgehammer_Minimize.minimize_facts prover_name params |
528 true 1 (Sledgehammer_Util.subgoal_count st) |
533 true 1 (Sledgehammer_Util.subgoal_count st) |
529 val _ = log separator |
534 val _ = log separator |
530 val (used_facts, (preplay, message, message_tail)) = |
535 val (used_facts, (preplay, message, message_tail)) = |
617 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) = |
622 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) = |
618 let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in |
623 let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in |
619 if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal |
624 if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal |
620 then () else |
625 then () else |
621 let |
626 let |
622 val reconstructor = Unsynchronized.ref "" |
|
623 val named_thms = |
|
624 Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) |
|
625 val max_calls = |
627 val max_calls = |
626 AList.lookup (op =) args max_callsK |> the_default "10000000" |
628 AList.lookup (op =) args max_callsK |> the_default "10000000" |
627 |> Int.fromString |> the |
629 |> Int.fromString |> the |
628 val minimize = AList.defined (op =) args minimizeK |
|
629 val metis_ft = AList.defined (op =) args metis_ftK |
|
630 val trivial = |
|
631 Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre |
|
632 handle TimeLimit.TimeOut => false |
|
633 fun apply_reconstructor m1 m2 = |
|
634 if metis_ft |
|
635 then |
|
636 if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false |
|
637 (run_reconstructor trivial false m1 name reconstructor |
|
638 (these (!named_thms))) id st) |
|
639 then |
|
640 (Mirabelle.catch_result (reconstructor_tag reconstructor) false |
|
641 (run_reconstructor trivial true m2 name reconstructor |
|
642 (these (!named_thms))) id st; ()) |
|
643 else () |
|
644 else |
|
645 (Mirabelle.catch_result (reconstructor_tag reconstructor) false |
|
646 (run_reconstructor trivial false m1 name reconstructor |
|
647 (these (!named_thms))) id st; ()) |
|
648 val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1; |
630 val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1; |
649 in |
631 in |
650 if !num_sledgehammer_calls > max_calls then () |
632 if !num_sledgehammer_calls > max_calls then () |
651 else |
633 else |
652 change_data id (set_mini minimize); |
634 let |
653 Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor |
635 val reconstructor = Unsynchronized.ref "" |
654 named_thms) id st; |
636 val named_thms = |
655 if is_some (!named_thms) |
637 Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) |
656 then |
638 val minimize = AList.defined (op =) args minimizeK |
657 (apply_reconstructor Unminimized UnminimizedFT; |
639 val metis_ft = AList.defined (op =) args metis_ftK |
658 if minimize andalso not (null (these (!named_thms))) |
640 val trivial = |
|
641 Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre |
|
642 handle TimeLimit.TimeOut => false |
|
643 fun apply_reconstructor m1 m2 = |
|
644 if metis_ft |
|
645 then |
|
646 if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false |
|
647 (run_reconstructor trivial false m1 name reconstructor |
|
648 (these (!named_thms))) id st) |
|
649 then |
|
650 (Mirabelle.catch_result (reconstructor_tag reconstructor) false |
|
651 (run_reconstructor trivial true m2 name reconstructor |
|
652 (these (!named_thms))) id st; ()) |
|
653 else () |
|
654 else |
|
655 (Mirabelle.catch_result (reconstructor_tag reconstructor) false |
|
656 (run_reconstructor trivial false m1 name reconstructor |
|
657 (these (!named_thms))) id st; ()) |
|
658 in |
|
659 change_data id (set_mini minimize); |
|
660 Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor |
|
661 named_thms) id st; |
|
662 if is_some (!named_thms) |
659 then |
663 then |
660 (Mirabelle.catch minimize_tag |
664 (apply_reconstructor Unminimized UnminimizedFT; |
661 (run_minimize args reconstructor named_thms) id st; |
665 if minimize andalso not (null (these (!named_thms))) |
662 apply_reconstructor Minimized MinimizedFT) |
666 then |
663 else ()) |
667 (Mirabelle.catch minimize_tag |
664 else () |
668 (run_minimize args reconstructor named_thms) id st; |
|
669 apply_reconstructor Minimized MinimizedFT) |
|
670 else ()) |
|
671 else () |
|
672 end |
665 end |
673 end |
666 end |
674 end |
667 |
675 |
668 fun invoke args = |
676 fun invoke args = |
669 Mirabelle.register (init, sledgehammer_action args, done) |
677 Mirabelle.register (init, sledgehammer_action args, done) |