author | blanchet |
Tue, 27 Jul 2010 18:33:10 +0200 | |
changeset 38023 | 962b0a7f544b |
parent 38021 | e024504943d1 |
child 38045 | f367847f5068 |
permissions | -rw-r--r-- |
36375
2482446a604c
move the minimizer to the Sledgehammer directory
blanchet
parents:
36370
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
2 |
Author: Philipp Meyer, TU Muenchen |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
4 |
|
35867 | 5 |
Minimization of theorem list for Metis using automatic theorem provers. |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
6 |
*) |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
7 |
|
36375
2482446a604c
move the minimizer to the Sledgehammer directory
blanchet
parents:
36370
diff
changeset
|
8 |
signature SLEDGEHAMMER_FACT_MINIMIZER = |
32525 | 9 |
sig |
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38015
diff
changeset
|
10 |
type params = Sledgehammer.params |
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38015
diff
changeset
|
11 |
type prover_result = Sledgehammer.prover_result |
35867 | 12 |
|
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
13 |
val minimize_theorems : |
36481
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset
|
14 |
params -> int -> int -> Proof.state -> (string * thm list) list |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
15 |
-> (string * thm list) list option * string |
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
16 |
end; |
32525 | 17 |
|
36375
2482446a604c
move the minimizer to the Sledgehammer directory
blanchet
parents:
36370
diff
changeset
|
18 |
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER = |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
19 |
struct |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
20 |
|
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset
|
21 |
open Metis_Clauses |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
22 |
open Sledgehammer_Util |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
23 |
open Sledgehammer_Proof_Reconstruct |
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38015
diff
changeset
|
24 |
open Sledgehammer |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
25 |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
26 |
(* wrapper for calling external prover *) |
31236 | 27 |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
28 |
fun string_for_failure Unprovable = "Unprovable." |
37418 | 29 |
| string_for_failure IncompleteUnprovable = "Failed." |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
30 |
| string_for_failure TimedOut = "Timed out." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
31 |
| string_for_failure OutOfResources = "Failed." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
32 |
| string_for_failure OldSpass = "Error." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
33 |
| string_for_failure MalformedOutput = "Error." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
34 |
| string_for_failure UnknownError = "Failed." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
35 |
fun string_for_outcome NONE = "Success." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
36 |
| string_for_outcome (SOME failure) = string_for_failure failure |
31236 | 37 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
38 |
fun sledgehammer_test_theorems (params : params) prover timeout subgoal state |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
39 |
filtered_clauses name_thms_pairs = |
31236 | 40 |
let |
37628 | 41 |
val thy = Proof.theory_of state |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
42 |
val num_theorems = length name_thms_pairs |
38015 | 43 |
val _ = |
44 |
priority ("Testing " ^ string_of_int num_theorems ^ |
|
45 |
" theorem" ^ plural_s num_theorems ^ |
|
46 |
(if num_theorems > 0 then |
|
47 |
": " ^ space_implode " " |
|
48 |
(name_thms_pairs |
|
49 |
|> map fst |> sort_distinct string_ord) |
|
50 |
else |
|
51 |
"") ^ "...") |
|
32525 | 52 |
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
36263
56bf63d70120
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
blanchet
parents:
36232
diff
changeset
|
53 |
val {context = ctxt, facts, goal} = Proof.goal state |
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32937
diff
changeset
|
54 |
val problem = |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
55 |
{subgoal = subgoal, goal = (ctxt, (facts, goal)), |
35969 | 56 |
relevance_override = {add = [], del = [], only = false}, |
38002
31705eccee23
get rid of obsolete "axiom ID" component, since it's now always 0
blanchet
parents:
37994
diff
changeset
|
57 |
axiom_clauses = SOME name_thm_pairs, |
31705eccee23
get rid of obsolete "axiom ID" component, since it's now always 0
blanchet
parents:
37994
diff
changeset
|
58 |
filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)} |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
59 |
in |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
60 |
prover params (K "") timeout problem |
36607
e5f7235f39c5
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
krauss
parents:
36488
diff
changeset
|
61 |
|> tap (fn result : prover_result => |
e5f7235f39c5
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
krauss
parents:
36488
diff
changeset
|
62 |
priority (string_for_outcome (#outcome result))) |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
63 |
end |
31236 | 64 |
|
65 |
(* minimalization of thms *) |
|
66 |
||
38015 | 67 |
fun filter_used_facts used = filter (member (op =) used o fst) |
68 |
||
69 |
fun sublinear_minimize _ [] p = p |
|
70 |
| sublinear_minimize test (x :: xs) (seen, result) = |
|
71 |
case test (xs @ seen) of |
|
72 |
result as {outcome = NONE, proof, used_thm_names, ...} |
|
73 |
: prover_result => |
|
74 |
sublinear_minimize test (filter_used_facts used_thm_names xs) |
|
75 |
(filter_used_facts used_thm_names seen, result) |
|
76 |
| _ => sublinear_minimize test xs (x :: seen, result) |
|
77 |
||
36909
7d5587f6d5f7
made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset
|
78 |
fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout, |
36924 | 79 |
isar_proof, isar_shrink_factor, ...}) |
36481
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset
|
80 |
i n state name_thms_pairs = |
31236 | 81 |
let |
36378 | 82 |
val thy = Proof.theory_of state |
83 |
val prover = case atps of |
|
38023 | 84 |
[atp_name] => get_prover_fun thy atp_name |
36378 | 85 |
| _ => error "Expected a single ATP." |
35969 | 86 |
val msecs = Time.toMilliseconds minimize_timeout |
31236 | 87 |
val _ = |
36378 | 88 |
priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^ |
36224 | 89 |
" with a time limit of " ^ string_of_int msecs ^ " ms.") |
38015 | 90 |
val test_facts = |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
91 |
sledgehammer_test_theorems params prover minimize_timeout i state |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
92 |
val {context = ctxt, goal, ...} = Proof.goal state; |
31236 | 93 |
in |
94 |
(* try prove first to check result and get used theorems *) |
|
38015 | 95 |
(case test_facts NONE name_thms_pairs of |
96 |
result as {outcome = NONE, pool, proof, used_thm_names, |
|
97 |
conjecture_shape, filtered_clauses, ...} => |
|
98 |
let |
|
99 |
val (min_thms, {proof, internal_thm_names, ...}) = |
|
100 |
sublinear_minimize (test_facts (SOME filtered_clauses)) |
|
101 |
(filter_used_facts used_thm_names name_thms_pairs) |
|
102 |
([], result) |
|
103 |
val m = length min_thms |
|
104 |
val _ = priority (cat_lines |
|
105 |
["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".") |
|
106 |
in |
|
107 |
(SOME min_thms, |
|
108 |
proof_text isar_proof |
|
109 |
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
|
110 |
(full_types, K "", proof, internal_thm_names, goal, i) |> fst) |
|
111 |
end |
|
112 |
| {outcome = SOME TimedOut, ...} => |
|
113 |
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \ |
|
114 |
\option (e.g., \"timeout = " ^ |
|
115 |
string_of_int (10 + msecs div 1000) ^ " s\").") |
|
116 |
| {outcome = SOME UnknownError, ...} => |
|
117 |
(* Failure sometimes mean timeout, unfortunately. *) |
|
118 |
(NONE, "Failure: No proof was found with the current time limit. You \ |
|
119 |
\can increase the time limit using the \"timeout\" \ |
|
120 |
\option (e.g., \"timeout = " ^ |
|
121 |
string_of_int (10 + msecs div 1000) ^ " s\").") |
|
122 |
| {message, ...} => (NONE, "ATP error: " ^ message)) |
|
37994
b04307085a09
make TPTP generator accept full first-order formulas
blanchet
parents:
37926
diff
changeset
|
123 |
handle ERROR msg => (NONE, "Error: " ^ msg) |
31236 | 124 |
end |
125 |
||
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
126 |
end; |