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