src/HOL/Tools/Sledgehammer/sledgehammer.ML
author blanchet
Wed, 21 May 2014 14:09:42 +0200
changeset 57037 c51132be8e16
parent 56303 4cc3f4db3447
child 57053 46000c075d07
permissions -rw-r--r--
avoid markup-generating @{make_string}
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
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
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
     9
signature SLEDGEHAMMER =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    10
sig
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
    11
  type fact = Sledgehammer_Fact.fact
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    12
  type fact_override = Sledgehammer_Fact.fact_override
55287
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
    13
  type minimize_command = Sledgehammer_Proof_Methods.minimize_command
55201
1ee776da8da7 renamed ML file
blanchet
parents: 54816
diff changeset
    14
  type mode = Sledgehammer_Prover.mode
1ee776da8da7 renamed ML file
blanchet
parents: 54816
diff changeset
    15
  type params = Sledgehammer_Prover.params
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    16
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    17
  val someN : string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    18
  val noneN : string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    19
  val timeoutN : string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    20
  val unknownN : string
55212
blanchet
parents: 55202
diff changeset
    21
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    22
  val string_of_factss : (string * fact list) list -> string
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
    23
  val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
    24
    ((string * string list) list -> string -> minimize_command) -> Proof.state ->
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
    25
    bool * (string * Proof.state)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    26
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    27
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
    28
structure Sledgehammer : SLEDGEHAMMER =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    29
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    30
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    31
open ATP_Util
55212
blanchet
parents: 55202
diff changeset
    32
open ATP_Proof
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    33
open ATP_Problem_Generate
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    34
open Sledgehammer_Util
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 47904
diff changeset
    35
open Sledgehammer_Fact
55287
ffa306239316 renamed ML file
blanchet
parents: 55286
diff changeset
    36
open Sledgehammer_Proof_Methods
55201
1ee776da8da7 renamed ML file
blanchet
parents: 54816
diff changeset
    37
open Sledgehammer_Prover
55212
blanchet
parents: 55202
diff changeset
    38
open Sledgehammer_Prover_ATP
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
    39
open Sledgehammer_Prover_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48321
diff changeset
    40
open Sledgehammer_MaSh
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    41
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    42
val someN = "some"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    43
val noneN = "none"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    44
val timeoutN = "timeout"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    45
val unknownN = "unknown"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    46
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    47
val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    48
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    49
fun max_outcome_code codes =
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    50
  NONE
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    51
  |> fold (fn candidate =>
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    52
              fn accum as SOME _ => accum
55286
blanchet
parents: 55212
diff changeset
    53
               | NONE => if member (op =) codes candidate then SOME candidate else NONE)
