16 |
16 |
17 val someN : string |
17 val someN : string |
18 val noneN : string |
18 val noneN : string |
19 val timeoutN : string |
19 val timeoutN : string |
20 val unknownN : string |
20 val unknownN : string |
21 val auto_minimize_min_facts : int Config.T |
21 val auto_min_min_facts : int Config.T |
22 val auto_minimize_max_time : real Config.T |
22 val auto_min_max_time : real Config.T |
23 val get_minimizing_prover : Proof.context -> mode -> string -> prover |
23 val get_minimizing_prover : Proof.context -> mode -> string -> prover |
24 val run_sledgehammer : |
24 val run_sledgehammer : |
25 params -> mode -> int -> relevance_override -> (string -> minimize_command) |
25 params -> mode -> int -> relevance_override -> (string -> minimize_command) |
26 -> Proof.state -> bool * (string * Proof.state) |
26 -> Proof.state -> bool * (string * Proof.state) |
27 end; |
27 end; |
64 (if blocking then |
64 (if blocking then |
65 "." |
65 "." |
66 else |
66 else |
67 "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
67 "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
68 |
68 |
69 val auto_minimize_min_facts = |
69 val auto_min_min_facts = |
70 Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} |
70 Attrib.setup_config_int @{binding sledgehammer_auto_min_min_facts} |
71 (fn generic => Config.get_generic generic binary_min_facts) |
71 (fn generic => Config.get_generic generic binary_min_facts) |
72 val auto_minimize_max_time = |
72 val auto_min_max_time = |
73 Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} |
73 Attrib.setup_config_real @{binding sledgehammer_auto_min_max_time} (K 0.0) (*###*) |
74 (K 5.0) |
|
75 |
74 |
76 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...}) |
75 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...}) |
77 ({state, subgoal, subgoal_count, facts, ...} : prover_problem) |
76 ({state, subgoal, subgoal_count, facts, ...} : prover_problem) |
78 (result as {outcome, used_facts, run_time_in_msecs, preplay, |
77 (result as {outcome, used_facts, run_time_in_msecs, preplay, |
79 message, message_tail} : prover_result) = |
78 message, message_tail} : prover_result) = |
82 else |
81 else |
83 let |
82 let |
84 val num_facts = length used_facts |
83 val num_facts = length used_facts |
85 val ((minimize, minimize_name), preplay) = |
84 val ((minimize, minimize_name), preplay) = |
86 if mode = Normal then |
85 if mode = Normal then |
87 if num_facts >= Config.get ctxt auto_minimize_min_facts then |
86 if num_facts >= Config.get ctxt auto_min_min_facts then |
88 ((true, name), preplay) |
87 ((true, name), preplay) |
89 else |
88 else |
90 let |
89 let |
91 fun can_min_fast_enough msecs = |
90 fun can_min_fast_enough msecs = |
92 0.001 * Real.fromInt ((num_facts + 2) * msecs) |
91 0.001 * Real.fromInt ((num_facts + 2) * msecs) |
93 <= Config.get ctxt auto_minimize_max_time |
92 <= Config.get ctxt auto_min_max_time |
94 val prover_fast_enough = |
93 val prover_fast_enough = |
95 run_time_in_msecs |> Option.map can_min_fast_enough |
94 run_time_in_msecs |> Option.map can_min_fast_enough |
96 |> the_default false |
95 |> the_default false |
97 in |
96 in |
98 if isar_proof then |
97 if isar_proof then |