src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Fri, 04 Oct 2013 11:12:28 +0200
changeset 54308 1a87db1f3701
parent 53815 e8aa538e959e
child 54062 427380d5d1d7
permissions -rw-r--r--
more parallelism in blocking mode
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_run.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
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
     9
signature SLEDGEHAMMER_RUN =
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
52555
6811291d1869 moved code -> easier debugging
smolkas
parents: 52196
diff changeset
    13
  type minimize_command = Sledgehammer_Reconstructor.minimize_command
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
    14
  type mode = Sledgehammer_Provers.mode
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    15
  type params = Sledgehammer_Provers.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
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    21
  val string_of_factss : (string * fact list) list -> string
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
    22
  val run_sledgehammer :
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
    23
    params -> mode -> (string -> unit) option -> int -> fact_override
45520
2b1dde0b1c30 thread in additional options to minimizer
blanchet
parents: 45379
diff changeset
    24
    -> ((string * string list) list -> string -> minimize_command)
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    25
    -> Proof.state -> 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
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    28
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
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
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    32
open ATP_Problem_Generate
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    33
open ATP_Proof
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    34
open ATP_Proof_Reconstruct
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    35
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
    36
open Sledgehammer_Fact
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    37
open Sledgehammer_Provers
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    38
open Sledgehammer_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48321
diff changeset
    39
open Sledgehammer_MaSh
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    40
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    41
val someN = "some"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    42
val noneN = "none"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    43
val timeoutN = "timeout"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    44
val unknownN = "unknown"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    45
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    46
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
    47
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    48
fun max_outcome_code codes =
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    49
  NONE
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    50
  |> fold (fn candidate =>
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    51
              fn accum as SOME _ => accum
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    52
               | NONE => if member (op =) codes candidate then SOME candidate
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    53
                         else NONE)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    54
          ordered_outcome_codes
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
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41180
diff changeset
    57
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    58
                       n goal =
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48299
diff changeset
    59
  (quote name,
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    60
   (if verbose then
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    61
      " 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
    62
    else
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    63
      "") ^
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    64
   " 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
    65
   (if blocking then "."
0147a4348ca1 try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents: 45370
diff changeset
    66
    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
    67
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    68
fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, slice,
43059
95b845a0edce make all messages urgent in verbose mode
blanchet
parents: 43058
diff changeset
    69
                              timeout, expect, ...})
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
    70
        mode output_result minimize_command only learn
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    71
        {state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    72
  let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    73
    val ctxt = Proof.context_of state
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    74
50749
82dee320d340 increased hard timeout -- minimization can take time
blanchet
parents: 50669
diff changeset
    75
    val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
53815
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53814
diff changeset
    76
    val _ = spying spy (fn () => (state, subgoal, name, "launched"));
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    77
    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
    78
    val death_time = Time.+ (birth_time, hard_timeout)
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    79
    val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt slice name)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    80
    val num_facts = length facts |> not only ? Integer.min max_facts
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    81
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    82
    fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    83
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    84
    val problem =
