src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Tue, 31 May 2011 16:38:36 +0200
changeset 43085 0a2f5b86bdd7
parent 43064 b6e61d22fa61
child 43164 b4edfe260d54
permissions -rw-r--r--
first step in sharing more code between ATP and Metis translation
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
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    11
  type minimize_command = ATP_Reconstruct.minimize_command
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    12
  type relevance_override = Sledgehammer_Filter.relevance_override
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
    13
  type mode = Sledgehammer_Provers.mode
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    14
  type params = Sledgehammer_Provers.params
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
    15
  type prover = Sledgehammer_Provers.prover
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
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    21
  val auto_minimize_min_facts : int Config.T
43058
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
    22
  val auto_minimize_max_seconds : real Config.T
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
    23
  val get_minimizing_prover : Proof.context -> mode -> string -> prover
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
    24
  val run_sledgehammer :
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
    25
    params -> mode -> int -> relevance_override -> (string -> minimize_command)
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
    26
    -> Proof.state -> bool * (string * Proof.state)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    27
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    28
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    29
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    30
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    31
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    32
open ATP_Util
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    33
open ATP_Translate
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    34
open ATP_Reconstruct
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    35
open Sledgehammer_Util
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    36
open Sledgehammer_Filter
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
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 =
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    58
  (name,
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) ^
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    64
   (if blocking then
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    65
      "."
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
    66
    else
43037
ade5c84f860f cleanup proof text generation code
blanchet
parents: 43027
diff changeset
    67
      "\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
    68
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    69
val auto_minimize_min_facts =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    70
  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
42968
74415622d293 more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents: 42966
diff changeset
    71
      (fn generic => Config.get_generic generic binary_min_facts)
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    72
val auto_minimize_max_seconds =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    73
  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds}
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    74
      (K 5.0)
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    75
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
    76
fun get_minimizing_prover ctxt mode name
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43059
diff changeset
    77
        (params as {debug, verbose, ...}) minimize_command
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
    78
        (problem as {state, subgoal, subgoal_count, facts, ...}) =
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
    79
  get_prover ctxt mode name params minimize_command problem
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    80
  |> (fn result as {outcome, used_facts, run_time_in_msecs, preplay, message} =>
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
    81
         if is_some outcome then
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
    82
           result
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
    83
         else
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
    84
           let
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    85
             val num_facts = length used_facts
43058
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
    86
             fun can_minimize_fast_enough msecs =
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
    87
               0.001 * Real.fromInt ((num_facts + 2) * msecs)
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
    88
               <= Config.get ctxt auto_minimize_max_seconds
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    89
             val ((minimize, minimize_name), preplay) =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    90
               if mode = Normal then
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    91
                 if num_facts >= Config.get ctxt auto_minimize_min_facts then
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    92
                   ((true, name), preplay)
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    93
                 else
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    94
                   let val preplay = preplay () in
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    95
                     (case preplay of
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
    96
                        Played (reconstructor, timeout) =>
43058
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
    97
                        (can_minimize_fast_enough (Time.toMilliseconds timeout),
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
    98
                         reconstructor_name reconstructor)
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
    99
                      | _ =>
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   100
                        case run_time_in_msecs of
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   101
                          SOME msecs => (can_minimize_fast_enough msecs, name)
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   102
                        | NONE => (false, name),
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   103
                     K preplay)
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   104
                   end
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   105
               else
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   106
                 ((false, name), preplay)
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   107
             val (used_facts, (preplay, message)) =
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   108
               if minimize then
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43059
diff changeset
   109
                 minimize_facts minimize_name params
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   110
                     (not verbose) subgoal subgoal_count state
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
   111
                     (filter_used_facts used_facts
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
                          (map (apsnd single o untranslated_fact) facts))
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
   113
                 |>> Option.map (map fst)
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
   114
               else
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   115
                 (SOME used_facts, (preplay, message))
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
   116
           in
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
   117
             case used_facts of
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
   118
               SOME used_facts =>
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
   119
               (if debug andalso not (null used_facts) then
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
   120
                  facts ~~ (0 upto length facts - 1)
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
   121
                  |> map (fn (fact, j) =>
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
   122
                             fact |> untranslated_fact |> apsnd (K j))
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
   123
                  |> filter_used_facts used_facts
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
   124
                  |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
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
   125
                  |> commas
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
   126
                  |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^
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
   127
                              quote name ^ " proof (of " ^
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
   128
                              string_of_int (length facts) ^ "): ") "."
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
   129
                  |> Output.urgent_message
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
   130
                else
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
   131
                  ();
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
   132
                {outcome = NONE, used_facts = used_facts,
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   133
                 run_time_in_msecs = run_time_in_msecs, preplay = preplay,
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   134
                 message = message})
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
   135
             | NONE => result
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
   136
           end)
