author | desharna |
Wed, 20 Mar 2024 12:26:52 +0100 | |
changeset 79942 | 7793e3161d2b |
parent 78695 | 41273636a82a |
child 80809 | 4a64fc4d1cde |
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 |
|
75026 | 17 |
type base_slice = Sledgehammer_ATP_Systems.base_slice |
75025 | 18 |
type atp_slice = Sledgehammer_ATP_Systems.atp_slice |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
19 |
|
58085 | 20 |
datatype mode = Auto_Try | Try | Normal | Minimize | MaSh |
43021 | 21 |
|
73940
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset
|
22 |
datatype induction_rules = Include | Exclude | Instantiate |
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset
|
23 |
val induction_rules_of_string : string -> induction_rules option |
74951
0b6f795d3b78
proper filtering inf induction rules in Mirabelle
desharna
parents:
74948
diff
changeset
|
24 |
val maybe_filter_out_induction_rules : induction_rules -> fact list -> fact list |
73940
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset
|
25 |
|
35969 | 26 |
type params = |
48321 | 27 |
{debug : bool, |
28 |
verbose : bool, |
|
29 |
overlord : bool, |
|
53800 | 30 |
spy : bool, |
48321 | 31 |
provers : string list, |
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
77269
diff
changeset
|
32 |
abduce : int option, |
77428 | 33 |
falsify : bool option, |
48321 | 34 |
type_enc : string option, |
35 |
strict : bool, |
|
36 |
lam_trans : string option, |
|
37 |
uncurried_aliases : bool option, |
|
38 |
learn : bool, |
|
39 |
fact_filter : string option, |
|
73939
9231ea46e041
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents:
72798
diff
changeset
|
40 |
induction_rules : induction_rules option, |
48321 | 41 |
max_facts : int option, |
42 |
fact_thresholds : real * real, |
|
43 |
max_mono_iters : int option, |
|
44 |
max_new_mono_instances : int option, |
|
75031 | 45 |
max_proofs : int, |
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
|
46 |
isar_proofs : bool option, |
57783 | 47 |
compress : real option, |
57245 | 48 |
try0 : bool, |
71931
0c8a9c028304
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents:
63692
diff
changeset
|
49 |
smt_proofs : bool, |
57721 | 50 |
minimize : bool, |
75023 | 51 |
slices : int, |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
52 |
timeout : Time.time, |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
53 |
preplay_timeout : Time.time, |
48321 | 54 |
expect : string} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
55 |
|
74948
15ce207f69c8
added support for initialization messages to Mirabelle
desharna
parents:
74897
diff
changeset
|
56 |
val string_of_params : params -> string |
75340
e1aa703c8cce
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
blanchet
parents:
75339
diff
changeset
|
57 |
val slice_timeout : int -> int -> Time.time -> Time.time |
74897
8b1ab558e3ee
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
desharna
parents:
74370
diff
changeset
|
58 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
59 |
type prover_problem = |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
60 |
{comment : string, |
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
61 |
state : Proof.state, |
48321 | 62 |
goal : thm, |
63 |
subgoal : int, |
|
64 |
subgoal_count : int, |
|
75025 | 65 |
factss : (string * fact list) list, |
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
77269
diff
changeset
|
66 |
has_already_found_something : unit -> bool, |
77269
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
67 |
found_something : string -> unit} |
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset
|
68 |
|
75063
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
69 |
datatype prover_slice_extra = |
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
70 |
ATP_Slice of atp_slice |
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
71 |
| SMT_Slice of string list |
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
72 |
|
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
73 |
type prover_slice = base_slice * prover_slice_extra |
75025 | 74 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
75 |
type prover_result = |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53551
diff
changeset
|
76 |
{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
|
77 |
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
|
78 |
used_from : fact list, |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
79 |
preferred_methss : proof_method * proof_method list list, |
48321 | 80 |
run_time : Time.time, |
57750 | 81 |
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
|
82 |
|
75025 | 83 |
type prover = params -> prover_problem -> prover_slice -> prover_result |
35867 | 84 |
|
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48314
diff
changeset
|
85 |
val SledgehammerN : string |
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
77269
diff
changeset
|
86 |
val default_abduce_max_candidates : int |
57037 | 87 |
val str_of_mode : mode -> string |
55205 | 88 |
val overlord_file_location_of_prover : string -> string * string |
89 |
val proof_banner : mode -> string -> string |
|
75036 | 90 |
val is_atp : string -> bool |
75868
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
91 |
val bunches_of_proof_methods : Proof.context -> bool -> bool -> string -> proof_method list list |
75060
789e0e1a9e33
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
blanchet
parents:
75040
diff
changeset
|
92 |
val facts_of_filter : string -> (string * fact list) list -> fact list |
75069
455d886009b1
uniformized fact selection for ATP and SMT in Sledgehammer
desharna
parents:
75063
diff
changeset
|
93 |
val facts_of_basic_slice : base_slice -> (string * fact list) list -> fact list |
48798 | 94 |
val is_fact_chained : (('a * stature) * 'b) -> bool |
57056 | 95 |
val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> |
48798 | 96 |
((''a * stature) * 'b) list |
55205 | 97 |
val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> |
98 |
Proof.context |
|
55212 | 99 |
val supported_provers : Proof.context -> unit |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
100 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
101 |
|
55201 | 102 |
structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
103 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
104 |
|
57154 | 105 |
open ATP_Proof |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43063
diff
changeset
|
106 |
open ATP_Util |
38028 | 107 |
open ATP_Problem |
46320 | 108 |
open ATP_Problem_Generate |
109 |
open ATP_Proof_Reconstruct |
|
45521 | 110 |
open Metis_Tactic |
51005
ce4290c33d73
eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents:
50927
diff
changeset
|
111 |
open Sledgehammer_Fact |
55287 | 112 |
open Sledgehammer_Proof_Methods |
72400 | 113 |
open Sledgehammer_ATP_Systems |
54000
9cfff7f61d0d
added experimental configuration options to tune use of builtin symbols in SMT
blanchet
parents:
53989
diff
changeset
|
114 |
|
58085 | 115 |
(* 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
|
116 |
val SledgehammerN = "Sledgehammer" |
37585 | 117 |
|
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
77269
diff
changeset
|
118 |
val default_abduce_max_candidates = 1 |
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
77269
diff
changeset
|
119 |
|
58085 | 120 |
datatype mode = Auto_Try | Try | Normal | Minimize | MaSh |
57037 | 121 |
|
122 |
fun str_of_mode Auto_Try = "Auto Try" |
|
123 |
| str_of_mode Try = "Try" |
|
124 |
| str_of_mode Normal = "Normal" |
|
58085 | 125 |
| str_of_mode Minimize = "Minimize" |
57037 | 126 |
| str_of_mode MaSh = "MaSh" |
127 |
||
73940
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset
|
128 |
datatype induction_rules = Include | Exclude | Instantiate |
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset
|
129 |
|
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset
|
130 |
fun induction_rules_of_string "include" = SOME Include |
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset
|
131 |
| induction_rules_of_string "exclude" = SOME Exclude |
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset
|
132 |
| induction_rules_of_string "instantiate" = SOME Instantiate |
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset
|
133 |
| induction_rules_of_string _ = NONE |
f58108b7a60c
refactored Sledgehammer option "induction_rules"
desharna
parents:
73939
diff
changeset
|
134 |
|
75465
d9b23902692d
excluded dummy ATPs from Sledgehammer's default provers
desharna
parents:
75340
diff
changeset
|
135 |
val is_atp = member (op =) all_atps |
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
136 |
|
35969 | 137 |
type params = |
48321 | 138 |
{debug : bool, |
139 |
verbose : bool, |
|
140 |
overlord : bool, |
|
53800 | 141 |
spy : bool, |
48321 | 142 |
provers : string list, |
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
77269
diff
changeset
|
143 |
abduce : int option, |
77428 | 144 |
falsify : bool option, |
48321 | 145 |
type_enc : string option, |
146 |
strict : bool, |
|
147 |
lam_trans : string option, |
|
148 |
uncurried_aliases : bool option, |
|
149 |
learn : bool, |
|
150 |
fact_filter : string option, |
|
73939
9231ea46e041
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
desharna
parents:
72798
diff
changeset
|
151 |
induction_rules : induction_rules option, |
48321 | 152 |
max_facts : int option, |
153 |
fact_thresholds : real * real, |
|
154 |
max_mono_iters : int option, |
|
155 |
max_new_mono_instances : int option, |
|
75031 | 156 |
max_proofs : int, |
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
|
157 |
isar_proofs : bool option, |
57783 | 158 |
compress : real option, |
57245 | 159 |
try0 : bool, |
71931
0c8a9c028304
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents:
63692
diff
changeset
|
160 |
smt_proofs : bool, |
57721 | 161 |
minimize : bool, |
75023 | 162 |
slices : int, |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
163 |
timeout : Time.time, |
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54815
diff
changeset
|
164 |
preplay_timeout : Time.time, |
48321 | 165 |
expect : string} |
35867 | 166 |
|
74948
15ce207f69c8
added support for initialization messages to Mirabelle
desharna
parents:
74897
diff
changeset
|
167 |
fun string_of_params (params : params) = |
15ce207f69c8
added support for initialization messages to Mirabelle
desharna
parents:
74897
diff
changeset
|
168 |
YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100))) |
15ce207f69c8
added support for initialization messages to Mirabelle
desharna
parents:
74897
diff
changeset
|
169 |
|
74951
0b6f795d3b78
proper filtering inf induction rules in Mirabelle
desharna
parents:
74948
diff
changeset
|
170 |
fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list = |
77269
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
171 |
induction_rules = Exclude ? |
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
172 |
filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false) |
74951
0b6f795d3b78
proper filtering inf induction rules in Mirabelle
desharna
parents:
74948
diff
changeset
|
173 |
|
75340
e1aa703c8cce
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
blanchet
parents:
75339
diff
changeset
|
174 |
fun slice_timeout slice_size slices timeout = |
75034 | 175 |
let |
176 |
val max_threads = Multithreading.max_threads () |
|
177 |
val batches = (slices + max_threads - 1) div max_threads |
|
178 |
in |
|
75340
e1aa703c8cce
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
blanchet
parents:
75339
diff
changeset
|
179 |
seconds (Real.fromInt slice_size * Time.toReal timeout / Real.fromInt batches) |
75034 | 180 |
end |
75023 | 181 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
182 |
type prover_problem = |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
183 |
{comment : string, |
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
184 |
state : Proof.state, |
48321 | 185 |
goal : thm, |
186 |
subgoal : int, |
|
187 |
subgoal_count : int, |
|
75025 | 188 |
factss : (string * fact list) list, |
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
77269
diff
changeset
|
189 |
has_already_found_something : unit -> bool, |
77269
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
190 |
found_something : string -> unit} |
35867 | 191 |
|
75063
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
192 |
datatype prover_slice_extra = |
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
193 |
ATP_Slice of atp_slice |
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
194 |
| SMT_Slice of string list |
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
195 |
|
7ff39293e265
added possibility of extra options to SMT slices
blanchet
parents:
75060
diff
changeset
|
196 |
type prover_slice = base_slice * prover_slice_extra |
75025 | 197 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
198 |
type prover_result = |
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53551
diff
changeset
|
199 |
{outcome : atp_failure option, |
48321 | 200 |
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
|
201 |
used_from : fact list, |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
202 |
preferred_methss : proof_method * proof_method list list, |
48321 | 203 |
run_time : Time.time, |
57750 | 204 |
message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} |
35867 | 205 |
|
75025 | 206 |
type prover = params -> prover_problem -> prover_slice -> prover_result |
35867 | 207 |
|
55205 | 208 |
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
|
209 |
|
75020
b087610592b4
rationalized output for forthcoming slicing model
blanchet
parents:
75017
diff
changeset
|
210 |
fun proof_banner mode prover_name = |
55205 | 211 |
(case mode of |
75034 | 212 |
Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof: " |
213 |
| Try => "Sledgehammer (" ^ prover_name ^ ") found a proof: " |
|
75040 | 214 |
| _ => "Try this: ") |
43033 | 215 |
|
75868
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
216 |
fun bunches_of_proof_methods ctxt smt_proofs needs_full_types desperate_lam_trans = |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
217 |
let |
75868
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
218 |
val misc_methodss = |
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
219 |
[[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method, |
78695 | 220 |
Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method, |
79942
7793e3161d2b
try proof method "order" in Sledgehammer's proof reconstruction
desharna
parents:
78695
diff
changeset
|
221 |
Argo_Method, Order_Method]] |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
222 |
|
75868
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
223 |
val metis_methodss = |
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
224 |
[Metis_Method (SOME full_typesN, NONE) :: |
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
225 |
Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) :: |
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
226 |
(if needs_full_types then |
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
227 |
[Metis_Method (SOME really_full_type_enc, NONE), |
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
228 |
Metis_Method (SOME full_typesN, SOME desperate_lam_trans)] |
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
229 |
else |
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
230 |
[Metis_Method (SOME no_typesN, SOME desperate_lam_trans)])] |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
231 |
|
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
232 |
val smt_methodss = |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
233 |
if smt_proofs then |
75956
1e2a9d2251b0
remove duplicate parsing for alethe; fix skolemization;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75868
diff
changeset
|
234 |
[map (SMT_Method o SMT_Verit) (Verit_Strategies.all_veriT_stgies (Context.Proof ctxt)), |
74370 | 235 |
[SMT_Method SMT_Z3]] |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
236 |
else |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
237 |
[] |
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
238 |
in |
75868
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75465
diff
changeset
|
239 |
misc_methodss @ metis_methodss @ smt_methodss |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72400
diff
changeset
|
240 |
end |
43033 | 241 |
|
75060
789e0e1a9e33
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
blanchet
parents:
75040
diff
changeset
|
242 |
fun facts_of_filter fact_filter factss = |
75025 | 243 |
(case AList.lookup (op =) factss fact_filter of |
244 |
SOME facts => facts |
|
245 |
| NONE => snd (hd factss)) |
|
246 |
||
77269
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
247 |
fun facts_of_basic_slice (_, _, _, num_facts, fact_filter) factss = |
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
248 |
let |
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
249 |
val facts = facts_of_filter fact_filter factss |
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
250 |
val (goal_facts, nongoal_facts) = |
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
251 |
List.partition (equal sledgehammer_goal_as_fact o fst o fst) facts |
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
252 |
in |
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
253 |
goal_facts @ take num_facts nongoal_facts |
bc43f86c9598
added refute mode to Sledgehammer to find 'counterexamples'
blanchet
parents:
76052
diff
changeset
|
254 |
end |
75069
455d886009b1
uniformized fact selection for ATP and SMT in Sledgehammer
desharna
parents:
75063
diff
changeset
|
255 |
|
48798 | 256 |
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained |
257 |
||
258 |
fun filter_used_facts keep_chained used = |
|
58654
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58498
diff
changeset
|
259 |
filter ((member (eq_fst (op =)) used o fst) orf |
3e1cad27fc2f
special treatment of extensionality in minimizer
blanchet
parents:
58498
diff
changeset
|
260 |
(if keep_chained then is_fact_chained else K false)) |
43033 | 261 |
|
53480
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
53478
diff
changeset
|
262 |
val max_fact_instances = 10 (* FUDGE *) |
76052
6a20d0ebd5b3
added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number
blanchet
parents:
75956
diff
changeset
|
263 |
val max_schematics = 20 (* FUDGE *) |
53480
247817dbb990
limit the number of instances of a single theorem
blanchet
parents:
53478
diff
changeset
|
264 |
|
55205 | 265 |
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
|
266 |
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
|
267 |
#> Config.put Monomorph.max_new_instances |
55205 | 268 |
(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
|
269 |
#> Config.put Monomorph.max_thm_instances max_fact_instances |
76052
6a20d0ebd5b3
added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number
blanchet
parents:
75956
diff
changeset
|
270 |
#> Config.put Monomorph.max_schematics max_schematics |
52034
11b48e7a4e7e
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents:
52031
diff
changeset
|
271 |
|
55212 | 272 |
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
|
273 |
let |
75036 | 274 |
val local_provers = sort_strings (local_atps @ SMT_Config.available_solvers_of ctxt) |
275 |
val remote_provers = sort_strings remote_atps |
|
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
276 |
in |
63692 | 277 |
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
|
278 |
end |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43044
diff
changeset
|
279 |
|
28582 | 280 |
end; |