47904
67663c968d70 distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents: 47531
diff changeset
    85
      {state = state, goal = goal, subgoal = subgoal,
67663c968d70 distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents: 47531
diff changeset
    86
       subgoal_count = subgoal_count,
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    87
       factss = factss
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    88
         |> map (apsnd ((not (is_ho_atp ctxt name)
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    89
                         ? filter_out (fn ((_, (_, Induction)), _) => true
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    90
                                        | _ => false))
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    91
                        #> take num_facts))}
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
    92
51009
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
    93
    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
    94
      tag_list 1 used_from
51005
ce4290c33d73 eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents: 51004
diff changeset
    95
      |> map (fn (j, fact) => fact |> apsnd (K j))
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48407
diff changeset
    96
      |> 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
    97
      |> 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
    98
      |> 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
    99
      |> 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
   100
                  " 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
   101
      |> Output.urgent_message
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   102
53814
255a2929c137 made SML/NJ happy
blanchet
parents: 53804
diff changeset
   103
    fun spying_str_of_res ({outcome = NONE, used_facts, ...} : prover_result) =
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   104
        let val num_used_facts = length used_facts in
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   105
          "success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   106
          plural_s num_used_facts
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   107
        end
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   108
      | spying_str_of_res {outcome = SOME failure, ...} =
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   109
        "failure: " ^ string_of_atp_failure failure
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   110
41255
a80024d7b71b added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents: 41245
diff changeset
   111
    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
   112
      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
   113
      |> 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
   114
      |> verbose
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
   115
         ? 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
   116
                   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
   117
                 | _ => ())
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   118
      |> spy
53815
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53814
diff changeset
   119
         ? 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
   120
      |> (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
   121
             (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
   122
              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
   123
              else someN, fn () => message (Lazy.force preplay) ^ message_tail))
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   124
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   125
    fun go () =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   126
      let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   127
        val (outcome_code, message) =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   128
          if debug then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   129
            really_go ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   130
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   131
            (really_go ()
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   132
             handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   133
                  | exn =>
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   134
                    if Exn.is_interrupt exn then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   135
                      reraise exn
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   136
                    else
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   137
                      (unknownN, fn () => "Internal error:\n" ^
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   138
                                          ML_Compiler.exn_message exn ^ "\n"))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   139
        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
   140
          (* 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
   141
             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
   142
             machine. *)
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
   143
          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
   144
             not (is_prover_installed ctxt name) then
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   145
            ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   146
          else if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   147
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   148
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   149
            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
   150
      in (outcome_code, message) end
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   151
  in
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   152
    if mode = Auto_Try then
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50201
diff changeset
   153
      let val (outcome_code, message) = time_limit timeout go () in
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   154
        (outcome_code,
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   155
         state
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   156
         |> outcome_code = someN
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   157
            ? Proof.goal_message (fn () =>
52643
34c29356930e more explicit Markup.information for messages produced by "auto" tools;
wenzelm
parents: 52555
diff changeset
   158
                  Pretty.mark Markup.information (Pretty.str (message ()))))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   159
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   160
    else if blocking then
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   161
      let
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   162
        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
   163
        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
   164
          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
   165
            quote name ^ ": " ^ message ()
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   166
          else ""
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   167
        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
   168
          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
   169
            the output_result outcome
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents: 52643
diff changeset
   170
          else
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   171
            outcome
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   172
            |> Async_Manager.break_into_chunks
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   173
            |> List.app Output.urgent_message
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   174
      in (outcome_code, state) end
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   175
    else
52048
9003b293e775 tuned signature -- emphasize thread creation here;
wenzelm
parents: 51998
diff changeset
   176
      (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   177
                            ((fn (outcome_code, message) =>
43059
95b845a0edce make all messages urgent in verbose mode
blanchet
parents: 43058
diff changeset
   178
                                 (verbose orelse outcome_code = someN,
95b845a0edce make all messages urgent in verbose mode
blanchet
parents: 43058
diff changeset
   179
                                  message ())) o go);
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   180
       (unknownN, state))
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
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   183
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
   184
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   185
fun string_of_facts facts =
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   186
  "Including " ^ string_of_int (length facts) ^
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   187
  " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   188
  (facts |> map (fst o fst) |> space_implode " ") ^ "."
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   189
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   190
fun string_of_factss factss =
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   191
  if forall (null o snd) factss then
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   192
    "Found no relevant facts."
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   193
  else case factss of
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   194
    [(_, facts)] => string_of_facts facts
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   195
  | _ =>
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   196
    factss
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   197
    |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   198
    |> space_implode "\n\n"
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   199
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   200
fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, slice, ...})
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   201
        mode 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
   202
  if null provers then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   203
    error "No prover is set."
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   204
  else case subgoal_count state of
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents: 52643
diff changeset
   205
    0 =>
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents: 52643
diff changeset
   206
      ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   207
  | n =>
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   208
    let