41262
095ecb0c687f factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents: 41260
diff changeset
   137
43059
95b845a0edce make all messages urgent in verbose mode
blanchet
parents: 43058
diff changeset
   138
fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
95b845a0edce make all messages urgent in verbose mode
blanchet
parents: 43058
diff changeset
   139
                              timeout, expect, ...})
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   140
        mode minimize_command only
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   141
        {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   142
  let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   143
    val ctxt = Proof.context_of state
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
   144
    val hard_timeout = Time.+ (timeout, timeout)
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   145
    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
   146
    val death_time = Time.+ (birth_time, hard_timeout)
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   147
    val max_relevant =
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   148
      max_relevant
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   149
      |> the_default (default_max_relevant_for_prover ctxt slicing name)
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   150
    val num_facts = length facts |> not only ? Integer.min max_relevant
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   151
    fun desc () =
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   152
      prover_description ctxt params name num_facts subgoal subgoal_count goal
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   153
    val problem =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   154
      {state = state, goal = goal, subgoal = subgoal,
42638
a7a30721767a have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents: 42613
diff changeset
   155
       subgoal_count = subgoal_count, facts = facts |> take num_facts,
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   156
       smt_filter = smt_filter}
41255
a80024d7b71b added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents: 41245
diff changeset
   157
    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
   158
      problem
43051
d7075adac3bd minimize with Metis if possible
blanchet
parents: 43043
diff changeset
   159
      |> get_minimizing_prover ctxt mode name params minimize_command
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   160
      |> (fn {outcome, preplay, message, ...} =>
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   161
             (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
   162
              else if is_some outcome then noneN
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   163
              else someN, message o preplay))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   164
    fun go () =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   165
      let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   166
        val (outcome_code, message) =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   167
          if debug then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   168
            really_go ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   169
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   170
            (really_go ()
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   171
             handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   172
                  | exn =>
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   173
                    if Exn.is_interrupt exn then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   174
                      reraise exn
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   175
                    else
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   176
                      (unknownN, fn () => "Internal error:\n" ^
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   177
                                          ML_Compiler.exn_message exn ^ "\n"))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   178
        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
   179
          (* 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
   180
             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
   181
             machine. *)
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
   182
          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
   183
             not (is_prover_installed ctxt name) then
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   184
            ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   185
          else if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   186
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   187
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   188
            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
   189
      in (outcome_code, message) end
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   190
  in
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   191
    if mode = Auto_Try then
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   192
      let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   193
        (outcome_code,
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   194
         state
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   195
         |> outcome_code = someN
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   196
            ? Proof.goal_message (fn () =>
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   197
                  [Pretty.str "",
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   198
                   Pretty.mark Markup.hilite (Pretty.str (message ()))]
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   199
                  |> Pretty.chunks))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   200
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   201
    else if blocking then
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   202
      let
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   203
        val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   204
      in
43058
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   205
        (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
   206
           quote name ^ ": " ^ message ()
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   207
         else
5f8bac7a2945 minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents: 43052
diff changeset
   208
           "")
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   209
        |> Async_Manager.break_into_chunks
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 43004
diff changeset
   210
        |> List.app Output.urgent_message;
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   211
        (outcome_code, state)
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   212
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   213
    else
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   214
      (Async_Manager.launch das_tool 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
   215
                            ((fn (outcome_code, message) =>
43059
95b845a0edce make all messages urgent in verbose mode
blanchet
parents: 43058
diff changeset
   216
                                 (verbose orelse outcome_code = someN,
95b845a0edce make all messages urgent in verbose mode
blanchet
parents: 43058
diff changeset
   217
                                  message ())) o go);
43006
ff631c45797e make output more concise
blanchet
parents: 43005
diff changeset
   218
       (unknownN, state))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   219
  end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   220
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
   221
fun class_of_smt_solver ctxt name =
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
   222
  ctxt |> select_smt_solver name
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
       |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
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
   224
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
   225
(* Makes backtraces more transparent and might well be more efficient as
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
   226
   well. *)
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
   227
fun smart_par_list_map _ [] = []
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
   228
  | smart_par_list_map f [x] = [f x]
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
   229
  | smart_par_list_map f xs = Par_List.map f xs
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
   230
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   231
fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   232
  | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   233
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   234
val auto_try_max_relevant_divisor = 2 (* FUDGE *)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   235
42946
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   236
fun run_sledgehammer (params as {debug, verbose, blocking, provers,
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   237
                                 relevance_thresholds, max_relevant, slicing,
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   238
                                 timeout, ...})
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   239
        mode i (relevance_override as {only, ...}) minimize_command state =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   240
  if null provers then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   241
    error "No prover is set."
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   242
  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
   243
    0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state)))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   244
  | n =>
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   245
    let
