author | wenzelm |
Wed, 23 Jul 2025 14:53:21 +0200 | |
changeset 82898 | 89da4dcd1fa8 |
parent 82620 | 2d854f1cd830 |
permissions | -rw-r--r-- |
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 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 |
|
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 |
|
75025 | 16 |
type prover_slice = Sledgehammer_Prover.prover_slice |
82205
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
17 |
type prover_result = Sledgehammer_Prover.prover_result |
35867 | 18 |
|
55205 | 19 |
val is_prover_supported : Proof.context -> string -> bool |
20 |
val is_prover_installed : Proof.context -> string -> bool |
|
21 |
val get_prover : Proof.context -> mode -> string -> prover |
|
75029 | 22 |
val get_slices : Proof.context -> string -> prover_slice list |
55205 | 23 |
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42579
diff
changeset
|
24 |
val binary_min_facts : int Config.T |
75431 | 25 |
val minimize_facts : (thm list -> unit) -> string -> params -> prover_slice -> bool -> int -> |
82205
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
26 |
int -> Proof.state -> thm -> ((string * stature) * thm list) list -> prover_result -> |
57739 | 27 |
((string * stature) * thm list) list option |
82620
2d854f1cd830
clarify Sledgehammer instantiations without preplay (dont_preplay option and tactic provers)
Lukas Bartl <lukas.bartl@uni-a.de>
parents:
82585
diff
changeset
|
28 |
* (((Pretty.T * stature) list * (proof_method * play_outcome)) option -> string) |
54503 | 29 |
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
|
30 |
end; |
32525 | 31 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
32 |
structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE = |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
33 |
struct |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
34 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset
|
35 |
open ATP_Util |
39496
a52a4e4399c1
got caught once again by SML's pattern maching (ctor vs. var)
blanchet
parents:
39491
diff
changeset
|
36 |
open ATP_Proof |
46320 | 37 |
open ATP_Problem_Generate |
55212 | 38 |
open ATP_Proof_Reconstruct |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
39 |
open Sledgehammer_Util |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
40 |
open Sledgehammer_Fact |
55287 | 41 |
open Sledgehammer_Proof_Methods |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
42 |
open Sledgehammer_Isar |
72400 | 43 |
open Sledgehammer_ATP_Systems |
55201 | 44 |
open Sledgehammer_Prover |
55205 | 45 |
open Sledgehammer_Prover_ATP |
58061 | 46 |
open Sledgehammer_Prover_SMT |
82202
a1f85f579a07
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna
parents:
81746
diff
changeset
|
47 |
open Sledgehammer_Prover_Tactic |
55205 | 48 |
|
49 |
fun is_prover_supported ctxt = |
|
82202
a1f85f579a07
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna
parents:
81746
diff
changeset
|
50 |
is_atp orf is_smt_solver ctxt orf is_tactic_prover |
55205 | 51 |
|
75036 | 52 |
fun is_prover_installed ctxt prover_name = |
53 |
if is_atp prover_name then |
|
54 |
let val thy = Proof_Context.theory_of ctxt in |
|
55 |
is_atp_installed thy prover_name |
|
56 |
end |
|
82202
a1f85f579a07
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna
parents:
81746
diff
changeset
|
57 |
else if is_smt_solver ctxt prover_name then |
a1f85f579a07
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna
parents:
81746
diff
changeset
|
58 |
is_smt_solver_installed ctxt prover_name |
75036 | 59 |
else |
82202
a1f85f579a07
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna
parents:
81746
diff
changeset
|
60 |
true |
55205 | 61 |
|
62 |
fun get_prover ctxt mode name = |
|
75036 | 63 |
if is_atp name then run_atp mode name |
82202
a1f85f579a07
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna
parents:
81746
diff
changeset
|
64 |
else if is_smt_solver ctxt name then run_smt_solver mode name |
a1f85f579a07
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna
parents:
81746
diff
changeset
|
65 |
else if is_tactic_prover name then run_tactic_prover mode name |
75036 | 66 |
else error ("No such prover: " ^ name) |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
67 |
|
75029 | 68 |
fun get_slices ctxt name = |
75025 | 69 |
let val thy = Proof_Context.theory_of ctxt in |
75036 | 70 |
if is_atp name then |
75063
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75036
diff
changeset
|
71 |
map (apsnd ATP_Slice) (#good_slices (get_atp thy name ()) ctxt) |
82202
a1f85f579a07
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna
parents:
81746
diff
changeset
|
72 |
else if is_smt_solver ctxt name then |
75063
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75036
diff
changeset
|
73 |
map (apsnd SMT_Slice) (SMT_Solver.good_slices ctxt name) |
82202
a1f85f579a07
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna
parents:
81746
diff
changeset
|
74 |
else if is_tactic_prover name then |
a1f85f579a07
initial work on Magnushammer-inspured tactic hammer (from Jasmin)
desharna
parents:
81746
diff
changeset
|
75 |
map (rpair No_Slice) (good_slices_of_tactic_prover name) |
75025 | 76 |
else |
77 |
error ("No such prover: " ^ name) |
|
78 |
end |
|
79 |
||
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
80 |
(* wrapper for calling external prover *) |
31236 | 81 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
82 |
fun n_facts names = |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
83 |
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
|
84 |
string_of_int n ^ " fact" ^ plural_s n ^ |
80910 | 85 |
(if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> implode_space) 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
|
86 |
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
|
87 |
|
58843 | 88 |
fun print silent f = if silent then () else writeln (f ()) |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
89 |
|
54824 | 90 |
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, |
57245 | 91 |
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, |
81746 | 92 |
instantiate, minimize, preplay_timeout, induction_rules, cache_dir, ...} : params) |
82205
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
93 |
((_, _, falsify, _, fact_filter), slice_extra) silent (prover : prover) timeout i n |
77428 | 94 |
state goal facts = |
31236 | 95 |
let |
57054 | 96 |
val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ |
97 |
(if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") |
|
98 |
||
51005
ce4290c33d73
eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents:
50669
diff
changeset
|
99 |
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
|
100 |
val params = |
61311
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
60924
diff
changeset
|
101 |
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, |
77428 | 102 |
type_enc = type_enc, abduce = SOME 0, falsify = SOME false, strict = strict, |
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
77269
diff
changeset
|
103 |
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false, |
77269
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
75664
diff
changeset
|
104 |
fact_filter = NONE, induction_rules = induction_rules, max_facts = SOME (length facts), |
73939
9231ea46e041
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents:
72400
diff
changeset
|
105 |
fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, |
75031 | 106 |
max_new_mono_instances = max_new_mono_instances, max_proofs = 1, |
107 |
isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, |
|
81746 | 108 |
instantiate = instantiate, minimize = minimize, slices = 1, timeout = timeout, |
81610 | 109 |
preplay_timeout = preplay_timeout, expect = "", cache_dir = cache_dir} |
40065 | 110 |
val problem = |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54130
diff
changeset
|
111 |
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
81610 | 112 |
factss = [("", facts)], has_already_found_something = K false, found_something = K (), |
113 |
memoize_fun_call = (fn f => f)} |
|
58654
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58494
diff
changeset
|
114 |
val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, |
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58494
diff
changeset
|
115 |
message} = |
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
77269
diff
changeset
|
116 |
prover params problem ((1, false, false, length facts, fact_filter), slice_extra) |
58654
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58494
diff
changeset
|
117 |
val result as {outcome, ...} = |
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58494
diff
changeset
|
118 |
if is_none outcome0 andalso |
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58494
diff
changeset
|
119 |
forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then |
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58494
diff
changeset
|
120 |
result0 |
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58494
diff
changeset
|
121 |
else |
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58494
diff
changeset
|
122 |
{outcome = SOME MaybeUnprovable, used_facts = [], used_from = used_from, |
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58494
diff
changeset
|
123 |
preferred_methss = preferred_methss, run_time = run_time, message = message} |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
124 |
in |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
125 |
print silent (fn () => |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
126 |
(case outcome of |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
127 |
SOME failure => string_of_atp_failure failure |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
128 |
| NONE => |
77428 | 129 |
"Found " ^ (if falsify then "falsification" else "proof") ^ |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
130 |
(if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^ |
63692 | 131 |
" (" ^ 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
|
132 |
result |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
133 |
end |
31236 | 134 |
|
45372 | 135 |
(* Give the external prover some slack. The ATP gets further slack because the |
136 |
Sledgehammer preprocessing time is included in the estimate below but isn't |
|
137 |
part of the timeout. *) |
|
138 |
val slack_msecs = 200 |
|
139 |
||
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
140 |
fun new_timeout timeout run_time = |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
141 |
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
|
142 |
|> Time.fromMilliseconds |
45372 | 143 |
|
45367 | 144 |
(* The linear algorithm usually outperforms the binary algorithm when over 60% |
145 |
of the facts are actually needed. The binary algorithm is much more |
|
146 |
appropriate for provers that cannot return the list of used facts and hence |
|
147 |
returns all facts as used. Since we cannot know in advance how many facts are |
|
82585
46591222e4fc
preserved facts order in Sledgehammer's linear minimizer
desharna
parents:
82205
diff
changeset
|
148 |
actually needed, we heuristically set the threshold. *) |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42579
diff
changeset
|
149 |
val binary_min_facts = |
69593 | 150 |
Attrib.setup_config_int \<^binding>\<open>sledgehammer_minimize_binary_min_facts\<close> (K 20) |
40977 | 151 |
|
45368 | 152 |
fun linear_minimize test timeout result xs = |
153 |
let |
|
154 |
fun min _ [] p = p |
|
155 |
| min timeout (x :: xs) (seen, result) = |
|
82585
46591222e4fc
preserved facts order in Sledgehammer's linear minimizer
desharna
parents:
82205
diff
changeset
|
156 |
(case test timeout (seen @ xs) of |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
157 |
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
|
158 |
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
|
159 |
(filter_used_facts false used_facts seen, result) |
82585
46591222e4fc
preserved facts order in Sledgehammer's linear minimizer
desharna
parents:
82205
diff
changeset
|
160 |
| _ => min timeout xs (seen @ [x], result)) |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
161 |
in |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
162 |
min timeout xs ([], result) |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
163 |
end |
38015 | 164 |
|
45368 | 165 |
fun binary_minimize test timeout result xs = |
40977 | 166 |
let |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
167 |
fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) = |
41743 | 168 |
let |
45367 | 169 |
val (l0, r0) = chop (length xs div 2) xs |
41743 | 170 |
(* |
80799 | 171 |
val _ = warning (Symbol.spaces depth ^ "{ " ^ "sup: " ^ n_facts (map fst sup)) |
172 |
val _ = warning (Symbol.spaces depth ^ " " ^ "xs: " ^ n_facts (map fst xs)) |
|
173 |
val _ = warning (Symbol.spaces depth ^ " " ^ "l0: " ^ n_facts (map fst l0)) |
|
174 |
val _ = warning (Symbol.spaces depth ^ " " ^ "r0: " ^ n_facts (map fst r0)) |
|
41743 | 175 |
*) |
45367 | 176 |
val depth = depth + 1 |
45372 | 177 |
val timeout = new_timeout timeout run_time |
41743 | 178 |
in |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
179 |
(case test timeout (sup @ l0) of |
45372 | 180 |
result as {outcome = NONE, used_facts, ...} => |
48798 | 181 |
min depth result (filter_used_facts true used_facts sup) |
57781 | 182 |
(filter_used_facts true used_facts l0) |
45367 | 183 |
| _ => |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
184 |
(case test timeout (sup @ r0) of |
45367 | 185 |
result as {outcome = NONE, used_facts, ...} => |
48798 | 186 |
min depth result (filter_used_facts true used_facts sup) |
57054 | 187 |
(filter_used_facts true used_facts r0) |
45367 | 188 |
| _ => |
189 |
let |
|
190 |
val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58843
diff
changeset
|
191 |
val (sup, r0) = (sup, r0) |> apply2 (filter_used_facts true (map fst sup_r0)) |
45367 | 192 |
val (sup_l, (r, result)) = min depth result (sup @ l) r0 |
48798 | 193 |
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
|
194 |
in (sup, (l @ r, result)) end)) |
40977 | 195 |
end |
41743 | 196 |
(* |
80799 | 197 |
|> tap (fn _ => warning (Symbol.spaces depth ^ "}")) |
41743 | 198 |
*) |
45367 | 199 |
| min _ result sup xs = (sup, (xs, result)) |
200 |
in |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
201 |
(case snd (min 0 result [] xs) of |
45372 | 202 |
([x], result as {run_time, ...}) => |
203 |
(case test (new_timeout timeout run_time) [] of |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
204 |
result as {outcome = NONE, ...} => ([], result) |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
205 |
| _ => ([x], result)) |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
206 |
| p => p) |
45367 | 207 |
end |
40977 | 208 |
|
75431 | 209 |
fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) slice silent i n state |
82205
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
210 |
goal facts result = |
31236 | 211 |
let |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40553
diff
changeset
|
212 |
val ctxt = Proof.context_of state |
58085 | 213 |
val prover = get_prover ctxt Minimize prover_name |
48796
0f94b8b69e79
consider removing chained facts last, so that they're more likely to be kept
blanchet
parents:
48399
diff
changeset
|
214 |
val (chained, non_chained) = List.partition is_fact_chained facts |
59355
533f6cfc04c0
don't minimize chained facts -- this leads to subtle failures, e.g. if a method succeeds without a chained fact but fails with it
blanchet
parents:
59058
diff
changeset
|
215 |
|
533f6cfc04c0
don't minimize chained facts -- this leads to subtle failures, e.g. if a method succeeds without a chained fact but fails with it
blanchet
parents:
59058
diff
changeset
|
216 |
fun test timeout non_chained = |
75025 | 217 |
test_facts params slice silent prover timeout i n state goal (chained @ non_chained) |
82205
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
218 |
|
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
219 |
fun minimize used_facts (result as {run_time, ...}) = |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
220 |
let |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
221 |
val non_chained = filter_used_facts true used_facts non_chained |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
222 |
val min = |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
223 |
if length non_chained >= Config.get ctxt binary_min_facts then binary_minimize |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
224 |
else linear_minimize |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
225 |
val (min_facts, {message, ...}) = |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
226 |
min test (new_timeout timeout run_time) result non_chained |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
227 |
val min_facts_and_chained = chained @ min_facts |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
228 |
in |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
229 |
print silent (fn () => cat_lines |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
230 |
["Minimized to " ^ n_facts (map fst min_facts)] ^ |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
231 |
(case length chained of |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
232 |
0 => "" |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
233 |
| n => " (plus " ^ string_of_int n ^ " chained)")); |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
234 |
(if learn then do_learn (maps snd min_facts_and_chained) else ()); |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
235 |
(SOME min_facts_and_chained, message) |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
236 |
end |
31236 | 237 |
in |
75020
b087610592b4
rationalized output for forthcoming slicing model
blanchet
parents:
75017
diff
changeset
|
238 |
(print silent (fn () => "Sledgehammer minimizer: " ^ prover_name); |
82205
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
239 |
if is_tactic_prover prover_name then |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
240 |
minimize (map fst facts) result |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
241 |
else |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
242 |
(case test timeout non_chained of |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
243 |
result as {outcome = NONE, used_facts, ...} => minimize used_facts result |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
244 |
| {outcome = SOME TimedOut, ...} => |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
245 |
(NONE, fn _ => |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
246 |
"Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
247 |
\timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")") |
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
248 |
| {message, ...} => (NONE, (prefix "Prover error: " o message)))) |
75664 | 249 |
handle ERROR msg => (NONE, fn _ => "Warning: " ^ msg) |
31236 | 250 |
end |
251 |
||
57732 | 252 |
fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...}) |
75431 | 253 |
({state, goal, subgoal, subgoal_count, ...} : prover_problem) slice |
57738 | 254 |
(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
|
255 |
: prover_result) = |
58494
ed380b9594b5
always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')
blanchet
parents:
58085
diff
changeset
|
256 |
if is_some outcome then |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
257 |
result |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
258 |
else |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
259 |
let |
57738 | 260 |
val (used_facts, message) = |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
261 |
if minimize then |
75431 | 262 |
minimize_facts do_learn name params slice |
54824 | 263 |
(not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state |
82205
1bfe383f69c0
don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)
desharna
parents:
82202
diff
changeset
|
264 |
goal (filter_used_facts true used_facts (map (apsnd single) used_from)) result |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
265 |
|>> Option.map (map fst) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
266 |
else |
57738 | 267 |
(SOME used_facts, message) |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
268 |
in |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
269 |
(case used_facts of |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
270 |
SOME used_facts => |
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
59355
diff
changeset
|
271 |
{outcome = NONE, used_facts = sort_by fst used_facts, used_from = used_from, |
57738 | 272 |
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
|
273 |
| NONE => result) |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
274 |
end |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
275 |
|
75025 | 276 |
fun get_minimizing_prover ctxt mode do_learn name params problem slice = |
277 |
get_prover ctxt mode name params problem slice |
|
75431 | 278 |
|> maybe_minimize mode do_learn name params problem slice |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
279 |
|
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
280 |
end; |