src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
author blanchet
Tue, 07 Jun 2011 14:38:42 +0200
changeset 43249 6c3a2c33fc39
parent 43248 69375eaa9016
child 43259 30c141dc22d6
permissions -rw-r--r--
prioritize more relevant facts for monomorphization
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
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43063
diff changeset
    12
  type locality = ATP_Translate.locality
43102
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
    13
  type type_sys = ATP_Translate.type_sys
43233
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
    14
  type reconstructor = ATP_Reconstruct.reconstructor
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43063
diff changeset
    15
  type play = ATP_Reconstruct.play
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43063
diff changeset
    16
  type minimize_command = ATP_Reconstruct.minimize_command
43233
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
    17
  type relevance_fudge = Sledgehammer_Filter.relevance_fudge
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    18
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
    19
  datatype mode = Auto_Try | Try | Normal | Minimize
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
    20
43102
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
    21
  datatype rich_type_sys =
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
    22
    Dumb_Type_Sys of type_sys |
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
    23
    Smart_Type_Sys of bool
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
    24
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    25
  type params =
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41171
diff changeset
    26
    {debug: bool,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    27
     verbose: bool,
36143
6490319b1703 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents: 36064
diff changeset
    28
     overlord: bool,
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41171
diff changeset
    29
     blocking: bool,
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    30
     provers: string list,
43102
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
    31
     type_sys: rich_type_sys,
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 42100
diff changeset
    32
     relevance_thresholds: real * real,
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 42100
diff changeset
    33
     max_relevant: int option,
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
    34
     max_mono_iters: int,
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42738
diff changeset
    35
     max_new_mono_instances: int,
43063
8f1f80a40498 don't slice if there are too few facts
blanchet
parents: 43052
diff changeset
    36
     explicit_apply: bool option,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    37
     isar_proof: bool,
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
    38
     isar_shrink_factor: int,
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
    39
     slicing: bool,
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
    40
     timeout: Time.time,
43015
21b6baec55b1 renamed "metis_timeout" to "preplay_timeout" and continued implementation
blanchet
parents: 43011
diff changeset
    41
     preplay_timeout: Time.time,
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
    42
     expect: string}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    43
41090
b98fe4de1ecd renamings
blanchet
parents: 41089
diff changeset
    44
  datatype prover_fact =
