src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
author blanchet
Sat, 15 Dec 2012 19:57:12 +0100
changeset 50557 31313171deb5
parent 50494 06b199a042ff
child 50558 a719106124d8
permissions -rw-r--r--
thread no timeout properly
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,
50020
6b9611abcd4c renamed Sledgehammer option
blanchet
parents: 50004
diff changeset
    37
     isar_shrink : 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,
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
    40
     timeout : Time.time option,
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
    41
     preplay_timeout : Time.time option,
48321
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,
50020
6b9611abcd4c renamed Sledgehammer option
blanchet
parents: 50004
diff changeset
   330
   isar_shrink : 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,
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   333
   timeout : Time.time option,
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   334
   preplay_timeout : Time.time option,
48321
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
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   482
  in time_limit 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
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   503
    fun get_preferred reconstrs =
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   504
      if member (op =) reconstrs preferred then preferred
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   505
      else List.last reconstrs
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   506
  in
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   507
    if timeout = SOME Time.zeroTime then
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   508
      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
   509
    else
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   510
      let
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   511
        val _ =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   512
          if mode = Minimize then Output.urgent_message "Preplaying proof..."
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   513
          else ()
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   514
        val ths = pairs |> sort_wrt (fst o fst) |> map snd
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   515
        fun play [] [] = Failed_to_Play (get_preferred reconstrs)
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   516
          | play timed_outs [] =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   517
            Trust_Playable (get_preferred timed_outs, timeout)
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   518
          | play timed_out (reconstr :: reconstrs) =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   519
            let
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   520
              val _ =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   521
                if verbose then
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   522
                  "Trying \"" ^ string_for_reconstructor reconstr ^ "\"" ^
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   523
                  (case timeout of
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   524
                     SOME timeout => " for " ^ string_from_time timeout
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   525
                   | NONE => "") ^ "..."
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   526
                  |> Output.urgent_message
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   527
                else
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   528
                  ()
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   529
              val timer = Timer.startRealTimer ()
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   530
            in
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   531
              case timed_reconstructor reconstr debug timeout ths state i of
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   532
                SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   533
              | _ => play timed_out reconstrs
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   534
            end
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   535
            handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   536
      in play [] reconstrs end
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   537
  end
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   538
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   539
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   540
(* 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
   541
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
   542
(* 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
   543
   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
   544
   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
   545
   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
   546
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
(* 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
   548
   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
   549
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
   550
  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
   551
    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
   552
        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
   553
      | 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
   554
      | 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
   555
    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
   556
    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
   557
      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
   558
        (_, @{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
   559
      | (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
   560
        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
   561
      | (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
   562
        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
   563
      | (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
   564
        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
   565
      | (_, @{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
   566
        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
   567
        (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
   568
      | (_, @{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
   569
        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
   570
        (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
   571
      | (_, @{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
   572
      | (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
   573
      | (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
   574
      | (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
   575
      | (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
   576
      | _ => 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
   577
  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
   578
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
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
   580
  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
   581
                   | 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
   582
                   | _ => 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
   583
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
(* 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
   585
   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
   586
   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
   587
   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
   588
   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
   589
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
(* 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
   591
   "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
   592
   are omitted. *)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   593
fun is_dangerous_prop ctxt =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   594
  transform_elim_prop
44393
23adec5984f1 make sound mode more sound (and clean up code)
blanchet
parents: 44088
diff changeset
   595
  #> (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
   596
      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
   597
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   598
(* Important messages are important but not so important that users want to see
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   599
   them each time. *)
44649
3d7b737d200a fewer TPTP important messages
blanchet
parents: 44636
diff changeset
   600
val atp_important_message_keep_quotient = 25
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   601
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44397
diff changeset
   602
fun choose_type_enc soundness best_type_enc format =
44397
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44394
diff changeset
   603
  the_default best_type_enc
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44394
diff changeset
   604
  #> type_enc_from_string soundness
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44397
diff changeset
   605
  #> adjust_type_enc format
42548
ea2a28b1938f make sure the minimizer monomorphizes when it should
blanchet
parents: 42544
diff changeset
   606
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   607
val metis_minimize_max_time = seconds 2.0
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   608
45561
57227eedce81 don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents: 45560
diff changeset
   609
fun choose_minimize_command params minimize_command name preplay =
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   610
  let
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   611
    val (name, override_params) =
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   612
      case preplay of
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   613
        Played (reconstr, time) =>
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   614
        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
   615
          extract_reconstructor params reconstr
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   616
        else
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
      | _ => (name, [])
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45519
diff changeset
   619
  in minimize_command override_params name end
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   620
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   621
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
   622
                             best_max_new_instances =
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   623
  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
   624
  #> Config.put Monomorph.max_new_instances
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   625
         (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
   626
  #> Config.put Monomorph.keep_partial_instances false
43226
a4a314a0a90a use new monomorphization code
blanchet
parents: 43224
diff changeset
   627
50494
06b199a042ff tuned debugging file names
blanchet
parents: 50486
diff changeset
   628
fun suffix_for_mode Auto_Try = "_try"
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
   629
  | 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
   630
  | suffix_for_mode Normal = ""
50494
06b199a042ff tuned debugging file names
blanchet
parents: 50486
diff changeset
   631
  | suffix_for_mode MaSh = ""
06b199a042ff tuned debugging file names
blanchet
parents: 50486
diff changeset
   632
  | suffix_for_mode Auto_Minimize = "_min"
44509
369e8c28a61a added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files
blanchet
parents: 44423
diff changeset
   633
  | 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
   634
44423
f74707e12d30 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents: 44416
diff changeset
   635
(* 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
   636
   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
   637
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
   638
48331
f190a6dbb29b make the monomorphizer more predictable by making the cutoff independent on the number of facts
blanchet
parents: 48321
diff changeset
   639
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
   640
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   641
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
   642
        ({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
   643
          best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46296
diff changeset
   644
        (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48288
diff changeset
   645
                    uncurried_aliases, max_facts, max_mono_iters,
50020
6b9611abcd4c renamed Sledgehammer option
blanchet
parents: 50004
diff changeset
   646
                    max_new_mono_instances, isar_proofs, isar_shrink,
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46407
diff changeset
   647
                    slice, timeout, preplay_timeout, ...})
43037
ade5c84f860f cleanup proof text generation code
blanchet
parents: 43034
diff changeset
   648
        minimize_command
ade5c84f860f cleanup proof text generation code
blanchet
parents: 43034
diff changeset
   649
        ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   650
  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
   651
    val thy = Proof.theory_of state
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   652
    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
   653
    val atp_mode =
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48131
diff changeset
   654
      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
   655
      else Sledgehammer
43004
20e9caff1f86 fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
blanchet
parents: 42998
diff changeset
   656
    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
   657
    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
   658
      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
   659
      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
   660
    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
   661
      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
   662
                  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
   663
    val prob_path =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   664
      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
   665
        File.tmp_path problem_file_name
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   666
      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
   667
        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
   668
      else
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   669
        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
   670
    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
   671
      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
   672
        SOME var =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   673
        let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   674
          val pref = getenv var ^ "/"
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   675
          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
   676
        in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   677
          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
   678
            SOME path => path
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   679
          | 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
   680
        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
   681
      | 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
   682
                       " is not set.")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   683
    fun split_time s =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   684
      let
42448
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   685
        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
   686
        val (output, t) =
63c939dcd055 made "split_last" more robust in the face of obscure low-level errors
blanchet
parents: 47606
diff changeset
   687
          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
   688
            |>> cat_lines
42448
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   689
        fun as_num f = f >> (fst o read_int)
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   690
        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   691
        val digit = Scan.one Symbol.is_ascii_digit
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   692
        val num3 = as_num (digit ::: digit ::: (digit >> single))
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   693
        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
45381
d17e7b4422e8 more millisecond cleanup
blanchet
parents: 45379
diff changeset
   694
        val as_time =
d17e7b4422e8 more millisecond cleanup
blanchet
parents: 45379
diff changeset
   695
          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
   696
      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
   697
    fun run () =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   698
      let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   699
        (* 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
   700
           time available. *)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   701
        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
   702
        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
   703
        fun monomorphize_facts facts =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   704
          let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   705
            val ctxt =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   706
              ctxt
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   707
              |> 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
   708
                      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
   709
            (* 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
   710
            val subgoal_th =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   711
              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
   712
            val rths =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   713
              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
   714
                    |>> map (pair 1 o snd)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   715
                    ||> map (pair 2 o snd)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   716
                    |> op @
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   717
                    |> cons (0, subgoal_th)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   718
          in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   719
            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
   720
            |> 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
   721
            |> maps (fn (name, rths) =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   722
                        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
   723
          end
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   724
        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
   725
                (slice, (time_frac,
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   726
                     (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
   727
                              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
   728
                      extra))) =
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   729
          let
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   730
            val num_facts =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   731
              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
   732
            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
   733
            val type_enc =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   734
              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
   735
            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
   736
            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
   737
            val slice_timeout =
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   738
              case time_left of
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   739
                SOME time_left =>
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   740
                ((real_ms time_left
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   741
                  |> (if slice < num_actual_slices - 1 then
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   742
                        curry Real.min (time_frac * real_ms (the timeout))
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   743
                      else
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   744
                        I))
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   745
                 * 0.001)
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   746
                |> seconds |> SOME
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   747
              | NONE => NONE
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   748
            val generous_slice_timeout =
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   749
              Option.map (curry Time.+ atp_timeout_slack) slice_timeout
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   750
            val _ =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   751
              if debug then
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   752
                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
   753
                " with " ^ string_of_int num_facts ^ " fact" ^
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   754
                plural_s num_facts ^
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   755
                (case slice_timeout of
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   756
                   SOME timeout => " for " ^ string_from_time timeout
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   757
                 | NONE => "") ^ "..."
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   758
                |> Output.urgent_message
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   759
              else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   760
                ()
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   761
            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
   762
            val lam_trans =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   763
              case lam_trans of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   764
                SOME s => s
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   765
              | NONE => best_lam_trans
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   766
            val uncurried_aliases =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   767
              case uncurried_aliases of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   768
                SOME b => b
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   769
              | NONE => best_uncurried_aliases
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   770
            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
   771
              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
   772
                cache_value
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   773
              else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   774
                facts
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   775
                |> map untranslated_fact
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   776
                |> not sound
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   777
                   ? 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
   778
                |> take num_facts
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   779
                |> 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
   780
                |> map (apsnd prop_of)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   781
                |> 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
   782
                                       lam_trans uncurried_aliases
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   783
                                       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
   784
            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
   785
            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
   786
            val ord = effective_term_order ctxt name
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49914
diff changeset
   787
            val full_proof = debug orelse isar_proofs
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   788
            val args = arguments ctxt full_proof extra
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   789
                                 (slice_timeout |> the_default one_day)
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   790
                                 (ord, ord_info, sel_weights)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   791
            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
   792
              "(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
   793
              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
   794
              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   795
            val _ =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   796
              atp_problem
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   797
              |> 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
   798
              |> cons ("% " ^ command ^ "\n")
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   799
              |> 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
   800
            val ((output, run_time), (atp_proof, outcome)) =
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   801
              time_limit generous_slice_timeout Isabelle_System.bash_output
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   802
                         command
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   803
              |>> (if overlord then
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   804
                     prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   805
                   else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   806
                     I)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   807
              |> fst |> split_time
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   808
              |> (fn accum as (output, _) =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   809
                     (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
   810
                      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
   811
                                                         known_failures output
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   812
                      |>> 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
   813
                      handle UNRECOGNIZED_ATP_PROOF () =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   814
                             ([], SOME ProofIncomplete)))
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   815
              handle TimeLimit.TimeOut =>
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   816
                     (("", the slice_timeout), ([], SOME TimedOut))
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   817
            val outcome =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   818
              case outcome of
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   819
                NONE =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   820
                (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
   821
                      |> 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
   822
                   SOME facts =>
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   823
                   let
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   824
                     val failure =
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   825
                       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
   826
                   in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   827
                     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
   828
                     else SOME failure
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   829
                   end
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   830
                 | NONE => NONE)
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   831
              | _ => outcome
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   832
          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
   833
        val timer = Timer.startRealTimer ()
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   834
        fun maybe_run_slice slice
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   835
                (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
   836
            let
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   837
              val time_left =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   838
                Option.map
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   839
                    (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   840
                    timeout
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   841
            in
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   842
              if time_left <> NONE andalso
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   843
                 Time.<= (the time_left, Time.zeroTime) then
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   844
                result
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   845
              else
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   846
                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
   847
                |> (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
   848
                       (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
   849
                                atp_proof, outcome)))
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   850
            end
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   851
          | maybe_run_slice _ result = result
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   852
      in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   853
        ((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
   854
         ("", Time.zeroTime, [], SOME InternalError))
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   855
        |> 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
   856
      end
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   857
    (* If the problem file has not been exported, remove it; otherwise, export
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   858
       the proof file too. *)
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   859
    fun clean_up () =
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   860
      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
   861
    fun export (_, (output, _, _, _)) =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48331
diff changeset
   862
      if dest_dir = "" then ()
48656
5caa414ce9a2 cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
blanchet
parents: 48532
diff changeset
   863
      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
   864
    val ((_, (_, pool, fact_names, _, sym_tab)),
30e9720cc0b9 optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents: 46405
diff changeset
   865
         (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
   866
      with_cleanup clean_up run () |> tap export
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   867
    val important_message =
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   868
      if mode = Normal andalso
42609
b5e94b70bc06 fixed random number invocation
blanchet
parents: 42593
diff changeset
   869
         random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   870
        extract_important_message output
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   871
      else
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   872
        ""
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   873
    val (used_facts, preplay, message, message_tail) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   874
      case outcome of
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   875
        NONE =>
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   876
        let
45551
a62c7a21f4ab removed needless baggage
blanchet
parents: 45521
diff changeset
   877
          val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
45590
dc9a7ff13e37 made SML/NJ happy
blanchet
parents: 45574
diff changeset
   878
          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
   879
          val reconstrs =
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45553
diff changeset
   880
            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
   881
                (lam_trans_from_atp_proof atp_proof
46405
76ed3b7092fc try to pass fewer options to Metis
blanchet
parents: 46365
diff changeset
   882
                 o (fn desperate => if desperate then hide_lamsN
76ed3b7092fc try to pass fewer options to Metis
blanchet
parents: 46365
diff changeset
   883
                                    else metis_default_lam_trans))
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   884
        in
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   885
          (used_facts,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   886
           fn () =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   887
              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
   888
                val used_pairs =
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   889
                  facts |> map untranslated_fact
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48797
diff changeset
   890
                        |> 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
   891
              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
   892
                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
   893
                    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
   894
              end,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   895
           fn preplay =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   896
              let
49921
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   897
                val _ =
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   898
                  if verbose then
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   899
                    Output.urgent_message "Generating proof text..."
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   900
                  else
073d69478207 tuned Isar output
blanchet
parents: 49918
diff changeset
   901
                    ()
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   902
                val isar_params =
50020
6b9611abcd4c renamed Sledgehammer option
blanchet
parents: 50004
diff changeset
   903
                  (debug, verbose, preplay_timeout, isar_shrink,
50004
c96e8e40d789 several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents: 49921
diff changeset
   904
                   pool, fact_names, sym_tab, atp_proof, goal)
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   905
                val one_line_params =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   906
                  (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
   907
                   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
   908
                   subgoal, subgoal_count)
48799
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   909
                val num_chained = length (#facts (Proof.goal state))
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   910
              in
49918
cf441f4a358b renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents: 49914
diff changeset
   911
                proof_text ctxt isar_proofs isar_params num_chained
48799
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   912
                           one_line_params
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
   913
              end,
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   914
           (if verbose then
45381
d17e7b4422e8 more millisecond cleanup
blanchet
parents: 45379
diff changeset
   915
              "\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
   916
            else
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   917
              "") ^
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   918
           (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
   919
              "\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
   920
              important_message
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   921
            else
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
   922
              ""))
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   923
        end
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   924
      | SOME failure =>
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   925
        ([], K (Failed_to_Play plain_metis),
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   926
         fn _ => string_for_failure failure, "")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   927
  in
45381
d17e7b4422e8 more millisecond cleanup
blanchet
parents: 45379
diff changeset
   928
    {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
   929
     preplay = preplay, message = message, message_tail = message_tail}
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   930
  end
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   931
40669
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   932
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   933
   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
   934
   ourselves. *)
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   935
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
   936
  [(2, NoLibwwwPerl),
4144d7b4ec77 enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents: 43626
diff changeset
   937
   (22, CantConnect)]
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   938
val z3_failures =
41236
def0a3013554 trap one more Z3 error
blanchet
parents: 41222
diff changeset
   939
  [(101, OutOfResources),
def0a3013554 trap one more Z3 error
blanchet
parents: 41222
diff changeset
   940
   (103, MalformedInput),
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   941
   (110, MalformedInput)]
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   942
val unix_failures =
48797
e65385336531 recognize bus errors as crash
blanchet
parents: 48716
diff changeset
   943
  [(138, Crashed),
e65385336531 recognize bus errors as crash
blanchet
parents: 48716
diff changeset
   944
   (139, Crashed)]
43631
4144d7b4ec77 enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet
parents: 43626
diff changeset
   945
val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
40555
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   946
42100
062381c5f9f8 more precise failure reporting in Sledgehammer/SMT
blanchet
parents: 42061
diff changeset
   947
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
   948
    if is_real_cex then Unprovable else GaveUp
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   949
  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   950
  | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   951
    (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
   952
       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
   953
     | 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
   954
                             string_of_int code ^ "."))
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   955
  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   956
  | 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
   957
    UnknownError msg
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   958
40698
8a3f7ea91370 cosmetics
blanchet
parents: 40693
diff changeset
   959
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   960
val smt_max_slices =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   961
  Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   962
val smt_slice_fact_frac =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   963
  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
   964
val smt_slice_time_frac =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   965
  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
   966
val smt_slice_min_secs =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   967
  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
   968
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   969
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
   970
                    ({debug, verbose, overlord, max_mono_iters,
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45590
diff changeset
   971
                      max_new_mono_instances, timeout, slice, ...} : params)
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 50020
diff changeset
   972
                    state goal i =
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   973
  let
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45590
diff changeset
   974
    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
   975
    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
   976
      select_smt_solver name
45557
b427b23ec89c quiet down SMT
blanchet
parents: 45556
diff changeset
   977
      #> 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
   978
      #> (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
   979
            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
   980
                       (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
   981
                        |> (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
   982
          else
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   983
            I)
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   984
      #> 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
   985
    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
   986
    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
   987
      let
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   988
        val timer = Timer.startRealTimer ()
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   989
        val state =
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   990
          state |> Proof.map_context
43267
dd38b8ef52b9 exploit new semantics of "max_new_instances"
blanchet
parents: 43261
diff changeset
   991
                       (repair_monomorph_context max_mono_iters
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   992
                            default_max_mono_iters max_new_mono_instances
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47946
diff changeset
   993
                            default_max_new_mono_instances)
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   994
        val slice_timeout =
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   995
          if slice < max_slices andalso timeout <> NONE then
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   996
            let val ms = timeout |> the |> Time.toMilliseconds in
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   997
              Int.min (ms,
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   998
                  Int.max (1000 * Config.get ctxt smt_slice_min_secs,
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
   999
                      Real.ceil (Config.get ctxt smt_slice_time_frac
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1000
                                 * Real.fromInt ms)))
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1001
              |> Time.fromMilliseconds |> SOME
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1002
            end
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1003
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1004
            timeout
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1005
        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
  1006
        val _ =
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1007
          if debug then
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1008
            quote name ^ " slice " ^ string_of_int slice ^ " with " ^
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1009
            string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1010
            (case slice_timeout of
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1011
               SOME timeout => " for " ^ string_from_time timeout
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1012
             | NONE => "") ^ "..."
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1013
            |> Output.urgent_message
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1014
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1015
            ()
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
  1016
        val birth = Timer.checkRealTimer timer
41171
043f8dc3b51f facilitate debugging
blanchet
parents: 41169
diff changeset
  1017
        val _ =
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41209
diff changeset
  1018
          if debug then Output.urgent_message "Invoking SMT solver..." else ()
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 50020
diff changeset
  1019
        val state_facts = these (try (#facts o Proof.goal) state)
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1020
        val (outcome, used_facts) =
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 50020
diff changeset
  1021
          SMT_Solver.smt_filter_preprocess ctxt state_facts goal facts i
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1022
          |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41236
diff changeset
  1023
          |> (fn {outcome, used_facts} => (outcome, used_facts))
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1024
          handle exn => if Exn.is_interrupt exn then
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1025
                          reraise exn
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1026
                        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
  1027
                          (ML_Compiler.exn_message exn
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
  1028
                           |> SMT_Failure.Other_Failure |> SOME, [])
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
  1029
        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
  1030
        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
  1031
        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
  1032
        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
  1033
          case outcome of
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1034
            NONE => false
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1035
          | SOME (SMT_Failure.Counterexample _) => false
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1036
          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1037
          | 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
  1038
          | 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
  1039
          | SOME (SMT_Failure.Other_Failure _) => true
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1040
        val timeout =
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1041
          Option.map
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1042
              (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1043
              timeout
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1044
      in
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1045
        if too_many_facts_perhaps andalso slice < max_slices andalso
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1046
           num_facts > 0 andalso
31313171deb5 thread no timeout properly
blanchet
parents: 50494
diff changeset
  1047
           (timeout = NONE orelse Time.> (the timeout, Time.zeroTime)) then
41169
95167879f675 clean up fudge factors a little bit
blanchet
parents: 41168
diff changeset
  1048
          let
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1049
            val new_num_facts =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1050
              Real.ceil (Config.get ctxt smt_slice_fact_frac
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1051
                         * Real.fromInt num_facts)
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1052
            val _ =
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1053
              if verbose andalso is_some outcome then
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1054
                quote name ^ " invoked with " ^ string_of_int num_facts ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1055
                " fact" ^ plural_s num_facts ^ ": " ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1056
                string_for_failure (failure_from_smt_failure (the outcome)) ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1057
                " 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
  1058
                plural_s new_num_facts ^ "..."
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1059
                |> Output.urgent_message
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1060
              else
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1061
                ()
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1062
          in
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1063
            facts |> take new_num_facts
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
  1064
                  |> 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
  1065
          end
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1066
        else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
  1067
          {outcome = if is_none outcome then NONE else the outcome0,
45370
bab52dafa63a use "Time.time" rather than milliseconds internally
blanchet
parents: 45369
diff changeset
  1068
           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
  1069
      end
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
  1070
  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
  1071
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1072
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
  1073
        minimize_command
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 50020
diff changeset
  1074
        ({state, goal, 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
  1075
  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
  1076
    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
  1077
    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
  1078
    val facts = facts ~~ (0 upto num_facts - 1)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
  1079
                |> 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
  1080
    val {outcome, used_facts = used_pairs, run_time} =
50486
d5dc28fafd9d made MaSh evaluation driver work with SMT solvers
blanchet
parents: 50020
diff changeset
  1081
      smt_filter_loop ctxt name params state goal 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
  1082
    val used_facts = used_pairs |> map fst
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
  1083
    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
  1084
    val (preplay, message, message_tail) =
40184
91b4b73dbafb proper error handling for SMT solvers in Sledgehammer
blanchet
parents: 40181
diff changeset
  1085
      case outcome of
91b4b73dbafb proper error handling for SMT solvers in Sledgehammer
blanchet
parents: 40181
diff changeset
  1086
        NONE =>
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1087
        (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
  1088
            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
  1089
                state subgoal SMT
45560
1606122a2d0f don't needlessly pass "lam_lifted" option to "metis" call for SMT proof
blanchet
parents: 45557
diff changeset
  1090
                (bunch_of_reconstructors false
48800
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
  1091
                     (fn desperate =>
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
  1092
                         if desperate then liftingN
943bb96b4e12 improved set of reconstructor methods
blanchet
parents: 48799
diff changeset
  1093
                         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
  1094
         fn preplay =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1095
            let
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1096
              val one_line_params =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1097
                (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
  1098
                 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
  1099
                 subgoal, subgoal_count)
48799
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
  1100
              val num_chained = length (#facts (Proof.goal state))
5c9356f8c968 warn users about unused "using" facts
blanchet
parents: 48798
diff changeset
  1101
            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
  1102
         if verbose then
45370
bab52dafa63a use "Time.time" rather than milliseconds internally
blanchet
parents: 45369
diff changeset
  1103
           "\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
  1104
         else
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43259
diff changeset
  1105
           "")
43166
68e3cd19fee8 show what failed to play
blanchet
parents: 43128
diff changeset
  1106
      | SOME failure =>
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
  1107
        (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
  1108
  in