author  blanchet 
Thu, 28 Aug 2014 16:58:27 +0200  
changeset 58085  ee65e9cfe284 
parent 58061  3d060f43accb 
child 58494  ed380b9594b5 
permissions  rwrr 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.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 ATPspecific 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 

40977  5 
Minimization of fact list for Metis using external 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 

55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

8 
signature SLEDGEHAMMER_PROVER_MINIMIZE = 
32525  9 
sig 
46340  10 
type stature = ATP_Problem_Generate.stature 
55287  11 
type proof_method = Sledgehammer_Proof_Methods.proof_method 
12 
type play_outcome = Sledgehammer_Proof_Methods.play_outcome 

55201  13 
type mode = Sledgehammer_Prover.mode 
14 
type params = Sledgehammer_Prover.params 

15 
type prover = Sledgehammer_Prover.prover 

35867  16 

55205  17 
val is_prover_supported : Proof.context > string > bool 
18 
val is_prover_installed : Proof.context > string > bool 

19 
val default_max_facts_of_prover : Proof.context > string > int 

20 
val get_prover : Proof.context > mode > string > prover 

21 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42579
diff
changeset

22 
val binary_min_facts : int Config.T 
54824  23 
val minimize_facts : (thm list > unit) > string > params > bool > int > int > 
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset

24 
Proof.state > thm > ((string * stature) * thm list) list > 
57739  25 
((string * stature) * thm list) list option 
57750  26 
* ((unit > (string * stature) list * (proof_method * play_outcome)) > string) 
54503  27 
val get_minimizing_prover : Proof.context > mode > (thm list > unit) > string > prover 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

28 
end; 
32525  29 

55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

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

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

32 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

33 
open ATP_Util 
39496
a52a4e4399c1
got caught once again by SML's pattern maching (ctor vs. var)
blanchet
parents:
39491
diff
changeset

34 
open ATP_Proof 
46320  35 
open ATP_Problem_Generate 
55212  36 
open ATP_Proof_Reconstruct 
51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51191
diff
changeset

37 
open ATP_Systems 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset

38 
open Sledgehammer_Util 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

39 
open Sledgehammer_Fact 
55287  40 
open Sledgehammer_Proof_Methods 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

41 
open Sledgehammer_Isar 
55201  42 
open Sledgehammer_Prover 
55205  43 
open Sledgehammer_Prover_ATP 
58061  44 
open Sledgehammer_Prover_SMT 
55205  45 

46 
fun is_prover_supported ctxt = 

47 
let val thy = Proof_Context.theory_of ctxt in 

58061  48 
is_atp thy orf is_smt_prover ctxt 
55205  49 
end 
50 

51 
fun is_prover_installed ctxt = 

58061  52 
is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) 
55205  53 

54 
fun default_max_facts_of_prover ctxt name = 

55 
let val thy = Proof_Context.theory_of ctxt in 

57732  56 
if is_atp thy name then 
55205  57 
fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0 
58061  58 
else if is_smt_prover ctxt name then 
59 
SMT_Solver.default_max_relevant ctxt name 

56081  60 
else 
61 
error ("No such prover: " ^ name ^ ".") 

55205  62 
end 
63 

64 
fun get_prover ctxt mode name = 

65 
let val thy = Proof_Context.theory_of ctxt in 

57732  66 
if is_atp thy name then run_atp mode name 
58061  67 
else if is_smt_prover ctxt name then run_smt_solver mode name 
55205  68 
else error ("No such prover: " ^ name ^ ".") 
69 
end 

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

70 

36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

71 
(* wrapper for calling external prover *) 
31236  72 

40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

73 
fun n_facts names = 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

74 
let val n = length names in 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

75 
string_of_int n ^ " fact" ^ plural_s n ^ 
57781  76 
(if n > 0 then ": " ^ (names > map fst > sort string_ord > space_implode " ") else "") 
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset

77 
end 
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset

78 

41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset

79 
fun print silent f = if silent then () else Output.urgent_message (f ()) 
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset

80 

54824  81 
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, 
57245  82 
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, 
57673
858c1a63967f
don't lose 'minimize' flag before it reaches Isar proof text generation
blanchet
parents:
57245
diff
changeset

