src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
author desharna
Wed, 20 Mar 2024 12:26:52 +0100
changeset 79942 7793e3161d2b
parent 78695 41273636a82a
child 80809 4a64fc4d1cde
permissions -rw-r--r--
try proof method "order" in Sledgehammer's proof reconstruction
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55201
1ee776da8da7 renamed ML file
blanchet
parents: 55183
diff changeset
     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
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
     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
1ee776da8da7 renamed ML file
blanchet
parents: 55183
diff changeset
     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
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
    12
  type stature = ATP_Problem_Generate.stature
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    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
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
    15
  type proof_method = Sledgehammer_Proof_Methods.proof_method
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
    16
  type play_outcome = Sledgehammer_Proof_Methods.play_outcome
75026
b61949cba32a rationalize slicing format
blanchet
parents: 75025
diff changeset
    17
  type base_slice = Sledgehammer_ATP_Systems.base_slice
75025
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
    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
ee65e9cfe284 merged minimize and auto_minimize
blanchet
parents: 58061
diff changeset
    20
  datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
    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
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    26
  type params =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    27
    {debug : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    28
     verbose : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    29
     overlord : bool,
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53764
diff changeset
    30
     spy : bool,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    31
     provers : string list,
77418
a8458f0df4ee implemented ad hoc abduction in Sledgehammer with E
blanchet
parents: 77269
diff changeset
    32
     abduce : int option,
77428
7c76221baecb adopt terminology suggested by Larry Paulson
blanchet
parents: 77423
diff changeset
    33
     falsify : bool option,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    34
     type_enc : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    35
     strict : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    36
     lam_trans : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    37
     uncurried_aliases : bool option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    38
     learn : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    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
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    41
     max_facts : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    42
     fact_thresholds : real * real,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    43
     max_mono_iters : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    44
     max_new_mono_instances : int option,
75031
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75026
diff changeset
    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
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57750
diff changeset
    47
     compress : real option,
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57208
diff changeset
    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
e4858f85e616 always minimize Sledgehammer results by default
blanchet
parents: 57718
diff changeset
    50
     minimize : bool,
75023
fdda7e754f45 changed logic of 'slice' option to 'slices'
blanchet
parents: 75020
diff changeset
    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
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    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
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    62
     goal : thm,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    63
     subgoal : int,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    64
     subgoal_count : int,
75025
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
    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
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
    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
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    80
     run_time : Time.time,
57750
670cbec816b9 restored a bit of laziness
blanchet
parents: 57742
diff changeset
    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
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
    83
  type prover = params -> prover_problem -> prover_slice -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
    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
c51132be8e16 avoid markup-generating @{make_string}
blanchet
parents: 56985
diff changeset
    87
  val str_of_mode : mode -> string
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    88
  val overlord_file_location_of_prover : string -> string * string
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    89
  val proof_banner : mode -> string -> string
75036
212e9ec706cf run all installed provers by default
blanchet
parents: 75034
diff changeset
    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
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
    94
  val is_fact_chained : (('a * stature) * 'b) -> bool
57056
8b2283566f6e properly reconstruct helpers in Z3 proofs
blanchet
parents: 57054
diff changeset
    95
  val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
    96
    ((''a * stature) * 'b) list
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    97
  val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    98
    Proof.context
55212
blanchet
parents: 55211
diff changeset
    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
1ee776da8da7 renamed ML file
blanchet
parents: 55183
diff changeset
   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
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 57056
diff changeset
   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
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
   107
open ATP_Problem
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
   108
open ATP_Problem_Generate
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
   109
open ATP_Proof_Reconstruct
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45520
diff changeset
   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
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
   112
open Sledgehammer_Proof_Methods
72400
abfeed05c323 tune filename
desharna
parents: 71931
diff changeset
   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
ee65e9cfe284 merged minimize and auto_minimize
blanchet
parents: 58061
diff changeset
   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
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   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
ee65e9cfe284 merged minimize and auto_minimize
blanchet
parents: 58061
diff changeset
   120
datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
57037
c51132be8e16 avoid markup-generating @{make_string}
blanchet
parents: 56985
diff changeset
   121
c51132be8e16 avoid markup-generating @{make_string}
blanchet
parents: 56985
diff changeset
   122
fun str_of_mode Auto_Try = "Auto Try"
c51132be8e16 avoid markup-generating @{make_string}
blanchet
parents: 56985
diff changeset
   123
  | str_of_mode Try = "Try"
c51132be8e16 avoid markup-generating @{make_string}
blanchet
parents: 56985
diff changeset
   124
  | str_of_mode Normal = "Normal"
58085
ee65e9cfe284 merged minimize and auto_minimize
blanchet
parents: 58061
diff changeset
   125
  | str_of_mode Minimize = "Minimize"
57037
c51132be8e16 avoid markup-generating @{make_string}
blanchet
parents: 56985
diff changeset
   126
  | str_of_mode MaSh = "MaSh"
c51132be8e16 avoid markup-generating @{make_string}
blanchet
parents: 56985
diff changeset
   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
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   137
type params =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   138
  {debug : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   139
   verbose : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   140
   overlord : bool,
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53764
diff changeset
   141
   spy : bool,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   142
   provers : string list,
77418
a8458f0df4ee implemented ad hoc abduction in Sledgehammer with E
blanchet
parents: 77269
diff changeset
   143
   abduce : int option,
77428
7c76221baecb adopt terminology suggested by Larry Paulson
blanchet
parents: 77423
diff changeset
   144
   falsify : bool option,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   145
   type_enc : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   146
   strict : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   147
   lam_trans : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   148
   uncurried_aliases : bool option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   149
   learn : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   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
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   152
   max_facts : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   153
   fact_thresholds : real * real,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   154
   max_mono_iters : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   155
   max_new_mono_instances : int option,
75031
ae4dc5ac983f implemented 'max_proofs' mechanism
blanchet
parents: 75026
diff changeset
   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
2bf99b3f62e1 cleaner 'compress' option
blanchet
parents: 57750
diff changeset
   158
   compress : real option,
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57208
diff changeset
   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
e4858f85e616 always minimize Sledgehammer results by default
blanchet
parents: 57718
diff changeset
   161
   minimize : bool,
75023
fdda7e754f45 changed logic of 'slice' option to 'slices'
blanchet
parents: 75020
diff changeset
   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
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   165
   expect : string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   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
890b70f96fe4 further work on new Sledgehammer slicing
blanchet
parents: 75031
diff changeset
   175
  let
890b70f96fe4 further work on new Sledgehammer slicing
blanchet
parents: 75031
diff changeset
   176
    val max_threads = Multithreading.max_threads ()
890b70f96fe4 further work on new Sledgehammer slicing
blanchet
parents: 75031
diff changeset
   177
    val batches = (slices + max_threads - 1) div max_threads
890b70f96fe4 further work on new Sledgehammer slicing
blanchet
parents: 75031
diff changeset
   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
890b70f96fe4 further work on new Sledgehammer slicing
blanchet
parents: 75031
diff changeset
   180
  end
75023
fdda7e754f45 changed logic of 'slice' option to 'slices'
blanchet
parents: 75020
diff changeset
   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
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   185
   goal : thm,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   186
   subgoal : int,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   187
   subgoal_count : int,
75025
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
   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
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   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
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
   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
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   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
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   203
   run_time : Time.time,
57750
670cbec816b9 restored a bit of laziness
blanchet
parents: 57742
diff changeset
   204
   message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   205
75025
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
   206
type prover = params -> prover_problem -> prover_slice -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   207
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   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
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   211
  (case mode of
75034
890b70f96fe4 further work on new Sledgehammer slicing
blanchet
parents: 75031
diff changeset
   212
    Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof: "
890b70f96fe4 further work on new Sledgehammer slicing
blanchet
parents: 75031
diff changeset
   213
  | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof: "
75040
fada390d49dd tweaked Auto Sledgehammer's behavior and output
blanchet
parents: 75036
diff changeset
   214
  | _ => "Try this: ")
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   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
41273636a82a added argo
blanchet
parents: 77428
diff changeset
   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
d8dc8fdc46fc prefer veriT over Z3 in sledgehammer
desharna
parents: 73940
diff changeset
   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
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   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
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
   243
  (case AList.lookup (op =) factss fact_filter of
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
   244
    SOME facts => facts
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
   245
  | NONE => snd (hd factss))
f741d55a81e5 thread slices through
blanchet
parents: 75023
diff changeset
   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
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   256
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   257
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   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
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   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
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   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
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   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
blanchet
parents: 55211
diff changeset
   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
212e9ec706cf run all installed provers by default
blanchet
parents: 75034
diff changeset
   274
    val local_provers = sort_strings (local_atps @ SMT_Config.available_solvers_of ctxt)
212e9ec706cf run all installed provers by default
blanchet
parents: 75034
diff changeset
   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
1bc4bc2c9fd1 killed final stops in Sledgehammer and friends
blanchet
parents: 62735
diff changeset
   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
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   280
end;