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