src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
author blanchet
Tue, 24 May 2011 10:01:03 +0200
changeset 42968 74415622d293
parent 42965 1403595ec38c
child 42972 79c191d3ea03
permissions -rw-r--r--
more work on parsing LEO-II proofs and extracting uses of extensionality
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
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    12
  type locality = Sledgehammer_Filter.locality
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
    13
  type relevance_fudge = Sledgehammer_Filter.relevance_fudge
40114
blanchet
parents: 40072
diff changeset
    14
  type translated_formula = Sledgehammer_ATP_Translate.translated_formula
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41136
diff changeset
    15
  type type_system = Sledgehammer_ATP_Translate.type_system
40068
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
    16
  type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    17
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
    18
  datatype rich_type_system =
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
    19
    Dumb_Type_Sys of type_system |
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
    20
    Smart_Type_Sys of bool
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
    21
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    22
  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
    23
    {debug: bool,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    24
     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
    25
     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
    26
     blocking: bool,
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    27
     provers: string list,
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
    28
     type_sys: rich_type_system,
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 42100
diff changeset
    29
     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
    30
     max_relevant: int option,
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
    31
     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
    32
     max_new_mono_instances: int,
36235
61159615a0c5 added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents: 36231
diff changeset
    33
     explicit_apply: bool,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    34
     isar_proof: bool,
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
    35
     isar_shrink_factor: int,
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
    36
     slicing: bool,
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
    37
     timeout: Time.time,
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
    38
     expect: string}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    39
41090
b98fe4de1ecd renamings
blanchet
parents: 41089
diff changeset
    40
  datatype prover_fact =
