author  blanchet 
Wed, 24 Mar 2010 14:49:32 +0100  
changeset 35969  c9565298df9e 
parent 35867  16279c4c7a33 
child 36063  cdc6855a6387 
permissions  rwrr 
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 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

12 
type 'a minimize_fun = ('a list > bool) > 'a list > 'a list 
35867  13 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

14 
val linear_minimize : 'a minimize_fun 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

15 
val binary_minimize : 'a minimize_fun 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

16 
val minimize_theorems : 
35969  17 
params > (string * thm list) minimize_fun > prover > string 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

18 
> Proof.state > (string * thm list) list 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

19 
> (string * thm list) list option * string 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

20 
end; 
32525  21 

35865  22 
structure ATP_Minimal : ATP_MINIMAL = 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

23 
struct 
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

24 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

25 
open Sledgehammer_Fact_Preprocessor 
35867  26 
open ATP_Manager 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

27 

513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

28 
type 'a minimize_fun = ('a list > bool) > 'a list > 'a list 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

29 

513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

30 
(* Linear minimization algorithm *) 
33492
4168294a9f96
Command atp_minimize uses the naive linear algorithm now
nipkow
parents:
33316
diff
changeset

31 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

32 
fun linear_minimize p s = 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

33 
let 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

34 
fun aux [] needed = needed 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

35 
 aux (x :: xs) needed = aux xs (needed > not (p (xs @ needed)) ? cons x) 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

36 
in aux s [] end; 
33492
4168294a9f96
Command atp_minimize uses the naive linear algorithm now
nipkow
parents:
33316
diff
changeset

37 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

38 
(* Binary minimalization *) 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

39 

31236  40 
local 
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

41 
fun isplit (l, r) [] = (l, r) 
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

42 
 isplit (l, r) [h] = (h :: l, r) 
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

43 
 isplit (l, r) (h1 :: h2 :: t) = isplit (h1 :: l, h2 :: r) t 
31236  44 
in 
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

45 
fun split lst = isplit ([], []) lst 
31236  46 
end 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

47 

31236  48 
local 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

49 
fun min _ _ [] = raise Empty 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

50 
 min _ _ [s0] = [s0] 
31236  51 
 min p sup s = 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

52 
let 
31236  53 
val (l0, r0) = split s 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

54 
in 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

55 
if p (sup @ l0) then 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

56 
min p sup l0 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

57 
else if p (sup @ r0) then 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

58 
min p sup r0 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

59 
else 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

60 
let 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

61 
val l = min p (sup @ r0) l0 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

62 
val r = min p (sup @ l) r0 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

63 
in l @ r 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 
*) 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

71 
fun binary_minimize p s = 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

72 
case min p [] s of 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

73 
[x] => if p [] then [] else [x] 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

74 
 m => m 
31236  75 
end 
76 

31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset

77 

31236  78 
(* failure check and producing answer *) 
79 

80 
datatype 'a prove_result = Success of 'a  Failure  Timeout  Error 

81 

82 
val string_of_result = 

83 
fn Success _ => "Success" 

84 
 Failure => "Failure" 

85 
 Timeout => "Timeout" 

86 
 Error => "Error" 

87 

88 
val failure_strings = 

89 
[("SPASS beiseite: Ran out of time.", Timeout), 

90 
("Timeout", Timeout), 

91 
("time limit exceeded", Timeout), 

92 
("# Cannot determine problem status within resource limit", Timeout), 

93 
("Error", Error)] 

94 

35867  95 
fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...} 
96 
: prover_result) = 

97 
if success then 

98 
(Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses), 

99 
proof) 

100 
else 

101 
let 

102 
val failure = failure_strings > get_first (fn (s, t) => 

103 
if String.isSubstring s proof then SOME (t, proof) else NONE) 

104 
in 

105 
(case failure of 

106 
SOME res => res 

107 
 NONE => (Failure, proof)) 

108 
end 

31236  109 

32936  110 

31236  111 
(* wrapper for calling external prover *) 
112 

35969  113 
fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover 
114 
timeout subgoalno state filtered name_thms_pairs = 

31236  115 
let 
35867  116 
val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ 
117 
" theorems... ") 

32525  118 
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

119 
val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
33492
diff
changeset

120 
val {context = ctxt, facts, goal} = Proof.goal state 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32937
diff
changeset

121 
val problem = 
35969  122 
{subgoal = subgoalno, goal = (ctxt, (facts, goal)), 
123 
relevance_override = {add = [], del = [], only = false}, 

124 
axiom_clauses = SOME axclauses, filtered_clauses = filtered} 

125 
val (result, proof) = produce_answer (prover params timeout problem) 

32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

126 
val _ = priority (string_of_result result) 
35867  127 
in (result, proof) end 
31236  128 

129 

130 
(* minimalization of thms *) 

131 

35969  132 
fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover 
133 
prover_name state name_thms_pairs = 

31236  134 
let 
35969  135 
val msecs = Time.toMilliseconds minimize_timeout 
31236  136 
val _ = 
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

137 
priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^ 
35969  138 
" theorems, ATP: " ^ prover_name ^ 
139 
", time limit: " ^ string_of_int msecs ^ " ms") 

140 
val test_thms_fun = 

141 
sledgehammer_test_theorems params prover minimize_timeout 1 state 

31752
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31409
diff
changeset

142 
fun test_thms filtered thms = 
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31409
diff
changeset

143 
case test_thms_fun filtered thms of (Success _, _) => true  _ => false 
31236  144 
in 
145 
(* 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

146 
(case test_thms_fun NONE name_thms_pairs of 
31752
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31409
diff
changeset

147 
(Success (used, filtered), _) => 
31236  148 
let 
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

149 
val ordered_used = sort_distinct string_ord used 
31236  150 
val to_use = 
151 
if length ordered_used < length name_thms_pairs then 

152 
filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs 

33305  153 
else name_thms_pairs 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

154 
val min_thms = 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

155 
if null to_use then [] 
33492
4168294a9f96
Command atp_minimize uses the naive linear algorithm now
nipkow
parents:
33316
diff
changeset

156 
else gen_min (test_thms (SOME filtered)) to_use 
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

157 
val min_names = sort_distinct string_ord (map fst min_thms) 
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

158 
val _ = priority (cat_lines 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

159 
["Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) 
31236  160 
in 
35969  161 
(SOME min_thms, 
162 
"Try this command: " ^ 

163 
Markup.markup Markup.sendback 

164 
("by (metis " ^ space_implode " " min_names ^ ")") 

165 
^ ".") 

31236  166 
end 
167 
 (Timeout, _) => 

32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

168 
(NONE, "Timeout: You may need to increase the time limit of " ^ 
35969  169 
string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".") 
31236  170 
 (Error, msg) => 
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

171 
(NONE, "Error in prover: " ^ msg) 
31236  172 
 (Failure, _) => 
32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

173 
(NONE, "Failure: No proof with the theorems supplied")) 
35865  174 
handle Sledgehammer_HOL_Clause.TRIVIAL => 
35969  175 
(SOME [], "Trivial: Try this command: " ^ 
176 
Markup.markup Markup.sendback "by metis" ^ ".") 

32947
3c19b98a35cd
ATP_Manager.get_prover: canonical argument order;
wenzelm
parents:
32942
diff
changeset

177 
 ERROR msg => (NONE, "Error: " ^ msg) 
31236  178 
end 
179 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

180 
end; 