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: string option, |
27 type_enc: string option, |
28 sound: bool, |
28 strict: bool, |
29 lam_trans: string option, |
29 lam_trans: string option, |
30 relevance_thresholds: real * real, |
30 relevance_thresholds: real * real, |
31 max_relevant: int option, |
31 max_relevant: int option, |
32 max_mono_iters: int, |
32 max_mono_iters: int, |
33 max_new_mono_instances: int, |
33 max_new_mono_instances: int, |
287 verbose: bool, |
287 verbose: bool, |
288 overlord: bool, |
288 overlord: bool, |
289 blocking: bool, |
289 blocking: bool, |
290 provers: string list, |
290 provers: string list, |
291 type_enc: string option, |
291 type_enc: string option, |
292 sound: bool, |
292 strict: bool, |
293 lam_trans: string option, |
293 lam_trans: string option, |
294 relevance_thresholds: real * real, |
294 relevance_thresholds: real * real, |
295 max_relevant: int option, |
295 max_relevant: int option, |
296 max_mono_iters: int, |
296 max_mono_iters: int, |
297 max_new_mono_instances: int, |
297 max_new_mono_instances: int, |
578 val atp_timeout_slack = seconds 1.0 |
578 val atp_timeout_slack = seconds 1.0 |
579 |
579 |
580 fun run_atp mode name |
580 fun run_atp mode name |
581 ({exec, required_execs, arguments, proof_delims, known_failures, |
581 ({exec, required_execs, arguments, proof_delims, known_failures, |
582 conj_sym_kind, prem_kind, best_slices, ...} : atp_config) |
582 conj_sym_kind, prem_kind, best_slices, ...} : atp_config) |
583 (params as {debug, verbose, overlord, type_enc, sound, lam_trans, |
583 (params as {debug, verbose, overlord, type_enc, strict, lam_trans, |
584 max_relevant, max_mono_iters, max_new_mono_instances, |
584 max_relevant, max_mono_iters, max_new_mono_instances, |
585 isar_proof, isar_shrink_factor, slice, timeout, |
585 isar_proof, isar_shrink_factor, slice, timeout, |
586 preplay_timeout, ...}) |
586 preplay_timeout, ...}) |
587 minimize_command |
587 minimize_command |
588 ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = |
588 ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = |
657 time_left = |
657 time_left = |
658 let |
658 let |
659 val num_facts = |
659 val num_facts = |
660 length facts |> is_none max_relevant |
660 length facts |> is_none max_relevant |
661 ? Integer.min best_max_relevant |
661 ? Integer.min best_max_relevant |
662 val soundness = if sound then Sound else Sound_Modulo_Infinity |
662 val soundness = if strict then Strict else Non_Strict |
663 val type_enc = |
663 val type_enc = |
664 type_enc |> choose_type_enc soundness best_type_enc format |
664 type_enc |> choose_type_enc soundness best_type_enc format |
665 val fairly_sound = is_type_enc_fairly_sound type_enc |
665 val fairly_sound = is_type_enc_fairly_sound type_enc |
666 val facts = |
666 val facts = |
667 facts |> map untranslated_fact |
667 facts |> map untranslated_fact |