blanchet
parents: 55212
diff changeset
    54
       ordered_outcome_codes
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    55
  |> the_default unknownN
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    56
55286
blanchet
parents: 55212
diff changeset
    57
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal =
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48299
diff changeset
    58
  (quote name,
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    59
   (if verbose then
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    60
      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    61
    else
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    62
      "") ^
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    63
   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
45379
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45370
diff changeset
    64
   (if blocking then "."
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45370
diff changeset
    65
    else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    66
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
    67
fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
    68
    output_result minimize_command only learn
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
    69
    {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    70
  let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    71
    val ctxt = Proof.context_of state
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    72
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
    73
    val hard_timeout = time_mult 3.0 timeout
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
    74
    val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    75
    val birth_time = Time.now ()
42850
c8709be8a40f distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
blanchet
parents: 42646
diff changeset
    76
    val death_time = Time.+ (birth_time, hard_timeout)
54126
6675cdc0d1ae if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
blanchet
parents: 54090
diff changeset
    77
    val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    78
    val num_facts = length facts |> not only ? Integer.min max_facts
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    79
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    80
    fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    81
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    82
    val problem =
54141
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54126
diff changeset
    83
      {comment = comment, state = state, goal = goal, subgoal = subgoal,
47904
67663c968d70 distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents: 47531
diff changeset
    84
       subgoal_count = subgoal_count,
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    85
       factss = factss
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    86
         |> map (apsnd ((not (is_ho_atp ctxt name)
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    87
                         ? filter_out (fn ((_, (_, Induction)), _) => true
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    88
                                        | _ => false))
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    89
                        #> take num_facts))}
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    90
51009
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
    91
    fun print_used_facts used_facts used_from =
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
    92
      tag_list 1 used_from
51005
ce4290c33d73 eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents: 51004
diff changeset
    93
      |> map (fn (j, fact) => fact |> apsnd (K j))
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48407
diff changeset
    94
      |> filter_used_facts false used_facts
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48384
diff changeset
    95
      |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48384
diff changeset
    96
      |> commas
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48384
diff changeset
    97
      |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48384
diff changeset
    98
                  " proof (of " ^ string_of_int (length facts) ^ "): ") "."
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48384
diff changeset
    99
      |> Output.urgent_message
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   100
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   101
    fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   102
        let
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   103
          val num_used_facts = length used_facts
54063
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   104
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   105
          fun find_indices facts =
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   106
            tag_list 1 facts
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   107
            |> map (fn (j, fact) => fact |> apsnd (K j))
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   108
            |> filter_used_facts false used_facts
54773
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   109
            |> distinct (eq_fst (op =))
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   110
            |> map (prefix "@" o string_of_int o snd)
54063
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   111
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   112
          fun filter_info (fact_filter, facts) =
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   113
            let
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   114
              val indices = find_indices facts
54773
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   115
              (* "Int.max" is there for robustness -- it shouldn't be necessary *)
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   116
              val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?"
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   117
            in
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   118
              (commas (indices @ unknowns), fact_filter)
79f66cd15d57 fixed source of 'Subscript' exception
blanchet
parents: 54503
diff changeset
   119
            end
54063
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   120
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   121
          val filter_infos =
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   122
            map filter_info (("actual", used_from) :: factss)
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   123
            |> AList.group (op =)
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   124
            |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   125
        in
54063
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   126
          "Success: Found proof with " ^ string_of_int num_used_facts ^
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   127
          " of " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
c0658286aa08 more thorough spying
blanchet
parents: 54062
diff changeset
   128
          (if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   129
        end
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   130
      | spying_str_of_res {outcome = SOME failure, ...} =
54062
427380d5d1d7 more Sledgehammer spying -- record fact indices
blanchet
parents: 54057
diff changeset
   131
        "Failure: " ^ string_of_atp_failure failure
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   132
41255
a80024d7b71b added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents: 41245
diff changeset
   133
    fun really_go () =
41263
4cac389c005f renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
blanchet
parents: 41262
diff changeset
   134
      problem
51187
c344cf148e8f avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents: 51010
diff changeset
   135
      |> get_minimizing_prover ctxt mode learn name params minimize_command
51009
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
   136
      |> verbose
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
   137
         ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
   138
                   print_used_facts used_facts used_from
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
   139
                 | _ => ())
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   140
      |> spy
53815
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53814
diff changeset
   141
         ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43233
diff changeset
   142
      |> (fn {outcome, preplay, message, message_tail, ...} =>
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   143
             (if outcome = SOME ATP_Proof.TimedOut then timeoutN
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   144
              else if is_some outcome then noneN
50669
84c7cf36b2e0 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents: 50668
diff changeset
   145
              else someN, fn () => message (Lazy.force preplay) ^ message_tail))
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   146
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   147
    fun go () =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   148
      let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   149
        val (outcome_code, message) =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   150
          if debug then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   151
            really_go ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   152
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   153
            (really_go ()
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   154
             handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   155
                  | exn =>
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   156
                    if Exn.is_interrupt exn then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   157
                      reraise exn
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   158
                    else
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   159
                      (unknownN, fn () => "Internal error:\n" ^
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 55452
diff changeset
   160
                                          Runtime.exn_message exn ^ "\n"))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   161
        val _ =
41142
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
   162
          (* The "expect" argument is deliberately ignored if the prover is
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
   163
             missing so that the "Metis_Examples" can be processed on any
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
   164
             machine. *)
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
   165
          if expect = "" orelse outcome_code = expect orelse
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
   166
             not (is_prover_installed ctxt name) then
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   167
            ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   168
          else if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   169
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   170
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   171
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   172
      in (outcome_code, message) end
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   173
  in
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   174
    if mode = Auto_Try then
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
   175
      let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   176
        (outcome_code,
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   177
         state
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   178
         |> outcome_code = someN
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   179
            ? Proof.goal_message (fn () =>
52643
34c29356930e more explicit Markup.information for messages produced by "auto" tools;
wenzelm
parents: 52555
diff changeset
   180
                  Pretty.mark Markup.information (Pretty.str (message ()))))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   181
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   182
    else if blocking then
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   183
      let
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   184
        val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   185
        val outcome =
53052
a0db255af8c5 sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents: 53048
diff changeset
   186
          if outcome_code = someN orelse mode = Normal then
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   187
            quote name ^ ": " ^ message ()
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   188
          else ""
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   189
        val _ =
53052
a0db255af8c5 sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents: 53048
diff changeset
   190
          if outcome <> "" andalso is_some output_result then
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   191
            the output_result outcome
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents: 52643
diff changeset
   192
          else
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   193
            outcome
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   194
            |> Async_Manager.break_into_chunks
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   195
            |> List.app Output.urgent_message
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   196
      in (outcome_code, state) end
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   197
    else
52048
9003b293e775 tuned signature -- emphasize thread creation here;
wenzelm
parents: 51998
diff changeset
   198
      (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
55212
blanchet
parents: 55202
diff changeset
   199
         ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   200
       (unknownN, state))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   201
  end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   202
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   203
val auto_try_max_facts_divisor = 2 (* FUDGE *)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   204
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   205
fun string_of_facts facts =
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   206
  "Including " ^ string_of_int (length facts) ^
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   207
  " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   208
  (facts |> map (fst o fst) |> space_implode " ") ^ "."
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   209
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   210
fun string_of_factss factss =
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   211
  if forall (null o snd) factss then
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   212
    "Found no relevant facts."
55286
blanchet
parents: 55212
diff changeset
   213
  else
blanchet
parents: 55212
diff changeset
   214
    (case factss of
blanchet
parents: 55212
diff changeset
   215
      [(_, facts)] => string_of_facts facts
blanchet
parents: 55212
diff changeset
   216
    | _ =>
blanchet
parents: 55212
diff changeset
   217
      factss
blanchet
parents: 55212
diff changeset
   218
      |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
blanchet
parents: 55212
diff changeset
   219
      |> space_implode "\n\n")
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   220
54799
blanchet
parents: 54773
diff changeset
   221
fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode
blanchet
parents: 54773
diff changeset
   222
    output_result i (fact_override as {only, ...}) minimize_command state =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   223
  if null provers then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   224
    error "No prover is set."
55286
blanchet
parents: 55212
diff changeset
   225
  else
blanchet
parents: 55212
diff changeset
   226
    (case subgoal_count state of
blanchet
parents: 55212
diff changeset
   227
      0 =>
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents: 52643
diff changeset
   228
      ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
55286
blanchet
parents: 55212
diff changeset
   229
    | n =>
blanchet
parents: 55212
diff changeset
   230
      let
blanchet
parents: 55212
diff changeset
   231
        val _ = Proof.assert_backward state
blanchet
parents: 55212
diff changeset
   232
        val print =
blanchet
parents: 55212
diff changeset
   233
          if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
blanchet
parents: 55212
diff changeset
   234
        val ctxt = Proof.context_of state
blanchet
parents: 55212
diff changeset
   235
        val {facts = chained, goal, ...} = Proof.goal state
blanchet
parents: 55212
diff changeset
   236
        val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
blanchet
parents: 55212
diff changeset
   237
        val ho_atp = exists (is_ho_atp ctxt) provers
blanchet
parents: 55212
diff changeset
   238
        val reserved = reserved_isar_keyword_table ()
blanchet
parents: 55212
diff changeset
   239
        val css = clasimpset_rule_table_of ctxt
blanchet
parents: 55212
diff changeset
   240
        val all_facts =
blanchet
parents: 55212
diff changeset
   241
          nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
blanchet
parents: 55212
diff changeset
   242
                           concl_t
blanchet
parents: 55212
diff changeset
   243
        val _ = () |> not blocking ? kill_provers
blanchet
parents: 55212
diff changeset
   244
        val _ =
blanchet
parents: 55212
diff changeset
   245
          (case find_first (not o is_prover_supported ctxt) provers of
blanchet
parents: 55212
diff changeset
   246
            SOME name => error ("No such prover: " ^ name ^ ".")
blanchet
parents: 55212
diff changeset
   247
          | NONE => ())
blanchet
parents: 55212
diff changeset
   248
        val _ = print "Sledgehammering..."
57037
c51132be8e16 avoid markup-generating @{make_string}
blanchet
parents: 56303
diff changeset
   249
        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode"))
54090
a28992e35032 run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
blanchet
parents: 54063
diff changeset
   250
55286
blanchet
parents: 55212
diff changeset
   251
        val spying_str_of_factss =
blanchet
parents: 55212
diff changeset
   252
          commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   253
55286
blanchet
parents: 55212
diff changeset
   254
        fun get_factss provers =
blanchet
parents: 55212
diff changeset
   255
          let
blanchet
parents: 55212
diff changeset
   256
            val max_max_facts =
blanchet
parents: 55212
diff changeset
   257
              (case max_facts of
blanchet
parents: 55212
diff changeset
   258
                SOME n => n
blanchet
parents: 55212
diff changeset
   259
              | NONE =>
blanchet
parents: 55212
diff changeset
   260
                0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
blanchet
parents: 55212
diff changeset
   261
                  |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
blanchet
parents: 55212
diff changeset
   262
            val _ = spying spy (fn () => (state, i, "All",
blanchet
parents: 55212
diff changeset
   263
              "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
blanchet
parents: 55212
diff changeset
   264
          in
blanchet
parents: 55212
diff changeset
   265
            all_facts
blanchet
parents: 55212
diff changeset
   266
            |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
blanchet
parents: 55212
diff changeset
   267
            |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
blanchet
parents: 55212
diff changeset
   268
            |> spy ? tap (fn factss => spying spy (fn () =>
blanchet
parents: 55212
diff changeset
   269
              (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
blanchet
parents: 55212
diff changeset
   270
          end
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   271
55286
blanchet
parents: 55212
diff changeset
   272
        fun launch_provers state =
blanchet
parents: 55212
diff changeset
   273
          let
blanchet
parents: 55212
diff changeset
   274
            val factss = get_factss provers
blanchet
parents: 55212
diff changeset
   275
            val problem =
blanchet
parents: 55212
diff changeset
   276
              {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet
parents: 55212
diff changeset
   277
               factss = factss}
blanchet
parents: 55212
diff changeset
   278
            val learn = mash_learn_proof ctxt params (prop_of goal) all_facts
blanchet
parents: 55212
diff changeset
   279
            val launch = launch_prover params mode output_result minimize_command only learn
blanchet
parents: 55212
diff changeset
   280
          in
blanchet
parents: 55212
diff changeset
   281
            if mode = Auto_Try then
blanchet
parents: 55212
diff changeset
   282
              (unknownN, state)
blanchet
parents: 55212
diff changeset
   283
              |> fold (fn prover => fn accum as (outcome_code, _) =>
blanchet
parents: 55212
diff changeset
   284
                          if outcome_code = someN then accum
blanchet
parents: 55212
diff changeset
   285
                          else launch problem prover)
blanchet
parents: 55212
diff changeset
   286
                      provers
blanchet
parents: 55212
diff changeset
   287
            else
blanchet
parents: 55212
diff changeset
   288
              provers
blanchet
parents: 55212
diff changeset
   289
              |> (if blocking then Par_List.map else map) (launch problem #> fst)
blanchet
parents: 55212
diff changeset
   290
              |> max_outcome_code |> rpair state
blanchet
parents: 55212
diff changeset
   291
          end
blanchet
parents: 55212
diff changeset
   292
      in
blanchet
parents: 55212
diff changeset
   293
        (if blocking then launch_provers state
blanchet
parents: 55212
diff changeset
   294
         else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
blanchet
parents: 55212
diff changeset
   295
        handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
blanchet
parents: 55212
diff changeset
   296
      end
blanchet
parents: 55212
diff changeset
   297
      |> `(fn (outcome_code, _) => outcome_code = someN))
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
   298
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   299
end;