src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
author blanchet
Tue, 10 Sep 2013 15:56:51 +0200
changeset 53500 53b9326196fe
parent 53492 c3d7d9911aae
child 53517 1165e8960f59
permissions -rw-r--r--
don't be so verbose about SMT solver failures
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_provers.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
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
     9
signature SLEDGEHAMMER_PROVERS =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    10
sig
40181
3788b7adab36 integrated "smt" proof method with Sledgehammer
blanchet
parents: 40132
diff changeset
    11
  type failure = ATP_Proof.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
52555
6811291d1869 moved code -> easier debugging
smolkas
parents: 52196
diff changeset
    15
  type reconstructor = Sledgehammer_Reconstructor.reconstructor
6811291d1869 moved code -> easier debugging
smolkas
parents: 52196
diff changeset
    16
  type play = Sledgehammer_Reconstructor.play
6811291d1869 moved code -> easier debugging
smolkas
parents: 52196
diff changeset
    17
  type minimize_command = Sledgehammer_Reconstructor.minimize_command
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    18
53052
a0db255af8c5 sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents: 53047
diff changeset
    19
  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
    20
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    21
  type params =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    22
    {debug : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    23
     verbose : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    24
     overlord : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    25
     blocking : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    26
     provers : string list,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    27
     type_enc : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    28
     strict : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    29
     lam_trans : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    30
     uncurried_aliases : bool option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    31
     learn : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    32
     fact_filter : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    33
     max_facts : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    34
     fact_thresholds : real * real,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    35
     max_mono_iters : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    36
     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
    37
     isar_proofs : bool option,
51130
76d68444cd59 renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents: 51024
diff changeset
    38
     isar_compress : real,
52556
c8357085217c completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents: 52555
diff changeset
    39
     isar_compress_degree : int,
c8357085217c completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents: 52555
diff changeset
    40
     merge_timeout_slack : real,
52632
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
    41
     isar_try0 : bool,
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
    42
     isar_minimize : bool,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    43
     slice : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    44
     minimize : bool option,
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
    45
     timeout : Time.time option,
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
    46
     preplay_timeout : Time.time option,
51879
ee9562d31778 added preplay tracing
smolkas
parents: 51575
diff changeset
    47
     preplay_trace : bool,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    48
     expect : string}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    49
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    50
  type relevance_fudge =
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    51
    {local_const_multiplier : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    52
     worse_irrel_freq : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    53
     higher_order_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    54
     abs_rel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    55
     abs_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    56
     skolem_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    57
     theory_const_rel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    58
     theory_const_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    59
     chained_const_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    60
     intro_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    61
     elim_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    62
     simp_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    63
     local_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    64
     assum_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    65
     chained_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    66
     max_imperfect : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    67
     max_imperfect_exp : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    68
     threshold_divisor : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    69
     ridiculous_threshold : real}
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    70
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    71
  type prover_problem =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    72
    {state : Proof.state,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    73
     goal : thm,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    74
     subgoal : int,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    75
     subgoal_count : int,
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    76
     factss : (string * fact list) list}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    77
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    78
  type prover_result =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    79
    {outcome : failure option,
51009
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51007
diff changeset
    80
     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
    81
     used_from : fact list,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    82
     run_time : Time.time,
50669
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50667
diff changeset
    83
     preplay : play Lazy.lazy,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    84
     message : play -> string,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    85
     message_tail : string}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    86
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
    87
  type prover =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
    88
    params -> ((string * string list) list -> string -> minimize_command)
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
    89
    -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
    90
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
    91
  val dest_dir : string Config.T
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
    92
  val problem_prefix : string Config.T
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48131
diff changeset
    93
  val completish : bool Config.T
44592
54906b0337ab flip logic of boolean option so it's off by default
blanchet
parents: 44586
diff changeset
    94
  val atp_full_names : bool Config.T
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    95
  val smt_triggers : bool Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    96
  val smt_weights : bool Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    97
  val smt_weight_min_facts : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    98
  val smt_min_weight : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    99
  val smt_max_weight : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   100
  val smt_max_weight_index : int Config.T
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   101
  val smt_weight_curve : (int -> int) Unsynchronized.ref
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   102
  val smt_max_slices : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   103
  val smt_slice_fact_frac : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   104
  val smt_slice_time_frac : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   105
  val smt_slice_min_secs : int Config.T
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   106
  val SledgehammerN : string
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   107
  val plain_metis : reconstructor
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41241
diff changeset
   108
  val select_smt_solver : string -> Proof.context -> Proof.context
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   109
  val extract_reconstructor :
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   110
    params -> reconstructor -> string * (string * string list) list
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   111
  val is_reconstructor : string -> bool
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   112
  val is_atp : theory -> string -> bool
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
   113
  val is_smt_prover : Proof.context -> string -> bool
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   114
  val is_ho_atp: Proof.context -> string -> bool
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   115
  val is_unit_equational_atp : Proof.context -> string -> bool
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   116
  val is_prover_supported : Proof.context -> string -> bool
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   117
  val is_prover_installed : Proof.context -> string -> bool
51200
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   118
  val remotify_prover_if_supported_and_not_already_remote :
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   119
    Proof.context -> string -> string option
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   120
  val remotify_prover_if_not_installed :
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   121
    Proof.context -> string -> string option
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   122
  val default_max_facts_of_prover : Proof.context -> bool -> string -> int
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   123
  val is_unit_equality : term -> bool
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   124
  val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   125
  val is_built_in_const_of_prover :
