author | blanchet |
Mon, 19 Apr 2010 18:44:12 +0200 | |
changeset 36231 | bede2d49ba3b |
parent 36224 | 109dce8410d5 |
child 36232 | 4d425766a47f |
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 |
|
35867 | 4 |
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
|
5 |
*) |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
6 |
|
32525 | 7 |
signature ATP_MINIMAL = |
8 |
sig |
|
35969 | 9 |
type params = ATP_Manager.params |
35867 | 10 |
type prover = ATP_Manager.prover |
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 : |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
14 |
params -> prover -> string -> 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 |
|
35865 | 18 |
structure ATP_Minimal : ATP_MINIMAL = |
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 |
|
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
21 |
open Sledgehammer_Util |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
22 |
open Sledgehammer_Fact_Preprocessor |
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 |
35867 | 24 |
open ATP_Manager |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
25 |
|
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
26 |
(* Linear minimization algorithm *) |
33492
4168294a9f96
Command atp_minimize uses the naive linear algorithm now
nipkow
parents:
33316
diff
changeset
|
27 |
|
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
28 |
fun linear_minimize test s = |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
29 |
let |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
30 |
fun aux [] p = p |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
31 |
| aux (x :: xs) (needed, result) = |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
32 |
case test (xs @ needed) of |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
33 |
SOME result => aux xs (needed, result) |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
34 |
| NONE => aux xs (x :: needed, result) |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
35 |
in aux s end |
31236 | 36 |
|
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
37 |
|
31236 | 38 |
(* failure check and producing answer *) |
39 |
||
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
40 |
datatype outcome = Success | Failure | Timeout | Error |
31236 | 41 |
|
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
42 |
val string_of_outcome = |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
43 |
fn Success => "Success" |
31236 | 44 |
| Failure => "Failure" |
45 |
| Timeout => "Timeout" |
|
46 |
| Error => "Error" |
|
47 |
||
48 |
val failure_strings = |
|
49 |
[("SPASS beiseite: Ran out of time.", Timeout), |
|
50 |
("Timeout", Timeout), |
|
51 |
("time limit exceeded", Timeout), |
|
52 |
("# Cannot determine problem status within resource limit", Timeout), |
|
53 |
("Error", Error)] |
|
54 |
||
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
55 |
fun outcome_of_result (result as {success, proof, ...} : prover_result) = |
35867 | 56 |
if success then |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
57 |
Success |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
58 |
else case get_first (fn (s, outcome) => |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
59 |
if String.isSubstring s proof then SOME outcome |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
60 |
else NONE) failure_strings of |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
61 |
SOME outcome => outcome |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
62 |
| NONE => Failure |
32936 | 63 |
|
31236 | 64 |
(* wrapper for calling external prover *) |
65 |
||
35969 | 66 |
fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
67 |
timeout subgoal state filtered_clauses name_thms_pairs = |
31236 | 68 |
let |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
69 |
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
|
70 |
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
|
71 |
" theorem" ^ plural_s num_theorems ^ "...") |
32525 | 72 |
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
|
73 |
val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs |
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset
|
74 |
val {context = ctxt, facts, goal} = Proof.raw_goal state |
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32937
diff
changeset
|
75 |
val problem = |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
76 |
{subgoal = subgoal, goal = (ctxt, (facts, goal)), |
35969 | 77 |
relevance_override = {add = [], del = [], only = false}, |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
78 |
axiom_clauses = SOME axclauses, filtered_clauses = filtered_clauses} |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
79 |
in |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
80 |
`outcome_of_result (prover params timeout problem) |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
81 |
|>> tap (priority o string_of_outcome) |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
82 |
end |
31236 | 83 |
|
84 |
(* minimalization of thms *) |
|
85 |
||
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
86 |
fun minimize_theorems (params as {minimize_timeout, isar_proof, modulus, |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
87 |
sorts, ...}) |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
88 |
prover atp_name i state name_thms_pairs = |
31236 | 89 |
let |
35969 | 90 |
val msecs = Time.toMilliseconds minimize_timeout |
36224 | 91 |
val n = length name_thms_pairs |
31236 | 92 |
val _ = |
36224 | 93 |
priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^ |
94 |
" with a time limit of " ^ string_of_int msecs ^ " ms.") |
|
35969 | 95 |
val test_thms_fun = |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
96 |
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
|
97 |
fun test_thms filtered thms = |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
98 |
case test_thms_fun filtered thms of |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
99 |
(Success, result) => SOME result |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
100 |
| _ => NONE |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
101 |
|
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
102 |
val {context = ctxt, facts, goal} = Proof.goal state; |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
103 |
val n = Logic.count_prems (prop_of goal) |
31236 | 104 |
in |
105 |
(* 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
|
106 |
(case test_thms_fun NONE name_thms_pairs of |
36224 | 107 |
(Success, result as {internal_thm_names, filtered_clauses, ...}) => |
31236 | 108 |
let |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
109 |
val used = internal_thm_names |> Vector.foldr (op ::) [] |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
110 |
|> sort_distinct string_ord |
31236 | 111 |
val to_use = |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
112 |
if length used < length name_thms_pairs then |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
113 |
filter (fn (name1, _) => List.exists (curry (op =) name1) used) |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
114 |
name_thms_pairs |
33305 | 115 |
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
|
116 |
val (min_thms, {proof, internal_thm_names, ...}) = |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
117 |
linear_minimize (test_thms (SOME filtered_clauses)) to_use |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
118 |
([], result) |
36224 | 119 |
val n = length min_thms |
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset
|
120 |
val _ = priority (cat_lines |
36224 | 121 |
["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".") |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
122 |
in |
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
123 |
(SOME min_thms, |
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
|
124 |
proof_text isar_proof true modulus sorts atp_name proof |
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
|
125 |
internal_thm_names ctxt goal i |> fst) |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
126 |
end |
31236 | 127 |
| (Timeout, _) => |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
128 |
(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
|
129 |
\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
|
130 |
string_of_int (10 + msecs div 1000) ^ " s\").") |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
131 |
| (Error, {message, ...}) => (NONE, "ATP error: " ^ message) |
31236 | 132 |
| (Failure, _) => |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
133 |
(* 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
|
134 |
(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
|
135 |
\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
|
136 |
\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
|
137 |
string_of_int (10 + msecs div 1000) ^ " s\").")) |
35865 | 138 |
handle Sledgehammer_HOL_Clause.TRIVIAL => |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
139 |
(SOME [], metis_line i n []) |
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset
|
140 |
| ERROR msg => (NONE, "Error: " ^ msg) |
31236 | 141 |
end |
142 |
||
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
143 |
end; |