29 open Sledgehammer_Provers |
29 open Sledgehammer_Provers |
30 open Sledgehammer_Minimize |
30 open Sledgehammer_Minimize |
31 |
31 |
32 fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i |
32 fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i |
33 n goal = |
33 n goal = |
34 quote name ^ |
34 (name, |
35 (if verbose then |
35 (if verbose then |
36 " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts |
36 " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts |
37 else |
37 else |
38 "") ^ |
38 "") ^ |
39 " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ |
39 " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ |
40 (if blocking then |
40 (if blocking then |
41 "." |
41 "." |
42 else |
42 else |
43 ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) |
43 ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
44 |
44 |
45 val auto_minimize_min_facts = |
45 val auto_minimize_min_facts = |
46 Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} |
46 Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} |
47 (fn generic => Config.get_generic generic binary_min_facts) |
47 (fn generic => Config.get_generic generic binary_min_facts) |
48 |
48 |
84 {outcome = NONE, used_facts = used_facts, |
84 {outcome = NONE, used_facts = used_facts, |
85 run_time_in_msecs = run_time_in_msecs, message = message}) |
85 run_time_in_msecs = run_time_in_msecs, message = message}) |
86 | NONE => result |
86 | NONE => result |
87 end) |
87 end) |
88 |
88 |
|
89 val someN = "some" |
|
90 val noneN = "none" |
|
91 val timeoutN = "timeout" |
|
92 val unknownN = "unknown" |
|
93 |
89 fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout, |
94 fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout, |
90 expect, ...}) |
95 expect, ...}) |
91 auto minimize_command only |
96 auto minimize_command only |
92 {state, goal, subgoal, subgoal_count, facts, smt_filter} name = |
97 {state, goal, subgoal, subgoal_count, facts, smt_filter} name = |
93 let |
98 let |
107 smt_filter = smt_filter} |
112 smt_filter = smt_filter} |
108 fun really_go () = |
113 fun really_go () = |
109 problem |
114 problem |
110 |> get_minimizing_prover ctxt auto name params (minimize_command name) |
115 |> get_minimizing_prover ctxt auto name params (minimize_command name) |
111 |> (fn {outcome, message, ...} => |
116 |> (fn {outcome, message, ...} => |
112 (if is_some outcome then "none" else "some" (* sic *), message)) |
117 (if outcome = SOME ATP_Proof.TimedOut then timeoutN |
|
118 else if is_some outcome then noneN |
|
119 else someN, message)) |
113 fun go () = |
120 fun go () = |
114 let |
121 let |
115 val (outcome_code, message) = |
122 val (outcome_code, message) = |
116 if debug then |
123 if debug then |
117 really_go () |
124 really_go () |
118 else |
125 else |
119 (really_go () |
126 (really_go () |
120 handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") |
127 handle ERROR message => (unknownN, "Error: " ^ message ^ "\n") |
121 | exn => |
128 | exn => |
122 if Exn.is_interrupt exn then |
129 if Exn.is_interrupt exn then |
123 reraise exn |
130 reraise exn |
124 else |
131 else |
125 ("unknown", "Internal error:\n" ^ |
132 (unknownN, "Internal error:\n" ^ |
126 ML_Compiler.exn_message exn ^ "\n")) |
133 ML_Compiler.exn_message exn ^ "\n")) |
127 val _ = |
134 val _ = |
128 (* The "expect" argument is deliberately ignored if the prover is |
135 (* The "expect" argument is deliberately ignored if the prover is |
129 missing so that the "Metis_Examples" can be processed on any |
136 missing so that the "Metis_Examples" can be processed on any |
130 machine. *) |
137 machine. *) |
131 if expect = "" orelse outcome_code = expect orelse |
138 if expect = "" orelse outcome_code = expect orelse |
133 () |
140 () |
134 else if blocking then |
141 else if blocking then |
135 error ("Unexpected outcome: " ^ quote outcome_code ^ ".") |
142 error ("Unexpected outcome: " ^ quote outcome_code ^ ".") |
136 else |
143 else |
137 warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); |
144 warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); |
138 in (outcome_code = "some", message) end |
145 in (outcome_code, message) end |
139 in |
146 in |
140 if auto then |
147 if auto then |
141 let val (success, message) = TimeLimit.timeLimit timeout go () in |
148 let |
|
149 val (outcome_code, message) = TimeLimit.timeLimit timeout go () |
|
150 val success = (outcome_code = someN) |
|
151 in |
142 (success, state |> success ? Proof.goal_message (fn () => |
152 (success, state |> success ? Proof.goal_message (fn () => |
143 Pretty.chunks [Pretty.str "", |
153 Pretty.chunks [Pretty.str "", |
144 Pretty.mark Markup.hilite (Pretty.str message)])) |
154 Pretty.mark Markup.hilite (Pretty.str message)])) |
145 end |
155 end |
146 else if blocking then |
156 else if blocking then |
147 let val (success, message) = TimeLimit.timeLimit hard_timeout go () in |
157 let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () in |
148 List.app Output.urgent_message |
158 Async_Manager.implode_desc desc ^ "\n" ^ message |
149 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]); |
159 |> Async_Manager.break_into_chunks |
150 (success, state) |
160 |> List.app Output.urgent_message; |
|
161 (outcome_code = someN, state) |
151 end |
162 end |
152 else |
163 else |
153 (Async_Manager.launch das_Tool birth_time death_time desc (snd o go); |
164 (Async_Manager.launch das_tool birth_time death_time desc |
|
165 (apfst (curry (op <>) timeoutN) o go); |
154 (false, state)) |
166 (false, state)) |
155 end |
167 end |
156 |
168 |
157 fun class_of_smt_solver ctxt name = |
169 fun class_of_smt_solver ctxt name = |
158 ctxt |> select_smt_solver name |
170 ctxt |> select_smt_solver name |