41336
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   126
    Proof.context -> string -> string * typ -> term list -> bool * term list
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
   127
  val atp_relevance_fudge : relevance_fudge
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
   128
  val smt_relevance_fudge : relevance_fudge
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   129
  val relevance_fudge_of_prover : Proof.context -> string -> relevance_fudge
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   130
  val weight_smt_fact :
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   131
    Proof.context -> int -> ((string * stature) * thm) * int
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   132
    -> (string * stature) * (int option * thm)
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   133
  val supported_provers : Proof.context -> unit
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   134
  val kill_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   135
  val running_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   136
  val messages : int option -> unit
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   137
  val is_fact_chained : (('a * stature) * 'b) -> bool
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   138
  val filter_used_facts :
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   139
    bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   140
    ((''a * stature) * 'b) list
51200
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   141
  val isar_proof_reconstructor : Proof.context -> string -> string
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   142
  val get_prover : Proof.context -> mode -> string -> prover
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   143
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   144
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
   145
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   146
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   147
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43063
diff changeset
   148
open ATP_Util
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
   149
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39453
diff changeset
   150
open ATP_Proof
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
   151
open ATP_Systems
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
   152
open ATP_Problem_Generate
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
   153
open ATP_Proof_Reconstruct
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45520
diff changeset
   154
open Metis_Tactic
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   155
open Sledgehammer_Util
51005
ce4290c33d73 eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents: 50927
diff changeset
   156
open Sledgehammer_Fact
52555
6811291d1869 moved code -> easier debugging
smolkas
parents: 52196
diff changeset
   157
open Sledgehammer_Reconstructor
6811291d1869 moved code -> easier debugging
smolkas
parents: 52196
diff changeset
   158
open Sledgehammer_Print
49881
d9d73ebf9274 added proof minimization code from Steffen Smolka
blanchet
parents: 48802
diff changeset
   159
open Sledgehammer_Reconstruct
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   160
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents: 37581
diff changeset
   161
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents: 37581
diff changeset
   162
(** The Sledgehammer **)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents: 37581
diff changeset
   163
53052
a0db255af8c5 sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents: 53047
diff changeset
   164
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   165
45376
blanchet
parents: 45370
diff changeset
   166
(* Identifier that distinguishes Sledgehammer from other tools that could use
38102
019a49759829 fix bug in the newly introduced "bound concealing" code
blanchet
parents: 38100
diff changeset
   167
   "Async_Manager". *)
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   168
val SledgehammerN = "Sledgehammer"
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   169
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   170
val reconstructor_names = [metisN, smtN]
46365
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46340
diff changeset
   171
val plain_metis = Metis (hd partial_type_encs, combsN)
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   172
val is_reconstructor = member (op =) reconstructor_names
43228
2ed2f092e990 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents: 43226
diff changeset
   173
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   174
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
   175
43233
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   176
val select_smt_solver = Context.proof_map o SMT_Config.select_solver
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41241
diff changeset
   177
45376
blanchet
parents: 45370
diff changeset
   178
fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   179
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   180
fun is_atp_of_format is_format ctxt name =
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   181
  let val thy = Proof_Context.theory_of ctxt in
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   182
    case try (get_atp thy) name of
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47531
diff changeset
   183
      SOME config =>
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48656
diff changeset
   184
      exists (fn (_, ((_, format, _, _, _), _)) => is_format format)
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47531
diff changeset
   185
             (#best_slices (config ()) ctxt)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   186
    | NONE => false
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   187
  end
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   188
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   189
val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ)
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   190
val is_ho_atp = is_atp_of_format is_format_higher_order
44597
blanchet
parents: 44592
diff changeset
   191
45376
blanchet
parents: 45370
diff changeset
   192
fun is_prover_supported ctxt =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   193
  let val thy = Proof_Context.theory_of ctxt in
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   194
    is_reconstructor orf is_atp thy orf is_smt_prover ctxt
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   195
  end
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   196
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   197
fun is_prover_installed ctxt =
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   198
  is_reconstructor orf is_smt_prover ctxt orf
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   199
  is_atp_installed (Proof_Context.theory_of ctxt)
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   200
51200
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   201
fun remotify_prover_if_supported_and_not_already_remote ctxt name =
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   202
  if String.isPrefix remote_prefix name then
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   203
    SOME name
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   204
  else
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   205
    let val remote_name = remote_prefix ^ name in
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   206
      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   207
    end
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   208
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   209
fun remotify_prover_if_not_installed ctxt name =
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   210
  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   211
    SOME name
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   212
  else
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   213
    remotify_prover_if_supported_and_not_already_remote ctxt name
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   214
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45590
diff changeset
   215
fun get_slices slice slices =
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45590
diff changeset
   216
  (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   217
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48288
diff changeset
   218
val reconstructor_default_max_facts = 20
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   219
51186
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   220
fun slice_max_facts (_, (_, ( ((max_facts, _), _, _, _, _), _))) = max_facts
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   221
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   222
fun default_max_facts_of_prover ctxt slice name =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   223
  let val thy = Proof_Context.theory_of ctxt in
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   224
    if is_reconstructor name then
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48288
diff changeset
   225
      reconstructor_default_max_facts
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   226
    else if is_atp thy name then
51186
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   227
      fold (Integer.max o slice_max_facts)
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47531
diff changeset
   228
           (get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   229
    else (* is_smt_prover ctxt name *)
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   230
      SMT_Solver.default_max_relevant ctxt name
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   231
  end
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   232
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   233
fun is_if (@{const_name If}, _) = true
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   234
  | is_if _ = false
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   235
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   236
(* Beware of "if and only if" (which is translated as such) and "If" (which is
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   237
   translated to conditional equations). *)
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   238
fun is_good_unit_equality T t u =
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   239
  T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u])
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   240
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   241
fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   242
  | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   243
    is_unit_equality t
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   244
  | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   245
    is_unit_equality t
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   246
  | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) =
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   247
    is_good_unit_equality T t u
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   248
  | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) =
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42952
diff changeset
   249
    is_good_unit_equality T t u
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   250
  | is_unit_equality _ = false
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   251
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   252
fun is_appropriate_prop_of_prover ctxt name =
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   253
  if is_unit_equational_atp ctxt name then is_unit_equality else K true
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   254
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   255
fun is_built_in_const_of_prover ctxt name =
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41241
diff changeset
   256
  if is_smt_prover ctxt name then
41336
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   257
    let val ctxt = ctxt |> select_smt_solver name in
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   258
      fn x => fn ts =>
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   259
         if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   260
           (true, [])
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   261
         else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   262
           (true, ts)
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   263
         else
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   264
           (false, ts)
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   265
    end
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41241
diff changeset
   266
  else
41336
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41335
diff changeset
   267
    fn (s, _) => fn ts => (member (op =) atp_irrelevant_consts s, ts)
