22 {debug: bool, |
22 {debug: bool, |
23 verbose: bool, |
23 verbose: bool, |
24 overlord: bool, |
24 overlord: bool, |
25 blocking: bool, |
25 blocking: bool, |
26 provers: string list, |
26 provers: string list, |
27 type_enc: type_enc option, |
27 type_enc: string option, |
28 sound: bool, |
28 sound: bool, |
29 relevance_thresholds: real * real, |
29 relevance_thresholds: real * real, |
30 max_relevant: int option, |
30 max_relevant: int option, |
31 max_mono_iters: int, |
31 max_mono_iters: int, |
32 max_new_mono_instances: int, |
32 max_new_mono_instances: int, |
289 {debug: bool, |
289 {debug: bool, |
290 verbose: bool, |
290 verbose: bool, |
291 overlord: bool, |
291 overlord: bool, |
292 blocking: bool, |
292 blocking: bool, |
293 provers: string list, |
293 provers: string list, |
294 type_enc: type_enc option, |
294 type_enc: string option, |
295 sound: bool, |
295 sound: bool, |
296 relevance_thresholds: real * real, |
296 relevance_thresholds: real * real, |
297 max_relevant: int option, |
297 max_relevant: int option, |
298 max_mono_iters: int, |
298 max_mono_iters: int, |
299 max_new_mono_instances: int, |
299 max_new_mono_instances: int, |
510 |
510 |
511 (* Important messages are important but not so important that users want to see |
511 (* Important messages are important but not so important that users want to see |
512 them each time. *) |
512 them each time. *) |
513 val atp_important_message_keep_quotient = 10 |
513 val atp_important_message_keep_quotient = 10 |
514 |
514 |
515 fun choose_format_and_type_enc best_type_enc formats type_enc_opt = |
515 fun choose_format_and_type_enc soundness best_type_enc formats = |
516 (case type_enc_opt of |
516 the_default best_type_enc |
517 SOME ts => ts |
517 #> type_enc_from_string soundness |
518 | NONE => type_enc_from_string best_type_enc) |
518 #> choose_format formats |
519 |> choose_format formats |
|
520 |
519 |
521 val metis_minimize_max_time = seconds 2.0 |
520 val metis_minimize_max_time = seconds 2.0 |
522 |
521 |
523 fun choose_minimize_command minimize_command name preplay = |
522 fun choose_minimize_command minimize_command name preplay = |
524 (case preplay of |
523 (case preplay of |
614 time_left = |
613 time_left = |
615 let |
614 let |
616 val num_facts = |
615 val num_facts = |
617 length facts |> is_none max_relevant |
616 length facts |> is_none max_relevant |
618 ? Integer.min best_max_relevant |
617 ? Integer.min best_max_relevant |
|
618 val soundness = |
|
619 if sound then |
|
620 if Config.get ctxt atp_sound_modulo_infiniteness then |
|
621 Sound_Modulo_Infiniteness |
|
622 else |
|
623 Sound |
|
624 else |
|
625 Unsound |
619 val (format, type_enc) = |
626 val (format, type_enc) = |
620 choose_format_and_type_enc best_type_enc formats type_enc |
627 choose_format_and_type_enc soundness best_type_enc formats |
|
628 type_enc |
621 val fairly_sound = is_type_enc_fairly_sound type_enc |
629 val fairly_sound = is_type_enc_fairly_sound type_enc |
622 val facts = |
630 val facts = |
623 facts |> map untranslated_fact |
631 facts |> map untranslated_fact |
624 |> not fairly_sound |
632 |> not fairly_sound |
625 ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |
633 ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |
644 plural_s num_facts ^ " for " ^ |
652 plural_s num_facts ^ " for " ^ |
645 string_from_time slice_timeout ^ "..." |
653 string_from_time slice_timeout ^ "..." |
646 |> Output.urgent_message |
654 |> Output.urgent_message |
647 else |
655 else |
648 () |
656 () |
649 val soundness = |
|
650 if sound then |
|
651 if Config.get ctxt atp_sound_modulo_infiniteness then |
|
652 Sound_Modulo_Infiniteness |
|
653 else |
|
654 Sound |
|
655 else |
|
656 Unsound |
|
657 val (atp_problem, pool, conjecture_offset, facts_offset, |
657 val (atp_problem, pool, conjecture_offset, facts_offset, |
658 fact_names, typed_helpers, sym_tab) = |
658 fact_names, typed_helpers, sym_tab) = |
659 prepare_atp_problem ctxt format conj_sym_kind prem_kind |
659 prepare_atp_problem ctxt format conj_sym_kind prem_kind |
660 type_enc soundness false |
660 type_enc false (Config.get ctxt atp_lambda_translation) |
661 (Config.get ctxt atp_lambda_translation) |
|
662 (Config.get ctxt atp_readable_names) true hyp_ts concl_t |
661 (Config.get ctxt atp_readable_names) true hyp_ts concl_t |
663 facts |
662 facts |
664 fun weights () = atp_problem_weights atp_problem |
663 fun weights () = atp_problem_weights atp_problem |
665 val full_proof = debug orelse isar_proof |
664 val full_proof = debug orelse isar_proof |
666 val core = |
665 val core = |
704 NONE => |
703 NONE => |
705 used_facts_in_unsound_atp_proof ctxt |
704 used_facts_in_unsound_atp_proof ctxt |
706 conjecture_shape facts_offset fact_names atp_proof |
705 conjecture_shape facts_offset fact_names atp_proof |
707 |> Option.map (fn facts => |
706 |> Option.map (fn facts => |
708 UnsoundProof |
707 UnsoundProof |
709 (if is_type_enc_virtually_sound type_enc then |
708 (if is_type_enc_quasi_sound type_enc then |
710 SOME sound |
709 SOME sound |
711 else |
710 else |
712 NONE, facts |> sort string_ord)) |
711 NONE, facts |> sort string_ord)) |
713 | _ => outcome |
712 | _ => outcome |
714 in |
713 in |