83 
minimize, preplay_timeout, ...} : params) 
54824  84 
silent (prover : prover) timeout i n state goal facts = 
31236  85 
let 
57054  86 
val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ 
87 
(if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") 

88 

51005
ce4290c33d73
eliminated needless speed optimization  and simplified code quite a bit
blanchet
parents:
50669
diff
changeset

89 
val facts = facts > maps (fn (n, ths) => map (pair n) ths) 
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset

90 
val params = 
53800  91 
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true, 
92 
provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, 

93 
uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, 

94 
max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), 

95 
max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, 

57245  96 
isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, 
57673
858c1a63967f
don't lose 'minimize' flag before it reaches Isar proof text generation
blanchet
parents:
57245
diff
changeset

97 
slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, 
57245  98 
expect = ""} 
40065  99 
val problem = 
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54130
diff
changeset

100 
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, 
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54130
diff
changeset

101 
factss = [("", facts)]} 
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57734
diff
changeset

102 
val result as {outcome, used_facts, run_time, ...} = prover params problem 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

103 
in 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

104 
print silent (fn () => 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

105 
(case outcome of 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

106 
SOME failure => string_of_atp_failure failure 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

107 
 NONE => 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

108 
"Found proof" ^ 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

109 
(if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^ 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

110 
" (" ^ string_of_time run_time ^ ").")); 
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset

111 
result 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset

112 
end 
31236  113 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40200
diff
changeset

114 
(* minimalization of facts *) 
31236  115 

45372  116 
(* Give the external prover some slack. The ATP gets further slack because the 
117 
Sledgehammer preprocessing time is included in the estimate below but isn't 

118 
part of the timeout. *) 

119 
val slack_msecs = 200 

120 

54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

121 
fun new_timeout timeout run_time = 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

122 
Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs) 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

123 
> Time.fromMilliseconds 
45372  124 

45367  125 
(* The linear algorithm usually outperforms the binary algorithm when over 60% 
126 
of the facts are actually needed. The binary algorithm is much more 

127 
appropriate for provers that cannot return the list of used facts and hence 

128 
returns all facts as used. Since we cannot know in advance how many facts are 

129 
actually needed, we heuristically set the threshold to 10 facts. *) 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42579
diff
changeset

130 
val binary_min_facts = 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

131 
Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts} (K 20) 
40977  132 

45368  133 
fun linear_minimize test timeout result xs = 
134 
let 

135 
fun min _ [] p = p 

136 
 min timeout (x :: xs) (seen, result) = 

54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

137 
(case test timeout (xs @ seen) of 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

138 
result as {outcome = NONE, used_facts, run_time, ...} : prover_result => 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

139 
min (new_timeout timeout run_time) (filter_used_facts true used_facts xs) 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

140 
(filter_used_facts false used_facts seen, result) 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

141 
 _ => min timeout xs (x :: seen, result)) 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

142 
in 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

143 
min timeout xs ([], result) 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

144 
end 
38015  145 

45368  146 
fun binary_minimize test timeout result xs = 
40977  147 
let 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

148 
fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) = 
41743  149 
let 
45367  150 
val (l0, r0) = chop (length xs div 2) xs 
41743  151 
(* 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

152 
val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup)) 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

153 
val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs)) 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

154 
val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0)) 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

155 
val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0)) 
41743  156 
*) 
45367  157 
val depth = depth + 1 
45372  158 
val timeout = new_timeout timeout run_time 
41743  159 
in 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

160 
(case test timeout (sup @ l0) of 
45372  161 
result as {outcome = NONE, used_facts, ...} => 
48798  162 
min depth result (filter_used_facts true used_facts sup) 
57781  163 
(filter_used_facts true used_facts l0) 
45367  164 
 _ => 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

165 
(case test timeout (sup @ r0) of 
45367  166 
result as {outcome = NONE, used_facts, ...} => 
48798  167 
min depth result (filter_used_facts true used_facts sup) 
57054  168 
(filter_used_facts true used_facts r0) 
45367  169 
 _ => 
170 
let 

171 
val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 

55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

172 
val (sup, r0) = (sup, r0) > pairself (filter_used_facts true (map fst sup_r0)) 
45367  173 
val (sup_l, (r, result)) = min depth result (sup @ l) r0 
48798  174 
val sup = sup > filter_used_facts true (map fst sup_l) 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

175 
in (sup, (l @ r, result)) end)) 
40977  176 
end 
41743  177 
(* 
178 
> tap (fn _ => warning (replicate_string depth " " ^ "}")) 

179 
*) 