39364
61f0d36840c5 Sledgehammer should be called in "prove" mode;
blanchet
parents: 39338
diff changeset
   209
      val _ = Proof.assert_backward state
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
   210
      val print =
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
   211
        if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   212
      val state =
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   213
        state |> Proof.map_context (Config.put SMT_Config.verbose debug)
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   214
      val ctxt = Proof.context_of state
48396
dd82d190c2af name tuning
blanchet
parents: 48394
diff changeset
   215
      val {facts = chained, goal, ...} = Proof.goal state
52196
2281f33e8da6 redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents: 52125
diff changeset
   216
      val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
51007
4f694d52bf62 thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
blanchet
parents: 51006
diff changeset
   217
      val ho_atp = exists (is_ho_atp ctxt) provers
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
   218
      val reserved = reserved_isar_keyword_table ()
48396
dd82d190c2af name tuning
blanchet
parents: 48394
diff changeset
   219
      val css = clasimpset_rule_table_of ctxt
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48399
diff changeset
   220
      val all_facts =
48396
dd82d190c2af name tuning
blanchet
parents: 48394
diff changeset
   221
        nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
dd82d190c2af name tuning
blanchet
parents: 48394
diff changeset
   222
                         concl_t
44586
eeba1eedf32d improved handling of induction rules in Sledgehammer
nik
parents: 44585
diff changeset
   223
      val _ = () |> not blocking ? kill_provers
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41432
diff changeset
   224
      val _ = case find_first (not o is_prover_supported ctxt) provers of
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   225
                SOME name => error ("No such prover: " ^ name ^ ".")
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   226
              | NONE => ()
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   227
      val _ = print "Sledgehammering..."
53815
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53814
diff changeset
   228
      val _ =
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53814
diff changeset
   229
        spying spy (fn () => (state, i, "***", "starting " ^ @{make_string} mode ^ " mode"))
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   230
      val (smts, (ueq_atps, full_atps)) =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   231
        provers |> List.partition (is_smt_prover ctxt)
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   232
                ||> List.partition (is_unit_equational_atp ctxt)
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   233
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   234
      val spying_str_of_factss =
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   235
        commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   236
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   237
      fun get_factss label is_appropriate_prop provers =
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   238
        let
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   239
          val max_max_facts =
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   240
            case max_facts of
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   241
              SOME n => n
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   242
            | NONE =>
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51741
diff changeset
   243
              0 |> fold (Integer.max o default_max_facts_of_prover ctxt slice)
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   244
                        provers
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   245
                |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
53815
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53814
diff changeset
   246
          val _ = spying spy (fn () => (state, i, label ^ "s",
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53814
diff changeset
   247
            "filtering " ^ string_of_int (length all_facts) ^ " facts"));
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   248
        in
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48399
diff changeset
   249
          all_facts
43351
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43306
diff changeset
   250
          |> (case is_appropriate_prop of
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43306
diff changeset
   251
                SOME is_app => filter (is_app o prop_of o snd)
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43306
diff changeset
   252
              | NONE => I)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   253
          |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   254
                            hyp_ts concl_t
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   255
          |> tap (fn factss =>
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
   256
                     if verbose then
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   257
                       label ^ plural_s (length provers) ^ ": " ^
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   258
                       string_of_factss factss
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   259
                       |> print
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   260
                     else
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   261
                       ())
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   262
          |> spy ? tap (fn factss =>
53815
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53814
diff changeset
   263
            spying spy (fn () =>
e8aa538e959e encode goal digest in spying log (to detect duplicates)
blanchet
parents: 53814
diff changeset
   264
              (state, i, label ^ "s", "selected facts: " ^ spying_str_of_factss factss)))
41242
8edeb1dbbc76 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents: 41208
diff changeset
   265
        end
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   266
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   267
      fun launch_provers state label is_appropriate_prop provers =
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   268
        let
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   269
          val factss = get_factss label is_appropriate_prop provers
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   270
          val problem =
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   271
            {state = state, goal = goal, subgoal = i, subgoal_count = n,
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   272
             factss = factss}
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   273
          fun learn prover =
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   274
            mash_learn_proof ctxt params prover (prop_of goal) all_facts
53549
blanchet
parents: 53155
diff changeset
   275
          val launch =
blanchet
parents: 53155
diff changeset
   276
            launch_prover params mode output_result minimize_command only learn
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   277
        in
53048
0f76e620561f more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents: 52997
diff changeset
   278
          if mode = Auto_Try then
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   279
            (unknownN, state)
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   280
            |> fold (fn prover => fn accum as (outcome_code, _) =>
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   281
                        if outcome_code = someN then accum
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   282
                        else launch problem prover)
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   283
                    provers
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   284
          else
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   285
            provers
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   286
            |> (if blocking then Par_List.map else map) (launch problem #> fst)
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   287
            |> max_outcome_code |> rpair state
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   288
        end
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   289
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42946
diff changeset
   290
      fun launch_atps label is_appropriate_prop atps accum =
42946
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   291
        if null atps then
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   292
          accum
43351
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43306
diff changeset
   293
        else if is_some is_appropriate_prop andalso
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43306
diff changeset
   294
                not (the is_appropriate_prop concl_t) then
42946
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   295
          (if verbose orelse length atps = length provers then
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   296
             "Goal outside the scope of " ^
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   297
             space_implode " " (serial_commas "and" (map quote atps)) ^ "."
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   298
             |> Output.urgent_message
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   299
           else
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   300
             ();
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   301
           accum)
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   302
        else
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   303
          launch_provers state label is_appropriate_prop atps
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   304
41746
e590971528b2 run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user
blanchet
parents: 41743
diff changeset
   305
      fun launch_smts accum =
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   306
        if null smts then accum else launch_provers state "SMT solver" NONE smts
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   307
43351
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43306
diff changeset
   308
      val launch_full_atps = launch_atps "ATP" NONE full_atps
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   309
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   310
      val launch_ueq_atps = launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   311
54308
1a87db1f3701 more parallelism in blocking mode
blanchet
parents: 53815
diff changeset
   312
      fun launch_atps_and_smt_solvers p =
43043
1406f6fc5dc3 normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
blanchet
parents: 43037
diff changeset
   313
        [launch_full_atps, launch_smts, launch_ueq_atps]
54308
1a87db1f3701 more parallelism in blocking mode
blanchet
parents: 53815
diff changeset
   314
        |> Par_List.map (fn f => fst (f p))
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   315
        handle ERROR msg => (print ("Error: " ^ msg); error msg)
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53549
diff changeset
   316
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   317
      fun maybe f (accum as (outcome_code, _)) =
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
   318
        accum |> (mode = Normal orelse outcome_code <> someN) ? f
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   319
    in
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   320
      (unknownN, state)
54308
1a87db1f3701 more parallelism in blocking mode
blanchet
parents: 53815
diff changeset
   321
      |> (if mode = Auto_Try then
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   322
            launch_full_atps
54308
1a87db1f3701 more parallelism in blocking mode
blanchet
parents: 53815
diff changeset
   323
          else if blocking then
1a87db1f3701 more parallelism in blocking mode
blanchet
parents: 53815
diff changeset
   324
            launch_atps_and_smt_solvers #> max_outcome_code #> rpair state
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   325
          else
54308
1a87db1f3701 more parallelism in blocking mode
blanchet
parents: 53815
diff changeset
   326
            (fn p => (Future.fork (tap (fn () => launch_atps_and_smt_solvers p)); p)))
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   327
      handle TimeLimit.TimeOut =>
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   328
             (print "Sledgehammer ran out of time."; (unknownN, state))
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   329
    end
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   330
    |> `(fn (outcome_code, _) => outcome_code = someN)
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
   331
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   332
end;