author | blanchet |
Thu, 13 Feb 2014 13:16:17 +0100 | |
changeset 55452 | 29ec8680e61f |
parent 55345 | 8a53ee72e595 |
child 55453 | 0b070d098d1a |
permissions | -rw-r--r-- |
55201 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover.ML |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
2 |
Author: Fabian Immler, TU Muenchen |
32996
d2e48879e65a
removed disjunctive group cancellation -- provers run independently;
wenzelm
parents:
32995
diff
changeset
|
3 |
Author: Makarius |
35969 | 4 |
Author: Jasmin Blanchette, TU Muenchen |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
5 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
6 |
Generic prover abstraction for Sledgehammer. |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
7 |
*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
8 |
|
55201 | 9 |
signature SLEDGEHAMMER_PROVER = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
10 |
sig |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53551
diff
changeset
|
11 |
type atp_failure = ATP_Proof.atp_failure |
46340 | 12 |
type stature = ATP_Problem_Generate.stature |
46320 | 13 |
type type_enc = ATP_Problem_Generate.type_enc |
51005
ce4290c33d73
eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents:
50927
diff
changeset
|
14 |
type fact = Sledgehammer_Fact.fact |
55287 | 15 |
type proof_method = Sledgehammer_Proof_Methods.proof_method |
16 |
type play_outcome = Sledgehammer_Proof_Methods.play_outcome |
|
17 |
type minimize_command = Sledgehammer_Proof_Methods.minimize_command |
|
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
18 |
|
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
19 |
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize |
43021 | 20 |
|
35969 | 21 |
type params = |
48321 | 22 |
{debug : bool, |
23 |
verbose : bool, |
|
24 |
overlord : bool, |
|
53800 | 25 |
spy : bool, |
48321 | 26 |
blocking : bool, |
27 |
provers : string list, |
|
28 |
type_enc : string option, |
|
29 |
strict : bool, |
|
30 |
lam_trans : string option, |
|
31 |
uncurried_aliases : bool option, |
|
32 |
learn : bool, |
|
33 |
fact_filter : string option, |
|
34 |
max_facts : int option, |
|
35 |
fact_thresholds : real * real, |
|
36 |
max_mono_iters : int option, |
|
37 |
max_new_mono_instances : int option, |
|
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51186
diff
changeset
|
38 |
isar_proofs : bool option, |
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55170
diff
changeset
|
39 |
compress_isar : real, |
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55170
diff
changeset
|
40 |
try0_isar : bool, |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset
|
41 |
smt_proofs : bool option, |
48321 | 42 |
slice : bool, |
43 |
minimize : bool option, |
|
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
44 |
timeout : Time.time, |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
45 |
preplay_timeout : Time.time, |
48321 | 46 |
expect : string} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
47 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
48 |
type prover_problem = |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
49 |
{comment : string, |
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
50 |
state : Proof.state, |
48321 | 51 |
goal : thm, |
52 |
subgoal : int, |
|
53 |
subgoal_count : int, |
|
51010 | 54 |
factss : (string * fact list) list} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
55 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
56 |
type prover_result = |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53551
diff
changeset
|
57 |
{outcome : atp_failure option, |
51009
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51007
diff
changeset
|
58 |
used_facts : (string * stature) list, |
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51007
diff
changeset
|
59 |
used_from : fact list, |
48321 | 60 |
run_time : Time.time, |
55285 | 61 |
preplay : (proof_method * play_outcome) Lazy.lazy, |
62 |
message : proof_method * play_outcome -> string, |
|
48321 | 63 |
message_tail : string} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
64 |
|
43051 | 65 |
type prover = |
45520 | 66 |
params -> ((string * string list) list -> string -> minimize_command) |
67 |
-> prover_problem -> prover_result |
|
35867 | 68 |
|
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset
|
69 |
val SledgehammerN : string |
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55308
diff
changeset
|
70 |
val smtN : string |
55205 | 71 |
val overlord_file_location_of_prover : string -> string * string |
72 |
val proof_banner : mode -> string -> string |
|
55285 | 73 |
val extract_proof_method : params -> proof_method -> string * (string * string list) list |
74 |
val is_proof_method : string -> bool |
|
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
75 |
val is_atp : theory -> string -> bool |
55288
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset
|
76 |
val bunch_of_proof_methods : bool -> bool -> string -> proof_method list |
48798 | 77 |
val is_fact_chained : (('a * stature) * 'b) -> bool |
78 |
val filter_used_facts : |
|
79 |
bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> |
|
80 |
((''a * stature) * 'b) list |
|
55452
29ec8680e61f
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
blanchet
parents:
55345
diff
changeset
|
81 |
val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list -> |
55285 | 82 |
Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome |
55205 | 83 |
val remotify_atp_if_not_installed : theory -> string -> string option |
84 |
val isar_supported_prover_of : theory -> string -> string |
|
85 |
val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) -> |
|
55285 | 86 |
string -> proof_method * play_outcome -> 'a |
55205 | 87 |
val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> |
88 |
Proof.context |
|
55212 | 89 |
|
90 |
val supported_provers : Proof.context -> unit |
|
91 |
val kill_provers : unit -> unit |
|
92 |
val running_provers : unit -> unit |
|
93 |
val messages : int option -> unit |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
94 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
95 |
|
55201 | 96 |
structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
97 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
98 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43063
diff
changeset
|
99 |
open ATP_Util |
38028 | 100 |
open ATP_Problem |
101 |
open ATP_Systems |
|
46320 | 102 |
open ATP_Problem_Generate |
103 |
open ATP_Proof_Reconstruct |
|
45521 | 104 |
open Metis_Tactic |
51005
ce4290c33d73
eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents:
50927
diff
changeset
|
105 |
open Sledgehammer_Fact |
55287 | 106 |
open Sledgehammer_Proof_Methods |
54000
9cfff7f61d0d
added experimental configuration options to tune use of builtin symbols in SMT
blanchet
parents:
53989
diff
changeset
|
107 |
|
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
108 |
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize |
43021 | 109 |
|
45376 | 110 |
(* Identifier that distinguishes Sledgehammer from other tools that could use |
38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset
|
111 |
"Async_Manager". *) |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset
|
112 |
val SledgehammerN = "Sledgehammer" |
37585 | 113 |
|
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55308
diff
changeset
|
114 |
val smtN = "smt" |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55308
diff
changeset
|
115 |
|
55285 | 116 |
val proof_method_names = [metisN, smtN] |
117 |
val is_proof_method = member (op =) proof_method_names |
|
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43226
diff
changeset
|
118 |
|
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
119 |
val is_atp = member (op =) o supported_atps |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
120 |
|
55205 | 121 |
fun remotify_atp_if_supported_and_not_already_remote thy name = |
51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset
|
122 |
if String.isPrefix remote_prefix name then |
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset
|
123 |
SOME name |
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset
|
124 |
else |
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset
|
125 |
let val remote_name = remote_prefix ^ name in |
55205 | 126 |
if is_atp thy remote_name then SOME remote_name else NONE |
51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset
|
127 |
end |
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset
|
128 |
|
55205 | 129 |
fun remotify_atp_if_not_installed thy name = |
55207 | 130 |
if is_atp thy name andalso is_atp_installed thy name then SOME name |
55205 | 131 |
else remotify_atp_if_supported_and_not_already_remote thy name |
40063
d086e3699e78
bring ATPs and SMT solvers more in line with each other
blanchet
parents:
40062
diff
changeset
|
132 |
|
35969 | 133 |
type params = |
48321 | 134 |
{debug : bool, |
135 |
verbose : bool, |
|
136 |
overlord : bool, |
|
53800 | 137 |
spy : bool, |
48321 | 138 |
blocking : bool, |
139 |
provers : string list, |
|
140 |
type_enc : string option, |
|
141 |
strict : bool, |
|
142 |
lam_trans : string option, |
|
143 |
uncurried_aliases : bool option, |
|
144 |
learn : bool, |
|
145 |
fact_filter : string option, |
|
146 |
max_facts : int option, |
|
147 |
fact_thresholds : real * real, |
|
148 |
max_mono_iters : int option, |
|
149 |
max_new_mono_instances : int option, |
|
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51186
diff
changeset
|
150 |
isar_proofs : bool option, |
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55170
diff
changeset
|
151 |
compress_isar : real, |
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55170
diff
changeset
|
152 |
try0_isar : bool, |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset
|
153 |
smt_proofs : bool option, |
48321 | 154 |
slice : bool, |
155 |
minimize : bool option, |
|
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
156 |
timeout : Time.time, |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
157 |
preplay_timeout : Time.time, |
48321 | 158 |
expect : string} |
35867 | 159 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
160 |
type prover_problem = |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
161 |
{comment : string, |
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
162 |
state : Proof.state, |
48321 | 163 |
goal : thm, |
164 |
subgoal : int, |
|
165 |
subgoal_count : int, |
|
51010 | 166 |
factss : (string * fact list) list} |
35867 | 167 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
168 |
type prover_result = |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53551
diff
changeset
|
169 |
{outcome : atp_failure option, |
48321 | 170 |
used_facts : (string * stature) list, |
51009
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51007
diff
changeset
|
171 |
used_from : fact list, |
48321 | 172 |
run_time : Time.time, |
55285 | 173 |
preplay : (proof_method * play_outcome) Lazy.lazy, |
174 |
message : proof_method * play_outcome -> string, |
|
48321 | 175 |
message_tail : string} |
35867 | 176 |
|
43051 | 177 |
type prover = |
45520 | 178 |
params -> ((string * string list) list -> string -> minimize_command) |
179 |
-> prover_problem -> prover_result |
|
35867 | 180 |
|
55205 | 181 |
fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) |
41313
a96ac4d180b7
optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents:
41259
diff
changeset
|
182 |
|
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
183 |
fun proof_banner mode name = |
55205 | 184 |
(case mode of |
43033 | 185 |
Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" |
186 |
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof" |
|
55205 | 187 |
| _ => "Try this") |
43033 | 188 |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset
|
189 |
fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans = |
55288
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset
|
190 |
(if needs_full_types then |
55345 | 191 |
[Metis_Method (SOME full_typesN, NONE), |
55288
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset
|
192 |
Metis_Method (SOME really_full_type_enc, NONE), |
55345 | 193 |
Metis_Method (SOME full_typesN, SOME desperate_lam_trans), |
194 |
Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] |
|
55288
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset
|
195 |
else |
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset
|
196 |
[Metis_Method (NONE, NONE), |
55345 | 197 |
Metis_Method (SOME full_typesN, NONE), |
198 |
Metis_Method (SOME no_typesN, SOME desperate_lam_trans), |
|
199 |
Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @ |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset
|
200 |
(if smt_proofs then [SMT_Method] else []) |
45561
57227eedce81
don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset
|
201 |
|
55285 | 202 |
fun extract_proof_method ({type_enc, lam_trans, ...} : params) |
203 |
(Metis_Method (type_enc', lam_trans')) = |
|
45561
57227eedce81
don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset
|
204 |
let |
57227eedce81
don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset
|
205 |
val override_params = |
55285 | 206 |
(if is_none type_enc' andalso is_none type_enc then [] |
207 |
else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @ |
|
208 |
(if is_none lam_trans' andalso is_none lam_trans then [] |
|
209 |
else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])]) |
|
45561
57227eedce81
don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset
|
210 |
in (metisN, override_params) end |
55285 | 211 |
| extract_proof_method _ SMT_Method = (smtN, []) |
45561
57227eedce81
don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45560
diff
changeset
|
212 |
|
43033 | 213 |
(* based on "Mirabelle.can_apply" and generalized *) |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset
|
214 |
fun timed_apply timeout tac state i = |
43033 | 215 |
let |
216 |
val {context = ctxt, facts, goal} = Proof.goal state |
|
217 |
val full_tac = Method.insert_tac facts i THEN tac ctxt i |
|
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
218 |
in |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
219 |
TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
220 |
end |
43033 | 221 |
|
55452
29ec8680e61f
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
blanchet
parents:
55345
diff
changeset
|
222 |
fun timed_proof_method debug timeout ths meth = |
29ec8680e61f
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
blanchet
parents:
55345
diff
changeset
|
223 |
timed_apply timeout (fn ctxt => tac_of_proof_method ctxt debug ([], ths) meth) |
43033 | 224 |
|
48798 | 225 |
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained |
226 |
||
227 |
fun filter_used_facts keep_chained used = |
|
54773 | 228 |
filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false)) |
43033 | 229 |
|
55452
29ec8680e61f
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
blanchet
parents:
55345
diff
changeset
|
230 |
fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) = |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset
|
231 |
let |
55288
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset
|
232 |
fun get_preferred meths = if member (op =) meths preferred then preferred else meth |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
43033
diff
changeset
|
233 |
in |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
234 |
if timeout = Time.zeroTime then |
55285 | 235 |
(get_preferred meths, Not_Played) |
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45378
diff
changeset
|
236 |
else |
50557 | 237 |
let |
54815 | 238 |
val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else () |
50557 | 239 |
val ths = pairs |> sort_wrt (fst o fst) |> map snd |
55285 | 240 |
fun play [] [] = (get_preferred meths, Play_Failed) |
54824 | 241 |
| play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout) |
55285 | 242 |
| play timed_out (meth :: meths) = |
50557 | 243 |
let |
244 |
val _ = |
|
245 |
if verbose then |
|
55285 | 246 |
Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^ |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
247 |
"\" for " ^ string_of_time timeout ^ "...") |
50557 | 248 |
else |
249 |
() |
|
250 |
val timer = Timer.startRealTimer () |
|
251 |
in |
|
55452
29ec8680e61f
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
blanchet
parents:
55345
diff
changeset
|
252 |
(case timed_proof_method debug timeout ths meth state i of |
55285 | 253 |
SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer)) |
55286 | 254 |
| _ => play timed_out meths) |
50557 | 255 |
end |
55285 | 256 |
handle TimeLimit.TimeOut => play (meth :: timed_out) meths |
54824 | 257 |
in |
55285 | 258 |
play [] meths |
54824 | 259 |
end |
43033 | 260 |
end |
261 |
||
55205 | 262 |
val canonical_isar_supported_prover = eN |
51013 | 263 |
|
55205 | 264 |
fun isar_supported_prover_of thy name = |
265 |
if is_atp thy name then name |
|
266 |
else the_default name (remotify_atp_if_not_installed thy canonical_isar_supported_prover) |
|
43051 | 267 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
268 |
(* FIXME: See the analogous logic in the function "maybe_minimize" in |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
269 |
"sledgehammer_prover_minimize.ML". *) |
55205 | 270 |
fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay = |
45520 | 271 |
let |
55205 | 272 |
val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy |
51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset
|
273 |
val (min_name, override_params) = |
54824 | 274 |
(case preplay of |
55285 | 275 |
(meth, Played _) => |
276 |
if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth |
|
54824 | 277 |
| _ => (maybe_isar_name, [])) |
51200
260cb10aac4b
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents:
51190
diff
changeset
|
278 |
in minimize_command override_params min_name end |
43051 | 279 |
|
53480
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
53478
diff
changeset
|
280 |
val max_fact_instances = 10 (* FUDGE *) |
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
53478
diff
changeset
|
281 |
|
55205 | 282 |
fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = |
52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset
|
283 |
Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters) |
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset
|
284 |
#> Config.put Monomorph.max_new_instances |
55205 | 285 |
(max_new_instances |> the_default best_max_new_instances) |
53480
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
53478
diff
changeset
|
286 |
#> Config.put Monomorph.max_thm_instances max_fact_instances |
52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset
|
287 |
|
55212 | 288 |
fun supported_provers ctxt = |
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
289 |
let |
55212 | 290 |
val thy = Proof_Context.theory_of ctxt |
291 |
val (remote_provers, local_provers) = |
|
55285 | 292 |
proof_method_names @ |
55212 | 293 |
sort_strings (supported_atps thy) @ |
294 |
sort_strings (SMT_Solver.available_solvers_of ctxt) |
|
295 |
|> List.partition (String.isPrefix remote_prefix) |
|
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
296 |
in |
55212 | 297 |
Output.urgent_message ("Supported provers: " ^ |
298 |
commas (local_provers @ remote_provers) ^ ".") |
|
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
299 |
end |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
300 |
|
55212 | 301 |
fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover" |
302 |
fun running_provers () = Async_Manager.running_threads SledgehammerN "prover" |
|
303 |
val messages = Async_Manager.thread_messages SledgehammerN "prover" |
|
304 |
||
28582 | 305 |
end; |