1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize.ML |
1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize.ML |
2 Author: Philipp Meyer, TU Muenchen |
2 Author: Philipp Meyer, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
4 |
4 |
5 Minimization of fact list for Metis using ATPs. |
5 Minimization of fact list for Metis using external provers. |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_MINIMIZE = |
8 signature SLEDGEHAMMER_MINIMIZE = |
9 sig |
9 sig |
10 type locality = Sledgehammer_Filter.locality |
10 type locality = Sledgehammer_Filter.locality |
60 val problem = |
60 val problem = |
61 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
61 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
62 facts = facts, only = true} |
62 facts = facts, only = true} |
63 val result as {outcome, used_facts, ...} = prover params (K "") problem |
63 val result as {outcome, used_facts, ...} = prover params (K "") problem |
64 in |
64 in |
65 Output.urgent_message (case outcome of |
65 Output.urgent_message |
66 SOME failure => string_for_failure failure |
66 (case outcome of |
67 | NONE => |
67 SOME failure => string_for_failure failure |
68 if length used_facts = length facts then "Found proof." |
68 | NONE => |
69 else "Found proof with " ^ n_facts used_facts ^ "."); |
69 if length used_facts = length facts then "Found proof." |
|
70 else "Found proof with " ^ n_facts used_facts ^ "."); |
70 result |
71 result |
71 end |
72 end |
72 |
73 |
73 (* minimalization of facts *) |
74 (* minimalization of facts *) |
|
75 |
|
76 (* The sublinear algorithm works well in almost all situations, except when the |
|
77 external prover cannot return the list of used facts and hence returns all |
|
78 facts as used. In that case, the binary algorithm is much more |
|
79 appropriate. We can usually detect that situation just by looking at the |
|
80 number of used facts reported by the prover. *) |
|
81 val binary_threshold = 50 |
74 |
82 |
75 fun filter_used_facts used = filter (member (op =) used o fst) |
83 fun filter_used_facts used = filter (member (op =) used o fst) |
76 |
84 |
77 fun sublinear_minimize _ [] p = p |
85 fun sublinear_minimize _ [] p = p |
78 | sublinear_minimize test (x :: xs) (seen, result) = |
86 | sublinear_minimize test (x :: xs) (seen, result) = |
80 result as {outcome = NONE, used_facts, ...} : prover_result => |
88 result as {outcome = NONE, used_facts, ...} : prover_result => |
81 sublinear_minimize test (filter_used_facts used_facts xs) |
89 sublinear_minimize test (filter_used_facts used_facts xs) |
82 (filter_used_facts used_facts seen, result) |
90 (filter_used_facts used_facts seen, result) |
83 | _ => sublinear_minimize test xs (x :: seen, result) |
91 | _ => sublinear_minimize test xs (x :: seen, result) |
84 |
92 |
85 (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer |
93 fun binary_minimize test xs = |
86 preprocessing time is included in the estimate below but isn't part of the |
94 let |
87 timeout. *) |
95 fun p xs = #outcome (test xs : prover_result) = NONE |
|
96 fun split [] p = p |
|
97 | split [h] (l, r) = (h :: l, r) |
|
98 | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r) |
|
99 fun min _ [] = raise Empty |
|
100 | min _ [s0] = [s0] |
|
101 | min sup xs = |
|
102 let val (l0, r0) = split xs ([], []) in |
|
103 if p (sup @ l0) then |
|
104 min sup l0 |
|
105 else if p (sup @ r0) then |
|
106 min sup r0 |
|
107 else |
|
108 let |
|
109 val l = min (sup @ r0) l0 |
|
110 val r = min (sup @ l) r0 |
|
111 in l @ r end |
|
112 end |
|
113 val xs = |
|
114 case min [] xs of |
|
115 [x] => if p [] then [] else [x] |
|
116 | xs => xs |
|
117 in (xs, test xs) end |
|
118 |
|
119 (* Give the external prover some slack. The ATP gets further slack because the |
|
120 Sledgehammer preprocessing time is included in the estimate below but isn't |
|
121 part of the timeout. *) |
88 val fudge_msecs = 1000 |
122 val fudge_msecs = 1000 |
89 |
123 |
90 fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set." |
124 fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set." |
91 | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n |
125 | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n |
92 state facts = |
126 state facts = |
93 let |
127 let |
94 val thy = Proof.theory_of state |
128 val thy = Proof.theory_of state |
95 val ctxt = Proof.context_of state |
129 val ctxt = Proof.context_of state |
96 val prover = get_prover ctxt false prover_name |
130 val prover = get_prover ctxt false prover_name |
97 val msecs = Time.toMilliseconds timeout |
131 val msecs = Time.toMilliseconds timeout |
98 val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".") |
132 val _ = Output.urgent_message ("Sledgehammer minimize: " ^ |
|
133 quote prover_name ^ ".") |
99 val {goal, ...} = Proof.goal state |
134 val {goal, ...} = Proof.goal state |
100 val (_, hyp_ts, concl_t) = strip_subgoal goal i |
135 val (_, hyp_ts, concl_t) = strip_subgoal goal i |
101 val explicit_apply = |
136 val explicit_apply = |
102 not (forall (Meson.is_fol_term thy) |
137 not (forall (Meson.is_fol_term thy) |
103 (concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) |
138 (concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) |
110 let |
145 let |
111 val time = Timer.checkRealTimer timer |
146 val time = Timer.checkRealTimer timer |
112 val new_timeout = |
147 val new_timeout = |
113 Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |
148 Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |
114 |> Time.fromMilliseconds |
149 |> Time.fromMilliseconds |
|
150 val facts = filter_used_facts used_facts facts |
115 val (min_thms, {message, ...}) = |
151 val (min_thms, {message, ...}) = |
116 sublinear_minimize (do_test new_timeout) |
152 if length facts >= binary_threshold then |
117 (filter_used_facts used_facts facts) ([], result) |
153 binary_minimize (do_test new_timeout) facts |
|
154 else |
|
155 sublinear_minimize (do_test new_timeout) facts ([], result) |
118 val n = length min_thms |
156 val n = length min_thms |
119 val _ = Output.urgent_message (cat_lines |
157 val _ = Output.urgent_message (cat_lines |
120 ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ |
158 ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ |
121 (case length (filter (curry (op =) Chained o snd o fst) min_thms) of |
159 (case length (filter (curry (op =) Chained o snd o fst) min_thms) of |
122 0 => "" |
160 0 => "" |
130 (* Failure sometimes mean timeout, unfortunately. *) |
168 (* Failure sometimes mean timeout, unfortunately. *) |
131 (NONE, "Failure: No proof was found with the current time limit. You \ |
169 (NONE, "Failure: No proof was found with the current time limit. You \ |
132 \can increase the time limit using the \"timeout\" \ |
170 \can increase the time limit using the \"timeout\" \ |
133 \option (e.g., \"timeout = " ^ |
171 \option (e.g., \"timeout = " ^ |
134 string_of_int (10 + msecs div 1000) ^ "\").") |
172 string_of_int (10 + msecs div 1000) ^ "\").") |
135 | {message, ...} => (NONE, "ATP error: " ^ message)) |
173 | {message, ...} => (NONE, "Prover error: " ^ message)) |
136 handle ERROR msg => (NONE, "Error: " ^ msg) |
174 handle ERROR msg => (NONE, "Error: " ^ msg) |
137 end |
175 end |
138 |
176 |
139 fun run_minimize params i refs state = |
177 fun run_minimize params i refs state = |
140 let |
178 let |