author | blanchet |
Sun, 14 Aug 2016 12:26:09 +0200 | |
changeset 63692 | 1bc4bc2c9fd1 |
parent 62735 | 23de054397e5 |
child 71931 | 0c8a9c028304 |
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 |
|
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
17 |
|
58085 | 18 |
datatype mode = Auto_Try | Try | Normal | Minimize | MaSh |
43021 | 19 |
|
35969 | 20 |
type params = |
48321 | 21 |
{debug : bool, |
22 |
verbose : bool, |
|
23 |
overlord : bool, |
|
53800 | 24 |
spy : bool, |
48321 | 25 |
provers : string list, |
26 |
type_enc : string option, |
|
27 |
strict : bool, |
|
28 |
lam_trans : string option, |
|
29 |
uncurried_aliases : bool option, |
|
30 |
learn : bool, |
|
31 |
fact_filter : string option, |
|
32 |
max_facts : int option, |
|
33 |
fact_thresholds : real * real, |
|
34 |
max_mono_iters : int option, |
|
35 |
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
|
36 |
isar_proofs : bool option, |
57783 | 37 |
compress : real option, |
57245 | 38 |
try0 : bool, |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset
|
39 |
smt_proofs : bool option, |
48321 | 40 |
slice : bool, |
57721 | 41 |
minimize : bool, |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
42 |
timeout : Time.time, |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
43 |
preplay_timeout : Time.time, |
48321 | 44 |
expect : string} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
45 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
46 |
type prover_problem = |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
47 |
{comment : string, |
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
48 |
state : Proof.state, |
48321 | 49 |
goal : thm, |
50 |
subgoal : int, |
|
51 |
subgoal_count : int, |
|
62735 | 52 |
factss : (string * fact list) list, |
53 |
found_proof : unit -> unit} |
|
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
54 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
55 |
type prover_result = |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53551
diff
changeset
|
56 |
{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
|
57 |
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
|
58 |
used_from : fact list, |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
59 |
preferred_methss : proof_method * proof_method list list, |
48321 | 60 |
run_time : Time.time, |
57750 | 61 |
message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
62 |
|
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57734
diff
changeset
|
63 |
type prover = params -> prover_problem -> prover_result |
35867 | 64 |
|
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset
|
65 |
val SledgehammerN : string |
57037 | 66 |
val str_of_mode : mode -> string |
55205 | 67 |
val overlord_file_location_of_prover : string -> string * string |
68 |
val proof_banner : mode -> string -> string |
|
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
69 |
val is_atp : theory -> string -> bool |
57742 | 70 |
val bunches_of_proof_methods : bool -> bool -> bool -> string -> proof_method list list |
48798 | 71 |
val is_fact_chained : (('a * stature) * 'b) -> bool |
57056 | 72 |
val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> |
48798 | 73 |
((''a * stature) * 'b) list |
55205 | 74 |
val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> |
75 |
Proof.context |
|
55212 | 76 |
val supported_provers : Proof.context -> unit |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
77 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
78 |
|
55201 | 79 |
structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
80 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
81 |
|
57154 | 82 |
open ATP_Proof |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43063
diff
changeset
|
83 |
open ATP_Util |
57154 | 84 |
open ATP_Systems |
38028 | 85 |
open ATP_Problem |
46320 | 86 |
open ATP_Problem_Generate |
87 |
open ATP_Proof_Reconstruct |
|
45521 | 88 |
open Metis_Tactic |
51005
ce4290c33d73
eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents:
50927
diff
changeset
|
89 |
open Sledgehammer_Fact |
55287 | 90 |
open Sledgehammer_Proof_Methods |
54000
9cfff7f61d0d
added experimental configuration options to tune use of builtin symbols in SMT
blanchet
parents:
53989
diff
changeset
|
91 |
|
58085 | 92 |
(* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *) |
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset
|
93 |
val SledgehammerN = "Sledgehammer" |
37585 | 94 |
|
58085 | 95 |
datatype mode = Auto_Try | Try | Normal | Minimize | MaSh |
57037 | 96 |
|
97 |
fun str_of_mode Auto_Try = "Auto Try" |
|
98 |
| str_of_mode Try = "Try" |
|
99 |
| str_of_mode Normal = "Normal" |
|
58085 | 100 |
| str_of_mode Minimize = "Minimize" |
57037 | 101 |
| str_of_mode MaSh = "MaSh" |
102 |
||
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
103 |
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
|
104 |
|
35969 | 105 |
type params = |
48321 | 106 |
{debug : bool, |
107 |
verbose : bool, |
|
108 |
overlord : bool, |
|
53800 | 109 |
spy : bool, |
48321 | 110 |
provers : string list, |
111 |
type_enc : string option, |
|
112 |
strict : bool, |
|
113 |
lam_trans : string option, |
|
114 |
uncurried_aliases : bool option, |
|
115 |
learn : bool, |
|
116 |
fact_filter : string option, |
|
117 |
max_facts : int option, |
|
118 |
fact_thresholds : real * real, |
|
119 |
max_mono_iters : int option, |
|
120 |
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
|
121 |
isar_proofs : bool option, |
57783 | 122 |
compress : real option, |
57245 | 123 |
try0 : bool, |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55288
diff
changeset
|
124 |
smt_proofs : bool option, |
48321 | 125 |
slice : bool, |
57721 | 126 |
minimize : bool, |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
127 |
timeout : Time.time, |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
128 |
preplay_timeout : Time.time, |
48321 | 129 |
expect : string} |
35867 | 130 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
131 |
type prover_problem = |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
132 |
{comment : string, |
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
133 |
state : Proof.state, |
48321 | 134 |
goal : thm, |
135 |
subgoal : int, |
|
136 |
subgoal_count : int, |
|
62735 | 137 |
factss : (string * fact list) list, |
138 |
found_proof : unit -> unit} |
|
35867 | 139 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
140 |
type prover_result = |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53551
diff
changeset
|
141 |
{outcome : atp_failure option, |
48321 | 142 |
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
|
143 |
used_from : fact list, |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
144 |
preferred_methss : proof_method * proof_method list list, |
48321 | 145 |
run_time : Time.time, |
57750 | 146 |
message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} |
35867 | 147 |
|
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57734
diff
changeset
|
148 |
type prover = params -> prover_problem -> prover_result |
35867 | 149 |
|
55205 | 150 |
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
|
151 |
|
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
152 |
fun proof_banner mode name = |
55205 | 153 |
(case mode of |
43033 | 154 |
Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" |
155 |
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof" |
|
55205 | 156 |
| _ => "Try this") |
43033 | 157 |
|
58498 | 158 |
fun bunches_of_proof_methods try0 smt_method needs_full_types desperate_lam_trans = |
57742 | 159 |
(if try0 then |
160 |
[[Simp_Method, Auto_Method, Blast_Method, Linarith_Method], |
|
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58085
diff
changeset
|
161 |
[Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]] |
57742 | 162 |
else |
163 |
[]) @ |
|
164 |
[[Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE)], |
|
165 |
(if needs_full_types then |
|
166 |
[Metis_Method (NONE, NONE), |
|
167 |
Metis_Method (SOME really_full_type_enc, NONE), |
|
168 |
Metis_Method (SOME full_typesN, SOME desperate_lam_trans), |
|
169 |
Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] |
|
170 |
else |
|
171 |
[Metis_Method (SOME full_typesN, NONE), |
|
172 |
Metis_Method (SOME no_typesN, SOME desperate_lam_trans), |
|
173 |
Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @ |
|
58498 | 174 |
(if smt_method then [[SMT_Method]] else []) |
43033 | 175 |
|
48798 | 176 |
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained |
177 |
||
178 |
fun filter_used_facts keep_chained used = |
|
58654
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58498
diff
changeset
|
179 |
filter ((member (eq_fst (op =)) used o fst) orf |
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58498
diff
changeset
|
180 |
(if keep_chained then is_fact_chained else K false)) |
43033 | 181 |
|
53480
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
53478
diff
changeset
|
182 |
val max_fact_instances = 10 (* FUDGE *) |
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
53478
diff
changeset
|
183 |
|
55205 | 184 |
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
|
185 |
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
|
186 |
#> Config.put Monomorph.max_new_instances |
55205 | 187 |
(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
|
188 |
#> 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
|
189 |
|
55212 | 190 |
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
|
191 |
let |
55212 | 192 |
val thy = Proof_Context.theory_of ctxt |
193 |
val (remote_provers, local_provers) = |
|
58061 | 194 |
sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt) |
55212 | 195 |
|> 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
|
196 |
in |
63692 | 197 |
writeln ("Supported provers: " ^ 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
|
198 |
end |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
199 |
|
28582 | 200 |
end; |