author | blanchet |
Fri, 25 Jun 2010 16:42:06 +0200 | |
changeset 37577 | 5379f41a1322 |
parent 37574 | b8c1f4c46983 |
child 37578 | 9367cb36b1c4 |
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 |
35969 | 10 |
type params = ATP_Manager.params |
35867 | 11 |
type prover_result = ATP_Manager.prover_result |
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 |
|
37574
b8c1f4c46983
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents:
37506
diff
changeset
|
21 |
open Clausifier |
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 |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37574
diff
changeset
|
23 |
open Sledgehammer_FOL_Clause |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
24 |
open Sledgehammer_Proof_Reconstruct |
35867 | 25 |
open ATP_Manager |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
26 |
|
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
27 |
(* Linear minimization algorithm *) |
33492
4168294a9f96
Command atp_minimize uses the naive linear algorithm now
nipkow
parents:
33316
diff
changeset
|
28 |
|
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
29 |
fun linear_minimize test s = |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
30 |
let |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
31 |
fun aux [] p = p |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
32 |
| aux (x :: xs) (needed, result) = |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
33 |
case test (xs @ needed) of |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
34 |
SOME result => aux xs (needed, result) |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
35 |
| NONE => aux xs (x :: needed, result) |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
36 |
in aux s end |
31236 | 37 |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
38 |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
39 |
(* wrapper for calling external prover *) |
31236 | 40 |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
41 |
fun string_for_failure Unprovable = "Unprovable." |
37418 | 42 |
| string_for_failure IncompleteUnprovable = "Failed." |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
43 |
| string_for_failure TimedOut = "Timed out." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
44 |
| string_for_failure OutOfResources = "Failed." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
45 |
| string_for_failure OldSpass = "Error." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
46 |
| string_for_failure MalformedOutput = "Error." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
47 |
| string_for_failure UnknownError = "Failed." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
48 |
fun string_for_outcome NONE = "Success." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
49 |
| string_for_outcome (SOME failure) = string_for_failure failure |
31236 | 50 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
51 |
fun sledgehammer_test_theorems (params : params) prover timeout subgoal state |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset
|
52 |
filtered_clauses name_thms_pairs = |
31236 | 53 |
let |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
54 |
val num_theorems = length name_thms_pairs |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
55 |
val _ = priority ("Testing " ^ string_of_int num_theorems ^ |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
56 |
" theorem" ^ plural_s num_theorems ^ "...") |
32525 | 57 |
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
58 |
val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_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
|
59 |
val {context = ctxt, facts, goal} = Proof.goal state |
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32937
diff
changeset
|
60 |
val problem = |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
61 |
{subgoal = subgoal, goal = (ctxt, (facts, goal)), |
35969 | 62 |
relevance_override = {add = [], del = [], only = false}, |
36232
4d425766a47f
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
blanchet
parents:
36231
diff
changeset
|
63 |
axiom_clauses = SOME axclauses, |
4d425766a47f
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
blanchet
parents:
36231
diff
changeset
|
64 |
filtered_clauses = SOME (the_default axclauses filtered_clauses)} |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
65 |
in |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
66 |
prover params (K "") timeout problem |
36607
e5f7235f39c5
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
krauss
parents:
36488
diff
changeset
|
67 |
|> tap (fn result : prover_result => |
e5f7235f39c5
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
krauss
parents:
36488
diff
changeset
|
68 |
priority (string_for_outcome (#outcome result))) |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
69 |
end |
31236 | 70 |
|
71 |
(* minimalization of thms *) |
|
72 |
||
36909
7d5587f6d5f7
made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset
|
73 |
fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout, |
36924 | 74 |
isar_proof, isar_shrink_factor, ...}) |
36481
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset
|
75 |
i n state name_thms_pairs = |
31236 | 76 |
let |
36378 | 77 |
val thy = Proof.theory_of state |
78 |
val prover = case atps of |
|
79 |
[atp_name] => get_prover thy atp_name |
|
80 |
| _ => error "Expected a single ATP." |
|
35969 | 81 |
val msecs = Time.toMilliseconds minimize_timeout |
31236 | 82 |
val _ = |
36378 | 83 |
priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^ |
36224 | 84 |
" with a time limit of " ^ string_of_int msecs ^ " ms.") |
35969 | 85 |
val test_thms_fun = |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
86 |
sledgehammer_test_theorems params prover minimize_timeout i state |
31752
19a5f1c8a844
use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents:
31409
diff
changeset
|
87 |
fun test_thms filtered thms = |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
88 |
case test_thms_fun filtered thms of |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
89 |
(result as {outcome = NONE, ...}) => SOME result |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
90 |
| _ => NONE |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
91 |
|
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 *) |
|
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31236
diff
changeset
|
95 |
(case test_thms_fun NONE name_thms_pairs of |
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
96 |
result as {outcome = NONE, pool, internal_thm_names, conjecture_shape, |
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
97 |
filtered_clauses, ...} => |
31236 | 98 |
let |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
99 |
val used = internal_thm_names |> Vector.foldr (op ::) [] |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
100 |
|> sort_distinct string_ord |
31236 | 101 |
val to_use = |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
102 |
if length used < length name_thms_pairs then |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36382
diff
changeset
|
103 |
filter (fn (name1, _) => exists (curry (op =) name1) used) |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
104 |
name_thms_pairs |
33305 | 105 |
else name_thms_pairs |
36231
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36224
diff
changeset
|
106 |
val (min_thms, {proof, internal_thm_names, ...}) = |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
107 |
linear_minimize (test_thms (SOME filtered_clauses)) to_use |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
108 |
([], result) |
36481
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset
|
109 |
val m = length min_thms |
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset
|
110 |
val _ = priority (cat_lines |
36481
af99c98121d6
make Sledgehammer more friendly if no subgoal is left
blanchet
parents:
36402
diff
changeset
|
111 |
["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".") |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
112 |
in |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
113 |
(SOME min_thms, |
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36393
diff
changeset
|
114 |
proof_text isar_proof |
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37418
diff
changeset
|
115 |
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37418
diff
changeset
|
116 |
(full_types, K "", proof, internal_thm_names, goal, i) |> fst) |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
117 |
end |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
118 |
| {outcome = SOME TimedOut, ...} => |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
119 |
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \ |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
120 |
\option (e.g., \"timeout = " ^ |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
121 |
string_of_int (10 + msecs div 1000) ^ " s\").") |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
122 |
| {outcome = SOME UnknownError, ...} => |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
123 |
(* Failure sometimes mean timeout, unfortunately. *) |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
124 |
(NONE, "Failure: No proof was found with the current time limit. You \ |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
125 |
\can increase the time limit using the \"timeout\" \ |
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
126 |
\option (e.g., \"timeout = " ^ |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
127 |
string_of_int (10 + msecs div 1000) ^ " s\").") |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
128 |
| {message, ...} => (NONE, "ATP error: " ^ message)) |
37506
32a1ee39c49b
missing "Unsynchronized" + make exception take a unit
blanchet
parents:
37498
diff
changeset
|
129 |
handle TRIVIAL () => (SOME [], metis_line full_types i n []) |
36382 | 130 |
| ERROR msg => (NONE, "Error: " ^ msg) |
31236 | 131 |
end |
132 |
||
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
133 |
end; |