src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
author blanchet
Thu, 18 Oct 2012 15:41:15 +0200
changeset 49921 073d69478207
parent 49918 cf441f4a358b
child 50004 c96e8e40d789
permissions -rw-r--r--
tuned Isar output
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
49914
23e36a4d28f1 refactor code
blanchet
parents: 49881
diff changeset
    14
  type reconstructor = Sledgehammer_Reconstruct.reconstructor
23e36a4d28f1 refactor code
blanchet
parents: 49881
diff changeset
    15
  type play = Sledgehammer_Reconstruct.play
23e36a4d28f1 refactor code
blanchet
parents: 49881
diff changeset
    16
  type minimize_command = Sledgehammer_Reconstruct.minimize_command
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    17
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48376
diff changeset
    18
  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
    19
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    20
  type params =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    21
    {debug : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    22
     verbose : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    23
     overlord : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    24
     blocking : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    25
     provers : string list,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    26
     type_enc : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    27
     strict : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    28
     lam_trans : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    29
     uncurried_aliases : bool option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    30
     learn : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    31
     fact_filter : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    32
     max_facts : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    33
     fact_thresholds : real * real,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    34
     max_mono_iters : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    35
     max_new_mono_instances : int option,
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49914
diff changeset
    36
     isar_proofs : bool,
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49914
diff changeset
    37
     isar_shrinkage : real,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    38
     slice : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    39
     minimize : bool option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    40
     timeout : Time.time,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    41
     preplay_timeout : Time.time,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    42
     expect : string}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    43
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    44
  type relevance_fudge =
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    45
    {local_const_multiplier : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    46
     worse_irrel_freq : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    47
     higher_order_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    48
     abs_rel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    49
     abs_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    50
     skolem_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    51
     theory_const_rel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    52
     theory_const_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    53
     chained_const_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    54
     intro_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    55
     elim_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    56
     simp_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    57
     local_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    58
     assum_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    59
     chained_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    60
     max_imperfect : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    61
     max_imperfect_exp : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    62
     threshold_divisor : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    63
     ridiculous_threshold : real}
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
    64
41090
b98fe4de1ecd renamings
blanchet
parents: 41089
diff changeset
    65
  datatype prover_fact =
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
    66
    Untranslated_Fact of (string * stature) * thm |
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
    67
    SMT_Weighted_Fact of (string * stature) * (int option * thm)
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    68
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    69
  type prover_problem =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    70
    {state : Proof.state,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    71
     goal : thm,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    72
     subgoal : int,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    73
     subgoal_count : int,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    74
     facts : prover_fact list}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    75
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    76
  type prover_result =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    77
    {outcome : failure option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    78
     used_facts : (string * stature) list,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    79
     run_time : Time.time,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    80
     preplay : unit -> play,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    81
     message : play -> string,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
    82
     message_tail : string}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    83
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
    84
  type prover =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
    85
    params -> ((string * string list) list -> string -> minimize_command)
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
    86
    -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
    87
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
    88
  val dest_dir : string Config.T
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
    89
  val problem_prefix : string Config.T
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48131
diff changeset
    90
  val completish : bool Config.T
