src/HOL/Tools/Sledgehammer/sledgehammer.ML
author wenzelm
Mon, 25 Oct 2010 21:06:56 +0200
changeset 40132 7ee65dbffa31
parent 40114 acb75271cdce
child 40181 3788b7adab36
permissions -rw-r--r--
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
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
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    11
  type failure = ATP_Systems.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
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    33
  datatype axiom =
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,
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    42
     axioms: axiom 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,
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    47
     used_axioms: (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
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
    57
  val irrelevant_consts_for_prover : string -> string list
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
    58
  val relevance_fudge_for_prover : string -> relevance_fudge
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    59
  val dest_dir : string Config.T
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    60
  val problem_prefix : string Config.T
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
    61
  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
    62
  val available_provers : theory -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    63
  val kill_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    64
  val running_provers : unit -> unit
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
    65
  val messages : int option -> unit
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
    66
  val get_prover : theory -> bool -> string -> prover
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
    67
  val run_sledgehammer :
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    68
    params -> bool -> int -> relevance_override -> (string -> minimize_command)
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    69
    -> Proof.state -> bool * Proof.state
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    70
  val setup : theory -> theory
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    71
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    72
38021
e024504943d1 rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents: 38020
diff changeset
    73
structure Sledgehammer : SLEDGEHAMMER =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    74
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    75
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
    76
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39453
diff changeset
    77
open ATP_Proof
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38023
diff changeset
    78
open ATP_Systems
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39493
diff changeset
    79
open Metis_Translate
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    80
open Sledgehammer_Util
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    81
open Sledgehammer_Filter
40068
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
    82
open Sledgehammer_ATP_Translate
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
    83
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
    84
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    85
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
    86
(** 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
    87
38102
019a49759829 fix bug in the newly introduced "bound concealing" code
blanchet
parents: 38100
diff changeset
    88
(* Identifier to distinguish Sledgehammer from other tools using
019a49759829 fix bug in the newly introduced "bound concealing" code
blanchet
parents: 38100
diff changeset
    89
   "Async_Manager". *)
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    90
val das_Tool = "Sledgehammer"
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    91
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
    92
val smtN = "smt"
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    93
val smt_prover_names = [smtN, remote_prefix ^ smtN]
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    94
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
    95
val is_smt_prover = member (op =) smt_prover_names
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
    96
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    97
fun is_prover_available thy name =
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    98
  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
    99
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   100
fun is_prover_installed ctxt name =
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   101
  let val thy = ProofContext.theory_of ctxt in
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   102
    if is_smt_prover name then true (* FIXME *)
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   103
    else is_atp_installed thy name
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   104
  end
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   105
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
   106
val smt_default_max_relevant = 300 (* FUDGE (FIXME) *)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   107
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
   108
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   109
fun default_max_relevant_for_prover thy name =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   110
  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
   111
  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
   112
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
   113
(* 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
   114
   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
   115
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
   116
  [@{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
   117
   @{const_name HOL.eq}]
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
val smt_irrelevant_consts = atp_irrelevant_consts (* FIXME *)
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
   119
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
   120
fun irrelevant_consts_for_prover name =
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
   121
  if is_smt_prover name then smt_irrelevant_consts else 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
   122
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   123
(* FUDGE *)
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   124
val atp_relevance_fudge =
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   125
  {worse_irrel_freq = 100.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   126
   higher_order_irrel_weight = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   127
   abs_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   128
   abs_irrel_weight = 2.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   129
   skolem_irrel_weight = 0.75,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   130
   theory_const_rel_weight = 0.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   131
   theory_const_irrel_weight = 0.25,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   132
   intro_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   133
   elim_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   134
   simp_bonus = 0.15,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   135
   local_bonus = 0.55,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   136
   assum_bonus = 1.05,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   137
   chained_bonus = 1.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   138
   max_imperfect = 11.5,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   139
   max_imperfect_exp = 1.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   140
   threshold_divisor = 2.0,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   141
   ridiculous_threshold = 0.1}
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   142
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
   143
(* FUDGE (FIXME) *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   144
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
   145
  {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
   146
   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
   147
   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
   148
   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
   149
   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
   150
   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
   151
   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
   152
   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
   153
   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
   154
   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
   155
   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
   156
   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
   157
   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
   158
   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
   159
   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
   160
   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
   161
   ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   162
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   163
fun relevance_fudge_for_prover name =
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   164
  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
   165
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   166
fun available_provers thy =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   167
  let
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   168
    val (remote_provers, local_provers) =
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   169
      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
   170
      |> List.partition (String.isPrefix remote_prefix)
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   171
  in
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40114
diff changeset
   172
    Output.urgent_message ("Available provers: " ^ commas (local_provers @ remote_provers) ^
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   173
              ".")
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   174
  end
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   175
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   176
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
   177
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
   178
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
   179
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   180
(** problems, results, ATPs, etc. **)
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   181
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   182
type params =
38982
820b8221ed48 added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents: 38893
diff changeset
   183
  {blocking: bool,
820b8221ed48 added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents: 38893
diff changeset
   184
   debug: bool,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   185
   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
   186
   overlord: bool,
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   187
   provers: string list,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   188
   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
   189
   explicit_apply: bool,
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   190
   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
   191
   max_relevant: int option,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   192
   isar_proof: bool,
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36922
diff changeset
   193
   isar_shrink_factor: int,
38985
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   194
   timeout: Time.time,
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   195
   expect: string}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   196
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   197
datatype axiom =
40114
blanchet
parents: 40072
diff changeset
   198
  Untranslated of (string * locality) * thm |
blanchet
parents: 40072
diff changeset
   199
  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
   200
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   201
type prover_problem =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   202
  {state: Proof.state,
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   203
   goal: thm,
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   204
   subgoal: int,
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   205
   subgoal_count: int,
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   206
   axioms: axiom list,
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
   207
   only: bool}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   208
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   209
type prover_result =
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   210
  {outcome: failure option,
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
   211
   message: string,
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   212
   used_axioms: (string * locality) list,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   213
   run_time_in_msecs: int option}
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   214
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   215
type prover = params -> minimize_command -> prover_problem -> prover_result
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
   216
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   217
(* configuration attributes *)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   218
38991
0e2798f30087 rename sledgehammer config attributes
blanchet
parents: 38988
diff changeset
   219
val (dest_dir, dest_dir_setup) =
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   220
  Attrib.config_string "sledgehammer_dest_dir" (K "")
38991
0e2798f30087 rename sledgehammer config attributes
blanchet
parents: 38988
diff changeset
   221
  (* Empty string means create files in Isabelle's temporary files directory. *)
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   222
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   223
val (problem_prefix, problem_prefix_setup) =
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   224
  Attrib.config_string "sledgehammer_problem_prefix" (K "prob")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   225
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   226
val (measure_run_time, measure_run_time_setup) =
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   227
  Attrib.config_bool "sledgehammer_measure_run_time" (K false)
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   228
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   229
fun with_path cleanup after f path =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   230
  Exn.capture f path
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   231
  |> tap (fn _ => cleanup path)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   232
  |> Exn.release
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   233
  |> tap (after path)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   234
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   235
fun prover_description ctxt ({blocking, verbose, ...} : params) name num_axioms
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   236
                       i n goal =
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   237
  quote name ^
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   238
  (if verbose then
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   239
     " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   240
   else
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   241
     "") ^
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   242
  " 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
   243
  (if blocking then
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   244
     ""
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   245
   else
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   246
     "\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
   247
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   248
fun proof_banner auto =
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   249
  if auto then "Sledgehammer found a proof" else "Try this command"
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   250
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   251
(* generic TPTP-based ATPs *)
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   252
40114
blanchet
parents: 40072
diff changeset
   253
fun dest_Untranslated (Untranslated p) = p
blanchet
parents: 40072
diff changeset
   254
  | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
blanchet
parents: 40072
diff changeset
   255
fun translated_axiom ctxt (Untranslated p) = translate_axiom ctxt p
blanchet
parents: 40072
diff changeset
   256
  | translated_axiom _ (Translated p) = p
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   257
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   258
fun int_option_add (SOME m) (SOME n) = SOME (m + n)
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   259
  | int_option_add _ _ = NONE
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   260
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   261
(* Important messages are important but not so important that users want to see
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   262
   them each time. *)
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
   263
val important_message_keep_factor = 0.1
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   264
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   265
fun run_atp auto atp_name
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   266
        {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
38997
78ac4468cf9d got rid of the "theory_relevant" option;
blanchet
parents: 38991
diff changeset
   267
         known_failures, default_max_relevant, explicit_forall,
78ac4468cf9d got rid of the "theory_relevant" option;
blanchet
parents: 38991
diff changeset
   268
         use_conjecture_for_hypotheses}
38455
131f7c46cf2c more debug output
blanchet
parents: 38290
diff changeset
   269
        ({debug, verbose, overlord, full_types, explicit_apply,
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   270
          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
   271
        minimize_command
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   272
        ({state, goal, subgoal, axioms, only, ...} : prover_problem) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   273
  let
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   274
    val ctxt = Proof.context_of state
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38997
diff changeset
   275
    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   276
    val axioms =
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   277
      axioms |> not only ? take (the_default default_max_relevant max_relevant)
40114
blanchet
parents: 40072
diff changeset
   278
             |> map (translated_axiom ctxt)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   279
    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
   280
                   else Config.get ctxt dest_dir
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   281
    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
   282
    val problem_file_name =
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   283
      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
   284
                   else problem_prefix ^ serial_string ())
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   285
                  ^ "_" ^ 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
   286
    val problem_path_name =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   287
      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
   288
        File.tmp_path problem_file_name
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   289
      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
   290
        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
   291
      else
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   292
        error ("No such directory: " ^ quote dest_dir ^ ".")
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   293
    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
   294
    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
   295
    (* write out problem file and call ATP *)
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   296
    fun command_line complete timeout probfile =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   297
      let
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   298
        val core = File.shell_path command ^ " " ^ arguments complete timeout ^
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   299
                   " " ^ File.shell_path probfile
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   300
      in
39010
344028ecc00e show real CPU time
blanchet
parents: 39009
diff changeset
   301
        (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
   302
         else "exec " ^ core) ^ " 2>&1"
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   303
      end
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   304
    fun split_time s =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   305
      let
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   306
        val split = String.tokens (fn c => str c = "\n");
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   307
        val (output, t) = s |> split |> split_last |> apfst cat_lines;
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   308
        fun as_num f = f >> (fst o read_int);
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   309
        val num = as_num (Scan.many1 Symbol.is_ascii_digit);
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   310
        val digit = Scan.one Symbol.is_ascii_digit;
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   311
        val num3 = as_num (digit ::: digit ::: (digit >> single));
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   312
        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
   313
        val as_time = Scan.read Symbol.stopper time o explode
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   314
      in (output, as_time t) end;
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   315
    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
   316
      case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   317
        (home_var, _) :: _ =>
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   318
        error ("The environment variable " ^ quote home_var ^ " is not set.")
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   319
      | [] =>
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   320
        if File.exists command then
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   321
          let
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   322
            fun run complete timeout =
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   323
              let
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   324
                val command = command_line complete timeout probfile
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   325
                val ((output, msecs), res_code) =
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   326
                  bash_output command
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   327
                  |>> (if overlord then
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   328
                         prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   329
                       else
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   330
                         I)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   331
                  |>> (if measure_run_time then split_time else rpair NONE)
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   332
                val (tstplike_proof, outcome) =
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   333
                  extract_tstplike_proof_and_outcome complete res_code
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   334
                      proof_delims known_failures output
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   335
              in (output, msecs, tstplike_proof, outcome) end
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   336
            val readable_names = debug andalso overlord
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   337
            val (atp_problem, pool, conjecture_offset, axiom_names) =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   338
              prepare_atp_problem ctxt readable_names explicit_forall full_types
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   339
                                  explicit_apply hyp_ts concl_t axioms
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   340
            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
   341
                                                  atp_problem
38631
979a0b37f981 prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents: 38600
diff changeset
   342
            val _ = File.write_list probfile ss
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   343
            val conjecture_shape =
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   344
              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
   345
              |> map single
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   346
            val run_twice = has_incomplete_mode andalso not auto
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   347
            val timer = Timer.startRealTimer ()
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   348
            val result =
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   349
              run false (if run_twice then
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   350
                           Time.fromMilliseconds
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   351
                                         (2 * Time.toMilliseconds timeout div 3)
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   352
                         else
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   353
                           timeout)
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   354
              |> run_twice
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   355
                 ? (fn (_, msecs0, _, SOME _) =>
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   356
                       run true (Time.- (timeout, Timer.checkRealTimer timer))
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   357
                       |> (fn (output, msecs, tstplike_proof, outcome) =>
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   358
                              (output, int_option_add msecs0 msecs,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   359
                               tstplike_proof, outcome))
38645
4d5bbec1a598 be more generous towards SPASS's -SOS mode
blanchet
parents: 38631
diff changeset
   360
                     | result => result)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents: 38277
diff changeset
   361
          in ((pool, conjecture_shape, axiom_names), result) end
38032
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   362
        else
54448f5d151f improve detection of installed SPASS
blanchet
parents: 38028
diff changeset
   363
          error ("Bad executable: " ^ Path.implode command ^ ".")
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   364
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   365
    (* If the problem file has not been exported, remove it; otherwise, export
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   366
       the proof file too. *)
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   367
    fun cleanup probfile =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   368
      if dest_dir = "" then try File.rm probfile else NONE
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   369
    fun export probfile (_, (output, _, _, _)) =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   370
      if dest_dir = "" then
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   371
        ()
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   372
      else
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   373
        File.write (Path.explode (Path.implode probfile ^ "_proof")) output
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents: 38277
diff changeset
   374
    val ((pool, conjecture_shape, axiom_names),
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39373
diff changeset
   375
         (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
   376
      with_path cleanup export run_on problem_path_name
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents: 38277
diff changeset
   377
    val (conjecture_shape, axiom_names) =
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
   378
      repair_conjecture_shape_and_axiom_names output conjecture_shape
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
   379
                                              axiom_names
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   380
    val important_message =
39493
cb2208f2c07d move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents: 39492
diff changeset
   381
      if random () <= important_message_keep_factor then
39492
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   382
        extract_important_message output
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   383
      else
b1172d65dd28 skip some "important" messages
blanchet
parents: 39491
diff changeset
   384
        ""
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   385
    val (message, used_axioms) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   386
      case outcome of
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   387
        NONE =>
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   388
        proof_text isar_proof
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   389
            (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
   390
            (proof_banner auto, full_types, minimize_command, tstplike_proof,
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   391
             axiom_names, goal, subgoal)
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38741
diff changeset
   392
        |>> (fn message =>
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38741
diff changeset
   393
                message ^ (if verbose then
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   394
                             "\nATP real CPU time: " ^
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   395
                             string_of_int (the msecs) ^ " ms."
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38741
diff changeset
   396
                           else
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
   397
                             "") ^
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
   398
                (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
   399
                   "\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
   400
                   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
   401
                 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
   402
                   ""))
38597
db482afec7f0 no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents: 38590
diff changeset
   403
      | SOME failure => (string_for_failure failure, [])
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   404
  in
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   405
    {outcome = outcome, message = message, used_axioms = used_axioms,
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   406
     run_time_in_msecs = msecs}
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   407
  end
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   408
40064
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   409
(* FIXME: dummy *)
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   410
fun saschas_run_smt_solver remote timeout state axioms i =
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   411
  (OS.Process.sleep (Time.fromMilliseconds 1500);
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   412
   {outcome = NONE, used_axioms = axioms |> take 5 |> map fst,
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   413
    run_time_in_msecs = NONE})
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   414
40064
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   415
fun run_smt_solver remote ({timeout, ...} : params) minimize_command
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   416
                   ({state, subgoal, subgoal_count, axioms, ...}
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   417
                    : 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
   418
  let
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   419
    val {outcome, used_axioms, run_time_in_msecs} =
40064
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   420
      saschas_run_smt_solver remote timeout state
40114
blanchet
parents: 40072
diff changeset
   421
                             (map_filter (try dest_Untranslated) axioms) subgoal
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   422
    val message =
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   423
      if outcome = NONE then
40064
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   424
        try_command_line (proof_banner false)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   425
                         (apply_on_subgoal subgoal subgoal_count ^
40064
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   426
                          command_call smtN (map fst used_axioms)) ^
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   427
        minimize_line minimize_command (map fst used_axioms)
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   428
      else
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   429
        ""
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   430
  in
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   431
    {outcome = outcome, used_axioms = used_axioms,
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   432
     run_time_in_msecs = run_time_in_msecs, message = message}
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   433
  end
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   434
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   435
fun get_prover thy auto name =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   436
  if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix)
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   437
  else 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
   438
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   439
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
   440
               auto minimize_command
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   441
               (problem as {state, goal, subgoal, subgoal_count, axioms, ...})
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   442
               name =
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   443
  let
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   444
    val thy = Proof.theory_of state
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   445
    val ctxt = Proof.context_of state
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   446
    val birth_time = Time.now ()
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   447
    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
   448
    val max_relevant =
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   449
      the_default (default_max_relevant_for_prover thy name) max_relevant
39110
a74bd9bfa880 show the number of facts for each prover in "verbose" mode
blanchet
parents: 39108
diff changeset
   450
    val num_axioms = Int.min (length axioms, max_relevant)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   451
    val desc =
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   452
      prover_description ctxt params name num_axioms subgoal subgoal_count goal
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   453
    fun go () =
38982
820b8221ed48 added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents: 38893
diff changeset
   454
      let
39453
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   455
        fun really_go () =
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   456
          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
   457
          |> (fn {outcome, message, ...} =>
162bbbea4e4d added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents: 38982
diff changeset
   458
                 (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
   459
        val (outcome_code, message) =
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   460
          if debug then
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   461
            really_go ()
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   462
          else
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   463
            (really_go ()
1740a2d6bef9 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
blanchet
parents: 39452
diff changeset
   464
             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
   465
                  | 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
   466
                                       ML_Compiler.exn_message exn ^ "\n"))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   467
        val _ =
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   468
          if expect = "" orelse outcome_code = expect then
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   469
            ()
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   470
          else if blocking then
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   471
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   472
          else
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   473
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   474
      in (outcome_code = "some", message) end
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   475
  in
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   476
    if auto then
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   477
      let val (success, message) = TimeLimit.timeLimit timeout go () in
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   478
        (success, state |> success ? Proof.goal_message (fn () =>
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   479
             Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
39327
blanchet
parents: 39318
diff changeset
   480
                 (Pretty.str message)]))
38982
820b8221ed48 added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents: 38893
diff changeset
   481
      end
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   482
    else if blocking then
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   483
      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
   484
        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
   485
                 (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
   486
        (success, state)
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   487
      end
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   488
    else
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   489
      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   490
       (false, state))
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   491
  end
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   492
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   493
fun run_sledgehammer (params as {blocking, provers, full_types,
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40068
diff changeset
   494
                                 relevance_thresholds, max_relevant, ...})
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
   495
                     auto i (relevance_override as {only, ...}) minimize_command
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
   496
                     state =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   497
  if null provers then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   498
    error "No prover is set."
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   499
  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
   500
    0 => (Output.urgent_message "No subgoal!"; (false, state))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   501
  | n =>
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   502
    let
39364
61f0d36840c5 Sledgehammer should be called in "prove" mode;
blanchet
parents: 39338
diff changeset
   503
      val _ = Proof.assert_backward state
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   504
      val thy = Proof.theory_of state
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   505
      val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   506
      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
   507
      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
   508
      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
   509
      val (smts, atps) = provers |> List.partition is_smt_prover
40114
blanchet
parents: 40072
diff changeset
   510
      fun run_provers full_types irrelevant_consts relevance_fudge
blanchet
parents: 40072
diff changeset
   511
                      maybe_translate provers (res as (success, state)) =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   512
        if success orelse null provers then
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   513
          res
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   514
        else
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   515
          let
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   516
            val max_max_relevant =
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   517
              case max_relevant of
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   518
                SOME n => n
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   519
              | NONE =>
40063
d086e3699e78 bring ATPs and SMT solvers more in line with each other
blanchet
parents: 40062
diff changeset
   520
                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
   521
                          provers
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   522
                  |> auto ? (fn n => n div auto_max_relevant_divisor)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   523
            val axioms =
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   524
              relevant_facts ctxt full_types relevance_thresholds
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
   525
                             max_max_relevant irrelevant_consts 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
   526
                             relevance_override chained_ths hyp_ts concl_t
40114
blanchet
parents: 40072
diff changeset
   527
              |> map maybe_translate
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   528
            val problem =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   529
              {state = state, goal = goal, subgoal = i, subgoal_count = n,
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   530
               axioms = axioms, only = only}
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   531
            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
   532
          in
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   533
            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
   534
              fold (fn prover => fn (true, state) => (true, state)
40064
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   535
                                  | (false, _) => run_prover problem prover)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   536
                   provers (false, state)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   537
            else
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   538
              provers |> (if blocking then Par_List.map else map)
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   539
                             (run_prover problem)
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   540
                      |> exists fst |> rpair state
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   541
          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
   542
      val run_atps =
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
   543
        run_provers full_types atp_irrelevant_consts atp_relevance_fudge
40114
blanchet
parents: 40072
diff changeset
   544
                    (Translated o translate_axiom 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
   545
      val run_smts =
40114
blanchet
parents: 40072
diff changeset
   546
        run_provers true smt_irrelevant_consts smt_relevance_fudge Untranslated
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
   547
                    smts
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   548
      fun run_atps_and_smt_solvers () =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   549
        [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
   550
    in
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   551
      (false, state)
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   552
      |> (if blocking then run_atps #> not auto ? run_smts
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   553
          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
   554
    end
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
   555
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   556
val setup =
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   557
  dest_dir_setup
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   558
  #> problem_prefix_setup
39003
c2aebd79981f run relevance filter in a thread, to avoid blocking
blanchet
parents: 39000
diff changeset
   559
  #> measure_run_time_setup
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
   560
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   561
end;