4 Minimization of theorem list for metis by using an external automated theorem prover |
4 Minimization of theorem list for metis by using an external automated theorem prover |
5 *) |
5 *) |
6 |
6 |
7 signature ATP_MINIMAL = |
7 signature ATP_MINIMAL = |
8 sig |
8 sig |
9 val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state -> |
9 type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list |
10 (string * thm list) list -> ((string * thm list) list * int) option * string |
10 val linear_minimize : 'a minimize_fun |
11 (* To be removed once TN has finished his measurements; |
11 val binary_minimize : 'a minimize_fun |
12 the int component of the result should then be removed: *) |
12 val minimize_theorems : |
13 val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state -> |
13 (string * thm list) minimize_fun -> ATP_Wrapper.prover -> string -> int |
14 (string * thm list) list -> ((string * thm list) list * int) option * string |
14 -> Proof.state -> (string * thm list) list |
15 end |
15 -> (string * thm list) list option * string |
|
16 end; |
16 |
17 |
17 structure ATP_Minimal : ATP_MINIMAL = |
18 structure ATP_Minimal : ATP_MINIMAL = |
18 struct |
19 struct |
19 |
20 |
20 (* Linear minimization *) |
21 open Sledgehammer_Fact_Preprocessor |
21 |
22 |
22 fun lin_gen_minimize p s = |
23 type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list |
23 let |
|
24 fun min [] needed = needed |
|
25 | min (x::xs) needed = |
|
26 if p(xs @ needed) then min xs needed else min xs (x::needed) |
|
27 in (min s [], length s) end; |
|
28 |
24 |
29 (* Clever minimalization algorithm *) |
25 (* Linear minimization algorithm *) |
|
26 |
|
27 fun linear_minimize p s = |
|
28 let |
|
29 fun aux [] needed = needed |
|
30 | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x) |
|
31 in aux s [] end; |
|
32 |
|
33 (* Binary minimalization *) |
30 |
34 |
31 local |
35 local |
32 fun isplit (l, r) [] = (l, r) |
36 fun isplit (l, r) [] = (l, r) |
33 | isplit (l, r) [h] = (h :: l, r) |
37 | isplit (l, r) [h] = (h :: l, r) |
34 | isplit (l, r) (h1 :: h2 :: t) = isplit (h1 :: l, h2 :: r) t |
38 | isplit (l, r) (h1 :: h2 :: t) = isplit (h1 :: l, h2 :: r) t |
35 in |
39 in |
36 fun split lst = isplit ([], []) lst |
40 fun split lst = isplit ([], []) lst |
37 end |
41 end |
38 |
42 |
39 local |
43 local |
40 fun min p sup [] = raise Empty |
44 fun min _ _ [] = raise Empty |
41 | min p sup [s0] = [s0] |
45 | min _ _ [s0] = [s0] |
42 | min p sup s = |
46 | min p sup s = |
43 let |
47 let |
44 val (l0, r0) = split s |
48 val (l0, r0) = split s |
45 in |
49 in |
46 if p (sup @ l0) |
50 if p (sup @ l0) then |
47 then min p sup l0 |
51 min p sup l0 |
|
52 else if p (sup @ r0) then |
|
53 min p sup r0 |
48 else |
54 else |
49 if p (sup @ r0) |
55 let |
50 then min p sup r0 |
56 val l = min p (sup @ r0) l0 |
51 else |
57 val r = min p (sup @ l) r0 |
52 let |
58 in l @ r end |
53 val l = min p (sup @ r0) l0 |
|
54 val r = min p (sup @ l) r0 |
|
55 in |
|
56 l @ r |
|
57 end |
|
58 end |
59 end |
59 in |
60 in |
60 (* return a minimal subset v of s that satisfies p |
61 (* return a minimal subset v of s that satisfies p |
61 @pre p(s) & ~p([]) & monotone(p) |
62 @pre p(s) & ~p([]) & monotone(p) |
62 @post v subset s & p(v) & |
63 @post v subset s & p(v) & |
63 forall e in v. ~p(v \ e) |
64 forall e in v. ~p(v \ e) |
64 *) |
65 *) |
65 fun minimal p s = |
66 fun binary_minimize p s = |
66 let |
67 case min p [] s of |
67 val count = Unsynchronized.ref 0 |
68 [x] => if p [] then [] else [x] |
68 fun p_count xs = (Unsynchronized.inc count; p xs) |
69 | m => m |
69 val v = |
|
70 (case min p_count [] s of |
|
71 [x] => if p_count [] then [] else [x] |
|
72 | m => m); |
|
73 in (v, ! count) end |
|
74 end |
70 end |
75 |
71 |
76 |
72 |
77 (* failure check and producing answer *) |
73 (* failure check and producing answer *) |
78 |
74 |
89 ("Timeout", Timeout), |
85 ("Timeout", Timeout), |
90 ("time limit exceeded", Timeout), |
86 ("time limit exceeded", Timeout), |
91 ("# Cannot determine problem status within resource limit", Timeout), |
87 ("# Cannot determine problem status within resource limit", Timeout), |
92 ("Error", Error)] |
88 ("Error", Error)] |
93 |
89 |
94 fun produce_answer (result: ATP_Wrapper.prover_result) = |
90 fun produce_answer (result : ATP_Wrapper.prover_result) = |
95 let |
91 let |
96 val {success, proof = result_string, internal_thm_names = thm_name_vec, |
92 val {success, proof = result_string, internal_thm_names = thm_name_vec, |
97 filtered_clauses = filtered, ...} = result |
93 filtered_clauses = filtered, ...} = result |
98 in |
94 in |
99 if success then |
95 if success then |
114 |
110 |
115 fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs = |
111 fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs = |
116 let |
112 let |
117 val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ") |
113 val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ") |
118 val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
114 val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
119 val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs |
115 val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs |
120 val {context = ctxt, facts, goal} = Proof.goal state |
116 val {context = ctxt, facts, goal} = Proof.goal state |
121 val problem = |
117 val problem = |
122 {with_full_types = ! ATP_Manager.full_types, |
118 {with_full_types = ! ATP_Manager.full_types, |
123 subgoal = subgoalno, |
119 subgoal = subgoalno, |
124 goal = (ctxt, (facts, goal)), |
120 goal = (ctxt, (facts, goal)), |
150 val ordered_used = sort_distinct string_ord used |
147 val ordered_used = sort_distinct string_ord used |
151 val to_use = |
148 val to_use = |
152 if length ordered_used < length name_thms_pairs then |
149 if length ordered_used < length name_thms_pairs then |
153 filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs |
150 filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs |
154 else name_thms_pairs |
151 else name_thms_pairs |
155 val (min_thms, n) = |
152 val min_thms = |
156 if null to_use then ([], 0) |
153 if null to_use then [] |
157 else gen_min (test_thms (SOME filtered)) to_use |
154 else gen_min (test_thms (SOME filtered)) to_use |
158 val min_names = sort_distinct string_ord (map fst min_thms) |
155 val min_names = sort_distinct string_ord (map fst min_thms) |
159 val _ = priority (cat_lines |
156 val _ = priority (cat_lines |
160 ["Iterations: " ^ string_of_int n (* FIXME TN remove later *), |
157 ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) |
161 "Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) |
|
162 in |
158 in |
163 (SOME (min_thms, n), "Try this command: " ^ |
159 (SOME min_thms, "Try this command: " ^ |
164 Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")")) |
160 Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")")) |
165 end |
161 end |
166 | (Timeout, _) => |
162 | (Timeout, _) => |
167 (NONE, "Timeout: You may need to increase the time limit of " ^ |
163 (NONE, "Timeout: You may need to increase the time limit of " ^ |
168 string_of_int time_limit ^ " seconds. Call atp_minimize [time=...] ") |
164 string_of_int time_limit ^ " seconds. Call atp_minimize [time=...] ") |
169 | (Error, msg) => |
165 | (Error, msg) => |
170 (NONE, "Error in prover: " ^ msg) |
166 (NONE, "Error in prover: " ^ msg) |
171 | (Failure, _) => |
167 | (Failure, _) => |
172 (NONE, "Failure: No proof with the theorems supplied")) |
168 (NONE, "Failure: No proof with the theorems supplied")) |
173 handle Sledgehammer_HOL_Clause.TRIVIAL => |
169 handle Sledgehammer_HOL_Clause.TRIVIAL => |
174 (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") |
170 (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") |
175 | ERROR msg => (NONE, "Error: " ^ msg) |
171 | ERROR msg => (NONE, "Error: " ^ msg) |
176 end |
172 end |
177 |
173 |
178 |
174 end; |
179 (* Isar command and parsing input *) |
|
180 |
|
181 local structure K = OuterKeyword and P = OuterParse and T = OuterLex in |
|
182 |
|
183 fun get_thms context = |
|
184 map (fn (name, interval) => |
|
185 let |
|
186 val thmref = Facts.Named ((name, Position.none), interval) |
|
187 val ths = ProofContext.get_fact context thmref |
|
188 val name' = Facts.string_of_ref thmref |
|
189 in |
|
190 (name', ths) |
|
191 end) |
|
192 |
|
193 val default_prover = "remote_vampire" |
|
194 val default_time_limit = 5 |
|
195 |
|
196 fun get_time_limit_arg time_string = |
|
197 (case Int.fromString time_string of |
|
198 SOME t => t |
|
199 | NONE => error ("Invalid time limit: " ^ quote time_string)) |
|
200 |
|
201 fun get_opt (name, a) (p, t) = |
|
202 (case name of |
|
203 "time" => (p, get_time_limit_arg a) |
|
204 | "atp" => (a, t) |
|
205 | n => error ("Invalid argument: " ^ n)) |
|
206 |
|
207 fun get_options args = fold get_opt args (default_prover, default_time_limit) |
|
208 |
|
209 val minimize = gen_minimalize lin_gen_minimize |
|
210 |
|
211 val minimalize = gen_minimalize minimal |
|
212 |
|
213 fun sh_min_command args thm_names state = |
|
214 let |
|
215 val (prover_name, time_limit) = get_options args |
|
216 val prover = |
|
217 (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of |
|
218 SOME prover => prover |
|
219 | NONE => error ("Unknown prover: " ^ quote prover_name)) |
|
220 val name_thms_pairs = get_thms (Proof.context_of state) thm_names |
|
221 in |
|
222 writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs)) |
|
223 end |
|
224 |
|
225 val parse_args = |
|
226 Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) [] |
|
227 val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel) |
|
228 |
|
229 val _ = |
|
230 OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag |
|
231 (parse_args -- parse_thm_names >> (fn (args, thm_names) => |
|
232 Toplevel.no_timing o Toplevel.unknown_proof o |
|
233 Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of))) |
|
234 |
|
235 end |
|
236 |
|
237 end |
|