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