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