39364
61f0d36840c5 Sledgehammer should be called in "prove" mode;
blanchet
parents: 39338
diff changeset
   246
      val _ = Proof.assert_backward state
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   247
      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
   248
      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
   249
        state |> Proof.map_context (Config.put SMT_Config.verbose debug)
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   250
      val ctxt = Proof.context_of state
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   251
      val {facts = chained_ths, goal, ...} = Proof.goal state
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
   252
      val chained_ths = chained_ths |> normalize_chained_theorems
43004
20e9caff1f86 fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
blanchet
parents: 42968
diff changeset
   253
      val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   254
      val _ = () |> not blocking ? kill_provers
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41432
diff changeset
   255
      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
   256
                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
   257
              | NONE => ()
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   258
      val _ = print "Sledgehammering..."
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   259
      val (smts, (ueq_atps, full_atps)) =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   260
        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
   261
                ||> List.partition (is_unit_equational_atp ctxt)
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   262
      fun launch_provers state get_facts translate maybe_smt_filter provers =
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   263
        let
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   264
          val facts = get_facts ()
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   265
          val num_facts = length facts
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   266
          val facts = facts ~~ (0 upto num_facts - 1)
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   267
                      |> map (translate num_facts)
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   268
          val problem =
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   269
            {state = state, goal = goal, subgoal = i, subgoal_count = n,
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   270
             facts = facts,
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   271
             smt_filter = maybe_smt_filter
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   272
                  (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   273
          val launch = launch_prover params mode minimize_command only
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   274
        in
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   275
          if mode = Auto_Try orelse mode = Try then
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   276
            (unknownN, state)
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   277
            |> fold (fn prover => fn accum as (outcome_code, _) =>
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   278
                        if outcome_code = someN then accum
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   279
                        else launch problem prover)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   280
                    provers
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   281
          else
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   282
            provers
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   283
            |> (if blocking then smart_par_list_map else map)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   284
                   (launch problem #> fst)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   285
            |> max_outcome_code |> rpair state
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   286
        end
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42946
diff changeset
   287
      fun get_facts label is_appropriate_prop relevance_fudge 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
   288
        let
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
   289
          val max_max_relevant =
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
   290
            case max_relevant of
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
   291
              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
   292
            | NONE =>
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   293
              0 |> fold (Integer.max
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   294
                         o default_max_relevant_for_prover ctxt slicing)
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
   295
                        provers
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   296
                |> mode = Auto_Try
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   297
                   ? (fn n => n div auto_try_max_relevant_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
   298
          val is_built_in_const =
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
   299
            is_built_in_const_for_prover ctxt (hd provers)
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
   300
        in
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42946
diff changeset
   301
          relevant_facts ctxt relevance_thresholds max_max_relevant
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42946
diff changeset
   302
                         is_appropriate_prop is_built_in_const relevance_fudge
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42946
diff changeset
   303
                         relevance_override chained_ths hyp_ts concl_t
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
   304
          |> tap (fn facts =>
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
   305
                     if debug then
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
   306
                       label ^ plural_s (length provers) ^ ": " ^
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
   307
                       (if null facts then
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
   308
                          "Found no relevant facts."
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
   309
                        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
   310
                          "Including (up to) " ^ string_of_int (length facts) ^
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
   311
                          " relevant fact" ^ plural_s (length facts) ^ ":\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
   312
                          (facts |> map (fst o fst) |> space_implode " ") ^ ".")
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   313
                       |> 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
   314
                     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
   315
                       ())
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
   316
        end
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42946
diff changeset
   317
      fun launch_atps label is_appropriate_prop atps accum =
42946
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   318
        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
   319
          accum
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42946
diff changeset
   320
        else if not (is_appropriate_prop concl_t) then
42946
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   321
          (if verbose orelse length atps = length provers then
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   322
             "Goal outside the scope of " ^
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   323
             space_implode " " (serial_commas "and" (map quote atps)) ^ "."
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   324
             |> Output.urgent_message
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   325
           else
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   326
             ();
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   327
           accum)
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   328
        else
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   329
          launch_provers state
42952
96f62b77748f tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents: 42946
diff changeset
   330
              (get_facts label is_appropriate_prop atp_relevance_fudge o K atps)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   331
              (K (Untranslated_Fact o fst)) (K (K NONE)) 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
   332
      fun launch_smts accum =
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
   333
        if null smts 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
   334
          accum
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
   335
        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
   336
          let
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   337
            val facts = get_facts "SMT solver" (K true) smt_relevance_fudge smts
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
   338
            val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   339
            fun smt_filter facts =
41788
adfd365c7ea4 added a timeout around SMT preprocessing (notably monomorphization)
blanchet
parents: 41773
diff changeset
   340
              (if debug then curry (op o) SOME
adfd365c7ea4 added a timeout around SMT preprocessing (notably monomorphization)
blanchet
parents: 41773
diff changeset
   341
               else TimeLimit.timeLimit timeout o try)
41432
3214c39777ab differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents: 41335
diff changeset
   342
                  (SMT_Solver.smt_filter_preprocess state (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
   343
          in
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
   344
            smts |> map (`(class_of_smt_solver ctxt))
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
   345
                 |> AList.group (op =)
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   346
                 |> map (snd #> launch_provers state (K facts) weight smt_filter
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   347
                             #> fst)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   348
                 |> max_outcome_code |> rpair state
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
   349
          end
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   350
      val launch_full_atps = launch_atps "ATP" (K true) full_atps
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   351
      val launch_ueq_atps =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   352
        launch_atps "Unit equational provers" is_unit_equality ueq_atps
41262
095ecb0c687f factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents: 41260
diff changeset
   353
      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
   354
        [launch_full_atps, launch_smts, launch_ueq_atps]
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   355
        |> smart_par_list_map (fn f => ignore (f (unknownN, state)))
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   356
        handle ERROR msg => (print ("Error: " ^ msg); error msg)
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   357
      fun maybe f (accum as (outcome_code, _)) =
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   358
        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
   359
    in
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   360
      (unknownN, state)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   361
      |> (if blocking then
43021
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   362
            launch_full_atps
5910dd009d0e handle non-auto try case of Sledgehammer better
blanchet
parents: 43020
diff changeset
   363
            #> 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
   364
          else
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   365
            (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   366
      handle TimeLimit.TimeOut =>
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   367
             (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
   368
    end
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43006
diff changeset
   369
    |> `(fn (outcome_code, _) => outcome_code = someN)
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
   370
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   371
end;