author | wenzelm |
Wed, 14 Oct 2009 23:44:37 +0200 | |
changeset 32936 | 9491bec20595 |
parent 32864 | a226f29d4bdc |
child 32937 | 34f66c9dd8a2 |
permissions | -rw-r--r-- |
32327
0971cc0b6a57
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents:
32091
diff
changeset
|
1 |
(* Title: HOL/Tools/ATP_Manager/atp_minimal.ML |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
2 |
Author: Philipp Meyer, TU Muenchen |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
3 |
|
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
4 |
Minimalization of theorem list for metis by using an external automated theorem prover |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
5 |
*) |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
6 |
|
32525 | 7 |
signature ATP_MINIMAL = |
8 |
sig |
|
32936 | 9 |
val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state -> |
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
10 |
(string * thm list) list -> ((string * thm list) list * int) option * string |
32525 | 11 |
end |
12 |
||
32936 | 13 |
structure ATP_Minimal: ATP_MINIMAL = |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
14 |
struct |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
15 |
|
31236 | 16 |
(* output control *) |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
17 |
|
31236 | 18 |
fun debug str = Output.debug (fn () => str) |
19 |
fun debug_fn f = if ! Output.debugging then f () else () |
|
20 |
fun answer str = Output.writeln str |
|
21 |
fun println str = Output.priority str |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
22 |
|
31236 | 23 |
fun order_unique name_list = OrdList.make (String.collate Char.compare) name_list |
24 |
fun length_string namelist = Int.toString (length namelist) |
|
25 |
||
26 |
fun print_names name_thms_pairs = |
|
27 |
let |
|
28 |
val names = map fst name_thms_pairs |
|
29 |
val ordered = order_unique names |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
30 |
in |
31236 | 31 |
app (fn name => (debug (" " ^ name))) ordered |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
32 |
end |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
33 |
|
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
34 |
|
31236 | 35 |
(* minimalization algorithm *) |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
36 |
|
31236 | 37 |
local |
38 |
fun isplit (l,r) [] = (l,r) |
|
39 |
| isplit (l,r) (h::[]) = (h::l, r) |
|
40 |
| isplit (l,r) (h1::h2::t) = isplit (h1::l, h2::r) t |
|
41 |
in |
|
42 |
fun split lst = isplit ([],[]) lst |
|
43 |
end |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
44 |
|
31236 | 45 |
local |
46 |
fun min p sup [] = raise Empty |
|
47 |
| min p sup [s0] = [s0] |
|
48 |
| min p sup s = |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
49 |
let |
31236 | 50 |
val (l0, r0) = split s |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
51 |
in |
31236 | 52 |
if p (sup @ l0) |
53 |
then min p sup l0 |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
54 |
else |
31236 | 55 |
if p (sup @ r0) |
56 |
then min p sup r0 |
|
57 |
else |
|
58 |
let |
|
59 |
val l = min p (sup @ r0) l0 |
|
60 |
val r = min p (sup @ l) r0 |
|
61 |
in |
|
62 |
l @ r |
|
63 |
end |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
64 |
end |
31236 | 65 |
in |
66 |
(* return a minimal subset v of s that satisfies p |
|
67 |
@pre p(s) & ~p([]) & monotone(p) |
|
68 |
@post v subset s & p(v) & |
|
69 |
forall e in v. ~p(v \ e) |
|
70 |
*) |
|
32538
86035c5f61b5
Fixed "minimal" to cover the case that "p []" holds (excluded in the article by Bradley & Manna)
nipkow
parents:
32525
diff
changeset
|
71 |
fun minimal p s = |
32740 | 72 |
let val c = Unsynchronized.ref 0 |
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
73 |
fun pc xs = (c := !c + 1; p xs) |
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
74 |
in |
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
75 |
(case min pc [] s of |
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
76 |
[x] => if pc [] then [] else [x] |
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
77 |
| m => m, |
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
78 |
!c) |
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
79 |
end |
31236 | 80 |
end |
81 |
||
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
82 |
|
31236 | 83 |
(* failure check and producing answer *) |
84 |
||
85 |
datatype 'a prove_result = Success of 'a | Failure | Timeout | Error |
|
86 |
||
87 |
val string_of_result = |
|
88 |
fn Success _ => "Success" |
|
89 |
| Failure => "Failure" |
|
90 |
| Timeout => "Timeout" |
|
91 |
| Error => "Error" |
|
92 |
||
93 |
val failure_strings = |
|
94 |
[("SPASS beiseite: Ran out of time.", Timeout), |
|
95 |
("Timeout", Timeout), |
|
96 |
("time limit exceeded", Timeout), |
|
97 |
("# Cannot determine problem status within resource limit", Timeout), |
|
98 |
("Error", Error)] |
|
99 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
100 |
fun produce_answer result = |
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
101 |
let |
32936 | 102 |
val ATP_Wrapper.Prover_Result {success, message, proof=result_string, |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
103 |
internal_thm_names=thm_name_vec, filtered_clauses=filtered, ...} = result |
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
104 |
in |
31236 | 105 |
if success then |
31752
19a5f1c8a844
use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents:
31409
diff
changeset
|
106 |
(Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string) |
31236 | 107 |
else |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
108 |
let |
31236 | 109 |
val failure = failure_strings |> get_first (fn (s, t) => |
110 |
if String.isSubstring s result_string then SOME (t, result_string) else NONE) |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
111 |
in |
31236 | 112 |
if is_some failure then |
113 |
the failure |
|
114 |
else |
|
115 |
(Failure, result_string) |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
116 |
end |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
117 |
end |
31236 | 118 |
|
32936 | 119 |
|
31236 | 120 |
(* wrapper for calling external prover *) |
121 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
122 |
fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs = |
31236 | 123 |
let |
124 |
val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ") |
|
32525 | 125 |
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
31236 | 126 |
val _ = debug_fn (fn () => print_names name_thm_pairs) |
127 |
val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs |
|
32936 | 128 |
val problem = ATP_Wrapper.ATP_Problem { |
129 |
with_full_types = ATP_Manager.get_full_types (), |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
130 |
subgoal = subgoalno, |
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
131 |
goal = Proof.get_goal state, |
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
132 |
axiom_clauses = SOME axclauses, |
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
133 |
filtered_clauses = filtered } |
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
134 |
val (result, proof) = produce_answer (prover problem time_limit) |
31236 | 135 |
val _ = println (string_of_result result) |
136 |
val _ = debug proof |
|
137 |
in |
|
138 |
(result, proof) |
|
139 |
end |
|
140 |
||
141 |
||
142 |
(* minimalization of thms *) |
|
143 |
||
144 |
fun minimalize prover prover_name time_limit state name_thms_pairs = |
|
145 |
let |
|
146 |
val _ = |
|
147 |
println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: " |
|
148 |
^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds") |
|
149 |
val _ = debug_fn (fn () => app (fn (n, tl) => |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31752
diff
changeset
|
150 |
(debug n; app (fn t => |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31752
diff
changeset
|
151 |
debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs) |
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset
|
152 |
val test_thms_fun = sh_test_thms prover time_limit 1 state |
31752
19a5f1c8a844
use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents:
31409
diff
changeset
|
153 |
fun test_thms filtered thms = |
19a5f1c8a844
use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents:
31409
diff
changeset
|
154 |
case test_thms_fun filtered thms of (Success _, _) => true | _ => false |
32525 | 155 |
val answer' = pair and answer'' = pair NONE |
31236 | 156 |
in |
157 |
(* try prove first to check result and get used theorems *) |
|
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31236
diff
changeset
|
158 |
(case test_thms_fun NONE name_thms_pairs of |
31752
19a5f1c8a844
use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents:
31409
diff
changeset
|
159 |
(Success (used, filtered), _) => |
31236 | 160 |
let |
161 |
val ordered_used = order_unique used |
|
162 |
val to_use = |
|
163 |
if length ordered_used < length name_thms_pairs then |
|
164 |
filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs |
|
165 |
else |
|
166 |
name_thms_pairs |
|
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
167 |
val (min_thms, n) = if null to_use then ([], 0) |
32525 | 168 |
else minimal (test_thms (SOME filtered)) to_use |
31236 | 169 |
val min_names = order_unique (map fst min_thms) |
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
170 |
val _ = println ("Interations: " ^ string_of_int n) |
31236 | 171 |
val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems") |
172 |
val _ = debug_fn (fn () => print_names min_thms) |
|
173 |
in |
|
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
174 |
answer' (SOME(min_thms,n)) ("Try this command: " ^ |
31236 | 175 |
Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")")) |
176 |
end |
|
177 |
| (Timeout, _) => |
|
32525 | 178 |
answer'' ("Timeout: You may need to increase the time limit of " ^ |
31236 | 179 |
Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ") |
180 |
| (Error, msg) => |
|
32525 | 181 |
answer'' ("Error in prover: " ^ msg) |
31236 | 182 |
| (Failure, _) => |
32525 | 183 |
answer'' "Failure: No proof with the theorems supplied") |
31236 | 184 |
handle ResHolClause.TOO_TRIVIAL => |
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32538
diff
changeset
|
185 |
answer' (SOME ([],0)) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") |
31236 | 186 |
| ERROR msg => |
32525 | 187 |
answer'' ("Error: " ^ msg) |
31236 | 188 |
end |
189 |
||
190 |
||
191 |
(* Isar command and parsing input *) |
|
192 |
||
193 |
local structure K = OuterKeyword and P = OuterParse and T = OuterLex in |
|
194 |
||
195 |
fun get_thms context = |
|
196 |
map (fn (name, interval) => |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
197 |
let |
31236 | 198 |
val thmref = Facts.Named ((name, Position.none), interval) |
199 |
val ths = ProofContext.get_fact context thmref |
|
200 |
val name' = Facts.string_of_ref thmref |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
201 |
in |
31236 | 202 |
(name', ths) |
203 |
end) |
|
204 |
||
205 |
val default_prover = "remote_vampire" |
|
206 |
val default_time_limit = 5 |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
207 |
|
31236 | 208 |
fun get_time_limit_arg time_string = |
209 |
(case Int.fromString time_string of |
|
210 |
SOME t => t |
|
211 |
| NONE => error ("Invalid time limit: " ^ quote time_string)) |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
212 |
|
31236 | 213 |
val get_options = |
214 |
let |
|
215 |
val def = (default_prover, default_time_limit) |
|
216 |
in |
|
217 |
foldl (fn ((name, a), (p, t)) => |
|
218 |
(case name of |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
219 |
"time" => (p, (get_time_limit_arg a)) |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
220 |
| "atp" => (a, t) |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
221 |
| n => error ("Invalid argument: " ^ n))) def |
31236 | 222 |
end |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
223 |
|
31236 | 224 |
fun sh_min_command args thm_names state = |
225 |
let |
|
226 |
val (prover_name, time_limit) = get_options args |
|
227 |
val prover = |
|
32936 | 228 |
case ATP_Manager.get_prover prover_name (Proof.theory_of state) of |
31236 | 229 |
SOME prover => prover |
230 |
| NONE => error ("Unknown prover: " ^ quote prover_name) |
|
231 |
val name_thms_pairs = get_thms (Proof.context_of state) thm_names |
|
32525 | 232 |
fun print_answer (_, msg) = answer msg |
31236 | 233 |
in |
32525 | 234 |
print_answer (minimalize prover prover_name time_limit state name_thms_pairs) |
31236 | 235 |
end |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
236 |
|
31236 | 237 |
val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) [] |
238 |
val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel) |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
239 |
|
31236 | 240 |
val _ = |
241 |
OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag |
|
242 |
(parse_args -- parse_thm_names >> (fn (args, thm_names) => |
|
243 |
Toplevel.no_timing o Toplevel.unknown_proof o |
|
244 |
Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of))) |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
245 |
|
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
246 |
end |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
247 |
|
31236 | 248 |
end |
249 |