equal
deleted
inserted
replaced
61 params -> (string -> minimize_command) -> prover_problem -> prover_result |
61 params -> (string -> minimize_command) -> prover_problem -> prover_result |
62 |
62 |
63 val dest_dir : string Config.T |
63 val dest_dir : string Config.T |
64 val problem_prefix : string Config.T |
64 val problem_prefix : string Config.T |
65 val measure_run_time : bool Config.T |
65 val measure_run_time : bool Config.T |
|
66 val atp_lambda_translation : string Config.T |
66 val atp_readable_names : bool Config.T |
67 val atp_readable_names : bool Config.T |
67 val smt_triggers : bool Config.T |
68 val smt_triggers : bool Config.T |
68 val smt_weights : bool Config.T |
69 val smt_weights : bool Config.T |
69 val smt_weight_min_facts : int Config.T |
70 val smt_weight_min_facts : int Config.T |
70 val smt_min_weight : int Config.T |
71 val smt_min_weight : int Config.T |
334 val problem_prefix = |
335 val problem_prefix = |
335 Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob") |
336 Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob") |
336 val measure_run_time = |
337 val measure_run_time = |
337 Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false) |
338 Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false) |
338 |
339 |
|
340 val atp_lambda_translation = |
|
341 Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation} |
|
342 (K smartN) |
339 (* In addition to being easier to read, readable names are often much shorter, |
343 (* In addition to being easier to read, readable names are often much shorter, |
340 especially if types are mangled in names. For these reason, they are enabled |
344 especially if types are mangled in names. For these reason, they are enabled |
341 by default. *) |
345 by default. *) |
342 val atp_readable_names = |
346 val atp_readable_names = |
343 Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true) |
347 Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true) |
507 fun choose_format_and_type_enc best_type_enc formats type_enc_opt = |
511 fun choose_format_and_type_enc best_type_enc formats type_enc_opt = |
508 (case type_enc_opt of |
512 (case type_enc_opt of |
509 SOME ts => ts |
513 SOME ts => ts |
510 | NONE => type_enc_from_string best_type_enc) |
514 | NONE => type_enc_from_string best_type_enc) |
511 |> choose_format formats |
515 |> choose_format formats |
|
516 |
|
517 fun effective_atp_lambda_translation ctxt type_enc = |
|
518 Config.get ctxt atp_lambda_translation |
|
519 |> (fn trans => |
|
520 if trans = smartN then |
|
521 if is_type_enc_higher_order type_enc then lambdasN else combinatorsN |
|
522 else |
|
523 trans) |
512 |
524 |
513 val metis_minimize_max_time = seconds 2.0 |
525 val metis_minimize_max_time = seconds 2.0 |
514 |
526 |
515 fun choose_minimize_command minimize_command name preplay = |
527 fun choose_minimize_command minimize_command name preplay = |
516 (case preplay of |
528 (case preplay of |
639 else |
651 else |
640 () |
652 () |
641 val (atp_problem, pool, conjecture_offset, facts_offset, |
653 val (atp_problem, pool, conjecture_offset, facts_offset, |
642 fact_names, typed_helpers, sym_tab) = |
654 fact_names, typed_helpers, sym_tab) = |
643 prepare_atp_problem ctxt format conj_sym_kind prem_kind |
655 prepare_atp_problem ctxt format conj_sym_kind prem_kind |
644 type_enc sound false (Config.get ctxt atp_readable_names) |
656 type_enc sound false |
645 true hyp_ts concl_t facts |
657 (effective_atp_lambda_translation ctxt type_enc) |
|
658 (Config.get ctxt atp_readable_names) true hyp_ts concl_t |
|
659 facts |
646 fun weights () = atp_problem_weights atp_problem |
660 fun weights () = atp_problem_weights atp_problem |
647 val full_proof = debug orelse isar_proof |
661 val full_proof = debug orelse isar_proof |
648 val core = |
662 val core = |
649 File.shell_path command ^ " " ^ |
663 File.shell_path command ^ " " ^ |
650 arguments ctxt full_proof extra slice_timeout weights ^ " " ^ |
664 arguments ctxt full_proof extra slice_timeout weights ^ " " ^ |