44592
54906b0337ab flip logic of boolean option so it's off by default
blanchet
parents: 44586
diff changeset
    91
  val atp_full_names : bool Config.T
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    92
  val smt_triggers : bool Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    93
  val smt_weights : bool Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    94
  val smt_weight_min_facts : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    95
  val smt_min_weight : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    96
  val smt_max_weight : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    97
  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
    98
  val smt_weight_curve : (int -> int) Unsynchronized.ref
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    99
  val smt_max_slices : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   100
  val smt_slice_fact_frac : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   101
  val smt_slice_time_frac : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   102
  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
   103
  val SledgehammerN : string
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   104
  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
   105
  val select_smt_solver : string -> Proof.context -> Proof.context
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   106
  val extract_reconstructor :
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   107
    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
   108
  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
   109
  val is_atp : theory -> string -> bool
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
   110
  val is_smt_prover : Proof.context -> string -> bool
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   111
  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
   112
  val is_unit_equational_atp : Proof.context -> string -> bool
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   113
  val is_prover_supported : Proof.context -> string -> bool
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   114
  val is_prover_installed : Proof.context -> string -> bool
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48288
diff changeset
   115
  val default_max_facts_for_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
   116
  val is_unit_equality : term -> bool
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42944
diff changeset
   117
  val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   118
  val is_built_in_const_for_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
   119
    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
   120
  val atp_relevance_fudge : relevance_fudge
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
   121
  val smt_relevance_fudge : relevance_fudge
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   122
  val relevance_fudge_for_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
   123
  val weight_smt_fact :
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   124
    Proof.context -> int -> ((string * stature) * thm) * int
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   125
    -> (string * stature) * (int option * thm)
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   126
  val untranslated_fact : prover_fact -> (string * stature) * thm
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
   127
  val smt_weighted_fact :
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   128
    Proof.context -> int -> prover_fact * int
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   129
    -> (string * stature) * (int option * thm)
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   130
  val supported_provers : Proof.context -> unit
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   131
  val kill_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   132
  val running_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   133
  val messages : int option -> unit
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   134
  val is_fact_chained : (('a * stature) * 'b) -> bool
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   135
  val filter_used_facts :
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   136
    bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   137
    ((''a * stature) * 'b) list
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   138
  val get_prover : Proof.context -> mode -> string -> prover
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   139
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   140
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
   141
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   142
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   143
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43063
diff changeset
   144
open ATP_Util
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
   145
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39453
diff changeset
   146
open ATP_Proof
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
   147
open ATP_Systems
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
   148
open ATP_Problem_Generate
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
   149
open ATP_Proof_Reconstruct
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45520
diff changeset
   150
open Metis_Tactic
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   151
open Sledgehammer_Util
49881
d9d73ebf9274 added proof minimization code from Steffen Smolka
blanchet
parents: 48802
diff changeset
   152
open Sledgehammer_Reconstruct
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   153
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
   154
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
   155
(** 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
   156
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48376
diff changeset
   157
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
   158
45376
blanchet
parents: 45370
diff changeset
   159
(* 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
   160
   "Async_Manager". *)
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   161
val SledgehammerN = "Sledgehammer"
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   162
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   163
val reconstructor_names = [metisN, smtN]
46365
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46340
diff changeset
   164
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
   165
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
   166
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   167
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
   168
43233
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   169
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
   170
45376
blanchet
parents: 45370
diff changeset
   171
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
   172
44597
blanchet
parents: 44592
diff changeset
   173
fun is_atp_for_format is_format ctxt name =
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   174
  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
   175
    case try (get_atp thy) name of
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47531
diff changeset
   176
      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
   177
      exists (fn (_, ((_, format, _, _, _), _)) => is_format format)
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47531
diff changeset
   178
             (#best_slices (config ()) ctxt)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   179
    | NONE => false
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   180
  end
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   181
44597
blanchet
parents: 44592
diff changeset
   182
val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ)
45303
bd03b08161ac added DFG unsorted support (like in the old days)
blanchet
parents: 45301
diff changeset
   183
val is_ho_atp = is_atp_for_format is_format_higher_order
44597
blanchet
parents: 44592
diff changeset
   184
45376
blanchet
parents: 45370
diff changeset
   185
fun is_prover_supported ctxt =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   186
  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
   187
    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
   188
  end
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   189
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   190
fun is_prover_installed ctxt =
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   191
  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
   192
  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
   193
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45590
diff changeset
   194
fun get_slices slice slices =
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45590
diff changeset
   195
  (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
   196
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48288
diff changeset
   197
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
   198
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48288
diff changeset
   199
fun default_max_facts_for_prover ctxt slice name =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   200
  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
   201
    if is_reconstructor name then
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48288
diff changeset
   202
      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
   203
    else if is_atp thy name then
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
   204
      fold (Integer.max o #1 o fst o snd o snd)
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47531
diff changeset
   205
           (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
   206
    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
   207
      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
   208
  end
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   209
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
   210
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
   211
  | 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
   212
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
   213
(* 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
   214
   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
   215
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
   216
  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
   217
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   218
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
   219
  | 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
   220
    is_unit_equality t
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   221
  | 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
   222
    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
   223
  | 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
   224
    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
   225
  | 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
   226
    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
   227
  | is_unit_equality _ = false
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   228
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42944
diff changeset
   229
fun is_appropriate_prop_for_prover ctxt name =
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   230
  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
   231
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
   232
fun is_built_in_const_for_prover ctxt name =
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
   233
  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
   234
    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
   235
      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
   236
         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
   237
           (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
   238
         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
   239
           (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
   240
         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
   241
           (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
   242
    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
   243
  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
   244
    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
   245
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   246
(* FUDGE *)
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   247
val atp_relevance_fudge =
42738
2a9dcff63b80 remove unused parameter
blanchet
parents: 42737
diff changeset
   248
  {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
   249
   worse_irrel_freq = 100.0,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   250
   higher_order_irrel_weight = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   251
   abs_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   252
   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
   253
   skolem_irrel_weight = 0.05,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   254
   theory_const_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   255
   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
   256
   chained_const_irrel_weight = 0.25,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   257
   intro_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   258
   elim_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   259
   simp_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   260
   local_bonus = 0.55,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   261
   assum_bonus = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   262
   chained_bonus = 1.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   263
   max_imperfect = 11.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   264
   max_imperfect_exp = 1.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   265
   threshold_divisor = 2.0,
41093
dfbc8759415f lower fudge factor
blanchet
parents: 41091
diff changeset
   266
   ridiculous_threshold = 0.01}
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   267
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
(* FUDGE (FIXME) *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   269
val smt_relevance_fudge =
42738
2a9dcff63b80 remove unused parameter
blanchet
parents: 42737
diff changeset
   270
  {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
   271
   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
   272
   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
   273
   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
   274
   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
   275
   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
   276
   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
   277
   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
   278
   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
   279
   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
   280
   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
   281
   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
   282
   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
   283
   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
   284
   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
   285
   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
   286
   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
   287
   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
   288
   ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   289
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   290
fun relevance_fudge_for_prover ctxt name =
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   291
  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
   292
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   293
fun supported_provers ctxt =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   294
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   295
    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
   296
    val (remote_provers, local_provers) =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   297
      reconstructor_names @
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   298
      sort_strings (supported_atps thy) @
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   299
      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
   300
      |> List.partition (String.isPrefix remote_prefix)
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   301
  in
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   302
    Output.urgent_message ("Supported provers: " ^
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   303
                           commas (local_provers @ remote_provers) ^ ".")
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   304
  end
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   305
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48314
diff changeset
   306
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
   307
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
   308
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
   309
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   310
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   311
(** problems, results, ATPs, etc. **)
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   312
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   313
type params =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   314
  {debug : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   315
   verbose : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   316
   overlord : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   317
   blocking : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   318
   provers : string list,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   319
   type_enc : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   320
   strict : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   321
   lam_trans : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   322
   uncurried_aliases : bool option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   323
   learn : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   324
   fact_filter : string option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   325
   max_facts : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   326
   fact_thresholds : real * real,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   327
   max_mono_iters : int option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   328
   max_new_mono_instances : int option,
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49914
diff changeset
   329
   isar_proofs : bool,
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49914
diff changeset
   330
   isar_shrinkage : real,
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   331
   slice : bool,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   332
   minimize : bool option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   333
   timeout : Time.time,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   334
   preplay_timeout : Time.time,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   335
   expect : string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   336
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   337
type relevance_fudge =
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   338
  {local_const_multiplier : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   339
   worse_irrel_freq : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   340
   higher_order_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   341
   abs_rel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   342
   abs_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   343
   skolem_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   344
   theory_const_rel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   345
   theory_const_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   346
   chained_const_irrel_weight : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   347
   intro_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   348
   elim_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   349
   simp_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   350
   local_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   351
   assum_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   352
   chained_bonus : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   353
   max_imperfect : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   354
   max_imperfect_exp : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   355
   threshold_divisor : real,
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   356
   ridiculous_threshold : real}
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   357
41090
b98fe4de1ecd renamings
blanchet
parents: 41089
diff changeset
   358
datatype prover_fact =
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   359
  Untranslated_Fact of (string * stature) * thm |
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   360
  SMT_Weighted_Fact of (string * stature) * (int option * thm)
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   361
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   362
type prover_problem =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   363
  {state : Proof.state,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   364
   goal : thm,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   365
   subgoal : int,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   366
   subgoal_count : int,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   367
   facts : prover_fact list}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   368
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   369
type prover_result =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   370
  {outcome : failure option,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   371
   used_facts : (string * stature) list,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   372
   run_time : Time.time,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   373
   preplay : unit -> play,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   374
   message : play -> string,
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48319
diff changeset
   375
   message_tail : string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   376
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   377
type prover =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   378
  params -> ((string * string list) list -> string -> minimize_command)
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   379
  -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   380
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   381
(* configuration attributes *)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   382
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   383
(* 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
   384
val dest_dir =
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   385
  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
   386
val problem_prefix =
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   387
  Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48131
diff changeset
   388
val completish =
0186df5074c8 renamed experimental option
blanchet
parents: 48131
diff changeset
   389
  Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   390
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   391
(* 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
   392
   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
   393
   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
   394
val atp_full_names =
54906b0337ab flip logic of boolean option so it's off by default
blanchet
parents: 44586
diff changeset
   395
  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
   396
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   397
val smt_triggers =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   398
  Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   399
val smt_weights =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   400
  Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   401
val smt_weight_min_facts =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   402
  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
   403
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   404
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   405
val smt_min_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   406
  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   407
val smt_max_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   408
  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   409
val smt_max_weight_index =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   410
  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
   411
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
   412
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   413
fun smt_fact_weight ctxt j num_facts =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   414
  if Config.get ctxt smt_weights andalso
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   415
     num_facts >= Config.get ctxt smt_weight_min_facts then
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   416
    let
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   417
      val min = Config.get ctxt smt_min_weight
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   418
      val max = Config.get ctxt smt_max_weight
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   419
      val max_index = Config.get ctxt smt_max_weight_index
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   420
      val curve = !smt_weight_curve
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   421
    in
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   422
      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
   423
            div curve max_index)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   424
    end
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   425
  else
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   426
    NONE
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   427
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   428
fun weight_smt_fact ctxt num_facts ((info, th), j) =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   429
  let val thy = Proof_Context.theory_of ctxt in
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   430
    (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
   431
  end
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   432
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
   433
fun untranslated_fact (Untranslated_Fact p) = p
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
   434
  | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   435
fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   436
  | smt_weighted_fact ctxt num_facts (fact, j) =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   437
    (untranslated_fact fact, j) |> weight_smt_fact ctxt num_facts
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   438
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   439
fun overlord_file_location_for_prover prover =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   440
  (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
   441
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   442
fun proof_banner mode name =
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   443
  case mode of
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   444
    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   445
  | 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
   446
  | _ => "Try this"
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   447
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   448
fun bunch_of_reconstructors needs_full_types lam_trans =
48800
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   449
  if needs_full_types then
48802
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   450
    [Metis (full_type_enc, lam_trans false),
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   451
     Metis (really_full_type_enc, lam_trans false),
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   452
     Metis (full_type_enc, lam_trans true),
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   453
     Metis (really_full_type_enc, lam_trans true),
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   454
     SMT]
b86e8cf3f464 fixed then-else confusion
blanchet
parents: 48800
diff changeset
   455
  else
48800
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   456
    [Metis (partial_type_enc, lam_trans false),
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   457
     Metis (full_type_enc, lam_trans false),
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   458
     Metis (no_typesN, lam_trans true),
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   459
     Metis (really_full_type_enc, lam_trans true),
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
   460
     SMT]
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   461
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   462
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
   463
                          (Metis (type_enc', lam_trans')) =
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   464
    let
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   465
      val override_params =
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   466
        (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
   467
           []
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   468
         else
45566
da05ce2de5a8 better threading of type encodings between Sledgehammer and "metis"
blanchet
parents: 45561
diff changeset
   469
           [("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
   470
        (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
   471
           []
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   472
         else
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   473
           [("lam_trans", [lam_trans'])])
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   474
    in (metisN, override_params) end
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   475
  | extract_reconstructor _ SMT = (smtN, [])
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   476
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   477
(* based on "Mirabelle.can_apply" and generalized *)
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   478
fun timed_apply timeout tac state i =
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   479
  let
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   480
    val {context = ctxt, facts, goal} = Proof.goal state
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   481
    val full_tac = Method.insert_tac facts i THEN tac ctxt i
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   482
  in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   483
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   484
fun tac_for_reconstructor (Metis (type_enc, lam_trans)) =
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45520
diff changeset
   485
    metis_tac [type_enc] lam_trans
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   486
  | tac_for_reconstructor SMT = SMT_Solver.smt_tac
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   487
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   488
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
   489
  (Config.put Metis_Tactic.verbose debug
45557
b427b23ec89c quiet down SMT
blanchet
parents: 45556
diff changeset
   490
   #> Config.put SMT_Config.verbose debug
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   491
   #> (fn ctxt => tac_for_reconstructor reconstr ctxt ths))
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   492
  |> timed_apply timeout
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   493
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   494
fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   495
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   496
fun filter_used_facts keep_chained used =
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   497
  filter ((member (op =) used o fst) orf
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   498
          (if keep_chained then is_fact_chained else K false))
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   499
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
   500
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
   501
                        reconstrs =
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   502
  let
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   503
    val _ =
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   504
      if mode = Minimize andalso Time.> (timeout, Time.zeroTime) then
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   505
        Output.urgent_message "Preplaying proof..."
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   506
      else
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   507
        ()
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
   508
    val ths = pairs |> sort_wrt (fst o fst) |> map snd
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   509
    fun get_preferred reconstrs =
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   510
      if member (op =) reconstrs preferred then preferred
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   511
      else List.last reconstrs
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   512
    fun play [] [] = Failed_to_Play (get_preferred reconstrs)
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   513
      | play timed_outs [] =
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   514
        Trust_Playable (get_preferred timed_outs, SOME timeout)
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   515
      | play timed_out (reconstr :: reconstrs) =
45378
67ed44d7c929 more detailed preplay output
blanchet
parents: 45376
diff changeset
   516
        let
67ed44d7c929 more detailed preplay output
blanchet
parents: 45376
diff changeset
   517
          val _ =
67ed44d7c929 more detailed preplay output
blanchet
parents: 45376
diff changeset
   518
            if verbose then
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45553
diff changeset
   519
              "Trying \"" ^ string_for_reconstructor reconstr ^ "\" for " ^
45378
67ed44d7c929 more detailed preplay output
blanchet
parents: 45376
diff changeset
   520
              string_from_time timeout ^ "..."
67ed44d7c929 more detailed preplay output
blanchet
parents: 45376
diff changeset
   521
              |> Output.urgent_message
67ed44d7c929 more detailed preplay output
blanchet
parents: 45376
diff changeset
   522
            else
67ed44d7c929 more detailed preplay output
blanchet
parents: 45376
diff changeset
   523
              ()
67ed44d7c929 more detailed preplay output
blanchet
parents: 45376
diff changeset
   524
          val timer = Timer.startRealTimer ()
67ed44d7c929 more detailed preplay output
blanchet
parents: 45376
diff changeset
   525
        in
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   526
          case timed_reconstructor reconstr debug timeout ths state i of
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   527
            SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   528
          | _ => play timed_out reconstrs
43044
5945375700aa always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
blanchet
parents: 43037
diff changeset
   529
        end
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   530
        handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   531
  in
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
   532
    if timeout = Time.zeroTime then
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   533
      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
   534
    else
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   535
      play [] reconstrs
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   536
  end
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   537
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   538
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   539
(* 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
   540
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
   541
(* 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
   542
   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
   543
   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
   544
   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
   545
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
   546
(* 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
   547
   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
   548
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
   549
  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
   550
    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
   551
        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
   552
      | 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
   553
      | 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
   554
    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
   555
    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
   556
      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
   557
        (_, @{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
   558
      | (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
   559
        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
   560
      | (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
   561
        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
   562
      | (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
   563
        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
   564
      | (_, @{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
   565
        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
   566
        (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
   567
      | (_, @{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
   568
        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
   569
        (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
   570
      | (_, @{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
   571
      | (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
   572
      | (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
   573
      | (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
   574
      | (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
   575
      | _ => 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
   576
  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
   577
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
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
   579
  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
   580
                   | 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
   581
                   | _ => 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
   582
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
(* 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
   584
   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
   585
   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
   586
   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
   587
   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
   588
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
(* 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
   590
   "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
   591
   are omitted. *)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   592
fun is_dangerous_prop ctxt =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   593
  transform_elim_prop
44393
23adec5984f1 make sound mode more sound (and clean up code)
blanchet
parents: 44088
diff changeset
   594
  #> (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
   595
      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
   596
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   597
(* Important messages are important but not so important that users want to see
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   598
   them each time. *)
44649
3d7b737d200a fewer TPTP important messages
blanchet
parents: 44636
diff changeset
   599
val atp_important_message_keep_quotient = 25
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   600
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44397
diff changeset
   601
fun choose_type_enc soundness best_type_enc format =
44397
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44394
diff changeset
   602
  the_default best_type_enc
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44394
diff changeset
   603
  #> type_enc_from_string soundness
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44397
diff changeset
   604
  #> adjust_type_enc format
42548
ea2a28b1938f make sure the minimizer monomorphizes when it should
blanchet
parents: 42544
diff changeset
   605
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   606
val metis_minimize_max_time = seconds 2.0
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   607
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   608
fun choose_minimize_command params minimize_command name preplay =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   609
  let
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   610
    val (name, override_params) =
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   611
      case preplay of
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   612
        Played (reconstr, time) =>
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   613
        if Time.<= (time, metis_minimize_max_time) then
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   614
          extract_reconstructor params reconstr
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   615
        else
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   616
          (name, [])
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   617
      | _ => (name, [])
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   618
  in minimize_command override_params name end
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   619
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   620
fun repair_monomorph_context max_iters best_max_iters max_new_instances
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   621
                             best_max_new_instances =
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   622
  Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   623
  #> Config.put Monomorph.max_new_instances
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   624
         (max_new_instances |> the_default best_max_new_instances)
43230
dabf6e311213 clarified meaning of monomorphization configuration option by renaming it
boehmes
parents: 43228
diff changeset
   625
  #> Config.put Monomorph.keep_partial_instances false
43226
a4a314a0a90a use new monomorphization code
blanchet
parents: 43224
diff changeset
   626
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
   627
fun suffix_for_mode Auto_Try = "_auto_try"
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
   628
  | suffix_for_mode Try = "_try"
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
   629
  | suffix_for_mode Normal = ""
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48376
diff changeset
   630
  | suffix_for_mode MaSh = "_mash"
45574
7a39df11bcf6 be more silent when auto minimizing
blanchet
parents: 45566
diff changeset
   631
  | suffix_for_mode Auto_Minimize = "_auto_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
   632
  | suffix_for_mode Minimize = "_min"
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
   633
44423
f74707e12d30 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents: 44416
diff changeset
   634
(* 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
   635
   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
   636
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
   637
48331
f190a6dbb29b make the monomorphizer more predictable by making the cutoff independent on the number of facts
blanchet
parents: 48321
diff changeset
   638
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
   639
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   640
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
   641
        ({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
   642
          best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46296
diff changeset
   643
        (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48288
diff changeset
   644
                    uncurried_aliases, max_facts, max_mono_iters,
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49914
diff changeset
   645
                    max_new_mono_instances, isar_proofs, isar_shrinkage,
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46407
diff changeset
   646
                    slice, timeout, preplay_timeout, ...})
43037
ade5c84f860f cleanup proof text generation code
blanchet
parents: 43034
diff changeset
   647
        minimize_command
ade5c84f860f cleanup proof text generation code
blanchet
parents: 43034
diff changeset
   648
        ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   649
  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
   650
    val thy = Proof.theory_of state
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   651
    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
   652
    val atp_mode =
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48131
diff changeset
   653
      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
   654
      else Sledgehammer
43004
20e9caff1f86 fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
blanchet
parents: 42998
diff changeset
   655
    val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
41159
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41152
diff changeset
   656
    val (dest_dir, problem_prefix) =
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41152
diff changeset
   657
      if overlord then overlord_file_location_for_prover name
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41152
diff changeset
   658
      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
   659
    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
   660
      Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
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
   661
                  suffix_for_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
   662
    val prob_path =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   663
      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
   664
        File.tmp_path problem_file_name
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   665
      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
   666
        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
   667
      else
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   668
        error ("No such directory: " ^ quote dest_dir ^ ".")
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   669
    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
   670
      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
   671
        SOME var =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   672
        let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   673
          val pref = getenv var ^ "/"
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   674
          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
   675
        in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   676
          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
   677
            SOME path => path
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   678
          | 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
   679
        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
   680
      | 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
   681
                       " is not set.")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   682
    fun split_time s =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   683
      let
42448
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   684
        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
   685
        val (output, t) =
63c939dcd055 made "split_last" more robust in the face of obscure low-level errors
blanchet
parents: 47606
diff changeset
   686
          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
   687
            |>> cat_lines
42448
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   688
        fun as_num f = f >> (fst o read_int)
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   689
        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   690
        val digit = Scan.one Symbol.is_ascii_digit
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   691
        val num3 = as_num (digit ::: digit ::: (digit >> single))
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   692
        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
45381
d17e7b4422e8 more millisecond cleanup
blanchet
parents: 45379
diff changeset
   693
        val as_time =
d17e7b4422e8 more millisecond cleanup
blanchet
parents: 45379
diff changeset
   694
          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
   695
      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
   696
    fun run () =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   697
      let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   698
        (* 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
   699
           time available. *)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   700
        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
   701
        val num_actual_slices = length actual_slices
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   702
        fun monomorphize_facts facts =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   703
          let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   704
            val ctxt =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   705
              ctxt
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   706
              |> repair_monomorph_context max_mono_iters best_max_mono_iters
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   707
                      max_new_mono_instances best_max_new_mono_instances
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   708
            (* 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
   709
            val subgoal_th =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   710
              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
   711
            val rths =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   712
              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
   713
                    |>> map (pair 1 o snd)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   714
                    ||> map (pair 2 o snd)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   715
                    |> op @
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   716
                    |> cons (0, subgoal_th)
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
            Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   719
            |> curry ListPair.zip (map fst facts)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   720
            |> maps (fn (name, rths) =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   721
                        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
   722
          end
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   723
        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
   724
                (slice, (time_frac,
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   725
                     (key as (best_max_facts, format, best_type_enc,
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   726
                              best_lam_trans, 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
   727
                      extra))) =
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   728
          let
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   729
            val num_facts =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   730
              length facts |> is_none max_facts ? Integer.min best_max_facts
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   731
            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
   732
            val type_enc =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   733
              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
   734
            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
   735
            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
   736
            val slice_timeout =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   737
              ((real_ms time_left
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   738
                |> (if slice < num_actual_slices - 1 then
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   739
                      curry Real.min (time_frac * real_ms timeout)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   740
                    else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   741
                      I))
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   742
               * 0.001) |> seconds
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   743
            val generous_slice_timeout =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   744
              Time.+ (slice_timeout, atp_timeout_slack)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   745
            val _ =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   746
              if debug then
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   747
                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
   748
                " with " ^ string_of_int num_facts ^ " fact" ^
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   749
                plural_s num_facts ^ " for " ^
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   750
                string_from_time slice_timeout ^ "..."
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   751
                |> Output.urgent_message
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   752
              else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   753
                ()
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   754
            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
   755
            val lam_trans =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   756
              case lam_trans of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   757
                SOME s => s
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   758
              | NONE => best_lam_trans
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   759
            val uncurried_aliases =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   760
              case uncurried_aliases of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   761
                SOME b => b
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   762
              | NONE => best_uncurried_aliases
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   763
            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
   764
              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
   765
                cache_value
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   766
              else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   767
                facts
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   768
                |> map untranslated_fact
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   769
                |> not sound
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   770
                   ? 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
   771
                |> take num_facts
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   772
                |> 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
   773
                |> map (apsnd prop_of)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   774
                |> 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
   775
                                       lam_trans uncurried_aliases
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   776
                                       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
   777
            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
   778
            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
   779
            val ord = effective_term_order ctxt name
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49914
diff changeset
   780
            val full_proof = debug orelse isar_proofs
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   781
            val args = arguments ctxt full_proof extra slice_timeout
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   782
                                 (ord, ord_info, sel_weights)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   783
            val command =
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
   784
              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   785
              File.shell_path prob_path ^ ")"
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
   786
              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   787
            val _ =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   788
              atp_problem
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   789
              |> lines_for_atp_problem format ord ord_info
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   790
              |> cons ("% " ^ command ^ "\n")
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   791
              |> File.write_list prob_path
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   792
            val ((output, run_time), (atp_proof, outcome)) =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   793
              TimeLimit.timeLimit generous_slice_timeout
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   794
                                  Isabelle_System.bash_output command
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   795
              |>> (if overlord then
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   796
                     prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   797
                   else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   798
                     I)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   799
              |> fst |> split_time
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   800
              |> (fn accum as (output, _) =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   801
                     (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
   802
                      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
   803
                                                         known_failures output
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   804
                      |>> atp_proof_from_tstplike_proof atp_problem
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   805
                      handle UNRECOGNIZED_ATP_PROOF () =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   806
                             ([], SOME ProofIncomplete)))
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   807
              handle TimeLimit.TimeOut =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   808
                     (("", slice_timeout), ([], SOME TimedOut))
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   809
            val outcome =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   810
              case outcome of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   811
                NONE =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   812
                (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
   813
                      |> 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
   814
                   SOME facts =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   815
                   let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   816
                     val failure =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   817
                       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
   818
                   in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   819
                     if debug then (warning (string_for_failure failure); NONE)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   820
                     else SOME failure
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   821
                   end
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   822
                 | NONE => NONE)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   823
              | _ => outcome
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   824
          in ((SOME key, value), (output, run_time, atp_proof, outcome)) end
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   825
        val timer = Timer.startRealTimer ()
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   826
        fun maybe_run_slice slice
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   827
                (result as (cache, (_, run_time0, _, SOME _))) =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   828
            let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   829
              val time_left = Time.- (timeout, Timer.checkRealTimer timer)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   830
            in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   831
              if Time.<= (time_left, Time.zeroTime) then
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   832
                result
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   833
              else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   834
                run_slice time_left cache slice
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   835
                |> (fn (cache, (output, run_time, atp_proof, outcome)) =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   836
                       (cache, (output, Time.+ (run_time0, run_time),
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   837
                                atp_proof, outcome)))
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   838
            end
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   839
          | maybe_run_slice _ result = result
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   840
      in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   841
        ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   842
         ("", Time.zeroTime, [], SOME InternalError))
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   843
        |> 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
   844
      end
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   845
    (* If the problem file has not been exported, remove it; otherwise, export
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   846
       the proof file too. *)
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   847
    fun clean_up () =
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   848
      if dest_dir = "" then (try File.rm prob_path; ()) else ()
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   849
    fun export (_, (output, _, _, _)) =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   850
      if dest_dir = "" then ()
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   851
      else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
46407
30e9720cc0b9 optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents: 46405
diff changeset
   852
    val ((_, (_, pool, fact_names, _, sym_tab)),
30e9720cc0b9 optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents: 46405
diff changeset
   853
         (output, run_time, atp_proof, outcome)) =
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   854
      with_cleanup clean_up run () |> tap export
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   855
    val important_message =
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   856
      if mode = Normal andalso
42609
b5e94b70bc06 fixed random number invocation
blanchet
parents: 42593
diff changeset
   857
         random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   858
        extract_important_message output
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   859
      else
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   860
        ""
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   861
    val (used_facts, preplay, message, message_tail) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   862
      case outcome of
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   863
        NONE =>
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   864
        let
45551
a62c7a21f4ab removed needless baggage
blanchet
parents: 45521
diff changeset
   865
          val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
45590
dc9a7ff13e37 made SML/NJ happy
blanchet
parents: 45574
diff changeset
   866
          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
   867
          val reconstrs =
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45553
diff changeset
   868
            bunch_of_reconstructors needs_full_types
45560
1606122a2d0f don't needlessly pass "lam_lifted" option to "metis" call for SMT proof
blanchet
parents: 45557
diff changeset
   869
                (lam_trans_from_atp_proof atp_proof
46405
76ed3b7092fc try to pass fewer options to Metis
blanchet
parents: 46365
diff changeset
   870
                 o (fn desperate => if desperate then hide_lamsN
76ed3b7092fc try to pass fewer options to Metis
blanchet
parents: 46365
diff changeset
   871
                                    else metis_default_lam_trans))
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   872
        in
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   873
          (used_facts,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   874
           fn () =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   875
              let
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
   876
                val used_pairs =
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   877
                  facts |> map untranslated_fact
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   878
                        |> filter_used_facts false used_facts
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   879
              in
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
   880
                play_one_line_proof mode debug verbose preplay_timeout
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
   881
                    used_pairs state subgoal (hd reconstrs) reconstrs
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   882
              end,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   883
           fn preplay =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   884
              let
49921
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   885
                val _ =
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   886
                  if verbose then
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   887
                    Output.urgent_message "Generating proof text..."
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   888
                  else
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   889
                    ()
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   890
                val isar_params =
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49914
diff changeset
   891
                  (debug, verbose, isar_shrinkage, pool, fact_names, sym_tab,
45552
d2139b4557fc removed more clutter
blanchet
parents: 45551
diff changeset
   892
                   atp_proof, goal)
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   893
                val one_line_params =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   894
                  (preplay, proof_banner mode name, used_facts,
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   895
                   choose_minimize_command params minimize_command name preplay,
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   896
                   subgoal, subgoal_count)
48799
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   897
                val num_chained = length (#facts (Proof.goal state))
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   898
              in
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49914
diff changeset
   899
                proof_text ctxt isar_proofs isar_params num_chained
48799
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   900
                           one_line_params
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   901
              end,
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   902
           (if verbose then
45381
d17e7b4422e8 more millisecond cleanup
blanchet
parents: 45379
diff changeset
   903
              "\nATP real CPU time: " ^ string_from_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
   904
            else
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   905
              "") ^
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   906
           (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
   907
              "\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
   908
              important_message
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   909
            else
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   910
              ""))
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   911
        end
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   912
      | SOME failure =>
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   913
        ([], K (Failed_to_Play plain_metis),
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   914
         fn _ => string_for_failure failure, "")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   915
  in
45381
d17e7b4422e8 more millisecond cleanup
blanchet
parents: 45379
diff changeset
   916
    {outcome = outcome, used_facts = used_facts, run_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
   917
     preplay = preplay, message = message, message_tail = message_tail}
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   918
  end
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   919
40669
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   920
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   921
   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
   922
   ourselves. *)
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   923
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
   924
  [(2, NoLibwwwPerl),
4144d7b4ec77 enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents: 43626
diff changeset
   925
   (22, CantConnect)]
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   926
val z3_failures =
41236
def0a3013554 trap one more Z3 error
blanchet
parents: 41222
diff changeset
   927
  [(101, OutOfResources),
def0a3013554 trap one more Z3 error
blanchet
parents: 41222
diff changeset
   928
   (103, MalformedInput),
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   929
   (110, MalformedInput)]
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   930
val unix_failures =
48797
e65385336531 recognize bus errors as crash
blanchet
parents: 48716
diff changeset
   931
  [(138, Crashed),
e65385336531 recognize bus errors as crash
blanchet
parents: 48716
diff changeset
   932
   (139, Crashed)]
43631
4144d7b4ec77 enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents: 43626
diff changeset
   933
val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
40555
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   934
42100
062381c5f9f8 more precise failure reporting in Sledgehammer/SMT
blanchet
parents: 42061
diff changeset
   935
fun failure_from_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
   936
    if is_real_cex then Unprovable else GaveUp
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   937
  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   938
  | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   939
    (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
   940
       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
   941
     | 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
   942
                             string_of_int code ^ "."))
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   943
  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   944
  | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
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
   945
    UnknownError msg
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   946
40698
8a3f7ea91370 cosmetics
blanchet
parents: 40693
diff changeset
   947
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   948
val smt_max_slices =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   949
  Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   950
val smt_slice_fact_frac =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   951
  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.5)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   952
val smt_slice_time_frac =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   953
  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.5)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   954
val smt_slice_min_secs =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   955
  Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5)
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   956
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   957
fun smt_filter_loop ctxt name
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   958
                    ({debug, verbose, overlord, max_mono_iters,
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45590
diff changeset
   959
                      max_new_mono_instances, timeout, slice, ...} : params)
47531
7fe7c7419489 get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
blanchet
parents: 47055
diff changeset
   960
                    state i =
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   961
  let
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45590
diff changeset
   962
    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
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
   963
    val repair_context =
43233
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   964
      select_smt_solver name
45557
b427b23ec89c quiet down SMT
blanchet
parents: 45556
diff changeset
   965
      #> Config.put SMT_Config.verbose debug
43233
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   966
      #> (if overlord then
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   967
            Config.put SMT_Config.debug_files
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   968
                       (overlord_file_location_for_prover name
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   969
                        |> (fn (path, name) => path ^ "/" ^ name))
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   970
          else
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   971
            I)
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   972
      #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
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
   973
    val state = state |> Proof.map_context repair_context
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   974
    fun do_slice timeout slice outcome0 time_so_far facts =
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   975
      let
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   976
        val timer = Timer.startRealTimer ()
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   977
        val state =
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   978
          state |> Proof.map_context
43267
dd38b8ef52b9 exploit new semantics of "max_new_instances"
blanchet
parents: 43261
diff changeset
   979
                       (repair_monomorph_context max_mono_iters
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   980
                            default_max_mono_iters max_new_mono_instances
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   981
                            default_max_new_mono_instances)
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   982
        val ms = timeout |> Time.toMilliseconds
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   983
        val slice_timeout =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   984
          if slice < max_slices then
41169
95167879f675 clean up fudge factors a little bit
blanchet
parents: 41168
diff changeset
   985
            Int.min (ms,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   986
                Int.max (1000 * Config.get ctxt smt_slice_min_secs,
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   987
                    Real.ceil (Config.get ctxt smt_slice_time_frac
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   988
                               * Real.fromInt ms)))
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   989
            |> Time.fromMilliseconds
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   990
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   991
            timeout
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   992
        val num_facts = length facts
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   993
        val _ =
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   994
          if debug then
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   995
            quote name ^ " slice " ^ string_of_int slice ^ " with " ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   996
            string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   997
            string_from_time slice_timeout ^ "..."
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   998
            |> Output.urgent_message
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   999
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1000
            ()
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
  1001
        val birth = Timer.checkRealTimer timer
41171
043f8dc3b51f facilitate debugging
blanchet
parents: 41169
diff changeset
  1002
        val _ =
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41209
diff changeset
  1003
          if debug then Output.urgent_message "Invoking SMT solver..." else ()
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1004
        val (outcome, used_facts) =
47531
7fe7c7419489 get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
blanchet
parents: 47055
diff changeset
  1005
          SMT_Solver.smt_filter_preprocess state facts i
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1006
          |> SMT_Solver.smt_filter_apply slice_timeout
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41236
diff changeset
  1007
          |> (fn {outcome, used_facts} => (outcome, used_facts))
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1008
          handle exn => if Exn.is_interrupt exn then
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1009
                          reraise exn
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1010
                        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
  1011
                          (ML_Compiler.exn_message exn
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1012
                           |> SMT_Failure.Other_Failure |> SOME, [])
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
  1013
        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
  1014
        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
  1015
        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
  1016
        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
  1017
          case outcome of
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1018
            NONE => false
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1019
          | SOME (SMT_Failure.Counterexample _) => false
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1020
          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1021
          | 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
  1022
          | 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
  1023
          | SOME (SMT_Failure.Other_Failure _) => true
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1024
        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1025
      in
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1026
        if too_many_facts_perhaps andalso slice < max_slices andalso
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1027
           num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
41169
95167879f675 clean up fudge factors a little bit
blanchet
parents: 41168
diff changeset
  1028
          let
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1029
            val new_num_facts =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1030
              Real.ceil (Config.get ctxt smt_slice_fact_frac
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1031
                         * Real.fromInt num_facts)
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1032
            val _ =
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1033
              if verbose andalso is_some outcome then
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1034
                quote name ^ " invoked with " ^ string_of_int num_facts ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1035
                " fact" ^ plural_s num_facts ^ ": " ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1036
                string_for_failure (failure_from_smt_failure (the outcome)) ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1037
                " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^
42638
a7a30721767a have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents: 42623
diff changeset
  1038
                plural_s new_num_facts ^ "..."
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1039
                |> Output.urgent_message
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1040
              else
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1041
                ()
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1042
          in
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1043
            facts |> take new_num_facts
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1044
                  |> do_slice timeout (slice + 1) outcome0 time_so_far
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1045
          end
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1046
        else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1047
          {outcome = if is_none outcome then NONE else the outcome0,
45370
bab52dafa63a use "Time.time" rather than milliseconds internally
blanchet
parents: 45369
diff changeset
  1048
           used_facts = used_facts, run_time = time_so_far}
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
  1049
      end
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1050
  in do_slice timeout 1 NONE Time.zeroTime end
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
  1051
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1052
fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
43011
5f8d74d3b297 added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents: 43006
diff changeset
  1053
        minimize_command
47531
7fe7c7419489 get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
blanchet
parents: 47055
diff changeset
  1054
        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
36379
20ef039bccff make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents: 36373
diff changeset
  1055
  let
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
  1056
    val ctxt = Proof.context_of state
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
  1057
    val num_facts = length facts
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
  1058
    val facts = facts ~~ (0 upto num_facts - 1)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1059
                |> map (smt_weighted_fact ctxt num_facts)
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
  1060
    val {outcome, used_facts = used_pairs, run_time} =
47531
7fe7c7419489 get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)
blanchet
parents: 47055
diff changeset
  1061
      smt_filter_loop ctxt name params state subgoal facts
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
  1062
    val used_facts = used_pairs |> map fst
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
  1063
    val outcome = outcome |> Option.map failure_from_smt_failure
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
  1064
    val (preplay, message, message_tail) =
40184
91b4b73dbafb proper error handling for SMT solvers in Sledgehammer
blanchet
parents: 40181
diff changeset
  1065
      case outcome of
91b4b73dbafb proper error handling for SMT solvers in Sledgehammer
blanchet
parents: 40181
diff changeset
  1066
        NONE =>
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1067
        (fn () =>
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
  1068
            play_one_line_proof mode debug verbose preplay_timeout used_pairs
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45553
diff changeset
  1069
                state subgoal SMT
45560
1606122a2d0f don't needlessly pass "lam_lifted" option to "metis" call for SMT proof
blanchet
parents: 45557
diff changeset
  1070
                (bunch_of_reconstructors false
48800
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
  1071
                     (fn desperate =>
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
  1072
                         if desperate then liftingN
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
  1073
                         else metis_default_lam_trans)),
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1074
         fn preplay =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1075
            let
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1076
              val one_line_params =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1077
                (preplay, proof_banner mode name, used_facts,
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
  1078
                 choose_minimize_command params minimize_command name preplay,
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1079
                 subgoal, subgoal_count)
48799
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
  1080
              val num_chained = length (#facts (Proof.goal state))
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
  1081
            in one_line_proof_text num_chained one_line_params end,
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
  1082
         if verbose then
45370
bab52dafa63a use "Time.time" rather than milliseconds internally
blanchet
parents: 45369
diff changeset
  1083
           "\nSMT solver real CPU time: " ^ string_from_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
  1084
         else
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
  1085
           "")
43166
68e3cd19fee8 show what failed to play
blanchet
parents: 43128
diff changeset
  1086
      | SOME failure =>
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
  1087
        (K (Failed_to_Play plain_metis), fn _ => string_for_failure failure, "")
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
  1088
  in
45370
bab52dafa63a use "Time.time" rather than milliseconds internally
blanchet
parents: 45369
diff changeset
  1089
    {outcome = outcome, used_facts = used_facts, run_time = run_time,
bab52dafa63a use "Time.time" rather than milliseconds internally
blanchet
parents: 45369
diff changeset
  1090
     preplay = preplay, message = message, message_tail = message_tail}
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
  1091
  end
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
  1092
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
  1093
fun run_reconstructor mode name
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
  1094
        (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
  1095
        minimize_command
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45378
diff changeset
  1096
        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1097
  let
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
  1098
    val reconstr =
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
  1099
      if name = metisN then
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
  1100
        Metis (type_enc |> the_default (hd partial_type_encs),
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
  1101
               lam_trans |> the_default metis_default_lam_trans)
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
  1102
      else if name = smtN then
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
  1103
        SMT
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
  1104
      else
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
  1105
        raise Fail ("unknown reconstructor: " ^ quote name)
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 fa