b98fe4de1ecd renamings
blanchet
parents: 41089
diff changeset
    41
    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
    42
    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
    43
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    44
  type prover_problem =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    45
    {state: Proof.state,
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
    46
     goal: thm,
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
    47
     subgoal: int,
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
    48
     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
    49
     facts: prover_fact list,
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
    50
     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
    51
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    52
  type prover_result =
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    53
    {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
    54
     used_facts: (string * locality) list,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    55
     run_time_in_msecs: int option,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    56
     message: string}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    57
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    58
  type prover = params -> minimize_command -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
    59
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    60
  val smt_triggers : bool Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    61
  val smt_weights : bool Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    62
  val smt_weight_min_facts : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    63
  val smt_min_weight : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    64
  val smt_max_weight : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    65
  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
    66
  val smt_weight_curve : (int -> int) Unsynchronized.ref
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    67
  val smt_max_slices : int Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    68
  val smt_slice_fact_frac : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    69
  val smt_slice_time_frac : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    70
  val smt_slice_min_secs : int Config.T
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    71
  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
    72
  val select_smt_solver : string -> Proof.context -> Proof.context
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    73
  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
    74
  val is_unit_equational_atp : Proof.context -> string -> bool
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
    75
  val is_prover_supported : Proof.context -> string -> bool
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    76
  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
    77
  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
    78
  val is_unit_equality : term -> bool
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42944
diff changeset
    79
  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
    80
  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
    81
    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
    82
  val atp_relevance_fudge : relevance_fudge
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    83
  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
    84
  val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    85
  val dest_dir : string Config.T
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    86
  val problem_prefix : string Config.T
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
    87
  val measure_run_time : bool 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
    88
  val weight_smt_fact :
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    89
    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
    90
    -> (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
    91
  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
    92
  val smt_weighted_fact :
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    93
    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
    94
    -> (string * locality) * (int option * thm)
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
    95
  val supported_provers : Proof.context -> unit
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    96
  val kill_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    97
  val running_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    98
  val messages : int option -> unit
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
    99
  val get_prover : Proof.context -> bool -> string -> prover
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   100
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   101
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
   102
structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   103
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   104
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
   105
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39453
diff changeset
   106
open ATP_Proof
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
   107
open ATP_Systems
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39493
diff changeset
   108
open Metis_Translate
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   109
open Sledgehammer_Util
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
   110
open Sledgehammer_Filter
40068
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
   111
open Sledgehammer_ATP_Translate
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
   112
open Sledgehammer_ATP_Reconstruct
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
   113
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
   114
(** 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
   115
38102
019a49759829 fix bug in the newly introduced "bound concealing" code
blanchet
parents: 38100
diff changeset
   116
(* Identifier to distinguish Sledgehammer from other tools using
019a49759829 fix bug in the newly introduced "bound concealing" code
blanchet
parents: 38100
diff changeset
   117
   "Async_Manager". *)
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   118
val das_Tool = "Sledgehammer"
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   119
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
   120
val select_smt_solver =
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   121
  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
   122
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   123
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
   124
  member (op =) (SMT_Solver.available_solvers_of ctxt) name
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   125
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   126
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
   127
  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
   128
    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
   129
      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
   130
    | NONE => false
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   131
  end
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   132
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   133
fun is_prover_supported ctxt name =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   134
  let val thy = Proof_Context.theory_of ctxt in
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   135
    is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   136
  end
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   137
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   138
fun is_prover_installed ctxt =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   139
  is_smt_prover ctxt orf 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
   140
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   141
fun get_slices slicing slices =
42447
blanchet
parents: 42445
diff changeset
   142
  (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
   143
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   144
fun default_max_relevant_for_prover ctxt slicing name =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   145
  let val thy = Proof_Context.theory_of ctxt in
40982
d06ffd777f1f honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents: 40979
diff changeset
   146
    if is_smt_prover ctxt name then
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   147
      SMT_Solver.default_max_relevant ctxt name
40982
d06ffd777f1f honor the default max relevant facts setting from the SMT solvers in Sledgehammer
blanchet
parents: 40979
diff changeset
   148
    else
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   149
      fold (Integer.max o fst o snd o snd o snd)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   150
           (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   151
  end
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   152
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   153
(* These are either simplified away by "Meson.presimplify" (most of the time) or
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   154
   handled specially via "fFalse", "fTrue", ..., "fequal". *)
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
   155
val atp_irrelevant_consts =
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   156
  [@{const_name False}, @{const_name True}, @{const_name Not},
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   157
   @{const_name conj}, @{const_name disj}, @{const_name implies},
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   158
   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
40206
8819ffd60357 better list of irrelevant SMT constants
blanchet
parents: 40205
diff changeset
   159
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
   160
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
   161
  | 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
   162
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
   163
(* 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
   164
   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
   165
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
   166
  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
   167
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   168
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
   169
  | 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
   170
    is_unit_equality t
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   171
  | 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
   172
    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
   173
  | 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
   174
    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
   175
  | 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
   176
    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
   177
  | is_unit_equality _ = false
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   178
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42944
diff changeset
   179
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
   180
  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
   181
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
   182
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
   183
  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
   184
    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
   185
      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
   186
         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
   187
           (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
   188
         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
   189
           (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
   190
         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
   191
           (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
   192
    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
   193
  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
   194
    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
   195
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   196
(* FUDGE *)
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   197
val atp_relevance_fudge =
42738
2a9dcff63b80 remove unused parameter
blanchet
parents: 42737
diff changeset
   198
  {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
   199
   worse_irrel_freq = 100.0,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   200
   higher_order_irrel_weight = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   201
   abs_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   202
   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
   203
   skolem_irrel_weight = 0.25,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   204
   theory_const_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   205
   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
   206
   chained_const_irrel_weight = 0.25,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   207
   intro_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   208
   elim_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   209
   simp_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   210
   local_bonus = 0.55,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   211
   assum_bonus = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   212
   chained_bonus = 1.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   213
   max_imperfect = 11.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   214
   max_imperfect_exp = 1.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   215
   threshold_divisor = 2.0,
41093
dfbc8759415f lower fudge factor
blanchet
parents: 41091
diff changeset
   216
   ridiculous_threshold = 0.01}
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   217
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
   218
(* FUDGE (FIXME) *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   219
val smt_relevance_fudge =
42738
2a9dcff63b80 remove unused parameter
blanchet
parents: 42737
diff changeset
   220
  {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
   221
   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
   222
   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
   223
   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
   224
   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
   225
   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
   226
   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
   227
   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
   228
   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
   229
   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
   230
   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
   231
   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
   232
   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
   233
   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
   234
   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
   235
   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
   236
   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
   237
   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
   238
   ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   239
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   240
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
   241
  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
   242
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   243
fun supported_provers ctxt =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   244
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   245
    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
   246
    val (remote_provers, local_provers) =
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   247
      sort_strings (supported_atps thy) @
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   248
      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
   249
      |> List.partition (String.isPrefix remote_prefix)
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   250
  in
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   251
    Output.urgent_message ("Supported provers: " ^
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   252
                           commas (local_provers @ remote_provers) ^ ".")
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   253
  end
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   254
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   255
fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   256
fun running_provers () = Async_Manager.running_threads das_Tool "provers"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   257
val messages = Async_Manager.thread_messages das_Tool "prover"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   258
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   259
(** problems, results, ATPs, etc. **)
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   260
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   261
datatype rich_type_system =
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   262
  Dumb_Type_Sys of type_system |
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   263
  Smart_Type_Sys of bool
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   264
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   265
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
   266
  {debug: bool,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   267
   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
   268
   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
   269
   blocking: bool,
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   270
   provers: string list,
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   271
   type_sys: rich_type_system,
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 42100
diff changeset
   272
   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
   273
   max_relevant: int option,
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   274
   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
   275
   max_new_mono_instances: int,
36235
61159615a0c5 added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents: 36231
diff changeset
   276
   explicit_apply: bool,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   277
   isar_proof: bool,
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
   278
   isar_shrink_factor: int,
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   279
   slicing: bool,
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   280
   timeout: Time.time,
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   281
   expect: string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   282
41090
b98fe4de1ecd renamings
blanchet
parents: 41089
diff changeset
   283
datatype prover_fact =
b98fe4de1ecd renamings
blanchet
parents: 41089
diff changeset
   284
  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
   285
  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
   286
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   287
type prover_problem =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   288
  {state: Proof.state,
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   289
   goal: thm,
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   290
   subgoal: int,
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   291
   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
   292
   facts: prover_fact list,
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   293
   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
   294
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   295
type prover_result =
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   296
  {outcome: failure option,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   297
   message: string,
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
   298
   used_facts: (string * locality) list,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   299
   run_time_in_msecs: int option}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   300
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   301
type prover = params -> minimize_command -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   302
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   303
(* configuration attributes *)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   304
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   305
val dest_dir =
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   306
  Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
38991
0e2798f30087 rename sledgehammer config attributes
blanchet
parents: 38988
diff changeset
   307
  (* Empty string means create files in Isabelle's temporary files directory. *)
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   308
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   309
val problem_prefix =
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   310
  Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   311
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   312
val measure_run_time =
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42593
diff changeset
   313
  Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   314
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   315
fun with_path cleanup after f path =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   316
  Exn.capture f path
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   317
  |> tap (fn _ => cleanup path)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   318
  |> Exn.release
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   319
  |> tap (after path)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   320
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   321
fun proof_banner auto =
40224
7883fefd6a7b clear identification;
blanchet
parents: 40207
diff changeset
   322
  if auto then "Auto Sledgehammer found a proof" else "Try this command"
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   323
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   324
val smt_triggers =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   325
  Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   326
val smt_weights =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   327
  Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   328
val smt_weight_min_facts =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   329
  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
   330
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   331
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   332
val smt_min_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   333
  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   334
val smt_max_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   335
  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   336
val smt_max_weight_index =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   337
  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
   338
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
   339
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   340
fun smt_fact_weight ctxt j num_facts =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   341
  if Config.get ctxt smt_weights andalso
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   342
     num_facts >= Config.get ctxt smt_weight_min_facts then
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   343
    let
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   344
      val min = Config.get ctxt smt_min_weight
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   345
      val max = Config.get ctxt smt_max_weight
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   346
      val max_index = Config.get ctxt smt_max_weight_index
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   347
      val curve = !smt_weight_curve
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   348
    in
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   349
      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
   350
            div curve max_index)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   351
    end
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   352
  else
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   353
    NONE
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   354
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   355
fun weight_smt_fact ctxt num_facts ((info, th), j) =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   356
  let val thy = Proof_Context.theory_of ctxt in
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   357
    (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
   358
  end
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   359
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
   360
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
   361
  | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   362
fun atp_translated_fact ctxt format fact =
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   363
  translate_atp_fact ctxt format false (untranslated_fact fact)
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   364
fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   365
  | smt_weighted_fact ctxt num_facts (fact, j) =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   366
    (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
   367
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   368
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
   369
  (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
   370
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   371
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41242
diff changeset
   372
(* 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
   373
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
   374
(* 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
   375
   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
   376
   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
   377
   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
   378
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   379
(* 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
   380
   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
   381
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
   382
  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
   383
    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
   384
        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
   385
      | 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
   386
      | 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
   387
    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
   388
    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
   389
      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
   390
        (_, @{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
   391
      | (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
   392
        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
   393
      | (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
   394
        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
   395
      | (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
   396
        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
   397
      | (_, @{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
   398
        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
   399
        (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
   400
      | (_, @{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
   401
        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
   402
        (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
   403
      | (_, @{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
   404
      | (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
   405
      | (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
   406
      | (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
   407
      | (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
   408
      | _ => 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
   409
  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
   410
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   411
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
   412
  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
   413
                   | 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
   414
                   | _ => 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
   415
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   416
(* 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
   417
   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
   418
   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
   419
   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
   420
   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
   421
d6db5a815477 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
blanchet
parents: 42729
diff changeset
   422
(* 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
   423
   "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
   424
   are omitted. *)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   425
fun is_dangerous_prop ctxt =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   426
  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
   427
  #> (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
   428
      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
   429
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   430
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
   431
  | int_opt_add _ _ = NONE
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   432
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   433
val atp_blacklist_max_iters = 10
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   434
(* Important messages are important but not so important that users want to see
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   435
   them each time. *)
42609
b5e94b70bc06 fixed random number invocation
blanchet
parents: 42593
diff changeset
   436
val atp_important_message_keep_quotient = 10
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   437
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
   438
val fallback_best_type_systems =
42853
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42849
diff changeset
   439
  [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   440
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   441
fun adjust_dumb_type_sys formats (Simple_Types level) =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   442
    if member (op =) formats THF then
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   443
      (THF, Simple_Types level)
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   444
    else if member (op =) formats TFF then
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   445
      (TFF, Simple_Types level)
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   446
    else
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   447
      adjust_dumb_type_sys formats (Preds (Mangled_Monomorphic, level, Heavy))
42849
ba45312308b5 reintroduce TFF workaround for limitations of actual TFF implementations (ToFoF, SNARK)
blanchet
parents: 42837
diff changeset
   448
  | adjust_dumb_type_sys formats type_sys =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   449
    if member (op =) formats FOF then
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   450
      (FOF, type_sys)
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   451
    else if member (op =) formats CNF_UEQ then
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   452
      (CNF_UEQ, case type_sys of
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   453
                  Tags _ => type_sys
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   454
                | _ => Preds (polymorphism_of_type_sys type_sys,
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   455
                              Const_Arg_Types, Light))
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   456
    else
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   457
      (* We could return "type_sys" unchanged for TFF but this would require the
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   458
         TFF provers to accept problems in which constants are implicitly
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   459
         declared. Today neither SNARK nor ToFoF-E meet this criterion. *)
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   460
      (hd formats, Simple_Types All_Types)
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   461
fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   462
    adjust_dumb_type_sys formats type_sys
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   463
  | determine_format_and_type_sys best_type_systems formats
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42578
diff changeset
   464
                                  (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
   465
    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
   466
    |> find_first (if full_types then is_type_sys_virtually_sound else K true)
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
   467
    |> the |> adjust_dumb_type_sys formats
42548
ea2a28b1938f make sure the minimizer monomorphizes when it should
blanchet
parents: 42544
diff changeset
   468
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42738
diff changeset
   469
fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   470
  Config.put SMT_Config.verbose debug
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   471
  #> Config.put SMT_Config.monomorph_full false
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   472
  #> Config.put SMT_Config.monomorph_limit max_mono_iters
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42738
diff changeset
   473
  #> Config.put SMT_Config.monomorph_instances max_mono_instances
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   474
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
   475
fun run_atp auto name
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   476
        ({exec, required_execs, arguments, proof_delims, known_failures,
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   477
          conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   478
        ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42738
diff changeset
   479
          max_new_mono_instances, explicit_apply, isar_proof,
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42738
diff changeset
   480
          isar_shrink_factor, slicing, timeout, ...} : params)
40983
07526f546680 handle "max_relevant" uniformly
blanchet
parents: 40982
diff changeset
   481
        minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   482
  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
   483
    val thy = Proof.theory_of state
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   484
    val ctxt = Proof.context_of state
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   485
    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
41159
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41152
diff changeset
   486
    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
   487
      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
   488
      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
   489
    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
   490
      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
   491
                  "_" ^ 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
   492
    val problem_path_name =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   493
      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
   494
        File.tmp_path problem_file_name
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   495
      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
   496
        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
   497
      else
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   498
        error ("No such directory: " ^ quote dest_dir ^ ".")
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   499
    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
   500
    val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   501
    fun split_time s =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   502
      let
42448
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   503
        val split = String.tokens (fn c => str c = "\n")
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   504
        val (output, t) = s |> split |> split_last |> apfst cat_lines
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   505
        fun as_num f = f >> (fst o read_int)
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   506
        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   507
        val digit = Scan.one Symbol.is_ascii_digit
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   508
        val num3 = as_num (digit ::: digit ::: (digit >> single))
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   509
        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
   510
        val as_time = Scan.read Symbol.stopper time o raw_explode
42448
95b2626c75a8 tuning -- local semicolon consistency
blanchet
parents: 42447
diff changeset
   511
      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
   512
    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
   513
      case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   514
        (home_var, _) :: _ =>
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   515
        error ("The environment variable " ^ quote home_var ^ " is not set.")
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   516
      | [] =>
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   517
        if File.exists command then
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   518
          let
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   519
            (* 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
   520
               entire time available. *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   521
            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
   522
            val num_actual_slices = length actual_slices
42445
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   523
            fun monomorphize_facts facts =
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   524
              let
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   525
                val facts = facts |> map untranslated_fact
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   526
                (* pseudo-theorem involving the same constants as the subgoal *)
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   527
                val subgoal_th =
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   528
                  Logic.list_implies (hyp_ts, concl_t)
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   529
                  |> Skip_Proof.make_thm thy
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   530
                val indexed_facts =
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   531
                  (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42738
diff changeset
   532
                val max_mono_instances = max_new_mono_instances + length facts
42445
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   533
              in
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   534
                ctxt |> repair_smt_monomorph_context debug max_mono_iters
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42738
diff changeset
   535
                                                     max_mono_instances
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   536
                     |> SMT_Monomorph.monomorph indexed_facts
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   537
                     |> fst |> sort (int_ord o pairself fst)
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   538
                     |> filter_out (curry (op =) ~1 o fst)
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   539
                     |> map (Untranslated_Fact o apfst (fst o nth facts))
42445
c6ea64ebb8c5 fixed interaction between monomorphization and slicing for ATPs
blanchet
parents: 42444
diff changeset
   540
              end
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   541
            fun run_slice blacklist (slice, (time_frac, (complete,
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   542
                                       (best_max_relevant, best_type_systems))))
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   543
                          time_left =
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   544
              let
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   545
                val num_facts =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   546
                  length facts |> is_none max_relevant
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   547
                                  ? Integer.min best_max_relevant
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   548
                val (format, type_sys) =
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   549
                  determine_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
   550
                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
   551
                val facts =
42671
390de893659a fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a
blanchet
parents: 42647
diff changeset
   552
                  facts |> not fairly_sound
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   553
                           ? 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
   554
                                         o untranslated_fact)
a7a30721767a have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents: 42623
diff changeset
   555
                        |> take num_facts
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   556
                        |> not (null blacklist)
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   557
                           ? filter_out (member (op =) blacklist o fst
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   558
                                         o untranslated_fact)
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
   559
                        |> 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
   560
                           ? monomorphize_facts
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   561
                        |> map (atp_translated_fact ctxt format)
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   562
                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
   563
                val slice_timeout =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   564
                  ((real_ms time_left
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   565
                    |> (if slice < num_actual_slices - 1 then
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   566
                          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
   567
                        else
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   568
                          I))
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   569
                   * 0.001) |> seconds
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   570
                val _ =
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   571
                  if debug then
42699
d4f5fec71ded no lies in debug output (e.g. "slice 2 of 1")
blanchet
parents: 42684
diff changeset
   572
                    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
   573
                    " with " ^ string_of_int num_facts ^ " fact" ^
d4f5fec71ded no lies in debug output (e.g. "slice 2 of 1")
blanchet
parents: 42684
diff changeset
   574
                    plural_s num_facts ^ " for " ^
d4f5fec71ded no lies in debug output (e.g. "slice 2 of 1")
blanchet
parents: 42684
diff changeset
   575
                    string_from_time slice_timeout ^ "..."
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   576
                    |> Output.urgent_message
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   577
                  else
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   578
                    ()
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42523
diff changeset
   579
                val (atp_problem, pool, conjecture_offset, facts_offset,
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   580
                     fact_names, typed_helpers, sym_tab) =
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   581
                  prepare_atp_problem ctxt format conj_sym_kind prem_kind
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42937
diff changeset
   582
                      type_sys explicit_apply hyp_ts concl_t facts
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   583
                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
   584
                val core =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   585
                  File.shell_path command ^ " " ^
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   586
                  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
   587
                  File.shell_path prob_file
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   588
                val command =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   589
                  (if measure_run_time then
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   590
                     "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   591
                   else
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   592
                     "exec " ^ core) ^ " 2>&1"
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   593
                val _ =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   594
                  atp_problem
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42699
diff changeset
   595
                  |> tptp_strings_for_atp_problem format
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   596
                  |> cons ("% " ^ command ^ "\n")
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   597
                  |> File.write_list prob_file
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   598
                val conjecture_shape =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   599
                  conjecture_offset + 1
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   600
                    upto conjecture_offset + length hyp_ts + 1
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   601
                  |> map single
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   602
                val ((output, msecs), res_code) =
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   603
                  bash_output command
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   604
                  |>> (if overlord then
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   605
                         prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   606
                       else
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   607
                         I)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   608
                  |>> (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
   609
                val (atp_proof, outcome) =
42849
ba45312308b5 reintroduce TFF workaround for limitations of actual TFF implementations (ToFoF, SNARK)
blanchet
parents: 42837
diff changeset
   610
                  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
   611
                      proof_delims known_failures output
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42939
diff changeset
   612
                  |>> atp_proof_from_tstplike_proof atp_problem
42965
1403595ec38c slightly gracefuller handling of LEO-II and Satallax output
blanchet
parents: 42963
diff changeset
   613
                  handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   614
                val (conjecture_shape, facts_offset, fact_names,
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   615
                     typed_helpers) =
42449
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42448
diff changeset
   616
                  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
   617
                    repair_conjecture_shape_and_fact_names type_sys output
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   618
                        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
   619
                  else
42587
4fbb1de05169 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
blanchet
parents: 42579
diff changeset
   620
                    (* don't bother repairing *)
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   621
                    (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
   622
                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
   623
                  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
   624
                    NONE =>
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42965
diff changeset
   625
                    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
   626
                        conjecture_shape facts_offset fact_names atp_proof
e336ef6313aa more informative message when Sledgehammer finds an unsound proof
blanchet
parents: 42853
diff changeset
   627
                    |> Option.map (fn facts =>
e336ef6313aa more informative message when Sledgehammer finds an unsound proof
blanchet
parents: 42853
diff changeset
   628
                           UnsoundProof (is_type_sys_virtually_sound type_sys,
42943
62a14c80d194 fish out axioms in Waldmeister output
blanchet
parents: 42939
diff changeset
   629
                                         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
   630
                  | SOME Unprovable =>
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   631
                    if null blacklist then 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
   632
                    else SOME IncompleteUnprovable
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
   633
                  | _ => outcome
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   634
              in
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   635
                ((pool, conjecture_shape, facts_offset, fact_names,
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   636
                  typed_helpers, sym_tab),
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   637
                 (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
   638
              end
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   639
            val timer = Timer.startRealTimer ()
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   640
            fun maybe_run_slice blacklist slice
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   641
                                (result as (_, (_, msecs0, _, _, SOME _))) =
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   642
                let
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   643
                  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
   644
                in
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   645
                  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
   646
                    result
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   647
                  else
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   648
                    (run_slice blacklist slice time_left
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   649
                     |> (fn (stuff, (output, msecs, type_sys, atp_proof,
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   650
                                     outcome)) =>
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   651
                            (stuff, (output, int_opt_add msecs0 msecs, type_sys,
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   652
                                     atp_proof, outcome))))
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   653
                end
42450
2765d4fb2b9c automatically retry with full-types upon unsound proof
blanchet
parents: 42449
diff changeset
   654
              | 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
   655
            fun maybe_blacklist_facts_and_retry iter blacklist
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   656
                    (result as ((_, _, facts_offset, fact_names, _, _),
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   657
                                (_, _, type_sys, atp_proof,
42876
e336ef6313aa more informative message when Sledgehammer finds an unsound proof
blanchet
parents: 42853
diff changeset
   658
                                 SOME (UnsoundProof (false, _))))) =
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42965
diff changeset
   659
                (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
   660
                                              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
   661
                   [] => result
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   662
                 | new_baddies =>
42835
8d723194dedf run blacklist algorithm only if slicing is on
blanchet
parents: 42832
diff changeset
   663
                   if slicing andalso iter < atp_blacklist_max_iters - 1 then
42777
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   664
                     let val blacklist = new_baddies @ blacklist in
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   665
                       result
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   666
                       |> maybe_run_slice blacklist (List.last actual_slices)
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   667
                       |> maybe_blacklist_facts_and_retry (iter + 1) blacklist
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   668
                     end
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   669
                   else
69640564a394 fixed off-by-one bug
blanchet
parents: 42755
diff changeset
   670
                     result)
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   671
              | 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
   672
          in
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   673
            ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   674
             ("", SOME 0, hd fallback_best_type_systems, [],
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   675
              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
   676
            |> 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
   677
               (* 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
   678
                  without the offending facts! *)
42452
f7f796ce5d68 iterate the unsound-fact-set removal process to recover even more unsound proofs
blanchet
parents: 42451
diff changeset
   679
            |> maybe_blacklist_facts_and_retry 0 []
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   680
          end
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   681
        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
   682
          error ("Bad executable: " ^ Path.print command ^ ".")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   683
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   684
    (* If the problem file has not been exported, remove it; otherwise, export
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   685
       the proof file too. *)
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   686
    fun cleanup prob_file =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   687
      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
   688
    fun export prob_file (_, (output, _, _, _, _)) =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   689
      if dest_dir = "" then
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   690
        ()
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   691
      else
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41259
diff changeset
   692
        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
   693
    val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   694
          sym_tab),
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42722
diff changeset
   695
         (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
   696
      with_path cleanup export run_on problem_path_name
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   697
    val important_message =
42609
b5e94b70bc06 fixed random number invocation
blanchet
parents: 42593
diff changeset
   698
      if not auto andalso
b5e94b70bc06 fixed random number invocation
blanchet
parents: 42593
diff changeset
   699
         random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   700
        extract_important_message output
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   701
      else
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   702
        ""
41742
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   703
    fun append_to_message message =
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   704
      message ^
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   705
      (if verbose then
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   706
         "\nATP real CPU time: " ^
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   707
         string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   708
       else
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   709
         "") ^
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   710
      (if important_message <> "" then
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   711
         "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   712
       else
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   713
         "")
42755
4603154a3018 robustly detect how many type args were passed to the ATP, even if some of them were omitted
blanchet
parents: 42746
diff changeset
   714
    val isar_params =
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42965
diff changeset
   715
      (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
41742
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   716
    val metis_params =
42647
59142dbfa3ba no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter
blanchet
parents: 42646
diff changeset
   717
      (proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset,
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42876
diff changeset
   718
       fact_names, typed_helpers, goal, subgoal)
41742
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   719
    val (outcome, (message, used_facts)) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   720
      case outcome of
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   721
        NONE =>
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42965
diff changeset
   722
        (NONE, proof_text ctxt isar_proof isar_params metis_params
41742
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   723
               |>> append_to_message)
42882
391e41ac038b make sure the Vampire incomplete proof detection code kicks in
blanchet
parents: 42881
diff changeset
   724
      | SOME failure =>
391e41ac038b make sure the Vampire incomplete proof detection code kicks in
blanchet
parents: 42881
diff changeset
   725
        if failure = ProofMissing orelse failure = ProofIncomplete then
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42965
diff changeset
   726
          (NONE, metis_proof_text ctxt metis_params |>> append_to_message)
42882
391e41ac038b make sure the Vampire incomplete proof detection code kicks in
blanchet
parents: 42881
diff changeset
   727
        else
391e41ac038b make sure the Vampire incomplete proof detection code kicks in
blanchet
parents: 42881
diff changeset
   728
          (outcome, (string_for_failure failure, []))
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   729
  in
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
   730
    {outcome = outcome, message = message, used_facts = used_facts,
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   731
     run_time_in_msecs = msecs}
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   732
  end
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   733
40669
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   734
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
5c316d1327d4 more precise error handling for Z3;
blanchet
parents: 40668
diff changeset
   735
   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
   736
   ourselves. *)
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   737
val remote_smt_failures =
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   738
  [(22, CantConnect),
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   739
   (2, NoLibwwwPerl)]
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   740
val z3_wrapper_failures =
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   741
  [(10, NoRealZ3),
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   742
   (11, InternalError),
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   743
   (12, InternalError),
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   744
   (13, InternalError)]
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   745
val z3_failures =
41236
def0a3013554 trap one more Z3 error
blanchet
parents: 41222
diff changeset
   746
  [(101, OutOfResources),
def0a3013554 trap one more Z3 error
blanchet
parents: 41222
diff changeset
   747
   (103, MalformedInput),
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   748
   (110, MalformedInput)]
40684
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   749
val unix_failures =
c7ba327eb58c more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
blanchet
parents: 40669
diff changeset
   750
  [(139, Crashed)]
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   751
val smt_failures =
41799
98b3d5ce0935 exit code 127 can mean many things -- not just (and probably not) Perl missing
blanchet
parents: 41790
diff changeset
   752
  remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
40555
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   753
42100
062381c5f9f8 more precise failure reporting in Sledgehammer/SMT
blanchet
parents: 42061
diff changeset
   754
fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
062381c5f9f8 more precise failure reporting in Sledgehammer/SMT
blanchet
parents: 42061
diff changeset
   755
    if is_real_cex then Unprovable else IncompleteUnprovable
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   756
  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   757
  | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   758
    (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
   759
       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
   760
     | 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
   761
                             string_of_int code ^ "."))
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   762
  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   763
  | 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
   764
    UnknownError msg
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   765
40698
8a3f7ea91370 cosmetics
blanchet
parents: 40693
diff changeset
   766
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   767
val smt_max_slices =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   768
  Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   769
val smt_slice_fact_frac =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   770
  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
   771
val smt_slice_time_frac =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   772
  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
   773
val smt_slice_min_secs =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   774
  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
   775
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   776
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
   777
                    ({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
   778
                      max_new_mono_instances, timeout, slicing, ...} : params)
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   779
                    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
   780
  let
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   781
    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
   782
    val repair_context =
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   783
          select_smt_solver name
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   784
          #> (if overlord then
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   785
                Config.put SMT_Config.debug_files
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   786
                           (overlord_file_location_for_prover name
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   787
                            |> (fn (path, name) => path ^ "/" ^ name))
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   788
              else
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   789
                I)
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   790
          #> 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
   791
    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
   792
    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
   793
      let
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   794
        val timer = Timer.startRealTimer ()
42724
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   795
        val state =
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   796
          state |> Proof.map_context
4d6bcf846759 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
blanchet
parents: 42723
diff changeset
   797
                       (repair_smt_monomorph_context debug max_mono_iters
42740
31334a7b109d renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
blanchet
parents: 42738
diff changeset
   798
                            (max_new_mono_instances + length facts))
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   799
        val ms = timeout |> Time.toMilliseconds
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   800
        val slice_timeout =
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   801
          if slice < max_slices then
41169
95167879f675 clean up fudge factors a little bit
blanchet
parents: 41168
diff changeset
   802
            Int.min (ms,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   803
                Int.max (1000 * Config.get ctxt smt_slice_min_secs,
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   804
                    Real.ceil (Config.get ctxt smt_slice_time_frac
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   805
                               * Real.fromInt ms)))
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   806
            |> Time.fromMilliseconds
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   807
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   808
            timeout
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   809
        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
   810
        val _ =
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   811
          if debug then
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   812
            quote name ^ " slice " ^ string_of_int slice ^ " with " ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   813
            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
   814
            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
   815
            |> Output.urgent_message
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   816
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   817
            ()
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   818
        val birth = Timer.checkRealTimer timer
41171
043f8dc3b51f facilitate debugging
blanchet
parents: 41169
diff changeset
   819
        val _ =
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41209
diff changeset
   820
          if debug then Output.urgent_message "Invoking SMT solver..." else ()
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
   821
        val (outcome, used_facts) =
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   822
          (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
   823
             (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
   824
           | _ => 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
   825
          |> SMT_Solver.smt_filter_apply slice_timeout
41239
d6e804ff29c3 split "smt_filter" into head and tail
blanchet
parents: 41236
diff changeset
   826
          |> (fn {outcome, used_facts} => (outcome, used_facts))
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
   827
          handle exn => if Exn.is_interrupt exn then
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
   828
                          reraise exn
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
   829
                        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
   830
                          (ML_Compiler.exn_message exn
41209
91fab0d3553b robustly handle SMT exceptions in Sledgehammer
blanchet
parents: 41208
diff changeset
   831
                           |> SMT_Failure.Other_Failure |> SOME, [])
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   832
        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
   833
        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   834
        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
   835
        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
   836
          case outcome of
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   837
            NONE => false
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   838
          | SOME (SMT_Failure.Counterexample _) => false
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   839
          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   840
          | 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
   841
          | 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
   842
          | 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
   843
        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
   844
      in
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   845
        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
   846
           num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
41169
95167879f675 clean up fudge factors a little bit
blanchet
parents: 41168
diff changeset
   847
          let
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   848
            val new_num_facts =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   849
              Real.ceil (Config.get ctxt smt_slice_fact_frac
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   850
                         * Real.fromInt num_facts)
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   851
            val _ =
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   852
              if verbose andalso is_some outcome then
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   853
                quote name ^ " invoked with " ^ string_of_int num_facts ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   854
                " fact" ^ plural_s num_facts ^ ": " ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   855
                string_for_failure (failure_from_smt_failure (the outcome)) ^
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   856
                " 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
   857
                plural_s new_num_facts ^ "..."
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   858
                |> Output.urgent_message
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   859
              else
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   860
                ()
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   861
          in
42614
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   862
            facts |> take new_num_facts
81953e554197 make "debug" more verbose and "verbose" less verbose
blanchet
parents: 42613
diff changeset
   863
                  |> 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
   864
          end
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   865
        else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   866
          {outcome = if is_none outcome then NONE else the outcome0,
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   867
           used_facts = used_facts,
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   868
           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
   869
      end
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   870
  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
   871
40666
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   872
(* taken from "Mirabelle" and generalized *)
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   873
fun can_apply timeout tac state i =
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   874
  let
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   875
    val {context = ctxt, facts, goal} = Proof.goal state
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   876
    val full_tac = Method.insert_tac facts i THEN tac ctxt i
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   877
  in
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   878
    case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   879
      SOME (SOME _) => true
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   880
    | _ => false
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   881
  end
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   882
41152
4a7410be4dfc crank up Metis's timeout for SMT solvers, since users love Metis
blanchet
parents: 41151
diff changeset
   883
val smt_metis_timeout = seconds 1.0
40666
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   884
40693
a4171afcc3c4 set Metis option on correct context, lest it be ignored
blanchet
parents: 40692
diff changeset
   885
fun can_apply_metis debug state i ths =
a4171afcc3c4 set Metis option on correct context, lest it be ignored
blanchet
parents: 40692
diff changeset
   886
  can_apply smt_metis_timeout
a4171afcc3c4 set Metis option on correct context, lest it be ignored
blanchet
parents: 40692
diff changeset
   887
            (Config.put Metis_Tactics.verbose debug
a4171afcc3c4 set Metis option on correct context, lest it be ignored
blanchet
parents: 40692
diff changeset
   888
             #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
40666
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   889
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
   890
fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   891
                   ({state, subgoal, subgoal_count, facts, smt_filter, ...}
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   892
                    : 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
   893
  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
   894
    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
   895
    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
   896
    val facts = facts ~~ (0 upto num_facts - 1)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   897
                |> map (smt_weighted_fact ctxt num_facts)
40181
3788b7adab36 integrated "smt" proof method with Sledgehammer
blanchet
parents: 40132
diff changeset
   898
    val {outcome, used_facts, run_time_in_msecs} =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   899
      smt_filter_loop ctxt name params state subgoal smt_filter facts
40723
a82badd0e6ef put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents: 40701
diff changeset
   900
    val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
41222
f9783376d9b1 more precise/correct SMT error handling
blanchet
parents: 41220
diff changeset
   901
    val outcome = outcome |> Option.map failure_from_smt_failure
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   902
    val message =
40184
91b4b73dbafb proper error handling for SMT solvers in Sledgehammer
blanchet
parents: 40181
diff changeset
   903
      case outcome of
91b4b73dbafb proper error handling for SMT solvers in Sledgehammer
blanchet
parents: 40181
diff changeset
   904
        NONE =>
40666
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   905
        let
41151
d58157bb1ae7 generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents: 41140
diff changeset
   906
          val (method, settings) =
40693
a4171afcc3c4 set Metis option on correct context, lest it be ignored
blanchet
parents: 40692
diff changeset
   907
            if can_apply_metis debug state subgoal (map snd used_facts) then
41151
d58157bb1ae7 generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents: 41140
diff changeset
   908
              ("metis", "")
40693
a4171afcc3c4 set Metis option on correct context, lest it be ignored
blanchet
parents: 40692
diff changeset
   909
            else
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   910
              ("smt", if name = SMT_Solver.solver_name_of ctxt then ""
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41336
diff changeset
   911
                      else "smt_solver = " ^ maybe_quote name)
40666
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   912
        in
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   913
          try_command_line (proof_banner auto)
41151
d58157bb1ae7 generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents: 41140
diff changeset
   914
              (apply_on_subgoal settings subgoal subgoal_count ^
d58157bb1ae7 generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents: 41140
diff changeset
   915
               command_call method (map fst other_lemmas)) ^
40723
a82badd0e6ef put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents: 40701
diff changeset
   916
          minimize_line minimize_command
41168
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   917
                        (map fst (other_lemmas @ chained_lemmas)) ^
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   918
          (if verbose then
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   919
             "\nSMT solver real CPU time: " ^
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   920
             string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   921
             "."
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   922
           else
f6f1ffd51d87 added weights to SMT problems
blanchet
parents: 41159
diff changeset
   923
             "")
40666
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   924
        end
41744
a18e7bbca258 make minimizer verbose
blanchet
parents: 41742
diff changeset
   925
      | SOME failure => string_for_failure failure
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   926
  in
40666
8db6c2b1591d try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents: 40627
diff changeset
   927
    {outcome = outcome, used_facts = map fst used_facts,
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
   928
     run_time_in_msecs = run_time_in_msecs, message = message}
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   929
  end
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   930
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
   931
fun get_prover ctxt auto name =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42193
diff changeset
   932
  let val thy = Proof_Context.theory_of ctxt in
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   933
    if is_smt_prover ctxt name then
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
   934
      run_smt_solver auto name
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41723
diff changeset
   935
    else if member (op =) (supported_atps thy) name then
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
   936
      run_atp auto name (get_atp thy name)
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   937
    else
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   938
      error ("No such prover: " ^ name ^ ".")
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   939
  end
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   940
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   941
end;