src/HOL/Tools/Sledgehammer/sledgehammer.ML
author blanchet
Mon, 15 Nov 2010 18:58:30 +0100
changeset 40556 d66403b60b3b
parent 40555 de581d7da0b6
child 40558 e75614d0a859
permissions -rw-r--r--
cosmetics
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38021
e024504943d1 rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents: 38020
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer.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
38021
e024504943d1 rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents: 38020
diff changeset
     6
Sledgehammer's heart.
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
38021
e024504943d1 rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents: 38020
diff changeset
     9
signature SLEDGEHAMMER =
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
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    14
  type relevance_override = Sledgehammer_Filter.relevance_override
40114
blanchet
parents: 40072
diff changeset
    15
  type translated_formula = Sledgehammer_ATP_Translate.translated_formula
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
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    18
  type params =
38982
820b8221ed48 added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents: 38893
diff changeset
    19
    {blocking: bool,
820b8221ed48 added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents: 38893
diff changeset
    20
     debug: bool,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    21
     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
    22
     overlord: bool,
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    23
     provers: string list,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    24
     full_types: bool,
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
    25
     explicit_apply: bool,
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
    26
     relevance_thresholds: real * real,
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38741
diff changeset
    27
     max_relevant: int option,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    28
     isar_proof: bool,
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
    29
     isar_shrink_factor: int,
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
    30
     timeout: Time.time,
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
    31
     expect: string}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    32
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
    33
  datatype fact =
40114
blanchet
parents: 40072
diff changeset
    34
    Untranslated of (string * locality) * thm |
blanchet
parents: 40072
diff changeset
    35
    Translated of term * ((string * locality) * translated_formula) option
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    36
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    37
  type prover_problem =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    38
    {state: Proof.state,
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
    39
     goal: thm,
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
    40
     subgoal: int,
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
    41
     subgoal_count: int,
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
    42
     facts: fact list,
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
    43
     only: bool}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    44
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    45
  type prover_result =
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    46
    {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
    47
     used_facts: (string * locality) list,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    48
     run_time_in_msecs: int option,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    49
     message: string}
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
    50
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    51
  type prover = params -> minimize_command -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
    52
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
    53
  val smtN : string
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    54
  val is_prover_available : theory -> string -> bool
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    55
  val is_prover_installed : Proof.context -> string -> bool
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
    56
  val default_max_relevant_for_prover : theory -> string -> int
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
    57
  val is_built_in_const_for_prover :
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
    58
    Proof.context -> string -> string * typ -> bool
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
    59
  val relevance_fudge_for_prover : string -> relevance_fudge
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    60
  val dest_dir : string Config.T
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    61
  val problem_prefix : string Config.T
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
    62
  val measure_run_time : bool Config.T
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    63
  val available_provers : theory -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    64
  val kill_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    65
  val running_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    66
  val messages : int option -> unit
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
    67
  val get_prover : theory -> bool -> string -> prover
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
    68
  val run_sledgehammer :
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    69
    params -> bool -> int -> relevance_override -> (string -> minimize_command)
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    70
    -> Proof.state -> bool * Proof.state
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    71
  val setup : theory -> theory
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    72
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    73
38021
e024504943d1 rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents: 38020
diff changeset
    74
structure Sledgehammer : SLEDGEHAMMER =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    75
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    76
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
    77
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39453
diff changeset
    78
open ATP_Proof
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
    79
open ATP_Systems
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39493
diff changeset
    80
open Metis_Translate
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    81
open Sledgehammer_Util
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    82
open Sledgehammer_Filter
40068
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
    83
open Sledgehammer_ATP_Translate
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
    84
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
    85
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    86
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
    87