b98fe4de1ecd renamings
blanchet
parents: 41089
diff changeset
    45
    Untranslated_Fact of (string * locality) * 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
    46
    SMT_Weighted_Fact of (string * locality) * (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
    47
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    48
  type prover_problem =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    49
    {state: Proof.state,
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
    50
     goal: thm,
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
    51
     subgoal: int,
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
    52
     subgoal_count: int,
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
    53
     facts: prover_fact list,
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
    54
     smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    55
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    56
  type prover_result =
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    57
    {outcome: failure option,
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40202
diff changeset
    58
     used_facts: (string * locality) list,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    59
     run_time_in_msecs: int option,
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    60
     preplay: unit -> play,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    61
     message: play -> string}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    62
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
    63
  type prover =
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
    64
    params -> (string -> minimize_command) -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
    65
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
    66
  val dest_dir : string Config.T
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
    67
  val problem_prefix : string Config.T
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
    68
  val measure_run_time : bool Config.T
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
    69
  val atp_readable_names : bool Config.T
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    70
  val smt_triggers : bool Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    71
  val smt_weights : bool Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    72
  val smt_weight_min_facts : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    73
  val smt_min_weight : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    74
  val smt_max_weight : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    75
  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
    76
  val smt_weight_curve : (int -> int) Unsynchronized.ref
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    77
  val smt_max_slices : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    78
  val smt_slice_fact_frac : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    79
  val smt_slice_time_frac : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    80
  val smt_slice_min_secs : int Config.T
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    81
  val das_tool : string
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
    82
  val select_smt_solver : string -> Proof.context -> Proof.context
43233
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
    83
  val prover_name_for_reconstructor : reconstructor -> string option
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
    84
  val is_metis_prover : string -> bool
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
    85
  val is_atp : theory -> string -> bool
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    86
  val is_smt_prover : Proof.context -> string -> bool
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
    87
  val is_unit_equational_atp : Proof.context -> string -> bool
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
    88
  val is_prover_supported : Proof.context -> string -> bool
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    89
  val is_prover_installed : Proof.context -> string -> bool
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
    90
  val default_max_relevant_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
    91
  val is_unit_equality : term -> bool
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42944
diff changeset
    92
  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
    93
  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
    94
    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
    95
  val atp_relevance_fudge : relevance_fudge
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    96
  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
    97
  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
    98
  val weight_smt_fact :
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    99
    Proof.context -> int -> ((string * locality) * thm) * int
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   100
    -> (string * locality) * (int option * thm)
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
   101
  val untranslated_fact : prover_fact -> (string * locality) * 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
   102
  val smt_weighted_fact :
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   103
    Proof.context -> int -> prover_fact * int
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   104
    -> (string * locality) * (int option * thm)
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   105
  val supported_provers : Proof.context -> unit
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   106
  val kill_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   107
  val running_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   108
  val messages : int option -> unit
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   109
  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
   110
  val get_prover : Proof.context -> mode -> string -> prover
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   111
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   112
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
   113
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   114
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   115
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43063
diff changeset
   116
open ATP_Util
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
   117
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39453
diff changeset
   118
open ATP_Proof
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
   119
open ATP_Systems
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43063
diff changeset
   120
open ATP_Translate
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43063
diff changeset
   121
open ATP_Reconstruct
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   122
open Sledgehammer_Util
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
   123
open Sledgehammer_Filter
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
   124
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
   125
(** 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
   126
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   127
datatype mode = Auto_Try | Try | Normal | Minimize
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   128
38102
019a49759829 fix bug in the newly introduced "bound concealing" code
blanchet
parents: 38100
diff changeset
   129
(* Identifier to distinguish Sledgehammer from other tools using
019a49759829 fix bug in the newly introduced "bound concealing" code
blanchet
parents: 38100
diff changeset
   130
   "Async_Manager". *)
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   131
val das_tool = "Sledgehammer"
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   132
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
   133
val metisN = Metis_Tactics.metisN
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
   134
val metis_full_typesN = metisN ^ "_" ^ Metis_Tactics.full_typesN
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
   135
val metis_no_typesN = metisN ^ "_" ^ Metis_Tactics.no_typesN
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   136
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
   137
val metis_prover_infos =
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
   138
  [(metisN, Metis),
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
   139
   (metis_full_typesN, Metis_Full_Types),
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
   140
   (metis_no_typesN, Metis_No_Types)]
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
   141
43233
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   142
val prover_name_for_reconstructor =
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   143
  AList.find (op =) metis_prover_infos #> try hd
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   144
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
   145
val metis_reconstructors = map snd metis_prover_infos
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
   146
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
   147
val is_metis_prover = AList.defined (op =) metis_prover_infos
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   148
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
   149
43233
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   150
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
   151
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   152
fun is_smt_prover ctxt name =
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   153
  member (op =) (SMT_Solver.available_solvers_of ctxt) name
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   154
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   155
fun is_unit_equational_atp ctxt name =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   156
  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
   157
    case try (get_atp thy) name of
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   158
      SOME {formats, ...} => member (op =) formats CNF_UEQ
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   159
    | NONE => false
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   160
  end
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   161
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   162
fun is_prover_supported ctxt name =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   163
  let val thy = Proof_Context.theory_of ctxt in
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   164
    is_metis_prover name orelse is_atp thy name orelse is_smt_prover ctxt name
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   165
  end
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   166
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   167
fun is_prover_installed ctxt =
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   168
  is_metis_prover orf is_smt_prover ctxt orf
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   169
  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
   170
43222
d90151a666cc pass props not thms to ATP translator
blanchet
parents: 43220
diff changeset
   171
fun get_slices slicing slices =
43220
a6bda1a47c0a removed confusing slicing logic
blanchet
parents: 43219
diff changeset
   172
  (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   173
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   174
val metis_default_max_relevant = 20
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   175
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   176
fun default_max_relevant_for_prover ctxt slicing name =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   177
  let val thy = Proof_Context.theory_of ctxt in
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   178
    if is_metis_prover name then
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   179
      metis_default_max_relevant
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   180
    else if is_atp thy name then
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   181
      fold (Integer.max o fst o snd o snd o snd)
43222
d90151a666cc pass props not thms to ATP translator
blanchet
parents: 43220
diff changeset
   182
           (get_slices slicing (#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
   183
    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
   184
      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
   185
  end
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   186
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
   187
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
   188
  | 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
   189
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
   190
(* 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
   191
   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
   192
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
   193
  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
   194
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   195
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
   196
  | 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
   197
    is_unit_equality t
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   198
  | 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
   199
    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
   200
  | 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
   201
    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
   202
  | 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
   203
    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
   204
  | is_unit_equality _ = false
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   205
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42944
diff changeset
   206
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
   207
  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
   208
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
   209
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
   210
  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
   211
    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
   212
      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
   213
         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
   214
           (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
   215
         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
   216
           (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
   217
         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
   218
           (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
   219
    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
   220
  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
   221
    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
   222
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   223
(* FUDGE *)
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   224
val atp_relevance_fudge =
42738
2a9dcff63b80 remove unused parameter
blanchet
parents: 42737
diff changeset
   225
  {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
   226
   worse_irrel_freq = 100.0,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   227
   higher_order_irrel_weight = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   228
   abs_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   229
   abs_irrel_weight = 2.0,
42746
7e227e9de779 further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up
blanchet
parents: 42740
diff changeset
   230
   skolem_irrel_weight = 0.25,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   231
   theory_const_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   232
   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
   233
   chained_const_irrel_weight = 0.25,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   234
   intro_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   235
   elim_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   236
   simp_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   237
   local_bonus = 0.55,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   238
   assum_bonus = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   239
   chained_bonus = 1.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   240
   max_imperfect = 11.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   241
   max_imperfect_exp = 1.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   242
   threshold_divisor = 2.0,
41093
dfbc8759415f lower fudge factor
blanchet
parents: 41091
diff changeset
   243
   ridiculous_threshold = 0.01}
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   244
40071
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   245
(* FUDGE (FIXME) *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   246
val smt_relevance_fudge =
42738
2a9dcff63b80 remove unused parameter
blanchet
parents: 42737
diff changeset
   247
  {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
   248
   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
   249
   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
   250
   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
   251
   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
   252
   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
   253
   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
   254
   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
   255
   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
   256
   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
   257
   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
   258
   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
   259
   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
   260
   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
   261
   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
   262
   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
   263
   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
   264
   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
   265
   ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   266
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   267
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
   268
  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
   269
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   270
fun supported_provers ctxt =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   271
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   272
    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
   273
    val (remote_provers, local_provers) =
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
   274
      map fst metis_prover_infos @
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   275
      sort_strings (supported_atps thy) @
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   276
      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
   277
      |> List.partition (String.isPrefix remote_prefix)
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   278
  in
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   279
    Output.urgent_message ("Supported provers: " ^
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   280
                           commas (local_provers @ remote_provers) ^ ".")
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   281
  end
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   282
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   283
fun kill_provers () = Async_Manager.kill_threads das_tool "prover"
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   284
fun running_provers () = Async_Manager.running_threads das_tool "prover"
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   285
val messages = Async_Manager.thread_messages das_tool "prover"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   286
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   287
(** problems, results, ATPs, etc. **)
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   288
43102
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   289
datatype rich_type_sys =
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   290
  Dumb_Type_Sys of type_sys |
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   291
  Smart_Type_Sys of bool
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   292
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   293
type params =
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41171
diff changeset
   294
  {debug: bool,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   295
   verbose: bool,
36143
6490319b1703 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents: 36064
diff changeset
   296
   overlord: bool,
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41171
diff changeset
   297
   blocking: bool,
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   298
   provers: string list,
43102
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   299
   type_sys: rich_type_sys,
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 42100
diff changeset
   300
   relevance_thresholds: real * real,
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 42100
diff changeset
   301
   max_relevant: int option,
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   302
   max_mono_iters: int,
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42738
diff changeset
   303
   max_new_mono_instances: int,
43063
8f1f80a40498 don't slice if there are too few facts
blanchet
parents: 43052
diff changeset
   304
   explicit_apply: bool option,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   305
   isar_proof: bool,
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
   306
   isar_shrink_factor: int,
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   307
   slicing: bool,
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   308
   timeout: Time.time,
43015
21b6baec55b1 renamed "metis_timeout" to "preplay_timeout" and continued implementation
blanchet
parents: 43011
diff changeset
   309
   preplay_timeout: Time.time,
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   310
   expect: string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   311
41090
b98fe4de1ecd renamings
blanchet
parents: 41089
diff changeset
   312
datatype prover_fact =
b98fe4de1ecd renamings
blanchet
parents: 41089
diff changeset
   313
  Untranslated_Fact of (string * locality) * 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
   314
  SMT_Weighted_Fact of (string * locality) * (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
   315
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   316
type prover_problem =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   317
  {state: Proof.state,
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   318
   goal: thm,
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   319
   subgoal: int,
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   320
   subgoal_count: int,
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
   321
   facts: prover_fact list,
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   322
   smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   323
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   324
type prover_result =
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   325
  {outcome: failure option,
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40202
diff changeset
   326
   used_facts: (string * locality) list,
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   327
   run_time_in_msecs: int option,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   328
   preplay: unit -> play,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   329
   message: play -> string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   330
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   331
type prover =
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   332
  params -> (string -> minimize_command) -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   333
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   334
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   335
(* configuration attributes *)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   336
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   337
(* 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
   338
val dest_dir =
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   339
  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
   340
val problem_prefix =
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   341
  Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   342
val measure_run_time =
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   343
  Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   344
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   345
(* In addition to being easier to read, readable names are often much shorter,
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   346
   especially if types are mangled in names. For these reason, they are enabled
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   347
   by default. *)
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   348
val atp_readable_names =
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   349
  Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   350
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   351
val smt_triggers =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   352
  Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   353
val smt_weights =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   354
  Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   355
val smt_weight_min_facts =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   356
  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
   357
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   358
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   359
val smt_min_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   360
  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   361
val smt_max_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   362
  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   363
val smt_max_weight_index =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   364
  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
   365
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
   366
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   367
fun smt_fact_weight ctxt j num_facts =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   368
  if Config.get ctxt smt_weights andalso
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   369
     num_facts >= Config.get ctxt smt_weight_min_facts then
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   370
    let
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   371
      val min = Config.get ctxt smt_min_weight
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   372
      val max = Config.get ctxt smt_max_weight
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   373
      val max_index = Config.get ctxt smt_max_weight_index
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   374
      val curve = !smt_weight_curve
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   375
    in
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   376
      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
   377
            div curve max_index)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   378
    end
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   379
  else
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   380
    NONE
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   381
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   382
fun weight_smt_fact ctxt num_facts ((info, th), j) =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   383
  let val thy = Proof_Context.theory_of ctxt in
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   384
    (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
   385
  end
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   386
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
   387
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
   388
  | 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
   389
fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   390
  | smt_weighted_fact ctxt num_facts (fact, j) =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   391
    (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
   392
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   393
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
   394
  (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
   395
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   396
fun with_path cleanup after f path =
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   397
  Exn.capture f path
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   398
  |> tap (fn _ => cleanup path)
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   399
  |> Exn.release
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   400
  |> tap (after path)
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   401
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   402
fun proof_banner mode name =
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   403
  case mode of
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   404
    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   405
  | 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
   406
  | _ => "Try this"
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   407
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   408
(* based on "Mirabelle.can_apply" and generalized *)
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   409
fun timed_apply timeout tac state i =
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   410
  let
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   411
    val {context = ctxt, facts, goal} = Proof.goal state
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   412
    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
   413
  in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   414
43211
77c432fe28ff enable new Metis
blanchet
parents: 43205
diff changeset
   415
fun tac_for_reconstructor Metis =
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
   416
    Metis_Tactics.metis_tac [Metis_Tactics.partial_type_sys]
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
   417
  | tac_for_reconstructor Metis_Full_Types =
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
   418
    Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
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
   419
  | tac_for_reconstructor Metis_No_Types =
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
   420
    Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   421
  | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   422
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   423
fun timed_reconstructor reconstructor debug timeout ths =
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   424
  (Config.put Metis_Tactics.verbose debug
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   425
   #> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths))
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   426
  |> timed_apply timeout
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   427
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   428
fun filter_used_facts used = filter (member (op =) used o fst)
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   429
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   430
fun play_one_line_proof debug timeout ths state i reconstructors =
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   431
  let
43166
68e3cd19fee8 show what failed to play
blanchet
parents: 43128
diff changeset
   432
    fun play [] [] = Failed_to_Play (hd reconstructors)
43219
371cdc675cf9 suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
blanchet
parents: 43218
diff changeset
   433
      | play timed_outs [] = Trust_Playable (List.last timed_outs, SOME timeout)
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   434
      | play timed_out (reconstructor :: reconstructors) =
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
   435
        let val timer = Timer.startRealTimer () in
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
   436
          case timed_reconstructor reconstructor debug timeout ths state i of
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   437
            SOME (SOME _) => Played (reconstructor, Timer.checkRealTimer timer)
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   438
          | _ => play timed_out reconstructors
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
   439
        end
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
   440
        handle TimeLimit.TimeOut =>
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   441
               play (reconstructor :: timed_out) reconstructors
43034
18259246abb5 try both "metis" and (on failure) "metisFT" in replay
blanchet
parents: 43033
diff changeset
   442
  in
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
   443
    if timeout = Time.zeroTime then Trust_Playable (hd reconstructors, NONE)
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   444
    else play [] reconstructors
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   445
  end
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   446
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   447
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   448
(* 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
   449
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
   450
(* 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
   451
   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
   452
   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
   453
   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
   454
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
   455
(* 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
   456
   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
   457
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
   458
  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
   459
    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
   460
        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
   461
      | 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
   462
      | 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
   463
    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
   464
    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
   465
      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
   466
        (_, @{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
   467
      | (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
   468
        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
   469
      | (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
   470
        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
   471
      | (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
   472
        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
   473
      | (_, @{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
   474
        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
   475
        (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
   476
      | (_, @{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
   477
        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
   478
        (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
   479
      | (_, @{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
   480
      | (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
   481
      | (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
   482
      | (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
   483
      | (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
   484
      | _ => 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
   485
  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
   486
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
   487
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
   488
  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
   489
                   | 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
   490
                   | _ => 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
   491
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
   492
(* 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
   493
   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
   494
   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
   495
   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
   496
   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
   497
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
   498
(* 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
   499
   "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
   500
   are omitted. *)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   501
fun is_dangerous_prop ctxt =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   502
  transform_elim_prop
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
   503
  #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
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
   504
      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
   505
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   506
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   507
  | int_opt_add _ _ = NONE
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   508
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   509
val atp_blacklist_max_iters = 10
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   510
(* Important messages are important but not so important that users want to see
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   511
   them each time. *)
42609
b5e94b70bc06 fixed random number invocation
blanchet
parents: 42593
diff changeset
   512
val atp_important_message_keep_quotient = 10
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   513
42589
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42588
diff changeset
   514
val fallback_best_type_systems =
43128
a19826080596 tuned names
blanchet
parents: 43102
diff changeset
   515
  [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Lightweight)]
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   516
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   517
fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
43101
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43096
diff changeset
   518
    choose_format formats type_sys
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   519
  | choose_format_and_type_sys best_type_systems formats
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   520
                               (Smart_Type_Sys full_types) =
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42609
diff changeset
   521
    map type_sys_from_string best_type_systems @ fallback_best_type_systems
42589
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42588
diff changeset
   522
    |> find_first (if full_types then is_type_sys_virtually_sound else K true)
43101
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43096
diff changeset
   523
    |> the |> choose_format formats
42548
ea2a28b1938f make sure the minimizer monomorphizes when it should
blanchet
parents: 42544
diff changeset
   524
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   525
val metis_minimize_max_time = seconds 2.0
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   526
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   527
fun choose_minimize_command minimize_command name preplay =
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   528
  (case preplay of
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   529
     Played (reconstructor, time) =>
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   530
     if Time.<= (time, metis_minimize_max_time) then
43233
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   531
       prover_name_for_reconstructor reconstructor |> the_default name
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   532
     else
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   533
       name
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   534
   | _ => name)
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   535
  |> minimize_command
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   536
43247
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   537
fun is_polymorphic_fact get_thm =
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   538
  get_thm #> prop_of #> Term.exists_type Monomorph.typ_has_tvars
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   539
fun num_polymorphic_facts get_thm facts =
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   540
  fold (fn fact => is_polymorphic_fact get_thm fact ? Integer.add 1) facts 0
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   541
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   542
fun repair_monomorph_context max_iters get_thm facts max_new_instances =
43232
bd4d26327633 removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)
blanchet
parents: 43231
diff changeset
   543
  Config.put Monomorph.max_rounds max_iters
43247
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   544
  #> Config.put Monomorph.max_new_instances
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   545
                (num_polymorphic_facts get_thm facts + max_new_instances)
43230
dabf6e311213 clarified meaning of monomorphization configuration option by renaming it
boehmes
parents: 43228
diff changeset
   546
  #> Config.put Monomorph.keep_partial_instances false
43226
a4a314a0a90a use new monomorphization code
blanchet
parents: 43224
diff changeset
   547
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   548
fun run_atp mode name
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   549
        ({exec, required_execs, arguments, proof_delims, known_failures,
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   550
          conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   551
        ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   552
          max_new_mono_instances, explicit_apply, isar_proof,
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   553
          isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
43037
ade5c84f860f cleanup proof text generation code
blanchet
parents: 43034
diff changeset
   554
        minimize_command
ade5c84f860f cleanup proof text generation code
blanchet
parents: 43034
diff changeset
   555
        ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   556
  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
   557
    val thy = Proof.theory_of state
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   558
    val ctxt = Proof.context_of state
43004
20e9caff1f86 fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
blanchet
parents: 42998
diff changeset
   559
    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
   560
    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
   561
      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
   562
      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
   563
    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
   564
      Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41152
diff changeset
   565
                  "_" ^ 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
   566
    val problem_path_name =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   567
      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
   568
        File.tmp_path problem_file_name
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   569
      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
   570
        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
   571
      else
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   572
        error ("No such directory: " ^ quote dest_dir ^ ".")
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   573
    val measure_run_time = verbose orelse Config.get ctxt measure_run_time
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38091
diff changeset
   574
    val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   575
    fun split_time s =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   576
      let
42448
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   577
        val split = String.tokens (fn c => str c = "\n")
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   578
        val (output, t) = s |> split |> split_last |> apfst cat_lines
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   579
        fun as_num f = f >> (fst o read_int)
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   580
        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   581
        val digit = Scan.one Symbol.is_ascii_digit
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   582
        val num3 = as_num (digit ::: digit ::: (digit >> single))
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   583
        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 40562
diff changeset
   584
        val as_time = Scan.read Symbol.stopper time o raw_explode
42448
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   585
      in (output, as_time t) end
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   586
    fun run_on prob_file =
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38091
diff changeset
   587
      case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   588
        (home_var, _) :: _ =>
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   589
        error ("The environment variable " ^ quote home_var ^ " is not set.")
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   590
      | [] =>
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   591
        if File.exists command then
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   592
          let
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   593
            (* If slicing is disabled, we expand the last slice to fill the
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   594
               entire time available. *)
43222
d90151a666cc pass props not thms to ATP translator
blanchet
parents: 43220
diff changeset
   595
            val actual_slices = get_slices slicing (best_slices ctxt)
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   596
            val num_actual_slices = length actual_slices
42445
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   597
            fun monomorphize_facts facts =
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   598
              let
43226
a4a314a0a90a use new monomorphization code
blanchet
parents: 43224
diff changeset
   599
                val ctxt =
43247
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   600
                  ctxt |> repair_monomorph_context max_mono_iters snd facts
43226
a4a314a0a90a use new monomorphization code
blanchet
parents: 43224
diff changeset
   601
                                                   max_new_mono_instances
42445
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   602
                (* pseudo-theorem involving the same constants as the subgoal *)
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   603
                val subgoal_th =
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   604
                  Logic.list_implies (hyp_ts, concl_t)
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   605
                  |> Skip_Proof.make_thm thy
43249
6c3a2c33fc39 prioritize more relevant facts for monomorphization
blanchet
parents: 43248
diff changeset
   606
                val rths =
6c3a2c33fc39 prioritize more relevant facts for monomorphization
blanchet
parents: 43248
diff changeset
   607
                  facts |> chop (length facts div 4)
6c3a2c33fc39 prioritize more relevant facts for monomorphization
blanchet
parents: 43248
diff changeset
   608
                        |>> map (pair 1 o snd)
6c3a2c33fc39 prioritize more relevant facts for monomorphization
blanchet
parents: 43248
diff changeset
   609
                        ||> map (pair 2 o snd)
6c3a2c33fc39 prioritize more relevant facts for monomorphization
blanchet
parents: 43248
diff changeset
   610
                        |> op @
6c3a2c33fc39 prioritize more relevant facts for monomorphization
blanchet
parents: 43248
diff changeset
   611
                        |> cons (0, subgoal_th)
42445
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   612
              in
43249
6c3a2c33fc39 prioritize more relevant facts for monomorphization
blanchet
parents: 43248
diff changeset
   613
                Monomorph.monomorph atp_schematic_consts_of rths ctxt
43226
a4a314a0a90a use new monomorphization code
blanchet
parents: 43224
diff changeset
   614
                |> fst |> tl
a4a314a0a90a use new monomorphization code
blanchet
parents: 43224
diff changeset
   615
                |> curry ListPair.zip (map fst facts)
a4a314a0a90a use new monomorphization code
blanchet
parents: 43224
diff changeset
   616
                |> maps (fn (name, rths) => map (pair name o snd) rths)
42445
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   617
              end
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   618
            fun run_slice blacklist (slice, (time_frac, (complete,
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   619
                                       (best_max_relevant, best_type_systems))))
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   620
                          time_left =
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   621
              let
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   622
                val num_facts =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   623
                  length facts |> is_none max_relevant
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   624
                                  ? Integer.min best_max_relevant
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   625
                val (format, type_sys) =
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43050
diff changeset
   626
                  choose_format_and_type_sys best_type_systems formats type_sys
42638
a7a30721767a have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents: 42623
diff changeset
   627
                val fairly_sound = is_type_sys_fairly_sound type_sys
42451
a75fcd103cbb automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
blanchet
parents: 42450
diff changeset
   628
                val facts =
43214
4e850b2c1f5c removed old optimization that isn't one anyone
blanchet
parents: 43212
diff changeset
   629
                  facts |> map untranslated_fact
4e850b2c1f5c removed old optimization that isn't one anyone
blanchet
parents: 43212
diff changeset
   630
                        |> not fairly_sound
4e850b2c1f5c removed old optimization that isn't one anyone
blanchet
parents: 43212
diff changeset
   631
                           ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
42638
a7a30721767a have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents: 42623
diff changeset
   632
                        |> take num_facts
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   633
                        |> not (null blacklist)
43214
4e850b2c1f5c removed old optimization that isn't one anyone
blanchet
parents: 43212
diff changeset
   634
                           ? filter_out (member (op =) blacklist o fst)
42589
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42588
diff changeset
   635
                        |> polymorphism_of_type_sys type_sys <> Polymorphic
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42588
diff changeset
   636
                           ? monomorphize_facts
43226
a4a314a0a90a use new monomorphization code
blanchet
parents: 43224
diff changeset
   637
                        |> map (apsnd prop_of)
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   638
                val real_ms = Real.fromInt o Time.toMilliseconds
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   639
                val slice_timeout =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   640
                  ((real_ms time_left
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   641
                    |> (if slice < num_actual_slices - 1 then
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   642
                          curry Real.min (time_frac * real_ms timeout)
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   643
                        else
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   644
                          I))
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   645
                   * 0.001) |> seconds
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   646
                val _ =
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   647
                  if debug then
42699
d4f5fec71ded no lies in debug output (e.g. "slice 2 of 1")
blanchet
parents: 42684
diff changeset
   648
                    quote name ^ " slice #" ^ string_of_int (slice + 1) ^
d4f5fec71ded no lies in debug output (e.g. "slice 2 of 1")
blanchet
parents: 42684
diff changeset
   649
                    " with " ^ string_of_int num_facts ^ " fact" ^
d4f5fec71ded no lies in debug output (e.g. "slice 2 of 1")
blanchet
parents: 42684
diff changeset
   650
                    plural_s num_facts ^ " for " ^
d4f5fec71ded no lies in debug output (e.g. "slice 2 of 1")
blanchet
parents: 42684
diff changeset
   651
                    string_from_time slice_timeout ^ "..."
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   652
                    |> Output.urgent_message
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   653
                  else
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   654
                    ()
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42523
diff changeset
   655
                val (atp_problem, pool, conjecture_offset, facts_offset,
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   656
                     fact_names, typed_helpers, sym_tab) =
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   657
                  prepare_atp_problem ctxt format conj_sym_kind prem_kind
43092
93ec303e1917 more work on new metis that exploits the powerful new type encodings
blanchet
parents: 43085
diff changeset
   658
                      type_sys explicit_apply
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43092
diff changeset
   659
                      (Config.get ctxt atp_readable_names) true hyp_ts concl_t
f181d66046d4 don't preprocess twice
blanchet
parents: 43092
diff changeset
   660
                      facts
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   661
                fun weights () = atp_problem_weights atp_problem
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   662
                val core =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   663
                  File.shell_path command ^ " " ^
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   664
                  arguments ctxt slice slice_timeout weights ^ " " ^
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   665
                  File.shell_path prob_file
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   666
                val command =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   667
                  (if measure_run_time then
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   668
                     "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   669
                   else
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   670
                     "exec " ^ core) ^ " 2>&1"
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   671
                val _ =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   672
                  atp_problem
43224
97906dfd39b7 renamed ML function
blanchet
parents: 43222
diff changeset
   673
                  |> tptp_lines_for_atp_problem format
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   674
                  |> cons ("% " ^ command ^ "\n")
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   675
                  |> File.write_list prob_file
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   676
                val conjecture_shape =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   677
                  conjecture_offset + 1
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   678
                    upto conjecture_offset + length hyp_ts + 1
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   679
                  |> map single
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   680
                val ((output, msecs), res_code) =
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   681
                  bash_output command
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   682
                  |>> (if overlord then
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   683
                         prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   684
                       else
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   685
                         I)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   686
                  |>> (if measure_run_time then split_time else rpair NONE)
42449
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42448
diff changeset
   687
                val (atp_proof, outcome) =
42849
ba45312308b5 reintroduce TFF workaround for limitations of actual TFF implementations (ToFoF, SNARK)
blanchet
parents: 42837
diff changeset
   688
                  extract_tstplike_proof_and_outcome verbose complete res_code
ba45312308b5 reintroduce TFF workaround for limitations of actual TFF implementations (ToFoF, SNARK)
blanchet
parents: 42837
diff changeset
   689
                      proof_delims known_failures output
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42939
diff changeset
   690
                  |>> atp_proof_from_tstplike_proof atp_problem
42965
1403595ec38c slightly gracefuller handling of LEO-II and Satallax output
blanchet
parents: 42963
diff changeset
   691
                  handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   692
                val (conjecture_shape, facts_offset, fact_names,
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   693
                     typed_helpers) =
42449
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42448
diff changeset
   694
                  if is_none outcome then
42647
59142dbfa3ba no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter
blanchet
parents: 42646
diff changeset
   695
                    repair_conjecture_shape_and_fact_names type_sys output
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   696
                        conjecture_shape facts_offset fact_names typed_helpers
42449
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42448
diff changeset
   697
                  else
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42579
diff changeset
   698
                    (* don't bother repairing *)
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   699
                    (conjecture_shape, facts_offset, fact_names, typed_helpers)
42449
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42448
diff changeset
   700
                val outcome =
42451
a75fcd103cbb automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
blanchet
parents: 42450
diff changeset
   701
                  case outcome of
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42579
diff changeset
   702
                    NONE =>
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42965
diff changeset
   703
                    used_facts_in_unsound_atp_proof ctxt type_sys
42876
e336ef6313aa more informative message when Sledgehammer finds an unsound proof
blanchet
parents: 42853
diff changeset
   704
                        conjecture_shape facts_offset fact_names atp_proof
e336ef6313aa more informative message when Sledgehammer finds an unsound proof
blanchet
parents: 42853
diff changeset
   705
                    |> Option.map (fn facts =>
e336ef6313aa more informative message when Sledgehammer finds an unsound proof
blanchet
parents: 42853
diff changeset
   706
                           UnsoundProof (is_type_sys_virtually_sound type_sys,
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42939
diff changeset
   707
                                         facts |> sort string_ord))
42451
a75fcd103cbb automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
blanchet
parents: 42450
diff changeset
   708
                  | SOME Unprovable =>
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
   709
                    if null blacklist then outcome else SOME GaveUp
42451
a75fcd103cbb automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
blanchet
parents: 42450
diff changeset
   710
                  | _ => outcome
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   711
              in
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   712
                ((pool, conjecture_shape, facts_offset, fact_names,
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   713
                  typed_helpers, sym_tab),
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   714
                 (output, msecs, type_sys, atp_proof, outcome))
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   715
              end
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   716
            val timer = Timer.startRealTimer ()
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   717
            fun maybe_run_slice blacklist slice
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   718
                                (result as (_, (_, msecs0, _, _, SOME _))) =
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   719
                let
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   720
                  val time_left = Time.- (timeout, Timer.checkRealTimer timer)
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   721
                in
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   722
                  if Time.<= (time_left, Time.zeroTime) then
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   723
                    result
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   724
                  else
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   725
                    (run_slice blacklist slice time_left
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   726
                     |> (fn (stuff, (output, msecs, type_sys, atp_proof,
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   727
                                     outcome)) =>
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   728
                            (stuff, (output, int_opt_add msecs0 msecs, type_sys,
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   729
                                     atp_proof, outcome))))
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   730
                end
42450
2765d4fb2b9c automatically retry with full-types upon unsound proof
blanchet
parents: 42449
diff changeset
   731
              | maybe_run_slice _ _ result = result
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   732
            fun maybe_blacklist_facts_and_retry iter blacklist
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   733
                    (result as ((_, _, facts_offset, fact_names, _, _),
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   734
                                (_, _, type_sys, atp_proof,
42876
e336ef6313aa more informative message when Sledgehammer finds an unsound proof
blanchet
parents: 42853
diff changeset
   735
                                 SOME (UnsoundProof (false, _))))) =
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42965
diff changeset
   736
                (case used_facts_in_atp_proof ctxt type_sys facts_offset
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42965
diff changeset
   737
                                              fact_names atp_proof of
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   738
                   [] => result
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   739
                 | new_baddies =>
42835
8d723194dedf run blacklist algorithm only if slicing is on
blanchet
parents: 42832
diff changeset
   740
                   if slicing andalso iter < atp_blacklist_max_iters - 1 then
42777
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   741
                     let val blacklist = new_baddies @ blacklist in
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   742
                       result
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   743
                       |> maybe_run_slice blacklist (List.last actual_slices)
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   744
                       |> maybe_blacklist_facts_and_retry (iter + 1) blacklist
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   745
                     end
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   746
                   else
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   747
                     result)
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   748
              | maybe_blacklist_facts_and_retry _ _ result = result
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   749
          in
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   750
            ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   751
             ("", SOME 0, hd fallback_best_type_systems, [],
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   752
              SOME InternalError))
42451
a75fcd103cbb automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
blanchet
parents: 42450
diff changeset
   753
            |> fold (maybe_run_slice []) actual_slices
a75fcd103cbb automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
blanchet
parents: 42450
diff changeset
   754
               (* The ATP found an unsound proof? Automatically try again
a75fcd103cbb automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
blanchet
parents: 42450
diff changeset
   755
                  without the offending facts! *)
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   756
            |> maybe_blacklist_facts_and_retry 0 []
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   757
          end
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   758
        else
41944
b97091ae583a Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents: 41799
diff changeset
   759
          error ("Bad executable: " ^ Path.print command ^ ".")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   760
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   761
    (* If the problem file has not been exported, remove it; otherwise, export
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   762
       the proof file too. *)
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   763
    fun cleanup prob_file =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   764
      if dest_dir = "" then try File.rm prob_file else NONE
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   765
    fun export prob_file (_, (output, _, _, _, _)) =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   766
      if dest_dir = "" then
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   767
        ()
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   768
      else
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   769
        File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   770
    val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   771
          sym_tab),
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   772
         (output, msecs, type_sys, 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
   773
      with_path cleanup export run_on problem_path_name
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   774
    val important_message =
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
   775
      if mode = Normal andalso
42609
b5e94b70bc06 fixed random number invocation
blanchet
parents: 42593
diff changeset
   776
         random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   777
        extract_important_message output
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   778
      else
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   779
        ""
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   780
    val (used_facts, preplay, message) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   781
      case outcome of
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   782
        NONE =>
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   783
        let
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   784
          val used_facts =
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   785
            used_facts_in_atp_proof ctxt type_sys facts_offset fact_names
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   786
                                    atp_proof
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   787
        in
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   788
          (used_facts,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   789
           fn () =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   790
              let
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   791
                val used_ths =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   792
                  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
   793
                        |> map snd
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   794
              in
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   795
                play_one_line_proof debug preplay_timeout used_ths state subgoal
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
   796
                                    metis_reconstructors
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   797
              end,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   798
           fn preplay =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   799
              let
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   800
                val full_types = uses_typed_helpers typed_helpers atp_proof
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   801
                val isar_params =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   802
                  (debug, full_types, isar_shrink_factor, type_sys, pool,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   803
                   conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   804
                   goal)
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   805
                val one_line_params =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   806
                  (preplay, proof_banner mode name, used_facts,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   807
                   choose_minimize_command minimize_command name preplay,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   808
                   subgoal, subgoal_count)
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   809
              in
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   810
                proof_text ctxt isar_proof isar_params one_line_params ^
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   811
                (if verbose then
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   812
                   "\nATP real CPU time: " ^
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   813
                   string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   814
                 else
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   815
                   "") ^
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   816
                (if important_message <> "" then
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   817
                   "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   818
                   important_message
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   819
                 else
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   820
                   "")
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   821
              end)
43033
c4b9b4be90c4 show time taken for reconstruction
blanchet
parents: 43031
diff changeset
   822
        end
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   823
      | SOME failure =>
43166
68e3cd19fee8 show what failed to play
blanchet
parents: 43128
diff changeset
   824
        ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure)
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   825
  in
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   826
    {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   827
     preplay = preplay, message = message}
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   828
  end
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   829
40669
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   830
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   831
   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
   832
   ourselves. *)
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   833
val remote_smt_failures =
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   834
  [(22, CantConnect),
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   835
   (2, NoLibwwwPerl)]
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   836
val z3_wrapper_failures =
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43063
diff changeset
   837
  [(11, InternalError),
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   838
   (12, InternalError),
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   839
   (13, InternalError)]
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   840
val z3_failures =
41236
def0a3013554 trap one more Z3 error
blanchet
parents: 41222
diff changeset
   841
  [(101, OutOfResources),
def0a3013554 trap one more Z3 error
blanchet
parents: 41222
diff changeset
   842
   (103, MalformedInput),
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   843
   (110, MalformedInput)]
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   844
val unix_failures =
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   845
  [(139, Crashed)]
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   846
val smt_failures =
41799
98b3d5ce0935 exit code 127 can mean many things -- not just (and probably not) Perl missing
blanchet
parents: 41790
diff changeset
   847
  remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
40555
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   848
42100
062381c5f9f8 more precise failure reporting in Sledgehammer/SMT
blanchet
parents: 42061
diff changeset
   849
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
   850
    if is_real_cex then Unprovable else GaveUp
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   851
  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   852
  | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   853
    (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
   854
       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
   855
     | 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
   856
                             string_of_int code ^ "."))
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   857
  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   858
  | 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
   859
    UnknownError msg
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   860
40698
8a3f7ea91370 cosmetics
blanchet
parents: 40693
diff changeset
   861
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   862
val smt_max_slices =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   863
  Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   864
val smt_slice_fact_frac =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   865
  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
   866
val smt_slice_time_frac =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   867
  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
   868
val smt_slice_min_secs =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   869
  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
   870
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   871
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
   872
                    ({debug, verbose, overlord, max_mono_iters,
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42738
diff changeset
   873
                      max_new_mono_instances, timeout, slicing, ...} : params)
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   874
                    state i smt_filter =
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   875
  let
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   876
    val max_slices = if slicing 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
   877
    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
   878
      select_smt_solver name
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   879
      #> (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
   880
            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
   881
                       (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
   882
                        |> (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
   883
          else
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   884
            I)
2749c357f865 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents: 43232
diff changeset
   885
      #> 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
   886
    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
   887
    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
   888
      let
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   889
        val timer = Timer.startRealTimer ()
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   890
        val state =
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   891
          state |> Proof.map_context
43247
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   892
                       (repair_monomorph_context max_mono_iters (snd o snd)
4387af606a09 workaround current "max_new_instances" semantics
blanchet
parents: 43236
diff changeset
   893
                                                 facts 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
   894
        val ms = timeout |> Time.toMilliseconds
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   895
        val slice_timeout =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   896
          if slice < max_slices then
41169
95167879f675 clean up fudge factors a little bit
blanchet
parents: 41168
diff changeset
   897
            Int.min (ms,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   898
                Int.max (1000 * Config.get ctxt smt_slice_min_secs,
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   899
                    Real.ceil (Config.get ctxt smt_slice_time_frac
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   900
                               * Real.fromInt ms)))
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   901
            |> Time.fromMilliseconds
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   902
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   903
            timeout
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   904
        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
   905
        val _ =
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   906
          if debug then
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   907
            quote name ^ " slice " ^ string_of_int slice ^ " with " ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   908
            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
   909
            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
   910
            |> Output.urgent_message
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   911
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   912
            ()
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   913
        val birth = Timer.checkRealTimer timer
41171
043f8dc3b51f facilitate debugging
blanchet
parents: 41169
diff changeset
   914
        val _ =
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41209
diff changeset
   915
          if debug then Output.urgent_message "Invoking SMT solver..." else ()
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
   916
        val (outcome, used_facts) =
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   917
          (case (slice, smt_filter) of
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   918
             (1, SOME head) => head |> apsnd (apsnd repair_context)
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   919
           | _ => 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
   920
          |> SMT_Solver.smt_filter_apply slice_timeout
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41236
diff changeset
   921
          |> (fn {outcome, used_facts} => (outcome, used_facts))
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
   922
          handle exn => if Exn.is_interrupt exn then
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
   923
                          reraise exn
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
   924
                        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
   925
                          (ML_Compiler.exn_message exn
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
   926
                           |> SMT_Failure.Other_Failure |> SOME, [])
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   927
        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
   928
        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   929
        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
   930
        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
   931
          case outcome of
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   932
            NONE => false
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   933
          | SOME (SMT_Failure.Counterexample _) => false
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   934
          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   935
          | 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
   936
          | 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
   937
          | 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
   938
        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
   939
      in
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   940
        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
   941
           num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
41169
95167879f675 clean up fudge factors a little bit
blanchet
parents: 41168
diff changeset
   942
          let
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   943
            val new_num_facts =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   944
              Real.ceil (Config.get ctxt smt_slice_fact_frac
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   945
                         * Real.fromInt num_facts)
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   946
            val _ =
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   947
              if verbose andalso is_some outcome then
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   948
                quote name ^ " invoked with " ^ string_of_int num_facts ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   949
                " fact" ^ plural_s num_facts ^ ": " ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   950
                string_for_failure (failure_from_smt_failure (the outcome)) ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   951
                " 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
   952
                plural_s new_num_facts ^ "..."
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   953
                |> Output.urgent_message
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   954
              else
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   955
                ()
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   956
          in
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   957
            facts |> take new_num_facts
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   958
                  |> 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
   959
          end
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   960
        else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   961
          {outcome = if is_none outcome then NONE else the outcome0,
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   962
           used_facts = used_facts,
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   963
           run_time_in_msecs = SOME (Time.toMilliseconds 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
   964
      end
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   965
  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
   966
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   967
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
   968
        minimize_command
5f8d74d3b297 added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents: 43006
diff changeset
   969
        ({state, subgoal, subgoal_count, facts, smt_filter, ...}
5f8d74d3b297 added syntax for specifying Metis timeout (currently used only by SMT solvers)
blanchet
parents: 43006
diff changeset
   970
         : 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
   971
  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
   972
    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
   973
    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
   974
    val facts = facts ~~ (0 upto num_facts - 1)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   975
                |> map (smt_weighted_fact ctxt num_facts)
40181
3788b7adab36 integrated "smt" proof method with Sledgehammer
blanchet
parents: 40132
diff changeset
   976
    val {outcome, used_facts, run_time_in_msecs} =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   977
      smt_filter_loop ctxt name params state subgoal smt_filter facts
43037
ade5c84f860f cleanup proof text generation code
blanchet
parents: 43034
diff changeset
   978
    val (used_facts, used_ths) = used_facts |> ListPair.unzip
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   979
    val outcome = outcome |> Option.map failure_from_smt_failure
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   980
    val (preplay, message) =
40184
91b4b73dbafb proper error handling for SMT solvers in Sledgehammer
blanchet
parents: 40181
diff changeset
   981
      case outcome of
91b4b73dbafb proper error handling for SMT solvers in Sledgehammer
blanchet
parents: 40181
diff changeset
   982
        NONE =>
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   983
        (fn () =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   984
            let
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   985
              fun smt_settings () =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   986
                if name = SMT_Solver.solver_name_of ctxt then ""
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   987
                else "smt_solver = " ^ maybe_quote name
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   988
            in
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   989
              case play_one_line_proof debug preplay_timeout used_ths state
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
   990
                                       subgoal metis_reconstructors of
43168
467d5b34e1f5 temporarily added "MetisX" as reconstructor and minimizer
blanchet
parents: 43166
diff changeset
   991
                p as Played _ => p
467d5b34e1f5 temporarily added "MetisX" as reconstructor and minimizer
blanchet
parents: 43166
diff changeset
   992
              | _ => Trust_Playable (SMT (smt_settings ()), NONE)
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   993
            end,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   994
         fn preplay =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   995
            let
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   996
              val one_line_params =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   997
                (preplay, proof_banner mode name, used_facts,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   998
                 choose_minimize_command minimize_command name preplay,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   999
                 subgoal, subgoal_count)
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1000
            in
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1001
              one_line_proof_text one_line_params ^
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1002
              (if verbose then
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1003
                 "\nSMT solver real CPU time: " ^
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1004
                 string_from_time (Time.fromMilliseconds
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1005
                                       (the run_time_in_msecs)) ^ "."
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1006
               else
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1007
                 "")
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1008
            end)
43166
68e3cd19fee8 show what failed to play
blanchet
parents: 43128
diff changeset
  1009
      | SOME failure =>
68e3cd19fee8 show what failed to play
blanchet
parents: 43128
diff changeset
  1010
        (K (Failed_to_Play Metis), fn _ => string_for_failure failure)
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
  1011
  in
43037
ade5c84f860f cleanup proof text generation code
blanchet
parents: 43034
diff changeset
  1012
    {outcome = outcome, used_facts = used_facts,
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1013
     run_time_in_msecs = run_time_in_msecs, preplay = preplay,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1014
     message = message}
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
  1015
  end
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
  1016
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1017
fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1018
              ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1019
  let
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
  1020
    val reconstructor =
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
  1021
      case AList.lookup (op =) metis_prover_infos name of
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
  1022
        SOME r => r
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
  1023
      | NONE => raise Fail ("unknown Metis version: " ^ quote name)
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1024
    val (used_facts, used_ths) =
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1025
      facts |> map untranslated_fact |> ListPair.unzip
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1026
  in
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1027
    case play_one_line_proof debug timeout used_ths state subgoal
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1028
                             [reconstructor] of
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1029
      play as Played (_, time) =>
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1030
      {outcome = NONE, used_facts = used_facts,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1031
       run_time_in_msecs = SOME (Time.toMilliseconds time),
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1032
       preplay = K play,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1033
       message = fn play =>
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1034
                    let
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1035
                      val one_line_params =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1036
                         (play, proof_banner mode name, used_facts,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1037
                          minimize_command name, subgoal, subgoal_count)
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1038
                    in one_line_proof_text one_line_params end}
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1039
    | play =>
43166
68e3cd19fee8 show what failed to play
blanchet
parents: 43128
diff changeset
  1040
      let
68e3cd19fee8 show what failed to play
blanchet
parents: 43128
diff changeset
  1041
        val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
68e3cd19fee8 show what failed to play
blanchet
parents: 43128
diff changeset
  1042
      in
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1043
        {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1044
         preplay = K play, message = fn _ => string_for_failure failure}
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1045
      end
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1046
  end
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 43044
diff changeset
  1047
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43015
diff changeset
  1048
fun get_prover ctxt mode name =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
  1049
  let val thy = Proof_Context.theory_of ctxt in
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1050
    if is_metis_prover name then run_metis mode name
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1051
    else if is_atp thy name then run_atp mode name (get_atp thy name)
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1052
    else if is_smt_prover ctxt name then run_smt_solver mode name
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
  1053
    else error ("No such prover: " ^ name ^ ".")
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
  1054
  end
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
  1055
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
  1056
end;