author | blanchet |
Wed, 18 Jul 2012 08:44:03 +0200 | |
changeset 48292 | 7fcee834c7f5 |
parent 48250 | 1065c307fafe |
child 48293 | 914ca0827804 |
permissions | -rw-r--r-- |
38988 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_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 |
|
38988 | 8 |
signature SLEDGEHAMMER_MINIMIZE = |
32525 | 9 |
sig |
46340 | 10 |
type stature = ATP_Problem_Generate.stature |
46320 | 11 |
type play = ATP_Proof_Reconstruct.play |
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
|
12 |
type mode = Sledgehammer_Provers.mode |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset
|
13 |
type params = Sledgehammer_Provers.params |
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
|
14 |
type prover = Sledgehammer_Provers.prover |
35867 | 15 |
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42579
diff
changeset
|
16 |
val binary_min_facts : int Config.T |
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
|
17 |
val auto_minimize_min_facts : int Config.T |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
18 |
val auto_minimize_max_time : real Config.T |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
19 |
val minimize_facts : |
43064
b6e61d22fa61
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43058
diff
changeset
|
20 |
string -> params -> bool -> int -> int -> Proof.state |
46340 | 21 |
-> ((string * stature) * thm list) list |
22 |
-> ((string * stature) * thm list) list option |
|
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset
|
23 |
* ((unit -> play) * (play -> string) * string) |
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
|
24 |
val get_minimizing_prover : Proof.context -> mode -> string -> prover |
38996 | 25 |
val run_minimize : |
26 |
params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit |
|
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
27 |
end; |
32525 | 28 |
|
38988 | 29 |
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
30 |
struct |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
31 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset
|
32 |
open ATP_Util |
39496
a52a4e4399c1
got caught once again by SML's pattern maching (ctor vs. var)
blanchet
parents:
39491
diff
changeset
|
33 |
open ATP_Proof |
46320 | 34 |
open ATP_Problem_Generate |
35 |
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
|
36 |
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
|
37 |
open Sledgehammer_Fact |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset
|
38 |
open Sledgehammer_Provers |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
39 |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
40 |
(* wrapper for calling external prover *) |
31236 | 41 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
42 |
fun n_facts names = |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
43 |
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
|
44 |
string_of_int n ^ " fact" ^ plural_s n ^ |
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
|
45 |
(if n > 0 then |
48085
ff5e900d7b1a
avoid dumping definitions several times in LEO-II proofs
blanchet
parents:
47531
diff
changeset
|
46 |
": " ^ (names |> map fst |> sort string_ord |> space_implode " ") |
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
|
47 |
else |
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
|
48 |
"") |
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
|
49 |
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
|
50 |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
51 |
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
|
52 |
|
42724
4d6bcf846759
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents:
42646
diff
changeset
|
53 |
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, |
46301 | 54 |
max_new_mono_instances, type_enc, strict, lam_trans, |
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46388
diff
changeset
|
55 |
uncurried_aliases, isar_proof, isar_shrink_factor, |
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46388
diff
changeset
|
56 |
preplay_timeout, ...} : params) |
43064
b6e61d22fa61
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43058
diff
changeset
|
57 |
silent (prover : prover) timeout i n state facts = |
31236 | 58 |
let |
41277
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
59 |
val _ = |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
60 |
print silent (fn () => |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
61 |
"Testing " ^ n_facts (map fst facts) ^ |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
62 |
(if verbose then " (timeout: " ^ string_from_time timeout ^ ")" |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset
|
63 |
else "") ^ "...") |
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
64 |
val {goal, ...} = Proof.goal state |
44463
c471a2b48fa1
make sure that all facts are passed to ATP from minimizer
blanchet
parents:
43630
diff
changeset
|
65 |
val facts = |
c471a2b48fa1
make sure that all facts are passed to ATP from minimizer
blanchet
parents:
43630
diff
changeset
|
66 |
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
67 |
val params = |
42060
889d767ce5f4
make Minimizer honor "verbose" and "debug" options better
blanchet
parents:
41824
diff
changeset
|
68 |
{debug = debug, verbose = verbose, overlord = overlord, blocking = true, |
46301 | 69 |
provers = provers, type_enc = type_enc, strict = strict, |
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46388
diff
changeset
|
70 |
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46388
diff
changeset
|
71 |
relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts), |
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46388
diff
changeset
|
72 |
max_mono_iters = max_mono_iters, |
42740
31334a7b109d
renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents:
42724
diff
changeset
|
73 |
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
45706 | 74 |
isar_shrink_factor = isar_shrink_factor, slice = false, |
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
75 |
minimize = SOME false, timeout = timeout, |
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
76 |
preplay_timeout = preplay_timeout, expect = ""} |
40065 | 77 |
val problem = |
78 |
{state = state, goal = goal, subgoal = i, subgoal_count = n, |
|
47531
7fe7c7419489
get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
blanchet
parents:
46409
diff
changeset
|
79 |
facts = facts} |
45370
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
80 |
val result as {outcome, used_facts, run_time, ...} = |
45520 | 81 |
prover params (K (K (K ""))) problem |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
82 |
in |
43259
30c141dc22d6
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
blanchet
parents:
43166
diff
changeset
|
83 |
print silent |
30c141dc22d6
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
blanchet
parents:
43166
diff
changeset
|
84 |
(fn () => |
30c141dc22d6
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
blanchet
parents:
43166
diff
changeset
|
85 |
case outcome of |
30c141dc22d6
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
blanchet
parents:
43166
diff
changeset
|
86 |
SOME failure => string_for_failure failure |
30c141dc22d6
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
blanchet
parents:
43166
diff
changeset
|
87 |
| NONE => |
30c141dc22d6
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
blanchet
parents:
43166
diff
changeset
|
88 |
"Found proof" ^ |
30c141dc22d6
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
blanchet
parents:
43166
diff
changeset
|
89 |
(if length used_facts = length facts then "" |
45370
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
90 |
else " with " ^ n_facts used_facts) ^ |
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
91 |
" (" ^ string_from_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
|
92 |
result |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
93 |
end |
31236 | 94 |
|
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
95 |
(* minimalization of facts *) |
31236 | 96 |
|
45372 | 97 |
(* Give the external prover some slack. The ATP gets further slack because the |
98 |
Sledgehammer preprocessing time is included in the estimate below but isn't |
|
99 |
part of the timeout. *) |
|
100 |
val slack_msecs = 200 |
|
101 |
||
102 |
fun new_timeout timeout run_time = |
|
103 |
Int.min (Time.toMilliseconds timeout, |
|
104 |
Time.toMilliseconds run_time + slack_msecs) |
|
105 |
|> Time.fromMilliseconds |
|
106 |
||
45367 | 107 |
(* The linear algorithm usually outperforms the binary algorithm when over 60% |
108 |
of the facts are actually needed. The binary algorithm is much more |
|
109 |
appropriate for provers that cannot return the list of used facts and hence |
|
110 |
returns all facts as used. Since we cannot know in advance how many facts are |
|
111 |
actually needed, we heuristically set the threshold to 10 facts. *) |
|
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42579
diff
changeset
|
112 |
val binary_min_facts = |
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42579
diff
changeset
|
113 |
Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts} |
45368 | 114 |
(K 20) |
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
|
115 |
val auto_minimize_min_facts = |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
116 |
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
117 |
(fn generic => Config.get_generic generic binary_min_facts) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
118 |
val auto_minimize_max_time = |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
119 |
Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
120 |
(K 5.0) |
40977 | 121 |
|
45368 | 122 |
fun linear_minimize test timeout result xs = |
123 |
let |
|
124 |
fun min _ [] p = p |
|
125 |
| min timeout (x :: xs) (seen, result) = |
|
126 |
case test timeout (xs @ seen) of |
|
45372 | 127 |
result as {outcome = NONE, used_facts, run_time, ...} |
128 |
: prover_result => |
|
129 |
min (new_timeout timeout run_time) (filter_used_facts used_facts xs) |
|
130 |
(filter_used_facts used_facts seen, result) |
|
45368 | 131 |
| _ => min timeout xs (x :: seen, result) |
132 |
in min timeout xs ([], result) end |
|
38015 | 133 |
|
45368 | 134 |
fun binary_minimize test timeout result xs = |
40977 | 135 |
let |
45372 | 136 |
fun min depth (result as {run_time, ...} : prover_result) sup |
137 |
(xs as _ :: _ :: _) = |
|
41743 | 138 |
let |
45367 | 139 |
val (l0, r0) = chop (length xs div 2) xs |
41743 | 140 |
(* |
45366
4339763edd55
speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
blanchet
parents:
44463
diff
changeset
|
141 |
val _ = warning (replicate_string depth " " ^ "{ " ^ |
4339763edd55
speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
blanchet
parents:
44463
diff
changeset
|
142 |
"sup: " ^ n_facts (map fst sup)) |
4339763edd55
speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
blanchet
parents:
44463
diff
changeset
|
143 |
val _ = warning (replicate_string depth " " ^ " " ^ |
4339763edd55
speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
blanchet
parents:
44463
diff
changeset
|
144 |
"xs: " ^ n_facts (map fst xs)) |
4339763edd55
speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
blanchet
parents:
44463
diff
changeset
|
145 |
val _ = warning (replicate_string depth " " ^ " " ^ |
4339763edd55
speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
blanchet
parents:
44463
diff
changeset
|
146 |
"l0: " ^ n_facts (map fst l0)) |
4339763edd55
speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
blanchet
parents:
44463
diff
changeset
|
147 |
val _ = warning (replicate_string depth " " ^ " " ^ |
4339763edd55
speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
blanchet
parents:
44463
diff
changeset
|
148 |
"r0: " ^ n_facts (map fst r0)) |
41743 | 149 |
*) |
45367 | 150 |
val depth = depth + 1 |
45372 | 151 |
val timeout = new_timeout timeout run_time |
41743 | 152 |
in |
45368 | 153 |
case test timeout (sup @ l0) of |
45372 | 154 |
result as {outcome = NONE, used_facts, ...} => |
45367 | 155 |
min depth result (filter_used_facts used_facts sup) |
156 |
(filter_used_facts used_facts l0) |
|
157 |
| _ => |
|
45368 | 158 |
case test timeout (sup @ r0) of |
45367 | 159 |
result as {outcome = NONE, used_facts, ...} => |
160 |
min depth result (filter_used_facts used_facts sup) |
|
161 |
(filter_used_facts used_facts r0) |
|
162 |
| _ => |
|
163 |
let |
|
164 |
val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 |
|
165 |
val (sup, r0) = |
|
166 |
(sup, r0) |> pairself (filter_used_facts (map fst sup_r0)) |
|
167 |
val (sup_l, (r, result)) = min depth result (sup @ l) r0 |
|
168 |
val sup = sup |> filter_used_facts (map fst sup_l) |
|
169 |
in (sup, (l @ r, result)) end |
|
40977 | 170 |
end |
41743 | 171 |
(* |
172 |
|> tap (fn _ => warning (replicate_string depth " " ^ "}")) |
|
173 |
*) |
|
45367 | 174 |
| min _ result sup xs = (sup, (xs, result)) |
175 |
in |
|
176 |
case snd (min 0 result [] xs) of |
|
45372 | 177 |
([x], result as {run_time, ...}) => |
178 |
(case test (new_timeout timeout run_time) [] of |
|
45367 | 179 |
result as {outcome = NONE, ...} => ([], result) |
180 |
| _ => ([x], result)) |
|
181 |
| p => p |
|
182 |
end |
|
40977 | 183 |
|
43064
b6e61d22fa61
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43058
diff
changeset
|
184 |
fun minimize_facts prover_name (params as {timeout, ...}) silent i n state |
b6e61d22fa61
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43058
diff
changeset
|
185 |
facts = |
31236 | 186 |
let |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40553
diff
changeset
|
187 |
val ctxt = Proof.context_of state |
45574 | 188 |
val prover = |
189 |
get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name |
|
43058
5f8bac7a2945
minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents:
43052
diff
changeset
|
190 |
val _ = print silent (fn () => "Sledgehammer minimizer: " ^ |
40977 | 191 |
quote prover_name ^ ".") |
45368 | 192 |
fun test timeout = test_facts params silent prover timeout i n state |
31236 | 193 |
in |
45368 | 194 |
(case test timeout facts of |
45371 | 195 |
result as {outcome = NONE, used_facts, run_time, ...} => |
38015 | 196 |
let |
40977 | 197 |
val facts = filter_used_facts used_facts facts |
45372 | 198 |
val min = |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42579
diff
changeset
|
199 |
if length facts >= Config.get ctxt binary_min_facts then |
45368 | 200 |
binary_minimize |
40977 | 201 |
else |
45368 | 202 |
linear_minimize |
203 |
val (min_facts, {preplay, message, message_tail, ...}) = |
|
45371 | 204 |
min test (new_timeout timeout run_time) result facts |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
205 |
val _ = print silent (fn () => cat_lines |
43630 | 206 |
["Minimized to " ^ n_facts (map fst min_facts)] ^ |
46340 | 207 |
(case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained) |
208 |
|> length of |
|
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
209 |
0 => "" |
43577 | 210 |
| n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".") |
211 |
in (SOME min_facts, (preplay, message, message_tail)) end |
|
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
212 |
| {outcome = SOME TimedOut, preplay, ...} => |
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
213 |
(NONE, |
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
214 |
(preplay, |
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
215 |
fn _ => "Timeout: You can increase the time limit using the \ |
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
216 |
\\"timeout\" option (e.g., \"timeout = " ^ |
45371 | 217 |
string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ |
218 |
"\").", |
|
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset
|
219 |
"")) |
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
220 |
| {preplay, message, ...} => |
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset
|
221 |
(NONE, (preplay, prefix "Prover error: " o message, ""))) |
43166 | 222 |
handle ERROR msg => |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
223 |
(NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, "")) |
31236 | 224 |
end |
225 |
||
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
|
226 |
fun adjust_reconstructor_params override_params |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
227 |
({debug, verbose, overlord, blocking, provers, type_enc, strict, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
228 |
lam_trans, uncurried_aliases, relevance_thresholds, max_relevant, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
229 |
max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
230 |
slice, minimize, timeout, preplay_timeout, expect} : params) = |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
231 |
let |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
232 |
fun lookup_override name default_value = |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
233 |
case AList.lookup (op =) override_params name of |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
234 |
SOME [s] => SOME s |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
235 |
| _ => default_value |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
236 |
(* Only those options that reconstructors are interested in are considered |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
237 |
here. *) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
238 |
val type_enc = lookup_override "type_enc" type_enc |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
239 |
val lam_trans = lookup_override "lam_trans" lam_trans |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
240 |
in |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
241 |
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
242 |
provers = provers, type_enc = type_enc, strict = strict, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
243 |
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
244 |
max_relevant = max_relevant, relevance_thresholds = relevance_thresholds, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
245 |
max_mono_iters = max_mono_iters, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
246 |
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
247 |
isar_shrink_factor = isar_shrink_factor, slice = slice, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
248 |
minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
249 |
expect = expect} |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
250 |
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
|
251 |
|
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
252 |
fun minimize ctxt mode name |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
253 |
(params as {debug, verbose, isar_proof, minimize, ...}) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
254 |
({state, subgoal, subgoal_count, facts, ...} : prover_problem) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
255 |
(result as {outcome, used_facts, run_time, preplay, message, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
256 |
message_tail} : prover_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
|
257 |
if is_some outcome orelse null used_facts then |
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 |
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
|
259 |
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
|
260 |
let |
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 |
val num_facts = length used_facts |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
262 |
val ((perhaps_minimize, (minimize_name, params)), preplay) = |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
263 |
if mode = Normal then |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
264 |
if num_facts >= Config.get ctxt auto_minimize_min_facts then |
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 |
((true, (name, params)), preplay) |
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 |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
267 |
let |
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 |
fun can_min_fast_enough time = |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
269 |
0.001 |
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 |
* Real.fromInt ((num_facts + 1) * Time.toMilliseconds time) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
271 |
<= Config.get ctxt auto_minimize_max_time |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
272 |
fun prover_fast_enough () = can_min_fast_enough run_time |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
273 |
in |
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 |
if isar_proof then |
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 |
((prover_fast_enough (), (name, params)), preplay) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
276 |
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
|
277 |
let val preplay = preplay () in |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
278 |
(case preplay of |
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 |
Played (reconstr, timeout) => |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
280 |
if can_min_fast_enough timeout then |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
281 |
(true, extract_reconstructor params reconstr |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
282 |
||> (fn override_params => |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
283 |
adjust_reconstructor_params |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
284 |
override_params params)) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
285 |
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
|
286 |
(prover_fast_enough (), (name, params)) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
287 |
| _ => (prover_fast_enough (), (name, params)), |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
288 |
K preplay) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
289 |
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
|
290 |
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
|
291 |
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
|
292 |
((false, (name, params)), preplay) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
293 |
val minimize = minimize |> the_default perhaps_minimize |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
294 |
val (used_facts, (preplay, message, _)) = |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
295 |
if minimize then |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
296 |
minimize_facts minimize_name params (not verbose) subgoal |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
297 |
subgoal_count state |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
298 |
(filter_used_facts used_facts |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
299 |
(map (apsnd single o untranslated_fact) facts)) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
300 |
|>> 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
|
301 |
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
|
302 |
(SOME used_facts, (preplay, message, "")) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
303 |
in |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
304 |
case used_facts of |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
305 |
SOME used_facts => |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
306 |
(if debug andalso not (null used_facts) then |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
307 |
facts ~~ (0 upto length facts - 1) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
308 |
|> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j)) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
309 |
|> filter_used_facts used_facts |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
310 |
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
311 |
|> commas |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
312 |
|> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
313 |
" proof (of " ^ string_of_int (length facts) ^ "): ") "." |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
314 |
|> Output.urgent_message |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
315 |
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
|
316 |
(); |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
317 |
{outcome = NONE, used_facts = used_facts, run_time = run_time, |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
318 |
preplay = preplay, message = message, message_tail = message_tail}) |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
319 |
| NONE => 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
|
320 |
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
|
321 |
|
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
322 |
fun get_minimizing_prover ctxt mode name params minimize_command problem = |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
323 |
get_prover ctxt mode name params minimize_command problem |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
324 |
|> minimize ctxt mode name params problem |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48085
diff
changeset
|
325 |
|
41265
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
326 |
fun run_minimize (params as {provers, ...}) i refs state = |
38045 | 327 |
let |
328 |
val ctxt = Proof.context_of state |
|
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38617
diff
changeset
|
329 |
val reserved = reserved_isar_keyword_table () |
48292 | 330 |
val chained_ths = #facts (Proof.goal state) |
46388 | 331 |
val css_table = clasimpset_rule_table_of ctxt |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
332 |
val facts = |
46388 | 333 |
refs |> maps (map (apsnd single) |
334 |
o fact_from_ref ctxt reserved chained_ths css_table) |
|
38045 | 335 |
in |
336 |
case subgoal_count state of |
|
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
337 |
0 => Output.urgent_message "No subgoal!" |
41265
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
338 |
| n => case provers of |
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
339 |
[] => error "No prover is set." |
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
340 |
| prover :: _ => |
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
341 |
(kill_provers (); |
43064
b6e61d22fa61
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43058
diff
changeset
|
342 |
minimize_facts prover params false i n state facts |
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset
|
343 |
|> (fn (_, (preplay, message, message_tail)) => |
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset
|
344 |
message (preplay ()) ^ message_tail |
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43259
diff
changeset
|
345 |
|> Output.urgent_message)) |
38045 | 346 |
end |
347 |
||
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
348 |
end; |