(** 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
    88
38102
019a49759829 fix bug in the newly introduced "bound concealing" code
blanchet
parents: 38100
diff changeset
    89
(* Identifier to distinguish Sledgehammer from other tools using
019a49759829 fix bug in the newly introduced "bound concealing" code
blanchet
parents: 38100
diff changeset
    90
   "Async_Manager". *)
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    91
val das_Tool = "Sledgehammer"
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    92
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
    93
val smtN = "smt"
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    94
val smt_prover_names = [smtN, remote_prefix ^ smtN]
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    95
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
    96
val is_smt_prover = member (op =) smt_prover_names
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
    97
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    98
fun is_prover_available thy name =
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    99
  is_smt_prover name orelse member (op =) (available_atps thy) name
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   100
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   101
fun is_prover_installed ctxt name =
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   102
  let val thy = ProofContext.theory_of ctxt in
40181
3788b7adab36 integrated "smt" proof method with Sledgehammer
blanchet
parents: 40132
diff changeset
   103
    if is_smt_prover name then SMT_Solver.is_locally_installed ctxt
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   104
    else is_atp_installed thy name
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   105
  end
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   106
40419
718b44dbd74d make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
blanchet
parents: 40417
diff changeset
   107
val smt_default_max_relevant = 200 (* FUDGE *)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   108
val auto_max_relevant_divisor = 2 (* FUDGE *)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   109
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   110
fun default_max_relevant_for_prover thy name =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   111
  if is_smt_prover name then smt_default_max_relevant
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   112
  else #default_max_relevant (get_atp thy name)
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   113
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
   114
(* These are typically simplified away by "Meson.presimplify". Equality is
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
   115
   handled specially via "fequal". *)
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
   116
val atp_irrelevant_consts =
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
   117
  [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
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
   118
   @{const_name HOL.eq}]
40206
8819ffd60357 better list of irrelevant SMT constants
blanchet
parents: 40205
diff changeset
   119
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   120
fun is_built_in_const_for_prover ctxt name (s, T) =
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   121
  if is_smt_prover name then SMT_Builtin.is_builtin ctxt (s, T)
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   122
  else member (op =) atp_irrelevant_consts s
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
   123
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   124
(* FUDGE *)
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   125
val atp_relevance_fudge =
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   126
  {worse_irrel_freq = 100.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   127
   higher_order_irrel_weight = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   128
   abs_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   129
   abs_irrel_weight = 2.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   130
   skolem_irrel_weight = 0.75,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   131
   theory_const_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   132
   theory_const_irrel_weight = 0.25,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   133
   intro_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   134
   elim_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   135
   simp_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   136
   local_bonus = 0.55,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   137
   assum_bonus = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   138
   chained_bonus = 1.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   139
   max_imperfect = 11.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   140
   max_imperfect_exp = 1.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   141
   threshold_divisor = 2.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   142
   ridiculous_threshold = 0.1}
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   143
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
   144
(* FUDGE (FIXME) *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   145
val smt_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
   146
  {worse_irrel_freq = #worse_irrel_freq 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
   147
   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
   148
   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
   149
   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
   150
   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
   151
   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
   152
   theory_const_irrel_weight = #theory_const_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
   153
   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
   154
   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
   155
   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
   156
   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
   157
   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
   158
   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
   159
   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
   160
   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
   161
   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
   162
   ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   163
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   164
fun relevance_fudge_for_prover name =
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   165
  if is_smt_prover name then smt_relevance_fudge else atp_relevance_fudge
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   166
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   167
fun available_provers thy =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   168
  let
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   169
    val (remote_provers, local_provers) =
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   170
      sort_strings (available_atps thy) @ smt_prover_names
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   171
      |> List.partition (String.isPrefix remote_prefix)
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   172
  in
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   173
    Output.urgent_message ("Available provers: " ^
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   174
                           commas (local_provers @ remote_provers) ^ ".")
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   175
  end
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   176
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   177
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
   178
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
   179
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
   180
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   181
(** problems, results, ATPs, etc. **)
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   182
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   183
type params =
38982
820b8221ed48 added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents: 38893
diff changeset
   184
  {blocking: bool,
820b8221ed48 added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents: 38893
diff changeset
   185
   debug: bool,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   186
   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
   187
   overlord: bool,
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   188
   provers: string list,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   189
   full_types: bool,
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
   190
   explicit_apply: bool,
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   191
   relevance_thresholds: real * real,
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38741
diff changeset
   192
   max_relevant: int option,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   193
   isar_proof: bool,
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
   194
   isar_shrink_factor: int,
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   195
   timeout: Time.time,
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   196
   expect: string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   197
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
   198
datatype fact =
40114
blanchet
parents: 40072
diff changeset
   199
  Untranslated of (string * locality) * thm |
blanchet
parents: 40072
diff changeset
   200
  Translated of term * ((string * locality) * translated_formula) option
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   201
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   202
type prover_problem =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   203
  {state: Proof.state,
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   204
   goal: thm,
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   205
   subgoal: int,
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   206
   subgoal_count: int,
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
   207
   facts: fact list,
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
   208
   only: bool}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   209
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   210
type prover_result =
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   211
  {outcome: failure option,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   212
   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
   213
   used_facts: (string * locality) list,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   214
   run_time_in_msecs: int option}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   215
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   216
type prover = params -> minimize_command -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   217
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   218
(* configuration attributes *)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   219
38991
0e2798f30087 rename sledgehammer config attributes
blanchet
parents: 38988
diff changeset
   220
val (dest_dir, dest_dir_setup) =
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   221
  Attrib.config_string "sledgehammer_dest_dir" (K "")
38991
0e2798f30087 rename sledgehammer config attributes
blanchet
parents: 38988
diff changeset
   222
  (* Empty string means create files in Isabelle's temporary files directory. *)
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   223
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   224
val (problem_prefix, problem_prefix_setup) =
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   225
  Attrib.config_string "sledgehammer_problem_prefix" (K "prob")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   226
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   227
val (measure_run_time, measure_run_time_setup) =
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   228
  Attrib.config_bool "sledgehammer_measure_run_time" (K false)
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   229
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   230
fun with_path cleanup after f path =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   231
  Exn.capture f path
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   232
  |> tap (fn _ => cleanup path)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   233
  |> Exn.release
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   234
  |> tap (after path)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   235
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
   236
fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
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
   237
                       n goal =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   238
  quote name ^
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   239
  (if verbose then
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
   240
     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   241
   else
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   242
     "") ^
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   243
  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   244
  (if blocking then
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   245
     ""
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   246
   else
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   247
     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   248
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   249
fun proof_banner auto =
40224
7883fefd6a7b clear identification;
blanchet
parents: 40207
diff changeset
   250
  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
   251
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   252
(* generic TPTP-based ATPs *)
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   253
40114
blanchet
parents: 40072
diff changeset
   254
fun dest_Untranslated (Untranslated p) = p
blanchet
parents: 40072
diff changeset
   255
  | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
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
   256
fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p
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
   257
  | translated_fact _ (Translated p) = p
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   258
fun fact_name (Untranslated ((name, _), _)) = SOME name
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   259
  | fact_name (Translated (_, p)) = Option.map (fst o fst) p
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   260
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   261
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
   262
  | int_opt_add _ _ = NONE
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   263
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   264
(* Important messages are important but not so important that users want to see
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   265
   them each time. *)
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
   266
val important_message_keep_factor = 0.1
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   267
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   268
fun run_atp auto atp_name
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   269
        {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
38997
78ac4468cf9d got rid of the "theory_relevant" option;
blanchet
parents: 38991
diff changeset
   270
         known_failures, default_max_relevant, explicit_forall,
78ac4468cf9d got rid of the "theory_relevant" option;
blanchet
parents: 38991
diff changeset
   271
         use_conjecture_for_hypotheses}
38455
131f7c46cf2c more debug output
blanchet
parents: 38290
diff changeset
   272
        ({debug, verbose, overlord, full_types, explicit_apply,
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   273
          max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   274
        minimize_command
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
   275
        ({state, goal, subgoal, facts, only, ...} : prover_problem) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   276
  let
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   277
    val ctxt = Proof.context_of state
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   278
    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
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
   279
    val facts =
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
   280
      facts |> not only ? take (the_default default_max_relevant max_relevant)
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
   281
            |> map (translated_fact ctxt)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   282
    val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   283
                   else Config.get ctxt dest_dir
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   284
    val problem_prefix = 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
   285
    val problem_file_name =
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   286
      Path.basic ((if overlord then "prob_" ^ atp_name
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   287
                   else problem_prefix ^ serial_string ())
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   288
                  ^ "_" ^ 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
   289
    val problem_path_name =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   290
      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
   291
        File.tmp_path problem_file_name
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   292
      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
   293
        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
   294
      else
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   295
        error ("No such directory: " ^ quote dest_dir ^ ".")
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   296
    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
   297
    val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   298
    (* write out problem file and call ATP *)
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   299
    fun command_line complete timeout probfile =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   300
      let
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   301
        val core = File.shell_path command ^ " " ^ arguments complete timeout ^
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   302
                   " " ^ File.shell_path probfile
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   303
      in
39010
344028ecc00e show real CPU time
blanchet
parents: 39009
diff changeset
   304
        (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38741
diff changeset
   305
         else "exec " ^ core) ^ " 2>&1"
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   306
      end
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   307
    fun split_time s =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   308
      let
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   309
        val split = String.tokens (fn c => str c = "\n");
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   310
        val (output, t) = s |> split |> split_last |> apfst cat_lines;
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   311
        fun as_num f = f >> (fst o read_int);
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   312
        val num = as_num (Scan.many1 Symbol.is_ascii_digit);
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   313
        val digit = Scan.one Symbol.is_ascii_digit;
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   314
        val num3 = as_num (digit ::: digit ::: (digit >> single));
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   315
        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   316
        val as_time = Scan.read Symbol.stopper time o explode
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   317
      in (output, as_time t) end;
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   318
    fun run_on probfile =
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
   319
      case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   320
        (home_var, _) :: _ =>
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   321
        error ("The environment variable " ^ quote home_var ^ " is not set.")
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   322
      | [] =>
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   323
        if File.exists command then
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   324
          let
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   325
            fun run complete timeout =
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   326
              let
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   327
                val command = command_line complete timeout probfile
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   328
                val ((output, msecs), res_code) =
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   329
                  bash_output command
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   330
                  |>> (if overlord then
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   331
                         prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   332
                       else
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   333
                         I)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   334
                  |>> (if measure_run_time then split_time else rpair NONE)
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   335
                val (tstplike_proof, outcome) =
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   336
                  extract_tstplike_proof_and_outcome complete res_code
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   337
                      proof_delims known_failures output
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   338
              in (output, msecs, tstplike_proof, outcome) end
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   339
            val readable_names = debug andalso overlord
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
   340
            val (atp_problem, pool, conjecture_offset, fact_names) =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   341
              prepare_atp_problem ctxt readable_names explicit_forall full_types
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
   342
                                  explicit_apply hyp_ts concl_t facts
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   343
            val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   344
                                                  atp_problem
38631
979a0b37f981 prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents: 38600
diff changeset
   345
            val _ = File.write_list probfile ss
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   346
            val conjecture_shape =
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   347
              conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
38040
174568533593 fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents: 38039
diff changeset
   348
              |> map single
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   349
            val run_twice = has_incomplete_mode andalso not auto
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   350
            val timer = Timer.startRealTimer ()
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   351
            val result =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   352
              run false (if run_twice then
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   353
                           Time.fromMilliseconds
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   354
                                         (2 * Time.toMilliseconds timeout div 3)
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   355
                         else
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   356
                           timeout)
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   357
              |> run_twice
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   358
                 ? (fn (_, msecs0, _, SOME _) =>
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   359
                       run true (Time.- (timeout, Timer.checkRealTimer timer))
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   360
                       |> (fn (output, msecs, tstplike_proof, outcome) =>
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   361
                              (output, int_opt_add msecs0 msecs, tstplike_proof,
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   362
                               outcome))
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   363
                     | result => result)
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
   364
          in ((pool, conjecture_shape, fact_names), result) end
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   365
        else
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   366
          error ("Bad executable: " ^ Path.implode command ^ ".")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   367
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   368
    (* If the problem file has not been exported, remove it; otherwise, export
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   369
       the proof file too. *)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   370
    fun cleanup probfile =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   371
      if dest_dir = "" then try File.rm probfile else NONE
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   372
    fun export probfile (_, (output, _, _, _)) =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   373
      if dest_dir = "" then
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   374
        ()
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   375
      else
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   376
        File.write (Path.explode (Path.implode probfile ^ "_proof")) output
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
   377
    val ((pool, conjecture_shape, fact_names),
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   378
         (output, msecs, tstplike_proof, outcome)) =
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   379
      with_path cleanup export run_on problem_path_name
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
   380
    val (conjecture_shape, fact_names) =
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
   381
      repair_conjecture_shape_and_fact_names output conjecture_shape fact_names
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   382
    val important_message =
40224
7883fefd6a7b clear identification;
blanchet
parents: 40207
diff changeset
   383
      if not auto andalso random () <= important_message_keep_factor then
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   384
        extract_important_message output
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   385
      else
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   386
        ""
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
   387
    val (message, used_facts) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   388
      case outcome of
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   389
        NONE =>
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   390
        proof_text isar_proof
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   391
            (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   392
            (proof_banner auto, full_types, minimize_command, tstplike_proof,
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
   393
             fact_names, goal, subgoal)
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38741
diff changeset
   394
        |>> (fn message =>
40341
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40224
diff changeset
   395
                message ^
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40224
diff changeset
   396
                (if verbose then
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40224
diff changeset
   397
                   "\nATP real CPU time: " ^
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40224
diff changeset
   398
                   string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40224
diff changeset
   399
                 else
03156257040f standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents: 40224
diff changeset
   400
                   "") ^
39107
0a62f8a94af3 If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents: 39010
diff changeset
   401
                (if important_message <> "" then
0a62f8a94af3 If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents: 39010
diff changeset
   402
                   "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
0a62f8a94af3 If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents: 39010
diff changeset
   403
                   important_message
0a62f8a94af3 If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents: 39010
diff changeset
   404
                 else
0a62f8a94af3 If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents: 39010
diff changeset
   405
                   ""))
38597
db482afec7f0 no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents: 38590
diff changeset
   406
      | SOME failure => (string_for_failure failure, [])
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   407
  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
   408
    {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
   409
     run_time_in_msecs = msecs}
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   410
  end
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   411
40555
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   412
(* "SMT_Failure.Solver_Crashed" is a misnomer; it should really be called
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   413
   "Abnormal_Termination". Return codes 1 to 127 are application-specific,
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   414
   whereas (at least on Unix) 128 to 255 are reserved for signals (e.g.,
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   415
   SIGSEGV) and other system codes. *)
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   416
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40419
diff changeset
   417
fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40419
diff changeset
   418
  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
40555
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   419
  | failure_from_smt_failure (SMT_Failure.Solver_Crashed code) =
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   420
    if code >= 128 then Crashed else IncompleteUnprovable
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40419
diff changeset
   421
  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
40207
5da3e8ede850 adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
blanchet
parents: 40206
diff changeset
   422
  | failure_from_smt_failure _ = UnknownError
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   423
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   424
val smt_max_iter = 8
40419
718b44dbd74d make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
blanchet
parents: 40417
diff changeset
   425
val smt_iter_fact_divisor = 2
718b44dbd74d make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
blanchet
parents: 40417
diff changeset
   426
val smt_iter_min_msecs = 5000
718b44dbd74d make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
blanchet
parents: 40417
diff changeset
   427
val smt_iter_timeout_divisor = 2
40439
fb6ee11e776a reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents: 40428
diff changeset
   428
val smt_monomorph_limit = 4
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   429
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   430
fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i =
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   431
  let
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   432
    val ctxt = Proof.context_of state
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   433
    fun iter timeout iter_num outcome0 msecs_so_far facts =
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   434
      let
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   435
        val timer = Timer.startRealTimer ()
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   436
        val ms = timeout |> Time.toMilliseconds
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   437
        val iter_timeout =
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   438
          if iter_num < smt_max_iter then
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   439
            Int.min (ms, Int.max (smt_iter_min_msecs,
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   440
                                  ms div smt_iter_timeout_divisor))
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   441
            |> Time.fromMilliseconds
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   442
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   443
            timeout
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   444
        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
   445
        val _ =
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   446
          if verbose then
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   447
            "SMT iteration with " ^ string_of_int num_facts ^ " fact" ^
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   448
            plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   449
            "..."
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   450
            |> Output.urgent_message
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   451
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   452
            ()
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   453
        val {outcome, used_facts, run_time_in_msecs} =
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   454
          TimeLimit.timeLimit iter_timeout
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   455
              (SMT_Solver.smt_filter remote iter_timeout state facts) i
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   456
          handle TimeLimit.TimeOut =>
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   457
                 {outcome = SOME SMT_Failure.Time_Out, used_facts = [],
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   458
                  run_time_in_msecs = NONE}
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   459
        val _ =
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   460
          if verbose andalso is_some outcome then
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   461
            "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   462
            |> Output.urgent_message
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   463
          else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   464
            ()
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   465
        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   466
        val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   467
        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
   468
          case outcome of
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   469
            NONE => false
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   470
          | SOME (SMT_Failure.Counterexample _) => false
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   471
          | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
40555
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   472
          | SOME (SMT_Failure.Solver_Crashed code) =>
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   473
            (if verbose then
40555
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   474
               "The SMT solver invoked with " ^ string_of_int num_facts ^
de581d7da0b6 interpret SMT_Failure.Solver_Crashed correctly
blanchet
parents: 40553
diff changeset
   475
               " fact" ^ plural_s num_facts ^ " terminated abnormally with \
40556
d66403b60b3b cosmetics
blanchet
parents: 40555
diff changeset
   476
               \exit code " ^ string_of_int code ^ "."
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   477
               |> (if debug then error else warning)
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   478
             else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   479
               ();
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   480
             true (* kind of *))
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   481
          | SOME SMT_Failure.Out_Of_Memory => true
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   482
          | SOME _ => true
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   483
        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
   484
      in
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   485
        if too_many_facts_perhaps andalso iter_num < smt_max_iter andalso
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   486
           num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   487
          let val facts = take (num_facts div smt_iter_fact_divisor) facts in
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   488
            iter timeout (iter_num + 1) outcome0 msecs_so_far facts
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   489
          end
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   490
        else
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   491
          {outcome = if is_none outcome then NONE else the outcome0,
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   492
           used_facts = used_facts, run_time_in_msecs = msecs_so_far}
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   493
      end
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   494
  in iter timeout 1 NONE (SOME 0) end
40409
3642dc3b72e8 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet
parents: 40370
diff changeset
   495
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   496
fun run_smt_solver auto remote (params as {debug, ...}) minimize_command
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   497
        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
36379
20ef039bccff make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents: 36373
diff changeset
   498
  let
40439
fb6ee11e776a reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents: 40428
diff changeset
   499
    val repair_context =
fb6ee11e776a reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents: 40428
diff changeset
   500
      Config.put SMT_Config.verbose debug
fb6ee11e776a reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents: 40428
diff changeset
   501
      #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
fb6ee11e776a reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet
parents: 40428
diff changeset
   502
    val state = state |> Proof.map_context repair_context
40207
5da3e8ede850 adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
blanchet
parents: 40206
diff changeset
   503
    val ctxt = Proof.context_of state
40181
3788b7adab36 integrated "smt" proof method with Sledgehammer
blanchet
parents: 40132
diff changeset
   504
    val {outcome, used_facts, run_time_in_msecs} =
40553
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   505
      smt_filter_loop params remote state subgoal
1264c9172338 pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents: 40471
diff changeset
   506
                      (map_filter (try dest_Untranslated) facts)
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   507
    val message =
40184
91b4b73dbafb proper error handling for SMT solvers in Sledgehammer
blanchet
parents: 40181
diff changeset
   508
      case outcome of
91b4b73dbafb proper error handling for SMT solvers in Sledgehammer
blanchet
parents: 40181
diff changeset
   509
        NONE =>
40224
7883fefd6a7b clear identification;
blanchet
parents: 40207
diff changeset
   510
        try_command_line (proof_banner auto)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   511
                         (apply_on_subgoal subgoal subgoal_count ^
40181
3788b7adab36 integrated "smt" proof method with Sledgehammer
blanchet
parents: 40132
diff changeset
   512
                          command_call smtN (map fst used_facts)) ^
3788b7adab36 integrated "smt" proof method with Sledgehammer
blanchet
parents: 40132
diff changeset
   513
        minimize_line minimize_command (map fst used_facts)
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40419
diff changeset
   514
      | SOME SMT_Failure.Time_Out => "Timed out."
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40419
diff changeset
   515
      | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
40207
5da3e8ede850 adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
blanchet
parents: 40206
diff changeset
   516
      | SOME failure =>
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40419
diff changeset
   517
        SMT_Failure.string_of_failure ctxt failure
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   518
    val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   519
  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
   520
    {outcome = outcome, used_facts = used_facts,
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
   521
     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
   522
  end
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   523
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   524
fun get_prover thy auto name =
40224
7883fefd6a7b clear identification;
blanchet
parents: 40207
diff changeset
   525
  if is_smt_prover name then
7883fefd6a7b clear identification;
blanchet
parents: 40207
diff changeset
   526
    run_smt_solver auto (String.isPrefix remote_prefix name)
7883fefd6a7b clear identification;
blanchet
parents: 40207
diff changeset
   527
  else
7883fefd6a7b clear identification;
blanchet
parents: 40207
diff changeset
   528
    run_atp auto name (get_atp thy name)
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   529
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   530
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   531
               auto minimize_command
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
   532
               (problem as {state, goal, subgoal, subgoal_count, facts, ...})
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   533
               name =
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   534
  let
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   535
    val thy = Proof.theory_of state
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   536
    val ctxt = Proof.context_of state
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   537
    val birth_time = Time.now ()
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   538
    val death_time = Time.+ (birth_time, timeout)
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   539
    val max_relevant =
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   540
      the_default (default_max_relevant_for_prover thy name) max_relevant
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
   541
    val num_facts = Int.min (length facts, max_relevant)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   542
    val desc =
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
   543
      prover_description ctxt params name num_facts subgoal subgoal_count goal
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   544
    fun go () =
38982
820b8221ed48 added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents: 38893
diff changeset
   545
      let
39453
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   546
        fun really_go () =
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   547
          get_prover thy auto name params (minimize_command name) problem
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   548
          |> (fn {outcome, message, ...} =>
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   549
                 (if is_some outcome then "none" else "some", message))
39453
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   550
        val (outcome_code, message) =
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   551
          if debug then
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   552
            really_go ()
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   553
          else
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   554
            (really_go ()
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   555
             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   556
                  | exn => ("unknown", "Internal error:\n" ^
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   557
                                       ML_Compiler.exn_message exn ^ "\n"))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   558
        val _ =
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   559
          if expect = "" orelse outcome_code = expect then
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   560
            ()
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   561
          else if blocking then
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   562
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   563
          else
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   564
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   565
      in (outcome_code = "some", message) end
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   566
  in
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   567
    if auto then
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   568
      let val (success, message) = TimeLimit.timeLimit timeout go () in
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   569
        (success, state |> success ? Proof.goal_message (fn () =>
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   570
             Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
39327
blanchet
parents: 39318
diff changeset
   571
                 (Pretty.str message)]))
38982
820b8221ed48 added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents: 38893
diff changeset
   572
      end
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   573
    else if blocking then
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   574
      let val (success, message) = TimeLimit.timeLimit timeout go () in
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40114
diff changeset
   575
        List.app Output.urgent_message
39370
f8292d3020db use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents: 39366
diff changeset
   576
                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
f8292d3020db use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents: 39366
diff changeset
   577
        (success, state)
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   578
      end
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   579
    else
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   580
      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   581
       (false, state))
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   582
  end
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   583
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   584
fun run_sledgehammer (params as {blocking, debug, provers, full_types,
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40068
diff changeset
   585
                                 relevance_thresholds, max_relevant, ...})
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
   586
                     auto i (relevance_override as {only, ...}) minimize_command
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
   587
                     state =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   588
  if null provers then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   589
    error "No prover is set."
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   590
  else case subgoal_count state of
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40114
diff changeset
   591
    0 => (Output.urgent_message "No subgoal!"; (false, state))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   592
  | n =>
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   593
    let
39364
61f0d36840c5 Sledgehammer should be called in "prove" mode;
blanchet
parents: 39338
diff changeset
   594
      val _ = Proof.assert_backward state
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   595
      val thy = Proof.theory_of state
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   596
      val ctxt = Proof.context_of state
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   597
      val {facts = chained_ths, goal, ...} = Proof.goal state
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   598
      val (_, hyp_ts, concl_t) = strip_subgoal goal i
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   599
      val _ = () |> not blocking ? kill_provers
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40114
diff changeset
   600
      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   601
      val (smts, atps) = provers |> List.partition is_smt_prover
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   602
      fun run_provers label full_types relevance_fudge maybe_translate provers
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   603
                      (res as (success, state)) =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   604
        if success orelse null provers then
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   605
          res
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   606
        else
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   607
          let
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   608
            val max_max_relevant =
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   609
              case max_relevant of
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   610
                SOME n => n
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   611
              | NONE =>
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   612
                0 |> fold (Integer.max o default_max_relevant_for_prover thy)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   613
                          provers
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   614
                  |> auto ? (fn n => n div auto_max_relevant_divisor)
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   615
            val is_built_in_const =
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   616
              is_built_in_const_for_prover ctxt (hd provers)
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
   617
            val facts =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   618
              relevant_facts ctxt full_types relevance_thresholds
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   619
                             max_max_relevant is_built_in_const 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
   620
                             relevance_override chained_ths hyp_ts concl_t
40114
blanchet
parents: 40072
diff changeset
   621
              |> map maybe_translate
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   622
            val problem =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   623
              {state = state, goal = goal, subgoal = i, subgoal_count = n,
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
   624
               facts = facts, only = only}
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   625
            val run_prover = run_prover params auto minimize_command
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   626
          in
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   627
            if debug then
40370
14456fd302f0 cosmetics
blanchet
parents: 40369
diff changeset
   628
              Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   629
                  (if null facts then
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   630
                     "Found no relevant facts."
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   631
                   else
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   632
                     "Including (up to) " ^ string_of_int (length facts) ^
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   633
                     " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   634
                     (facts |> map_filter fact_name
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   635
                            |> space_implode " ") ^ "."))
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   636
            else
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   637
              ();
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   638
            if auto then
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   639
              fold (fn prover => fn (true, state) => (true, state)
40064
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   640
                                  | (false, _) => run_prover problem prover)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   641
                   provers (false, state)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   642
            else
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   643
              provers |> (if blocking then Par_List.map else map)
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   644
                             (run_prover problem)
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   645
                      |> exists fst |> rpair state
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   646
          end
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
   647
      val run_atps =
40370
14456fd302f0 cosmetics
blanchet
parents: 40369
diff changeset
   648
        run_provers "ATP" full_types atp_relevance_fudge
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
   649
                    (Translated o translate_fact ctxt) atps
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
   650
      val run_smts =
40370
14456fd302f0 cosmetics
blanchet
parents: 40369
diff changeset
   651
        run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   652
      fun run_atps_and_smt_solvers () =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   653
        [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   654
    in
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   655
      (false, state)
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   656
      |> (if blocking then run_atps #> not auto ? run_smts
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   657
          else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   658
    end
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
   659
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   660
val setup =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   661
  dest_dir_setup
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   662
  #> problem_prefix_setup
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   663
  #> measure_run_time_setup
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   664
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   665
end;