author | desharna |
Tue, 11 Jan 2022 22:07:04 +0100 | |
changeset 74981 | 10df7a627ab6 |
parent 74967 | 3f55c5feca58 |
child 74996 | 1f4c39ffb116 |
permissions | -rw-r--r-- |
47847 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Munich |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
3 |
Author: Sascha Boehme, TU Munich |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
4 |
Author: Tobias Nipkow, TU Munich |
73697 | 5 |
Author: Makarius |
74897
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
6 |
Author: Martin Desharnais, UniBw Munich, MPI-INF Saarbruecken |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73292
diff
changeset
|
7 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
73292
diff
changeset
|
8 |
Mirabelle action: "sledgehammer". |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
9 |
*) |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
10 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
11 |
structure Mirabelle_Sledgehammer: MIRABELLE_ACTION = |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
12 |
struct |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
13 |
|
47480
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents:
47477
diff
changeset
|
14 |
(*To facilitate synching the description of Mirabelle Sledgehammer parameters |
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents:
47477
diff
changeset
|
15 |
(in ../lib/Tools/mirabelle) with the parameters actually used by this |
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents:
47477
diff
changeset
|
16 |
interface, the former extracts PARAMETER and DESCRIPTION from code below which |
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents:
47477
diff
changeset
|
17 |
has this pattern (provided it appears in a single line): |
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents:
47477
diff
changeset
|
18 |
val .*K = "PARAMETER" (*DESCRIPTION*) |
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents:
47477
diff
changeset
|
19 |
*) |
72342
4195e75a92ef
[mirabelle] add initial documentation in Sledgehammer's doc
desharna
parents:
72173
diff
changeset
|
20 |
(* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) |
72173 | 21 |
|
22 |
val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) |
|
23 |
val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) |
|
24 |
val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) |
|
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
25 |
val keep_probsK = "keep_probs" (*=BOOL: keep temporary problem files created by sledgehammer*) |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
26 |
val keep_proofsK = "keep_proofs" (*=BOOL: keep temporary proof files created by ATPs*) |
73849 | 27 |
val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*) |
72173 | 28 |
val term_orderK = "term_order" (*=STRING: term order (in E)*) |
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset
|
29 |
|
47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset
|
30 |
(*defaults used in this Mirabelle action*) |
73292
f84a93f1de2f
tuned Mirabelle to parse option check_trivial only once
desharna
parents:
73289
diff
changeset
|
31 |
val check_trivial_default = false |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
32 |
val keep_probs_default = false |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
33 |
val keep_proofs_default = false |
46826
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents:
46825
diff
changeset
|
34 |
|
32549 | 35 |
datatype sh_data = ShData of { |
36 |
calls: int, |
|
37 |
success: int, |
|
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
38 |
nontriv_calls: int, |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
39 |
nontriv_success: int, |
32585 | 40 |
lemmas: int, |
32818 | 41 |
max_lems: int, |
32549 | 42 |
time_isa: int, |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
43 |
time_prover: int} |
32549 | 44 |
|
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset
|
45 |
datatype re_data = ReData of { |
32549 | 46 |
calls: int, |
47 |
success: int, |
|
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
48 |
nontriv_calls: int, |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
49 |
nontriv_success: int, |
32676 | 50 |
proofs: int, |
32549 | 51 |
time: int, |
32550 | 52 |
timeout: int, |
32990 | 53 |
lemmas: int * int * int, |
39341
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset
|
54 |
posns: (Position.T * bool) list |
32550 | 55 |
} |
32549 | 56 |
|
32818 | 57 |
fun make_sh_data |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
58 |
(calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
59 |
time_prover) = |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
60 |
ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
61 |
nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
62 |
time_isa=time_isa, time_prover=time_prover} |
32521 | 63 |
|
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset
|
64 |
fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
65 |
timeout,lemmas,posns) = |
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset
|
66 |
ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
67 |
nontriv_success=nontriv_success, proofs=proofs, time=time, |
32990 | 68 |
timeout=timeout, lemmas=lemmas, posns=posns} |
32549 | 69 |
|
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
70 |
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0) |
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset
|
71 |
val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
72 |
|
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
73 |
fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
74 |
time_isa, time_prover}) = |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
75 |
(calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
76 |
|
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset
|
77 |
fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
78 |
proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
79 |
nontriv_success, proofs, time, timeout, lemmas, posns) |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
80 |
|
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
81 |
datatype data = Data of { |
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
82 |
sh: sh_data, |
57753 | 83 |
re_u: re_data (* proof method with unminimized set of lemmas *) |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
84 |
} |
32521 | 85 |
|
73697 | 86 |
type change_data = (data -> data) -> unit |
87 |
||
57753 | 88 |
fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u} |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
89 |
|
57753 | 90 |
val empty_data = make_data (empty_sh_data, empty_re_data) |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
91 |
|
57753 | 92 |
fun map_sh_data f (Data {sh, re_u}) = |
57752 | 93 |
let val sh' = make_sh_data (f (tuple_of_sh_data sh)) |
57753 | 94 |
in make_data (sh', re_u) end |
32521 | 95 |
|
57753 | 96 |
fun map_re_data f (Data {sh, re_u}) = |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
97 |
let |
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset
|
98 |
val f' = make_re_data o f o tuple_of_re_data |
57753 | 99 |
val re_u' = f' re_u |
100 |
in make_data (sh, re_u') end |
|
32990 | 101 |
|
102 |
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); |
|
32521 | 103 |
|
32818 | 104 |
val inc_sh_calls = map_sh_data |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
105 |
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
106 |
(calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover)) |
32549 | 107 |
|
32818 | 108 |
val inc_sh_success = map_sh_data |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
109 |
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
110 |
(calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover)) |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
111 |
|
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
112 |
val inc_sh_nontriv_calls = map_sh_data |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
113 |
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
114 |
(calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover)) |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
115 |
|
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
116 |
val inc_sh_nontriv_success = map_sh_data |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
117 |
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) => |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
118 |
(calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover)) |
32585 | 119 |
|
32818 | 120 |
fun inc_sh_lemmas n = map_sh_data |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
121 |
(fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
122 |
(calls, success, nontriv_calls, nontriv_success, lemmas+n, max_lems, time_isa, time_prover)) |
32521 | 123 |
|
32818 | 124 |
fun inc_sh_max_lems n = map_sh_data |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
125 |
(fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
126 |
(calls, success,nontriv_calls, nontriv_success, lemmas, Int.max (max_lems, n), time_isa, |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
127 |
time_prover)) |
32549 | 128 |
|
32818 | 129 |
fun inc_sh_time_isa t = map_sh_data |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
130 |
(fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
131 |
(calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa + t, time_prover)) |
32818 | 132 |
|
40062 | 133 |
fun inc_sh_time_prover t = map_sh_data |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
134 |
(fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) => |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
135 |
(calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover + t)) |
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset
|
136 |
|
55285 | 137 |
val inc_proof_method_calls = map_re_data |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
138 |
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
139 |
=> (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) |
32533 | 140 |
|
55285 | 141 |
val inc_proof_method_success = map_re_data |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
142 |
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
143 |
=> (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
144 |
|
55285 | 145 |
val inc_proof_method_nontriv_calls = map_re_data |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
146 |
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
147 |
=> (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
148 |
|
55285 | 149 |
val inc_proof_method_nontriv_success = map_re_data |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
150 |
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
151 |
=> (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) |
32676 | 152 |
|
55285 | 153 |
val inc_proof_method_proofs = map_re_data |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
154 |
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
155 |
=> (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) |
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset
|
156 |
|
57753 | 157 |
fun inc_proof_method_time t = map_re_data |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
158 |
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
159 |
=> (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) |
32536 | 160 |
|
55285 | 161 |
val inc_proof_method_timeout = map_re_data |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
162 |
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) |
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
163 |
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) |
32549 | 164 |
|
57753 | 165 |
fun inc_proof_method_lemmas n = map_re_data |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
166 |
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) |
57753 | 167 |
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) |
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset
|
168 |
|
57753 | 169 |
fun inc_proof_method_posns pos = map_re_data |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
170 |
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) |
57753 | 171 |
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) |
32521 | 172 |
|
44090 | 173 |
val str0 = string_of_int o the_default 0 |
174 |
||
32521 | 175 |
local |
176 |
||
177 |
val str = string_of_int |
|
178 |
val str3 = Real.fmt (StringCvt.FIX (SOME 3)) |
|
179 |
fun percentage a b = string_of_int (a * 100 div b) |
|
73697 | 180 |
fun ms t = Real.fromInt t / 1000.0 |
32521 | 181 |
fun avg_time t n = |
182 |
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 |
|
183 |
||
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
184 |
fun log_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
185 |
time_prover}) = |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
186 |
"\nTotal number of sledgehammer calls: " ^ str calls ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
187 |
"\nNumber of successful sledgehammer calls: " ^ str success ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
188 |
"\nNumber of sledgehammer lemmas: " ^ str lemmas ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
189 |
"\nMax number of sledgehammer lemmas: " ^ str max_lems ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
190 |
"\nSuccess rate: " ^ percentage success calls ^ "%" ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
191 |
"\nTotal number of nontrivial sledgehammer calls: " ^ str nontriv_calls ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
192 |
"\nNumber of successful nontrivial sledgehammer calls: " ^ str nontriv_success ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
193 |
"\nTotal time for sledgehammer calls (Isabelle): " ^ str3 (ms time_isa) ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
194 |
"\nTotal time for successful sledgehammer calls (ATP): " ^ str3 (ms time_prover) ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
195 |
"\nAverage time for sledgehammer calls (Isabelle): " ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
196 |
str3 (avg_time time_isa calls) ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
197 |
"\nAverage time for successful sledgehammer calls (ATP): " ^ |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
198 |
str3 (avg_time time_prover success) |
32521 | 199 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
200 |
fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
201 |
timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) = |
73697 | 202 |
let |
203 |
val proved = |
|
204 |
posns |> map (fn (pos, triv) => |
|
205 |
str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ |
|
206 |
(if triv then "[T]" else "")) |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
207 |
in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
208 |
"\nTotal number of proof method calls: " ^ str calls ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
209 |
"\nNumber of successful proof method calls: " ^ str success ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
210 |
" (proof: " ^ str proofs ^ ")" ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
211 |
"\nNumber of proof method timeouts: " ^ str timeout ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
212 |
"\nSuccess rate: " ^ percentage success sh_calls ^ "%" ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
213 |
"\nTotal number of nontrivial proof method calls: " ^ str nontriv_calls ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
214 |
"\nNumber of successful nontrivial proof method calls: " ^ str nontriv_success ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
215 |
" (proof: " ^ str proofs ^ ")" ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
216 |
"\nNumber of successful proof method lemmas: " ^ str lemmas ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
217 |
"\nSOS of successful proof method lemmas: " ^ str lems_sos ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
218 |
"\nMax number of successful proof method lemmas: " ^ str lems_max ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
219 |
"\nTotal time for successful proof method calls: " ^ str3 (ms time) ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
220 |
"\nAverage time for successful proof method calls: " ^ str3 (avg_time time success) ^ |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
221 |
"\nProved: " ^ space_implode " " proved |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
222 |
end |
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset
|
223 |
|
32521 | 224 |
in |
225 |
||
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
226 |
fun log_data (Data {sh, re_u}) = |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
227 |
let |
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
228 |
val ShData {calls=sh_calls, ...} = sh |
73697 | 229 |
val ReData {calls=re_calls, ...} = re_u |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
230 |
in |
73697 | 231 |
if sh_calls > 0 then |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
232 |
let val text1 = log_sh_data sh in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
233 |
if re_calls > 0 then text1 ^ "\n" ^ log_re_data sh_calls re_u else text1 |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
234 |
end |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
235 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
236 |
"" |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset
|
237 |
end |
32521 | 238 |
|
239 |
end |
|
240 |
||
46340 | 241 |
type stature = ATP_Problem_Generate.stature |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38700
diff
changeset
|
242 |
|
58473 | 243 |
fun is_good_line s = |
53081
2a62d848a56a
improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents:
52555
diff
changeset
|
244 |
(String.isSubstring " ms)" s orelse String.isSubstring " s)" s) |
2a62d848a56a
improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents:
52555
diff
changeset
|
245 |
andalso not (String.isSubstring "(> " s) |
2a62d848a56a
improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents:
52555
diff
changeset
|
246 |
andalso not (String.isSubstring ", > " s) |
2a62d848a56a
improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents:
52555
diff
changeset
|
247 |
andalso not (String.isSubstring "may fail" s) |
2a62d848a56a
improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents:
52555
diff
changeset
|
248 |
|
51206 | 249 |
(* Fragile hack *) |
55285 | 250 |
fun proof_method_from_msg args msg = |
251 |
(case AList.lookup (op =) args proof_methodK of |
|
58473 | 252 |
SOME name => |
253 |
if name = "smart" then |
|
254 |
if exists is_good_line (split_lines msg) then |
|
255 |
"none" |
|
256 |
else |
|
257 |
"fail" |
|
258 |
else |
|
259 |
name |
|
41357
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset
|
260 |
| NONE => |
58473 | 261 |
if exists is_good_line (split_lines msg) then |
51203 | 262 |
"none" (* trust the preplayed proof *) |
263 |
else if String.isSubstring "metis (" msg then |
|
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
264 |
msg |> Substring.full |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
265 |
|> Substring.position "metis (" |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
266 |
|> snd |> Substring.position ")" |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
267 |
|> fst |> Substring.string |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
268 |
|> suffix ")" |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
269 |
else if String.isSubstring "metis" msg then |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
270 |
"metis" |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
271 |
else |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
272 |
"smt") |
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset
|
273 |
|
32521 | 274 |
local |
275 |
||
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
276 |
fun run_sh params e_selection_heuristic term_order force_sos keep pos state = |
32521 | 277 |
let |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
278 |
fun set_file_name (SOME (dir, keep_probs, keep_proofs)) = |
74892 | 279 |
let |
280 |
val filename = "prob_" ^ |
|
74472 | 281 |
StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^ |
74892 | 282 |
StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos)) |
283 |
in |
|
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
284 |
Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__") |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
285 |
#> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir) |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
286 |
#> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir) |
74892 | 287 |
#> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ()) |
288 |
end |
|
44090 | 289 |
| set_file_name NONE = I |
74950
b350a1f2115d
added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
desharna
parents:
74948
diff
changeset
|
290 |
val state' = |
b350a1f2115d
added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
desharna
parents:
74948
diff
changeset
|
291 |
state |
47030 | 292 |
|> Proof.map_context |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
293 |
(set_file_name keep |
72400 | 294 |
#> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) |
47032 | 295 |
e_selection_heuristic |> the_default I) |
72400 | 296 |
#> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) |
47049 | 297 |
term_order |> the_default I) |
72400 | 298 |
#> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) |
47030 | 299 |
force_sos |> the_default I)) |
74952
ae2185967e67
exported Sledgehammer.launch_prover and use it in Mirabelle
desharna
parents:
74951
diff
changeset
|
300 |
|
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
301 |
val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () => |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
302 |
Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1 |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
303 |
Sledgehammer_Fact.no_fact_override state') () |
32521 | 304 |
in |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
305 |
(sledgehammer_outcome, msg, cpu_time) |
32521 | 306 |
end |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
307 |
handle |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
308 |
ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0) |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
309 |
| _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0) |
32521 | 310 |
|
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
311 |
in |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
312 |
|
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
313 |
fun run_sledgehammer change_data (params as {provers, ...}) output_dir |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
314 |
e_selection_heuristic term_order force_sos keep_probs keep_proofs proof_method_from_msg thy_index |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
315 |
trivial proof_method named_thms pos st = |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
316 |
let |
55205 | 317 |
val thy = Proof.theory_of st |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
318 |
val thy_name = Context.theory_name thy |
39340 | 319 |
val triv_str = if trivial then "[T] " else "" |
73697 | 320 |
val _ = change_data inc_sh_calls |
321 |
val _ = if trivial then () else change_data inc_sh_nontriv_calls |
|
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
322 |
val keep = |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
323 |
if keep_probs orelse keep_proofs then |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
324 |
let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in |
74078
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
73849
diff
changeset
|
325 |
Path.append output_dir (Path.basic subdir) |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
326 |
|> Isabelle_System.make_directory |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
327 |
|> Path.implode |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
328 |
|> (fn dir => SOME (dir, keep_probs, keep_proofs)) |
74078
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
73849
diff
changeset
|
329 |
end |
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
73849
diff
changeset
|
330 |
else |
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
73849
diff
changeset
|
331 |
NONE |
74897
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
332 |
val prover_name = hd provers |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
333 |
val (sledgehamer_outcome, msg, cpu_time) = |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
334 |
run_sh params e_selection_heuristic term_order force_sos keep pos st |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
335 |
val outcome_msg = |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
336 |
(case sledgehamer_outcome of |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
337 |
Sledgehammer.SH_Some {used_facts, run_time, ...} => |
38700 | 338 |
let |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
339 |
val num_used_facts = length used_facts |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
340 |
val time_prover = Time.toMilliseconds run_time |
46340 | 341 |
fun get_thms (name, stature) = |
50267
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
49916
diff
changeset
|
342 |
try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) |
49916
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49914
diff
changeset
|
343 |
name |
47154
2c357e2b8436
more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
blanchet
parents:
47060
diff
changeset
|
344 |
|> Option.map (pair (name, stature)) |
32525 | 345 |
in |
73697 | 346 |
change_data inc_sh_success; |
347 |
if trivial then () else change_data inc_sh_nontriv_success; |
|
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
348 |
change_data (inc_sh_lemmas num_used_facts); |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
349 |
change_data (inc_sh_max_lems num_used_facts); |
73697 | 350 |
change_data (inc_sh_time_prover time_prover); |
74897
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
351 |
proof_method := proof_method_from_msg msg; |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
352 |
named_thms := SOME (map_filter get_thms used_facts); |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
353 |
" (" ^ string_of_int cpu_time ^ "+" ^ string_of_int time_prover ^ ")" ^ |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
354 |
" [" ^ prover_name ^ "]:\n" |
32525 | 355 |
end |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
356 |
| _ => "") |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
357 |
in |
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
358 |
change_data (inc_sh_time_isa cpu_time); |
74967
3f55c5feca58
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
desharna
parents:
74953
diff
changeset
|
359 |
(sledgehamer_outcome, triv_str ^ outcome_msg ^ msg) |
32525 | 360 |
end |
361 |
||
362 |
end |
|
363 |
||
44542 | 364 |
fun override_params prover type_enc timeout = |
365 |
[("provers", prover), |
|
48293 | 366 |
("max_facts", "0"), |
44542 | 367 |
("type_enc", type_enc), |
46386 | 368 |
("strict", "true"), |
45706 | 369 |
("slice", "false"), |
44461 | 370 |
("timeout", timeout |> Time.toSeconds |> string_of_int)] |
44430 | 371 |
|
73697 | 372 |
fun run_proof_method change_data trivial full name meth named_thms timeout pos st = |
32525 | 373 |
let |
55285 | 374 |
fun do_method named_thms ctxt = |
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset
|
375 |
let |
59083 | 376 |
val ref_of_str = (* FIXME proper wrapper for parser combinators *) |
377 |
suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none |
|
62969 | 378 |
#> Parse.thm #> fst |
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset
|
379 |
val thms = named_thms |> maps snd |
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset
|
380 |
val facts = named_thms |> map (ref_of_str o fst o fst) |
48292 | 381 |
val fact_override = {add = facts, del = [], only = true} |
44566
bf8331161ad9
split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents:
44542
diff
changeset
|
382 |
fun my_timeout time_slice = |
62826 | 383 |
timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal |
44566
bf8331161ad9
split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents:
44542
diff
changeset
|
384 |
fun sledge_tac time_slice prover type_enc = |
44542 | 385 |
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
57814 | 386 |
(override_params prover type_enc (my_timeout time_slice)) fact_override [] |
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset
|
387 |
in |
55285 | 388 |
if !meth = "sledgehammer_tac" then |
57154 | 389 |
sledge_tac 0.2 ATP_Proof.vampireN "mono_native" |
390 |
ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" |
|
391 |
ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" |
|
392 |
ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" |
|
58061 | 393 |
ORELSE' SMT_Solver.smt_tac ctxt thms |
55285 | 394 |
else if !meth = "smt" then |
58061 | 395 |
SMT_Solver.smt_tac ctxt thms |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
396 |
else if full then |
46320 | 397 |
Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] |
54500 | 398 |
ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms |
55285 | 399 |
else if String.isPrefix "metis (" (!meth) then |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
400 |
let |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
401 |
val (type_encs, lam_trans) = |
55285 | 402 |
!meth |
59083 | 403 |
|> Token.explode (Thy_Header.get_keywords' ctxt) Position.start |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
404 |
|> filter Token.is_proper |> tl |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
405 |
|> Metis_Tactic.parse_metis_options |> fst |
46320 | 406 |
|>> the_default [ATP_Proof_Reconstruct.partial_typesN] |
54500 | 407 |
||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
408 |
in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end |
55285 | 409 |
else if !meth = "metis" then |
55211 | 410 |
Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms |
58473 | 411 |
else if !meth = "none" then |
412 |
K all_tac |
|
413 |
else if !meth = "fail" then |
|
414 |
K no_tac |
|
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset
|
415 |
else |
58473 | 416 |
(warning ("Unknown method " ^ quote (!meth)); K no_tac) |
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset
|
417 |
end |
55285 | 418 |
fun apply_method named_thms = |
419 |
Mirabelle.can_apply timeout (do_method named_thms) st |
|
32521 | 420 |
|
421 |
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
422 |
| with_time (true, t) = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
423 |
(change_data inc_proof_method_success; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
424 |
if trivial then () else change_data inc_proof_method_nontriv_success; |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
425 |
change_data (inc_proof_method_lemmas (length named_thms)); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
426 |
change_data (inc_proof_method_time t); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
427 |
change_data (inc_proof_method_posns (pos, trivial)); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
428 |
if name = "proof" then change_data inc_proof_method_proofs else (); |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
429 |
"succeeded (" ^ string_of_int t ^ ")") |
55285 | 430 |
fun timed_method named_thms = |
73697 | 431 |
with_time (Mirabelle.cpu_time apply_method named_thms) |
432 |
handle Timeout.TIMEOUT _ => (change_data inc_proof_method_timeout; "timeout") |
|
433 |
| ERROR msg => ("error: " ^ msg) |
|
32521 | 434 |
|
73697 | 435 |
val _ = change_data inc_proof_method_calls |
436 |
val _ = if trivial then () else change_data inc_proof_method_nontriv_calls |
|
437 |
in timed_method named_thms end |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
438 |
|
41276
285aea0c153c
two layers of timeouts seem to be less reliable than a single layer
blanchet
parents:
41275
diff
changeset
|
439 |
val try_timeout = seconds 5.0 |
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset
|
440 |
|
74078
a2cbe81e1e32
changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents:
73849
diff
changeset
|
441 |
fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) = |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
442 |
let |
74897
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
443 |
(* Parse Mirabelle-specific parameters *) |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
444 |
val check_trivial = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
445 |
Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default) |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
446 |
val keep_probs = Mirabelle.get_bool_argument arguments (keep_probsK, keep_probs_default) |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
447 |
val keep_proofs = Mirabelle.get_bool_argument arguments (keep_proofsK, keep_proofs_default) |
74897
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
448 |
val e_selection_heuristic = AList.lookup (op =) arguments e_selection_heuristicK |
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
449 |
val term_order = AList.lookup (op =) arguments term_orderK |
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
450 |
val force_sos = AList.lookup (op =) arguments force_sosK |
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
451 |
|> Option.map (curry (op <>) "false") |
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
452 |
val proof_method_from_msg = proof_method_from_msg arguments |
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
453 |
|
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
454 |
(* Parse Sledgehammer parameters *) |
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
455 |
val params = Sledgehammer_Commands.default_params \<^theory> arguments |
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
456 |
|> (fn (params as {provers, ...}) => |
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
457 |
(case provers of |
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
458 |
prover :: _ => Sledgehammer_Prover.set_params_provers params [prover] |
74953
aade20a03edb
tuned run_sledgehammer and called it directly from Mirabelle
desharna
parents:
74952
diff
changeset
|
459 |
| _ => error "sledgehammer action requires one and only one prover")) |
44431
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset
|
460 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
461 |
val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
462 |
val change_data = Synchronized.change data |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
463 |
|
74948
15ce207f69c8
added support for initialization messages to Mirabelle
desharna
parents:
74897
diff
changeset
|
464 |
val init_msg = "Params for sledgehammer: " ^ Sledgehammer_Prover.string_of_params params |
15ce207f69c8
added support for initialization messages to Mirabelle
desharna
parents:
74897
diff
changeset
|
465 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
466 |
fun run_action ({theory_index, name, pos, pre, ...} : Mirabelle.command) = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
467 |
let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
468 |
if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
469 |
"" |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
470 |
else |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
471 |
let |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
472 |
val meth = Unsynchronized.ref "" |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
473 |
val named_thms = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
474 |
Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
475 |
val trivial = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
476 |
check_trivial andalso Try0.try0 (SOME try_timeout) ([], [], [], []) pre |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
477 |
handle Timeout.TIMEOUT _ => false |
74967
3f55c5feca58
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
desharna
parents:
74953
diff
changeset
|
478 |
val (outcome, log1) = |
74897
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74892
diff
changeset
|
479 |
run_sledgehammer change_data params output_dir e_selection_heuristic term_order |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
480 |
force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial meth |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74967
diff
changeset
|
481 |
named_thms pos pre |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
482 |
val log2 = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
483 |
(case !named_thms of |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
484 |
SOME thms => |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
485 |
!meth ^ " (sledgehammer): " ^ run_proof_method change_data trivial false name meth |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
486 |
thms timeout pos pre |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
487 |
| NONE => "") |
74967
3f55c5feca58
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
desharna
parents:
74953
diff
changeset
|
488 |
in |
3f55c5feca58
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
desharna
parents:
74953
diff
changeset
|
489 |
log1 ^ "\n" ^ log2 |
3f55c5feca58
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
desharna
parents:
74953
diff
changeset
|
490 |
|> Symbol.trim_blanks |
3f55c5feca58
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
desharna
parents:
74953
diff
changeset
|
491 |
|> prefix_lines (Sledgehammer.short_string_of_sledgehammer_outcome outcome ^ " ") |
3f55c5feca58
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
desharna
parents:
74953
diff
changeset
|
492 |
end |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
493 |
end |
73697 | 494 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
495 |
fun finalize () = log_data (Synchronized.value data) |
74948
15ce207f69c8
added support for initialization messages to Mirabelle
desharna
parents:
74897
diff
changeset
|
496 |
in (init_msg, {run_action = run_action, finalize = finalize}) end |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
497 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73797
diff
changeset
|
498 |
val () = Mirabelle.register_action "sledgehammer" make_action |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
499 |
|
74951
0b6f795d3b78
proper filtering inf induction rules in Mirabelle
desharna
parents:
74950
diff
changeset
|
500 |
end |