40071
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   268
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   269
(* FUDGE *)
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   270
val atp_relevance_fudge =
42738
2a9dcff63b80 remove unused parameter
blanchet
parents: 42737
diff changeset
   271
  {local_const_multiplier = 1.5,
41159
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41152
diff changeset
   272
   worse_irrel_freq = 100.0,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   273
   higher_order_irrel_weight = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   274
   abs_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   275
   abs_irrel_weight = 2.0,
47934
08d7aff8c7e6 lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
blanchet
parents: 47912
diff changeset
   276
   skolem_irrel_weight = 0.05,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   277
   theory_const_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   278
   theory_const_irrel_weight = 0.25,
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42730
diff changeset
   279
   chained_const_irrel_weight = 0.25,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   280
   intro_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   281
   elim_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   282
   simp_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   283
   local_bonus = 0.55,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   284
   assum_bonus = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   285
   chained_bonus = 1.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   286
   max_imperfect = 11.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   287
   max_imperfect_exp = 1.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   288
   threshold_divisor = 2.0,
41093
dfbc8759415f lower fudge factor
blanchet
parents: 41091
diff changeset
   289
   ridiculous_threshold = 0.01}
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   290
40071
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   291
(* FUDGE (FIXME) *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   292
val smt_relevance_fudge =
42738
2a9dcff63b80 remove unused parameter
blanchet
parents: 42737
diff changeset
   293
  {local_const_multiplier = #local_const_multiplier atp_relevance_fudge,
41159
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41152
diff changeset
   294
   worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
40071
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   295
   higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   296
   abs_rel_weight = #abs_rel_weight atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   297
   abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   298
   skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   299
   theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   300
   theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42730
diff changeset
   301
   chained_const_irrel_weight = #chained_const_irrel_weight atp_relevance_fudge,
40071
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   302
   intro_bonus = #intro_bonus atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   303
   elim_bonus = #elim_bonus atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   304
   simp_bonus = #simp_bonus atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   305
   local_bonus = #local_bonus atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   306
   assum_bonus = #assum_bonus atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   307
   chained_bonus = #chained_bonus atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   308
   max_imperfect = #max_imperfect atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   309
   max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   310
   threshold_divisor = #threshold_divisor atp_relevance_fudge,
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   311
   ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   312
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   313
fun relevance_fudge_of_prover ctxt name =
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   314
  if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   315
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   316
fun supported_provers ctxt =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   317
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   318
    val thy = Proof_Context.theory_of ctxt
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   319
    val (remote_provers, local_provers) =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   320
      reconstructor_names @
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   321
      sort_strings (supported_atps thy) @
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   322
      sort_strings (SMT_Solver.available_solvers_of ctxt)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   323
      |> List.partition (String.isPrefix remote_prefix)
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   324
  in
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   325
    Output.urgent_message ("Supported provers: " ^
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   326
                           commas (local_provers @ remote_provers) ^ ".")
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   327
  end
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   328
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   329
fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   330
fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   331
val messages = Async_Manager.thread_messages SledgehammerN "prover"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   332
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   333
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   334
(** problems, results, ATPs, etc. **)
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   335
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   336
type params =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   337
  {debug : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   338
   verbose : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   339
   overlord : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   340
   blocking : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   341
   provers : string list,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   342
   type_enc : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   343
   strict : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   344
   lam_trans : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   345
   uncurried_aliases : bool option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   346
   learn : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   347
   fact_filter : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   348
   max_facts : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   349
   fact_thresholds : real * real,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   350
   max_mono_iters : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   351
   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
   352
   isar_proofs : bool option,
51130
76d68444cd59 renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents: 51024
diff changeset
   353
   isar_compress : real,
52556
c8357085217c completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents: 52555
diff changeset
   354
   isar_compress_degree : int,
c8357085217c completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents: 52555
diff changeset
   355
   merge_timeout_slack : real,
52632
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   356
   isar_try0 : bool,
23393c31c7fe added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
smolkas
parents: 52556
diff changeset
   357
   isar_minimize : bool,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   358
   slice : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   359
   minimize : bool option,
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   360
   timeout : Time.time option,
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   361
   preplay_timeout : Time.time option,
51879
ee9562d31778 added preplay tracing
smolkas
parents: 51575
diff changeset
   362
   preplay_trace : bool,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   363
   expect : string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   364
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   365
type relevance_fudge =
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   366
  {local_const_multiplier : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   367
   worse_irrel_freq : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   368
   higher_order_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   369
   abs_rel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   370
   abs_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   371
   skolem_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   372
   theory_const_rel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   373
   theory_const_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   374
   chained_const_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   375
   intro_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   376
   elim_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   377
   simp_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   378
   local_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   379
   assum_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   380
   chained_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   381
   max_imperfect : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   382
   max_imperfect_exp : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   383
   threshold_divisor : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   384
   ridiculous_threshold : real}
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   385
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   386
type prover_problem =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   387
  {state : Proof.state,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   388
   goal : thm,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   389
   subgoal : int,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   390
   subgoal_count : int,
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   391
   factss : (string * fact list) list}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   392
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   393
type prover_result =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   394
  {outcome : failure option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   395
   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
   396
   used_from : fact list,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   397
   run_time : Time.time,
50669
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50667
diff changeset
   398
   preplay : play Lazy.lazy,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   399
   message : play -> string,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   400
   message_tail : string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   401
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   402
type prover =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   403
  params -> ((string * string list) list -> string -> minimize_command)
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   404
  -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   405
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   406
(* configuration attributes *)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   407
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   408
(* Empty string means create files in Isabelle's temporary files directory. *)
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   409
val dest_dir =
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   410
  Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   411
val problem_prefix =
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   412
  Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48131
diff changeset
   413
val completish =
0186df5074c8 renamed experimental option
blanchet
parents: 48131
diff changeset
   414
  Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   415
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   416
(* In addition to being easier to read, readable names are often much shorter,
44394
20bd9f90accc added option to control soundness of encodings more precisely, for evaluation purposes
blanchet
parents: 44393
diff changeset
   417
   especially if types are mangled in names. This makes a difference for some
20bd9f90accc added option to control soundness of encodings more precisely, for evaluation purposes
blanchet
parents: 44393
diff changeset
   418
   provers (e.g., E). For these reason, short names are enabled by default. *)
44592
54906b0337ab flip logic of boolean option so it's off by default
blanchet
parents: 44586
diff changeset
   419
val atp_full_names =
54906b0337ab flip logic of boolean option so it's off by default
blanchet
parents: 44586
diff changeset
   420
  Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   421
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   422
val smt_triggers =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   423
  Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   424
val smt_weights =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   425
  Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   426
val smt_weight_min_facts =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   427
  Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   428
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   429
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   430
val smt_min_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   431
  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   432
val smt_max_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   433
  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   434
val smt_max_weight_index =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   435
  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   436
val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   437
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   438
fun smt_fact_weight ctxt j num_facts =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   439
  if Config.get ctxt smt_weights andalso
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   440
     num_facts >= Config.get ctxt smt_weight_min_facts then
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   441
    let
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   442
      val min = Config.get ctxt smt_min_weight
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   443
      val max = Config.get ctxt smt_max_weight
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   444
      val max_index = Config.get ctxt smt_max_weight_index
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   445
      val curve = !smt_weight_curve
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   446
    in
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   447
      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   448
            div curve max_index)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   449
    end
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   450
  else
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   451
    NONE
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   452
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   453
fun weight_smt_fact ctxt num_facts ((info, th), j) =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   454
  let val thy = Proof_Context.theory_of ctxt in
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   455
    (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   456
  end
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   457
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   458
fun overlord_file_location_of_prover prover =
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   459
  (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   460
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   461
fun proof_banner mode name =
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   462
  case mode of
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   463
    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   464
  | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   465
  | _ => "Try this"
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   466
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   467
fun bunch_of_reconstructors needs_full_types lam_trans =
48800
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   468
  if needs_full_types then
48802
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   469
    [Metis (full_type_enc, lam_trans false),
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   470
     Metis (really_full_type_enc, lam_trans false),
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   471
     Metis (full_type_enc, lam_trans true),
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   472
     Metis (really_full_type_enc, lam_trans true),
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   473
     SMT]
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   474
  else
48800
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   475
    [Metis (partial_type_enc, lam_trans false),
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   476
     Metis (full_type_enc, lam_trans false),
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   477
     Metis (no_typesN, lam_trans true),
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   478
     Metis (really_full_type_enc, lam_trans true),
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   479
     SMT]
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   480
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   481
fun extract_reconstructor ({type_enc, lam_trans, ...} : params)
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   482
                          (Metis (type_enc', lam_trans')) =
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   483
    let
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   484
      val override_params =
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   485
        (if is_none type_enc andalso type_enc' = hd partial_type_encs then
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   486
           []
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   487
         else
45566
da05ce2de5a8 better threading of type encodings between Sledgehammer and "metis"
blanchet
parents: 45561
diff changeset
   488
           [("type_enc", [hd (unalias_type_enc type_enc')])]) @
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   489
        (if is_none lam_trans andalso lam_trans' = metis_default_lam_trans then
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   490
           []
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   491
         else
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   492
           [("lam_trans", [lam_trans'])])
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   493
    in (metisN, override_params) end
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   494
  | extract_reconstructor _ SMT = (smtN, [])
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   495
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   496
(* based on "Mirabelle.can_apply" and generalized *)
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   497
fun timed_apply timeout tac state i =
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   498
  let
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   499
    val {context = ctxt, facts, goal} = Proof.goal state
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   500
    val full_tac = Method.insert_tac facts i THEN tac ctxt i
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   501
  in time_limit timeout (try (Seq.pull o full_tac)) goal end
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   502
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   503
fun tac_of_reconstructor (Metis (type_enc, lam_trans)) =
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45520
diff changeset
   504
    metis_tac [type_enc] lam_trans
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   505
  | tac_of_reconstructor SMT = SMT_Solver.smt_tac
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   506
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   507
fun timed_reconstructor reconstr debug timeout ths =
44651
5d6a11e166cf renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents: 44649
diff changeset
   508
  (Config.put Metis_Tactic.verbose debug
45557
b427b23ec89c quiet down SMT
blanchet
parents: 45556
diff changeset
   509
   #> Config.put SMT_Config.verbose debug
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   510
   #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   511
  |> timed_apply timeout
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   512
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   513
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   514
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   515
fun filter_used_facts keep_chained used =
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   516
  filter ((member (op =) used o fst) orf
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   517
          (if keep_chained then is_fact_chained else K false))
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   518
45781
fc2c368b5f54 use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts
blanchet
parents: 45707
diff changeset
   519
fun play_one_line_proof mode debug verbose timeout pairs state i preferred
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   520
                        reconstrs =
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   521
  let
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   522
    fun get_preferred reconstrs =
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   523
      if member (op =) reconstrs preferred then preferred
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   524
      else List.last reconstrs
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   525
  in
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   526
    if timeout = SOME Time.zeroTime then
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   527
      Trust_Playable (get_preferred reconstrs, NONE)
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   528
    else
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   529
      let
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   530
        val _ =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   531
          if mode = Minimize then Output.urgent_message "Preplaying proof..."
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   532
          else ()
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   533
        val ths = pairs |> sort_wrt (fst o fst) |> map snd
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   534
        fun play [] [] = Failed_to_Play (get_preferred reconstrs)
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   535
          | play timed_outs [] =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   536
            Trust_Playable (get_preferred timed_outs, timeout)
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   537
          | play timed_out (reconstr :: reconstrs) =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   538
            let
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   539
              val _ =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   540
                if verbose then
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   541
                  "Trying \"" ^ string_of_reconstructor reconstr ^ "\"" ^
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   542
                  (case timeout of
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   543
                     SOME timeout => " for " ^ string_of_time timeout
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   544
                   | NONE => "") ^ "..."
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   545
                  |> Output.urgent_message
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   546
                else
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   547
                  ()
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   548
              val timer = Timer.startRealTimer ()
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   549
            in
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   550
              case timed_reconstructor reconstr debug timeout ths state i of
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   551
                SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   552
              | _ => play timed_out reconstrs
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   553
            end
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   554
            handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   555
      in play [] reconstrs end
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   556
  end
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   557
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   558
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   559
(* generic TPTP-based ATPs *)
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   560
42730
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   561
(* Too general means, positive equality literal with a variable X as one
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   562
   operand, when X does not occur properly in the other operand. This rules out
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   563
   clearly inconsistent facts such as X = a | X = b, though it by no means
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   564
   guarantees soundness. *)
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   565
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   566
fun get_facts_of_filter _ [(_, facts)] = facts
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   567
  | get_facts_of_filter fact_filter factss =
51013
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   568
    case AList.lookup (op =) factss fact_filter of
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   569
      SOME facts => facts
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   570
    | NONE => snd (hd factss)
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   571
42730
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   572
(* Unwanted equalities are those between a (bound or schematic) variable that
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   573
   does not properly occur in the second operand. *)
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   574
val is_exhaustive_finite =
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   575
  let
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   576
    fun is_bad_equal (Var z) t =
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   577
        not (exists_subterm (fn Var z' => z = z' | _ => false) t)
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   578
      | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   579
      | is_bad_equal _ _ = false
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   580
    fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   581
    fun do_formula pos t =
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   582
      case (pos, t) of
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   583
        (_, @{const Trueprop} $ t1) => do_formula pos t1
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   584
      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   585
        do_formula pos t'
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   586
      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   587
        do_formula pos t'
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   588
      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   589
        do_formula pos t'
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   590
      | (_, @{const "==>"} $ t1 $ t2) =>
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   591
        do_formula (not pos) t1 andalso
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   592
        (t2 = @{prop False} orelse do_formula pos t2)
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   593
      | (_, @{const HOL.implies} $ t1 $ t2) =>
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   594
        do_formula (not pos) t1 andalso
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   595
        (t2 = @{const False} orelse do_formula pos t2)
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   596
      | (_, @{const Not} $ t1) => do_formula (not pos) t1
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   597
      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   598
      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   599
      | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   600
      | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   601
      | _ => false
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   602
  in do_formula true end
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   603
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   604
fun has_bound_or_var_of_type pred =
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   605
  exists_subterm (fn Var (_, T as Type _) => pred T
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   606
                   | Abs (_, T as Type _, _) => pred T
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   607
                   | _ => false)
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   608
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   609
(* Facts are forbidden to contain variables of these types. The typical reason
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   610
   is that they lead to unsoundness. Note that "unit" satisfies numerous
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   611
   equations like "?x = ()". The resulting clauses will have no type constraint,
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   612
   yielding false proofs. Even "bool" leads to many unsound proofs, though only
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   613
   for higher-order problems. *)
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   614
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   615
(* Facts containing variables of type "unit" or "bool" or of the form
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   616
   "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   617
   are omitted. *)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   618
fun is_dangerous_prop ctxt =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   619
  transform_elim_prop
44393
23adec5984f1 make sound mode more sound (and clean up code)
blanchet
parents: 44088
diff changeset
   620
  #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
42730
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   621
      is_exhaustive_finite)
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   622
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   623
(* Important messages are important but not so important that users want to see
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   624
   them each time. *)
44649
3d7b737d200a fewer TPTP important messages
blanchet
parents: 44636
diff changeset
   625
val atp_important_message_keep_quotient = 25
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   626
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44397
diff changeset
   627
fun choose_type_enc soundness best_type_enc format =
44397
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44394
diff changeset
   628
  the_default best_type_enc
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   629
  #> type_enc_of_string soundness
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44397
diff changeset
   630
  #> adjust_type_enc format
42548
ea2a28b1938f make sure the minimizer monomorphizes when it should
blanchet
parents: 42544
diff changeset
   631
51200
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   632
fun isar_proof_reconstructor ctxt name =
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   633
  let val thy = Proof_Context.theory_of ctxt in
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   634
    if is_atp thy name then name
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   635
    else remotify_prover_if_not_installed ctxt eN |> the_default name
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   636
  end
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   637
51200
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   638
(* See the analogous logic in the function "maybe_minimize" in
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   639
  "sledgehammer_minimize.ML". *)
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   640
fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   641
                            name preplay =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   642
  let
51200
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   643
    val maybe_isar_name =
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   644
      name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   645
    val (min_name, override_params) =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   646
      case preplay of
51200
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   647
        Played (reconstr, _) =>
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   648
        if isar_proofs = SOME true then (maybe_isar_name, [])
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   649
        else extract_reconstructor params reconstr
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   650
      | _ => (maybe_isar_name, [])
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   651
  in minimize_command override_params min_name end
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   652
53480
247817dbb990 limit the number of instances of a single theorem
blanchet
parents: 53478
diff changeset
   653
val max_fact_instances = 10 (* FUDGE *)
247817dbb990 limit the number of instances of a single theorem
blanchet
parents: 53478
diff changeset
   654
52034
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
   655
fun repair_monomorph_context max_iters best_max_iters max_new_instances
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
   656
                             best_max_new_instances =
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
   657
  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
   658
  #> Config.put Monomorph.max_new_instances
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
   659
         (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
   660
  #> 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
   661
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   662
fun suffix_of_mode Auto_Try = "_try"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   663
  | suffix_of_mode Try = "_try"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   664
  | suffix_of_mode Normal = ""
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   665
  | suffix_of_mode MaSh = ""
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   666
  | suffix_of_mode Auto_Minimize = "_min"
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   667
  | suffix_of_mode Minimize = "_min"
44509
369e8c28a61a added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files
blanchet
parents: 44423
diff changeset
   668
44423
f74707e12d30 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents: 44416
diff changeset
   669
(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
43631
4144d7b4ec77 enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents: 43626
diff changeset
   670
   Linux appears to be the only ATP that does not honor its time limit. *)
43690
92f78a4a5628 better setup for experimental "z3_atp"
blanchet
parents: 43655
diff changeset
   671
val atp_timeout_slack = seconds 1.0
43631
4144d7b4ec77 enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents: 43626
diff changeset
   672
48331
f190a6dbb29b make the monomorphizer more predictable by making the cutoff independent on the number of facts
blanchet
parents: 48321
diff changeset
   673
val mono_max_privileged_facts = 10
f190a6dbb29b make the monomorphizer more predictable by making the cutoff independent on the number of facts
blanchet
parents: 48321
diff changeset
   674
51186
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   675
(* For low values of "max_facts", this fudge value ensures that most slices are
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   676
   invoked with a nontrivial amount of facts. *)
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   677
val max_fact_factor_fudge = 5
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   678
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   679
fun run_atp mode name
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   680
        ({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   681
          best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46296
diff changeset
   682
        (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
51024
98fb341d32e3 distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents: 51014
diff changeset
   683
                    uncurried_aliases, fact_filter, max_facts, max_mono_iters,
51130
76d68444cd59 renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents: 51024
diff changeset
   684
                    max_new_mono_instances, isar_proofs, isar_compress,
53137
blanchet
parents: 53052
diff changeset
   685
                    isar_compress_degree, merge_timeout_slack, isar_try0,
blanchet
parents: 53052
diff changeset
   686
                    isar_minimize, slice, timeout, preplay_timeout,
blanchet
parents: 53052
diff changeset
   687
                    preplay_trace, ...})
43037
ade5c84f860f cleanup proof text generation code
blanchet
parents: 43034
diff changeset
   688
        minimize_command
51013
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   689
        ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   690
  let
42182
a630978fc967 start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
blanchet
parents: 42181
diff changeset
   691
    val thy = Proof.theory_of state
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   692
    val ctxt = Proof.context_of state
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47934
diff changeset
   693
    val atp_mode =
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48131
diff changeset
   694
      if Config.get ctxt completish then Sledgehammer_Completish
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47934
diff changeset
   695
      else Sledgehammer
52196
2281f33e8da6 redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents: 52150
diff changeset
   696
    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
41159
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41152
diff changeset
   697
    val (dest_dir, problem_prefix) =
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   698
      if overlord then overlord_file_location_of_prover name
41159
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41152
diff changeset
   699
      else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   700
    val problem_file_name =
41159
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41152
diff changeset
   701
      Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   702
                  suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   703
    val prob_path =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   704
      if dest_dir = "" then
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   705
        File.tmp_path problem_file_name
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   706
      else if File.exists (Path.explode dest_dir) then
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   707
        Path.append (Path.explode dest_dir) problem_file_name
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   708
      else
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   709
        error ("No such directory: " ^ quote dest_dir ^ ".")
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52697
diff changeset
   710
    val exec = exec ()
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   711
    val command0 =
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47038
diff changeset
   712
      case find_first (fn var => getenv var <> "") (fst exec) of
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   713
        SOME var =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   714
        let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   715
          val pref = getenv var ^ "/"
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   716
          val paths = map (Path.explode o prefix pref) (snd exec)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   717
        in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   718
          case find_first File.exists paths of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   719
            SOME path => path
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   720
          | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   721
        end
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47038
diff changeset
   722
      | NONE => error ("The environment variable " ^ quote (hd (fst exec)) ^
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47038
diff changeset
   723
                       " is not set.")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   724
    fun split_time s =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   725
      let
42448
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   726
        val split = String.tokens (fn c => str c = "\n")
47737
63c939dcd055 made "split_last" more robust in the face of obscure low-level errors
blanchet
parents: 47606
diff changeset
   727
        val (output, t) =
63c939dcd055 made "split_last" more robust in the face of obscure low-level errors
blanchet
parents: 47606
diff changeset
   728
          s |> split |> (try split_last #> the_default ([], "0"))
63c939dcd055 made "split_last" more robust in the face of obscure low-level errors
blanchet
parents: 47606
diff changeset
   729
            |>> cat_lines
42448
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   730
        fun as_num f = f >> (fst o read_int)
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   731
        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   732
        val digit = Scan.one Symbol.is_ascii_digit
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   733
        val num3 = as_num (digit ::: digit ::: (digit >> single))
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   734
        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
45381
d17e7b4422e8 more millisecond cleanup
blanchet
parents: 45379
diff changeset
   735
        val as_time =
d17e7b4422e8 more millisecond cleanup
blanchet
parents: 45379
diff changeset
   736
          raw_explode #> Scan.read Symbol.stopper time #> the_default 0
47737
63c939dcd055 made "split_last" more robust in the face of obscure low-level errors
blanchet
parents: 47606
diff changeset
   737
      in (output, as_time t |> Time.fromMilliseconds) end
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   738
    fun run () =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   739
      let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   740
        (* If slicing is disabled, we expand the last slice to fill the entire
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   741
           time available. *)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   742
        val actual_slices = get_slices slice (best_slices ctxt)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   743
        val num_actual_slices = length actual_slices
51186
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   744
        val max_fact_factor =
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   745
          case max_facts of
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   746
            NONE => 1.0
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   747
          | SOME max =>
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   748
            Real.fromInt max
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   749
            / Real.fromInt (fold (Integer.max o slice_max_facts)
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   750
                                 actual_slices 0)
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   751
        fun monomorphize_facts facts =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   752
          let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   753
            val ctxt =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   754
              ctxt
53478
8c3ccb314469 use new monomorphizer in Sledgehammer
blanchet
parents: 53137
diff changeset
   755
              |> repair_monomorph_context max_mono_iters
52034
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
   756
                     best_max_mono_iters max_new_mono_instances
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
   757
                     best_max_new_mono_instances
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   758
            (* pseudo-theorem involving the same constants as the subgoal *)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   759
            val subgoal_th =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   760
              Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   761
            val rths =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   762
              facts |> chop mono_max_privileged_facts
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   763
                    |>> map (pair 1 o snd)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   764
                    ||> map (pair 2 o snd)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   765
                    |> op @
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   766
                    |> cons (0, subgoal_th)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   767
          in
53478
8c3ccb314469 use new monomorphizer in Sledgehammer
blanchet
parents: 53137
diff changeset
   768
            Monomorph.monomorph atp_schematic_consts_of ctxt rths
8c3ccb314469 use new monomorphizer in Sledgehammer
blanchet
parents: 53137
diff changeset
   769
            |> tl |> curry ListPair.zip (map fst facts)
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   770
            |> maps (fn (name, rths) =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   771
                        map (pair name o zero_var_indexes o snd) rths)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   772
          end
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   773
        fun run_slice time_left (cache_key, cache_value)
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48656
diff changeset
   774
                (slice, (time_frac,
51011
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 51010
diff changeset
   775
                     (key as ((best_max_facts, best_fact_filter), format,
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 51010
diff changeset
   776
                              best_type_enc, best_lam_trans,
62b992e53eb8 store fact filter along with ATP slice
blanchet
parents: 51010
diff changeset
   777
                              best_uncurried_aliases),
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48656
diff changeset
   778
                      extra))) =
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   779
          let
51024
98fb341d32e3 distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents: 51014
diff changeset
   780
            val effective_fact_filter =
98fb341d32e3 distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents: 51014
diff changeset
   781
              fact_filter |> the_default best_fact_filter
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   782
            val facts = get_facts_of_filter effective_fact_filter factss
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   783
            val num_facts =
51186
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   784
              Real.ceil (max_fact_factor * Real.fromInt best_max_facts) +
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   785
              max_fact_factor_fudge
c8721406511a interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices
blanchet
parents: 51181
diff changeset
   786
              |> Integer.min (length facts)
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   787
            val soundness = if strict then Strict else Non_Strict
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   788
            val type_enc =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   789
              type_enc |> choose_type_enc soundness best_type_enc format
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   790
            val sound = is_type_enc_sound type_enc
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   791
            val real_ms = Real.fromInt o Time.toMilliseconds
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   792
            val slice_timeout =
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   793
              case time_left of
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   794
                SOME time_left =>
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   795
                ((real_ms time_left
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   796
                  |> (if slice < num_actual_slices - 1 then
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   797
                        curry Real.min (time_frac * real_ms (the timeout))
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   798
                      else
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   799
                        I))
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   800
                 * 0.001)
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   801
                |> seconds |> SOME
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   802
              | NONE => NONE
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   803
            val generous_slice_timeout =
50558
a719106124d8 avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)
blanchet
parents: 50557
diff changeset
   804
              if mode = MaSh then NONE
a719106124d8 avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)
blanchet
parents: 50557
diff changeset
   805
              else Option.map (curry Time.+ atp_timeout_slack) slice_timeout
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   806
            val _ =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   807
              if debug then
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   808
                quote name ^ " slice #" ^ string_of_int (slice + 1) ^
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   809
                " with " ^ string_of_int num_facts ^ " fact" ^
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   810
                plural_s num_facts ^
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   811
                (case slice_timeout of
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   812
                   SOME timeout => " for " ^ string_of_time timeout
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   813
                 | NONE => "") ^ "..."
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   814
                |> Output.urgent_message
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   815
              else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   816
                ()
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   817
            val readable_names = not (Config.get ctxt atp_full_names)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   818
            val lam_trans =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   819
              case lam_trans of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   820
                SOME s => s
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   821
              | NONE => best_lam_trans
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   822
            val uncurried_aliases =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   823
              case uncurried_aliases of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   824
                SOME b => b
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   825
              | NONE => best_uncurried_aliases
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   826
            val value as (atp_problem, _, fact_names, _, _) =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   827
              if cache_key = SOME key then
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   828
                cache_value
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   829
              else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   830
                facts
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   831
                |> not sound
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   832
                   ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   833
                |> take num_facts
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   834
                |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   835
                |> map (apsnd prop_of)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   836
                |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   837
                                       lam_trans uncurried_aliases
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   838
                                       readable_names true hyp_ts concl_t
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   839
            fun sel_weights () = atp_problem_selection_weights atp_problem
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   840
            fun ord_info () = atp_problem_term_order_info atp_problem
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   841
            val ord = effective_term_order ctxt name
53492
c3d7d9911aae since "full_proofs" can influence the proof search significantly (e.g. by disabling splitting for SPASS), it shouldn't be affected by the "debug" flag in the interest of minimizing confusion
blanchet
parents: 53480
diff changeset
   842
            val full_proof = isar_proofs |> the_default (mode = Minimize)
50927
31d864d5057a added E-Par support
blanchet
parents: 50759
diff changeset
   843
            val args =
31d864d5057a added E-Par support
blanchet
parents: 50759
diff changeset
   844
              arguments ctxt full_proof extra
31d864d5057a added E-Par support
blanchet
parents: 50759
diff changeset
   845
                        (slice_timeout |> the_default one_day)
31d864d5057a added E-Par support
blanchet
parents: 50759
diff changeset
   846
                        (File.shell_path prob_path) (ord, ord_info, sel_weights)
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   847
            val command =
50927
31d864d5057a added E-Par support
blanchet
parents: 50759
diff changeset
   848
              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
48532
c0f44941e674 Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
blanchet
parents: 48392
diff changeset
   849
              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   850
            val _ =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   851
              atp_problem
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   852
              |> lines_of_atp_problem format ord ord_info
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   853
              |> cons ("% " ^ command ^ "\n")
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   854
              |> File.write_list prob_path
52034
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
   855
            val ((output, run_time), (atp_proof, outcome)) =
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   856
              time_limit generous_slice_timeout Isabelle_System.bash_output
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   857
                         command
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   858
              |>> (if overlord then
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   859
                     prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   860
                   else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   861
                     I)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   862
              |> fst |> split_time
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   863
              |> (fn accum as (output, _) =>
52034
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
   864
                     (accum,
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48656
diff changeset
   865
                      extract_tstplike_proof_and_outcome verbose proof_delims
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48656
diff changeset
   866
                                                         known_failures output
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   867
                      |>> atp_proof_of_tstplike_proof atp_problem
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   868
                      handle UNRECOGNIZED_ATP_PROOF () =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   869
                             ([], SOME ProofIncomplete)))
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   870
              handle TimeLimit.TimeOut =>
52034
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
   871
                     (("", the slice_timeout), ([], SOME TimedOut))
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   872
            val outcome =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   873
              case outcome of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   874
                NONE =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   875
                (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   876
                      |> Option.map (sort string_ord) of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   877
                   SOME facts =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   878
                   let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   879
                     val failure =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   880
                       UnsoundProof (is_type_enc_sound type_enc, facts)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   881
                   in
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   882
                     if debug then (warning (string_of_failure failure); NONE)
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   883
                     else SOME failure
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   884
                   end
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   885
                 | NONE => NONE)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   886
              | _ => outcome
51013
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   887
          in
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   888
            ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   889
          end
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   890
        val timer = Timer.startRealTimer ()
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   891
        fun maybe_run_slice slice
51013
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   892
                (result as (cache, (_, run_time0, _, _, SOME _))) =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   893
            let
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   894
              val time_left =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   895
                Option.map
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   896
                    (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   897
                    timeout
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   898
            in
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   899
              if time_left <> NONE andalso
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   900
                 Time.<= (the time_left, Time.zeroTime) then
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   901
                result
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   902
              else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   903
                run_slice time_left cache slice
51013
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   904
                |> (fn (cache, (output, run_time, used_from, atp_proof,
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   905
                                outcome)) =>
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   906
                       (cache, (output, Time.+ (run_time0, run_time), used_from,
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   907
                                atp_proof, outcome)))
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   908
            end
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   909
          | maybe_run_slice _ result = result
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   910
      in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   911
        ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
51013
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   912
         ("", Time.zeroTime, [], [], SOME InternalError))
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   913
        |> fold maybe_run_slice actual_slices
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   914
      end
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   915
    (* If the problem file has not been exported, remove it; otherwise, export
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   916
       the proof file too. *)
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   917
    fun clean_up () =
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   918
      if dest_dir = "" then (try File.rm prob_path; ()) else ()
51013
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   919
    fun export (_, (output, _, _, _, _)) =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   920
      if dest_dir = "" then ()
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   921
      else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
52150
41c885784e04 handle lambda-lifted problems in Isar construction code
blanchet
parents: 52125
diff changeset
   922
    val ((_, (_, pool, fact_names, lifted, sym_tab)),
51013
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   923
         (output, run_time, used_from, atp_proof, outcome)) =
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   924
      with_cleanup clean_up run () |> tap export
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   925
    val important_message =
53052
a0db255af8c5 sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents: 53047
diff changeset
   926
      if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0
a0db255af8c5 sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents: 53047
diff changeset
   927
      then
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   928
        extract_important_message output
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   929
      else
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   930
        ""
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   931
    val (used_facts, preplay, message, message_tail) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   932
      case outcome of
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   933
        NONE =>
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   934
        let
45551
a62c7a21f4ab removed needless baggage
blanchet
parents: 45521
diff changeset
   935
          val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
45590
dc9a7ff13e37 made SML/NJ happy
blanchet
parents: 45574
diff changeset
   936
          val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45520
diff changeset
   937
          val reconstrs =
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45553
diff changeset
   938
            bunch_of_reconstructors needs_full_types
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   939
                (lam_trans_of_atp_proof atp_proof
46405
76ed3b7092fc try to pass fewer options to Metis
blanchet
parents: 46365
diff changeset
   940
                 o (fn desperate => if desperate then hide_lamsN
76ed3b7092fc try to pass fewer options to Metis
blanchet
parents: 46365
diff changeset
   941
                                    else metis_default_lam_trans))
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   942
        in
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   943
          (used_facts,
50669
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50667
diff changeset
   944
           Lazy.lazy (fn () =>
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50667
diff changeset
   945
             let
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50667
diff changeset
   946
               val used_pairs =
51013
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   947
                 used_from |> filter_used_facts false used_facts
50669
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50667
diff changeset
   948
             in
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50667
diff changeset
   949
               play_one_line_proof mode debug verbose preplay_timeout
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50667
diff changeset
   950
                   used_pairs state subgoal (hd reconstrs) reconstrs
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50667
diff changeset
   951
             end),
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   952
           fn preplay =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   953
              let
49921
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   954
                val _ =
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   955
                  if verbose then
51232
1f614b4eb367 tuned misleading message
blanchet
parents: 51215
diff changeset
   956
                    Output.urgent_message "Generating proof text..."
49921
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   957
                  else
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   958
                    ()
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   959
                val isar_params =
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52697
diff changeset
   960
                  (debug, verbose, preplay_timeout, preplay_trace,
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52697
diff changeset
   961
                   isar_compress, isar_compress_degree, merge_timeout_slack,
53137
blanchet
parents: 53052
diff changeset
   962
                   isar_try0, isar_minimize, pool, fact_names, lifted, sym_tab,
blanchet
parents: 53052
diff changeset
   963
                   atp_proof, goal)
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   964
                val one_line_params =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   965
                  (preplay, proof_banner mode name, used_facts,
51200
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   966
                   choose_minimize_command ctxt params minimize_command name
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51190
diff changeset
   967
                                           preplay,
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   968
                   subgoal, subgoal_count)
48799
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   969
                val num_chained = length (#facts (Proof.goal state))
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   970
              in
53052
a0db255af8c5 sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents: 53047
diff changeset
   971
                proof_text ctxt isar_proofs isar_params
52754
d9d90d29860e added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
blanchet
parents: 52697
diff changeset
   972
                           num_chained one_line_params
48799
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   973
              end,
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   974
           (if verbose then
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
   975
              "\nATP real CPU time: " ^ string_of_time run_time ^ "."
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   976
            else
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   977
              "") ^
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   978
           (if important_message <> "" then
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   979
              "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   980
              important_message
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   981
            else
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   982
              ""))
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   983
        end
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   984
      | SOME failure =>
50669
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50667
diff changeset
   985
        ([], Lazy.value (Failed_to_Play plain_metis),
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
   986
         fn _ => string_of_failure failure, "")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   987
  in
51013
2d07f0fdcb29 use the right filter in each slice
blanchet
parents: 51011
diff changeset
   988
    {outcome = outcome, used_facts = used_facts, used_from = used_from,
51009
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51007
diff changeset
   989
     run_time = run_time, preplay = preplay, message = message,
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51007
diff changeset
   990
     message_tail = message_tail}
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   991
  end
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   992
51014
cca90dd51e82 also have SMT solvers alternate fact filter
blanchet
parents: 51013
diff changeset
   993
fun rotate_one (x :: xs) = xs @ [x]
cca90dd51e82 also have SMT solvers alternate fact filter
blanchet
parents: 51013
diff changeset
   994
40669
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   995
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   996
   these are sorted out properly in the SMT module, we have to interpret these
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   997
   ourselves. *)
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   998
val remote_smt_failures =
43631
4144d7b4ec77 enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents: 43626
diff changeset
   999
  [(2, NoLibwwwPerl),
4144d7b4ec77 enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents: 43626
diff changeset
  1000
   (22, CantConnect)]
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
  1001
val z3_failures =
41236
def0a3013554 trap one more Z3 error
blanchet
parents: 41222
diff changeset
  1002
  [(101, OutOfResources),
def0a3013554 trap one more Z3 error
blanchet
parents: 41222
diff changeset
  1003
   (103, MalformedInput),
50667
e0cba8893691 added 112 to list of known Z3 error codes
blanchet
parents: 50558
diff changeset
  1004
   (110, MalformedInput),
e0cba8893691 added 112 to list of known Z3 error codes
blanchet
parents: 50558
diff changeset
  1005
   (112, TimedOut)]
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
  1006
val unix_failures =
48797
e65385336531 recognize bus errors as crash
blanchet
parents: 48716
diff changeset
  1007
  [(138, Crashed),
e65385336531 recognize bus errors as crash
blanchet
parents: 48716
diff changeset
  1008
   (139, Crashed)]
43631
4144d7b4ec77 enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents: 43626
diff changeset
  1009
val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
40555
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
  1010
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
  1011
fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1012
    if is_real_cex then Unprovable else GaveUp
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
  1013
  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
  1014
  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
  1015
    (case AList.lookup (op =) smt_failures code of
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
  1016
       SOME failure => failure
41259
13972ced98d9 more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents: 41256
diff changeset
  1017
     | NONE => UnknownError ("Abnormal termination with exit code " ^
13972ced98d9 more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents: 41256
diff changeset
  1018
                             string_of_int code ^ "."))
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
  1019
  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
  1020
  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
  1021
40698
8a3f7ea91370 cosmetics
blanchet
parents: 40693
diff changeset
  1022
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1023
val smt_max_slices =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1024
  Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1025
val smt_slice_fact_frac =
51014
cca90dd51e82 also have SMT solvers alternate fact filter
blanchet
parents: 51013
diff changeset
  1026
  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac}
cca90dd51e82 also have SMT solvers alternate fact filter
blanchet
parents: 51013
diff changeset
  1027
                           (K 0.667)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1028
val smt_slice_time_frac =
51014
cca90dd51e82 also have SMT solvers alternate fact filter
blanchet
parents: 51013
diff changeset
  1029
  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1030
val smt_slice_min_secs =
51014
cca90dd51e82 also have SMT solvers alternate fact filter
blanchet
parents: 51013
diff changeset
  1031
  Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
  1032
50759
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1033
fun smt_filter_loop name
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
  1034
                    ({debug, verbose, overlord, max_mono_iters,
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45590
diff changeset
  1035
                      max_new_mono_instances, timeout, slice, ...} : params)
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 50020
diff changeset
  1036
                    state goal i =
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
  1037
  let
50759
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1038
    fun repair_context ctxt =
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1039
      ctxt |> select_smt_solver name
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1040
           |> Config.put SMT_Config.verbose debug
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1041
           |> (if overlord then
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1042
                 Config.put SMT_Config.debug_files
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51879
diff changeset
  1043
                            (overlord_file_location_of_prover name
50759
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1044
                             |> (fn (path, name) => path ^ "/" ^ name))
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1045
               else
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1046
                 I)
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1047
           |> Config.put SMT_Config.infer_triggers
495ae21b0958 cleaner context threading
blanchet
parents: 50669
diff changeset
  1048
                         (Config.get ctxt smt_triggers)
52034
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
  1049
           |> repair_monomorph_context max_mono_iters default_max_mono_iters
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
  1050
                  max_new_mono_instances default_max_new_mono_instances
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
  1051
    val state = Proof.map_context (repair_context) state
11b48e7a4e7e correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
blanchet
parents: 52031
diff changeset
  1052
    val ctxt = Proof.context_of state
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45590
diff changeset
  1053
    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
51024
98fb341d32e3 distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents: 51014
diff changeset
  1054
    fun do_slice timeout slice outcome0 time_so_far
98fb341d32e3 distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents: 51014
diff changeset
  1055
                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1056
      let
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1057
        val timer = Timer.startRealTimer ()
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1058
        val slice_timeout =
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1059
          if slice < max_slices andalso timeout <> NONE then
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1060
            let val ms = timeout |> the |> Time.toMilliseconds in
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1061
              Int.min (ms,
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1062
                  Int.max (1000 * Config.get ctxt smt_slice_min_secs,
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1063
                      Real.ceil (Config.get ctxt smt_slice_time_frac
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1064
                                 * Real.fromInt ms)))
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1065
              |> Time.fromMilliseconds |> SOME
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1066
            end
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1067
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1068
            timeout
51009
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51007
diff changeset
  1069
        val num_facts = length weighted_facts
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1070
        val _ =
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1071
          if debug then
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1072
            quote name ^ " slice " ^ string_of_int slice ^ " with " ^
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1073
            string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1074
            (case slice_timeout of
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
  1075
               SOME timeout => " for " ^ string_of_time timeout
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1076
             | NONE => "") ^ "..."
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1077
            |> Output.urgent_message
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1078
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1079
            ()
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
  1080
        val birth = Timer.checkRealTimer timer
41171
043f8dc3b51f facilitate debugging
blanchet
parents: 41169
diff changeset
  1081
        val _ =
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41209
diff changeset
  1082
          if debug then Output.urgent_message "Invoking SMT solver..." else ()
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1083
        val (outcome, used_facts) =
51204
20f6d400cc68 don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary
blanchet
parents: 51200
diff changeset
  1084
          SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1085
          |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41236
diff changeset
  1086
          |> (fn {outcome, used_facts} => (outcome, used_facts))
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1087
          handle exn => if Exn.is_interrupt exn then
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1088
                          reraise exn
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1089
                        else
42061
71077681eaf6 let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
blanchet
parents: 42060
diff changeset
  1090
                          (ML_Compiler.exn_message exn
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1091
                           |> SMT_Failure.Other_Failure |> SOME, [])
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
  1092
        val death = Timer.checkRealTimer timer
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1093
        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
  1094
        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1095
        val too_many_facts_perhaps =
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1096
          case outcome of
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1097
            NONE => false
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1098
          | SOME (SMT_Failure.Counterexample _) => false
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1099
          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1100
          | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1101
          | SOME SMT_Failure.Out_Of_Memory => true
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41209
diff changeset
  1102
          | SOME (SMT_Failure.Other_Failure _) => true
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1103
        val timeout =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1104
          Option.map
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1105
              (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
31313171deb5 thread no timeout properly
blanchet
parents: