src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Tue, 28 May 2013 08:52:41 +0200
changeset 52196 2281f33e8da6
parent 52125 ac7830871177
child 52555 6811291d1869
permissions -rw-r--r--
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
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
49914
23e36a4d28f1 refactor code
blanchet
parents: 49358
diff changeset
    13
  type minimize_command = Sledgehammer_Reconstruct.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 :
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    23
    params -> mode -> 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
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    33
open ATP_Proof_Reconstruct
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
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    36
open Sledgehammer_Provers
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    37
open Sledgehammer_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48321
diff changeset
    38
open Sledgehammer_MaSh
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    39
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    40
val someN = "some"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    41
val noneN = "none"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    42
val timeoutN = "timeout"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    43
val unknownN = "unknown"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    44
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    45
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
    46
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    47
fun max_outcome_code codes =
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    48
  NONE
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    49
  |> fold (fn candidate =>
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    50
              fn accum as SOME _ => accum
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    51
               | 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
    52
                         else NONE)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    53
          ordered_outcome_codes
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    54
  |> the_default unknownN
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    55
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41180
diff changeset
    56
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    57
                       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
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    67
fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
43059
95b845a0edce make all messages urgent in verbose mode
blanchet
parents: 43058
diff changeset
    68
                              timeout, expect, ...})
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    69
        mode minimize_command only learn
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    70
        {state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    71
  let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    72
    val ctxt = Proof.context_of state
50749
82dee320d340 increased hard timeout -- minimization can take time
blanchet
parents: 50669
diff changeset
    73
    val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    74
    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
    75
    val death_time = Time.+ (birth_time, hard_timeout)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    76
    val max_facts =
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51741
diff changeset
    77
      max_facts |> the_default (default_max_facts_of_prover ctxt slice name)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    78
    val num_facts = length facts |> not only ? Integer.min max_facts
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
    79
    fun desc () =
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    80
      prover_description ctxt params name num_facts subgoal subgoal_count goal
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    81
    val problem =
47904
67663c968d70 distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents: 47531
diff changeset
    82
      {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
    83
       subgoal_count = subgoal_count,
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    84
       factss =
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
    85
         factss
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))}
51009
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
    90
    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
    91
      tag_list 1 used_from
51005
ce4290c33d73 eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents: 51004
diff changeset
    92
      |> map (fn (j, fact) => fact |> apsnd (K j))
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48407
diff changeset
    93
      |> 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
    94
      |> 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
    95
      |> 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
    96
      |> 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
    97
                  " 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
    98
      |> Output.urgent_message
41255
a80024d7b71b added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents: 41245
diff changeset
    99
    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
   100
      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
   101
      |> 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
   102
      |> verbose
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
   103
         ? 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
   104
                   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
   105
                 | _ => ())
43261
a4aeb26a6362 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents: 43233
diff changeset
   106
      |> (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
   107
             (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
   108
              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
   109
              else someN, fn () => message (Lazy.force preplay) ^ message_tail))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   110
    fun go () =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   111
      let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   112
        val (outcome_code, message) =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   113
          if debug then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   114
            really_go ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   115
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   116
            (really_go ()
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   117
             handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   118
                  | exn =>
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   119
                    if Exn.is_interrupt exn then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   120
                      reraise exn
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   121
                    else
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   122
                      (unknownN, fn () => "Internal error:\n" ^
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   123
                                          ML_Compiler.exn_message exn ^ "\n"))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   124
        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
   125
          (* 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
   126
             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
   127
             machine. *)
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
   128
          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
   129
             not (is_prover_installed ctxt name) then
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   130
            ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   131
          else if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   132
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   133
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   134
            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
   135
      in (outcome_code, message) end
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   136
  in
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   137
    if mode = Auto_Try then
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50201
diff changeset
   138
      let val (outcome_code, message) = time_limit timeout go () in
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   139
        (outcome_code,
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   140
         state
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   141
         |> outcome_code = someN
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   142
            ? Proof.goal_message (fn () =>
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   143
                  [Pretty.str "",
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49914
diff changeset
   144
                   Pretty.mark Markup.intensify (Pretty.str (message ()))]
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   145
                  |> Pretty.chunks))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   146
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   147
    else if blocking then
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   148
      let
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   149
        val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   150
      in
43058
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   151
        (if outcome_code = someN orelse mode = Normal then
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   152
           quote name ^ ": " ^ message ()
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   153
         else
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   154
           "")
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   155
        |> Async_Manager.break_into_chunks
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   156
        |> List.app Output.urgent_message;
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   157
        (outcome_code, state)
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   158
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   159
    else
52048
9003b293e775 tuned signature -- emphasize thread creation here;
wenzelm
parents: 51998
diff changeset
   160
      (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
   161
                            ((fn (outcome_code, message) =>
43059
95b845a0edce make all messages urgent in verbose mode
blanchet
parents: 43058
diff changeset
   162
                                 (verbose orelse outcome_code = someN,
95b845a0edce make all messages urgent in verbose mode
blanchet
parents: 43058
diff changeset
   163
                                  message ())) o go);
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   164
       (unknownN, state))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   165
  end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   166
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   167
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
   168
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   169
fun eq_facts p = eq_list (op = o pairself fst) p
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   170
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   171
fun string_of_facts facts =
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   172
  "Including " ^ string_of_int (length facts) ^
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   173
  " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   174
  (facts |> map (fst o fst) |> space_implode " ") ^ "."
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   175
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   176
fun string_of_factss factss =
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   177
  if forall (null o snd) factss then
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   178
    "Found no relevant facts."
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   179
  else case factss of
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   180
    [(_, facts)] => string_of_facts facts
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   181
  | _ =>
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   182
    factss
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   183
    |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   184
    |> space_implode "\n\n"
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   185
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   186
fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts,
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   187
                                 slice, ...})
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   188
        mode 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
   189
  if null provers then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   190
    error "No prover is set."
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   191
  else case subgoal_count state of
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   192
    0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state)))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   193
  | n =>
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   194
    let
39364
61f0d36840c5 Sledgehammer should be called in "prove" mode;
blanchet
parents: 39338
diff changeset
   195
      val _ = Proof.assert_backward state
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   196
      val print = if mode = Normal 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
   197
      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
   198
        state |> Proof.map_context (Config.put SMT_Config.verbose debug)
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   199
      val ctxt = Proof.context_of state
48396
dd82d190c2af name tuning
blanchet
parents: 48394
diff changeset
   200
      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
   201
      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
   202
      val ho_atp = exists (is_ho_atp ctxt) provers
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
   203
      val reserved = reserved_isar_keyword_table ()
48396
dd82d190c2af name tuning
blanchet
parents: 48394
diff changeset
   204
      val css = clasimpset_rule_table_of ctxt
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48399
diff changeset
   205
      val all_facts =
48396
dd82d190c2af name tuning
blanchet
parents: 48394
diff changeset
   206
        nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
dd82d190c2af name tuning
blanchet
parents: 48394
diff changeset
   207
                         concl_t
44586
eeba1eedf32d improved handling of induction rules in Sledgehammer
nik
parents: 44585
diff changeset
   208
      val _ = () |> not blocking ? kill_provers
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41432
diff changeset
   209
      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
   210
                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
   211
              | NONE => ()
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   212
      val _ = print "Sledgehammering..."
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   213
      val (smts, (ueq_atps, full_atps)) =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   214
        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
   215
                ||> List.partition (is_unit_equational_atp ctxt)
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   216
      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
   217
        let
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   218
          val max_max_facts =
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   219
            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
   220
              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
   221
            | NONE =>
51998
f732a674db1b renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents: 51741
diff changeset
   222
              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
   223
                        provers
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   224
                |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
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
   225
        in
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48399
diff changeset
   226
          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
   227
          |> (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
   228
                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
   229
              | NONE => I)
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   230
          |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   231
                            hyp_ts concl_t
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   232
          |> 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
   233
                     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
   234
                       label ^ plural_s (length provers) ^ ": " ^
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   235
                       string_of_factss factss
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   236
                       |> 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
   237
                     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
   238
                       ())
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
   239
        end
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   240
      fun launch_provers state label is_appropriate_prop provers =
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   241
        let
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   242
          val factss = get_factss label is_appropriate_prop provers
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   243
          val problem =
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   244
            {state = state, goal = goal, subgoal = i, subgoal_count = n,
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   245
             factss = factss}
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   246
          fun learn prover =
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   247
            mash_learn_proof ctxt params prover (prop_of goal) all_facts
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   248
          val launch = launch_prover params mode minimize_command only learn
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   249
        in
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   250
          if mode = Auto_Try then
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   251
            (unknownN, state)
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   252
            |> fold (fn prover => fn accum as (outcome_code, _) =>
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   253
                        if outcome_code = someN then accum
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   254
                        else launch problem prover)
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   255
                    provers
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   256
          else
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   257
            provers
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   258
            |> (if blocking then Par_List.map else map) (launch problem #> fst)
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   259
            |> max_outcome_code |> rpair state
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   260
        end
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42946
diff changeset
   261
      fun launch_atps label is_appropriate_prop atps accum =
42946
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   262
        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
   263
          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
   264
        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
   265
                not (the is_appropriate_prop concl_t) then
42946
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   266
          (if verbose orelse length atps = length provers then
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   267
             "Goal outside the scope of " ^
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   268
             space_implode " " (serial_commas "and" (map quote atps)) ^ "."
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   269
             |> Output.urgent_message
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   270
           else
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   271
             ();
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   272
           accum)
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   273
        else
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   274
          launch_provers state label is_appropriate_prop atps
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
   275
      fun launch_smts accum =
51006
0ecffccf9359 simplified SMT solver code in Sledgehammer
blanchet
parents: 51005
diff changeset
   276
        if null smts then accum else launch_provers state "SMT solver" NONE smts
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
   277
      val launch_full_atps = launch_atps "ATP" NONE full_atps
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   278
      val launch_ueq_atps =
51741
blanchet
parents: 51187
diff changeset
   279
        launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps
41262
095ecb0c687f factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents: 41260
diff changeset
   280
      fun launch_atps_and_smt_solvers () =
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
   281
        [launch_full_atps, launch_smts, launch_ueq_atps]
46892
9920f9a75b51 Par_List.map is already smart;
wenzelm
parents: 46409
diff changeset
   282
        |> Par_List.map (fn f => ignore (f (unknownN, state)))
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   283
        handle ERROR msg => (print ("Error: " ^ msg); error msg)
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   284
      fun maybe f (accum as (outcome_code, _)) =
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   285
        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
   286
    in
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   287
      (unknownN, state)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   288
      |> (if blocking then
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   289
            launch_full_atps
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   290
            #> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   291
          else
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   292
            (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   293
      handle TimeLimit.TimeOut =>
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   294
             (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
   295
    end
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   296
    |> `(fn (outcome_code, _) => outcome_code = someN)
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
   297
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   298
end;