45367  180 
 min _ result sup xs = (sup, (xs, result)) 
181 
in 

55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

182 
(case snd (min 0 result [] xs) of 
45372  183 
([x], result as {run_time, ...}) => 
184 
(case test (new_timeout timeout run_time) [] of 

55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

185 
result as {outcome = NONE, ...} => ([], result) 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

186 
 _ => ([x], result)) 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

187 
 p => p) 
45367  188 
end 
40977  189 

54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

190 
fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal 
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset

191 
facts = 
31236  192 
let 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40553
diff
changeset

193 
val ctxt = Proof.context_of state 
58085  194 
val prover = get_prover ctxt Minimize prover_name 
54130
b4e6cd4cab92
thread the goal through instead of relying on unreliable (possibly fake) state
blanchet
parents:
54127
diff
changeset

195 
fun test timeout = test_facts params silent prover timeout i n state goal 
48796
0f94b8b69e79
consider removing chained facts last, so that they're more likely to be kept
blanchet
parents:
48399
diff
changeset

196 
val (chained, non_chained) = List.partition is_fact_chained facts 
57054  197 
(* Push chained facts to the back, so that they are less likely to be kicked out by the linear 
198 
minimization algorithm. *) 

48796
0f94b8b69e79
consider removing chained facts last, so that they're more likely to be kept
blanchet
parents:
48399
diff
changeset

199 
val facts = non_chained @ chained 
31236  200 
in 
54815  201 
(print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ "."); 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

202 
(case test timeout facts of 
45371  203 
result as {outcome = NONE, used_facts, run_time, ...} => 
38015  204 
let 
48798  205 
val facts = filter_used_facts true used_facts facts 
45372  206 
val min = 
54815  207 
if length facts >= Config.get ctxt binary_min_facts then binary_minimize 
208 
else linear_minimize 

57738  209 
val (min_facts, {message, ...}) = min test (new_timeout timeout run_time) result facts 
48321  210 
in 
211 
print silent (fn () => cat_lines 

57750  212 
["Minimized to " ^ n_facts (map fst min_facts)] ^ 
213 
(case min_facts > filter is_fact_chained > length of 

214 
0 => "" 

215 
 n => "\n(including " ^ string_of_int n ^ " chained)") ^ "."); 

54503  216 
(if learn then do_learn (maps snd min_facts) else ()); 
57738  217 
(SOME min_facts, message) 
48321  218 
end 
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset

219 
 {outcome = SOME TimedOut, ...} => 
57738  220 
(NONE, fn _ => 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
54815
diff
changeset

221 
"Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ 
57738  222 
\timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").") 
223 
 {message, ...} => (NONE, (prefix "Prover error: " o message)))) 

224 
handle ERROR msg => (NONE, fn _ => "Error: " ^ msg) 

31236  225 
end 
226 

57732  227 
fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...}) 
55205  228 
({state, goal, subgoal, subgoal_count, ...} : prover_problem) 
57738  229 
(result as {outcome, used_facts, used_from, preferred_methss, run_time, message} 
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset

230 
: prover_result) = 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

231 
if is_some outcome orelse null used_facts then 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

232 
result 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

233 
else 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

234 
let 
57738  235 
val (used_facts, message) = 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

236 
if minimize then 
57732  237 
minimize_facts do_learn name params 
54824  238 
(not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state 
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset

239 
goal (filter_used_facts true used_facts (map (apsnd single) used_from)) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

240 
>> Option.map (map fst) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

241 
else 
57738  242 
(SOME used_facts, message) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

243 
in 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

244 
(case used_facts of 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

245 
SOME used_facts => 
57781  246 
{outcome = NONE, used_facts = sort_wrt fst used_facts, used_from = used_from, 
57738  247 
preferred_methss = preferred_methss, run_time = run_time, message = message} 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset

248 
 NONE => result) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

249 
end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

250 

57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57734
diff
changeset

251 
fun get_minimizing_prover ctxt mode do_learn name params problem = 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57734
diff
changeset

252 
get_prover ctxt mode name params problem 
57732  253 
> maybe_minimize mode do_learn name params problem 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset

254 

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

255 
end; 