src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Sun, 22 May 2011 14:51:42 +0200
changeset 42946 ddff373cf3ad
parent 42944 9e620869a576
child 42952 96f62b77748f
permissions -rw-r--r--
added message when Waldmeister isn't run
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
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    11
  type relevance_override = Sledgehammer_Filter.relevance_override
40068
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
    12
  type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    13
  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
    14
  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
    15
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    16
  val auto_minimize_min_facts : int Config.T
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
    17
  val get_minimizing_prover : Proof.context -> bool -> string -> prover
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
    18
  val run_sledgehammer :
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
    19
    params -> bool -> int -> relevance_override -> (string -> minimize_command)
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
    20
    -> Proof.state -> bool * Proof.state
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    21
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    22
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    23
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    24
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    25
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    26
open Sledgehammer_Util
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    27
open Sledgehammer_Filter
40068
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
    28
open Sledgehammer_ATP_Translate
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    29
open Sledgehammer_Provers
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    30
open Sledgehammer_Minimize
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    31
41208
1b28c43a7074 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents: 41180
diff changeset
    32
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    33
                       n goal =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    34
  quote name ^
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    35
  (if verbose then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    36
     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    37
   else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    38
     "") ^
41743
blanchet
parents: 41742
diff changeset
    39
  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    40
  (if blocking then
41743
blanchet
parents: 41742
diff changeset
    41
     "."
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    42
   else
41743
blanchet
parents: 41742
diff changeset
    43
     ":\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
    44
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    45
val auto_minimize_min_facts =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    46
  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    47
      (fn generic => Config.get_generic generic binary_min_facts)
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    48
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
    49
fun get_minimizing_prover ctxt auto name
41742
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
    50
        (params as {debug, verbose, explicit_apply, ...}) 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
    51
        (problem as {state, subgoal, subgoal_count, facts, ...}) =
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
    52
  get_prover ctxt auto name params minimize_command problem
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
    53
  |> (fn result as {outcome, used_facts, run_time_in_msecs, 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
    54
         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
    55
           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
    56
         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
    57
           let
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
    58
             val (used_facts, message) =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    59
               if length used_facts
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42642
diff changeset
    60
                  >= Config.get ctxt auto_minimize_min_facts then
41742
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
    61
                 minimize_facts name params (SOME explicit_apply) (not verbose)
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
    62
                     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
    63
                     (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
    64
                          (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
    65
                 |>> 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
    66
               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
    67
                 (SOME used_facts, 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
    68
           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
    69
             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
    70
               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
    71
               (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
    72
                  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
    73
                  |> 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
    74
                             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
    75
                  |> 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
    76
                  |> 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
    77
                  |> 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
    78
                  |> 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
    79
                              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
    80
                              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
    81
                  |> 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
    82
                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
    83
                  ();
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
                {outcome = NONE, 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
    85
                 run_time_in_msecs = run_time_in_msecs, message = 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
    86
             | 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
    87
           end)
41262
095ecb0c687f factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents: 41260
diff changeset
    88
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
    89
fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
    90
                              expect, ...})
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
    91
        auto minimize_command only
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
    92
        {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    93
  let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    94
    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
    95
    val hard_timeout = Time.+ (timeout, timeout)
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    96
    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
    97
    val death_time = Time.+ (birth_time, hard_timeout)
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    98
    val max_relevant =
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
    99
      max_relevant
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   100
      |> the_default (default_max_relevant_for_prover ctxt slicing name)
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   101
    val num_facts = length facts |> not only ? Integer.min max_relevant
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   102
    val desc =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   103
      prover_description ctxt params name num_facts subgoal subgoal_count goal
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   104
    val problem =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   105
      {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
   106
       subgoal_count = subgoal_count, facts = facts |> take num_facts,
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   107
       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
   108
    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
   109
      problem
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
   110
      |> get_minimizing_prover ctxt auto name params (minimize_command name)
41262
095ecb0c687f factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents: 41260
diff changeset
   111
      |> (fn {outcome, message, ...} =>
095ecb0c687f factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents: 41260
diff changeset
   112
             (if is_some outcome then "none" else "some" (* sic *), message))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   113
    fun go () =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   114
      let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   115
        val (outcome_code, message) =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   116
          if debug then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   117
            really_go ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   118
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   119
            (really_go ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   120
             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   121
                  | exn =>
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   122
                    if Exn.is_interrupt exn then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   123
                      reraise exn
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   124
                    else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   125
                      ("unknown", "Internal error:\n" ^
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   126
                                  ML_Compiler.exn_message exn ^ "\n"))
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   127
        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
   128
          (* 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
   129
             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
   130
             machine. *)
43e2b051339c weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents: 41138
diff changeset
   131
          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
   132
             not (is_prover_installed ctxt name) then
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   133
            ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   134
          else if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   135
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   136
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   137
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   138
      in (outcome_code = "some", message) end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   139
  in
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   140
    if auto then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   141
      let val (success, message) = TimeLimit.timeLimit timeout go () in
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   142
        (success, state |> success ? Proof.goal_message (fn () =>
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
   143
             Pretty.chunks [Pretty.str "",
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
   144
                            Pretty.mark Markup.hilite (Pretty.str message)]))
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   145
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   146
    else if blocking then
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
   147
      let val (success, message) = TimeLimit.timeLimit hard_timeout go () in
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   148
        List.app Output.urgent_message
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   149
                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   150
        (success, state)
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   151
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   152
    else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   153
      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   154
       (false, state))
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   155
  end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   156
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
   157
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
   158
  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
   159
       |> 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
   160
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
   161
(* Makes backtraces more transparent and might be more efficient as well. *)
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
   162
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
   163
  | 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
   164
  | 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
   165
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   166
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
   167
  | 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
   168
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42544
diff changeset
   169
val auto_max_relevant_divisor = 2 (* FUDGE *)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   170
42946
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   171
fun run_sledgehammer (params as {debug, verbose, blocking, provers,
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   172
                                 relevance_thresholds, max_relevant, slicing,
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   173
                                 timeout, ...})
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
   174
        auto 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
   175
  if null provers then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   176
    error "No prover is set."
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   177
  else case subgoal_count state of
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40114
diff changeset
   178
    0 => (Output.urgent_message "No subgoal!"; (false, state))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   179
  | n =>
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   180
    let
39364
61f0d36840c5 Sledgehammer should be called in "prove" mode;
blanchet
parents: 39338
diff changeset
   181
      val _ = Proof.assert_backward state
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   182
      val print = if auto then K () else Output.urgent_message
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
   183
      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
   184
        state |> Proof.map_context (Config.put SMT_Config.verbose debug)
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   185
      val ctxt = Proof.context_of state
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   186
      val {facts = chained_ths, goal, ...} = Proof.goal state
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   187
      val (_, hyp_ts, concl_t) = strip_subgoal goal i
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   188
      val _ = () |> not blocking ? kill_provers
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41432
diff changeset
   189
      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
   190
                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
   191
              | NONE => ()
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   192
      val _ = print "Sledgehammering..."
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   193
      val (smts, (ueq_atps, full_atps)) =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   194
        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
   195
                ||> List.partition (is_unit_equational_atp ctxt)
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   196
      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
   197
        let
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   198
          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
   199
          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
   200
          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
   201
                      |> 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
   202
          val problem =
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   203
            {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
   204
             facts = facts,
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   205
             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
   206
                  (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
42444
8e5438dc70bb cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents: 42443
diff changeset
   207
          val launch = launch_prover params auto 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
   208
        in
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   209
          if auto then
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   210
            fold (fn prover => fn (true, state) => (true, state)
41262
095ecb0c687f factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents: 41260
diff changeset
   211
                                | (false, _) => launch problem prover)
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   212
                 provers (false, state)
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   213
          else
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   214
            provers
41262
095ecb0c687f factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents: 41260
diff changeset
   215
            |> (if blocking then smart_par_list_map else map) (launch problem)
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   216
            |> exists fst |> rpair state
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   217
        end
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   218
      fun get_facts label is_good_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
   219
        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
   220
          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
   221
            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
   222
              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
   223
            | NONE =>
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   224
              0 |> fold (Integer.max
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42361
diff changeset
   225
                         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
   226
                        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
   227
                |> auto ? (fn n => n div auto_max_relevant_divisor)
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
          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
   229
            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
   230
        in
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   231
          relevant_facts ctxt relevance_thresholds max_max_relevant is_good_prop
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42544
diff changeset
   232
                         is_built_in_const relevance_fudge relevance_override
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42544
diff changeset
   233
                         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
   234
          |> 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
   235
                     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
   236
                       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
   237
                       (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
   238
                          "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
   239
                        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
   240
                          "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
   241
                          " 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
   242
                          (facts |> map (fst o fst) |> space_implode " ") ^ ".")
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   243
                       |> 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
   244
                     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
   245
                       ())
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
   246
        end
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   247
      fun launch_atps label is_good_prop atps accum =
42946
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   248
        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
   249
          accum
42946
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   250
        else if not (is_good_prop concl_t) then
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   251
          (if verbose orelse length atps = length provers then
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   252
             "Goal outside the scope of " ^
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   253
             space_implode " " (serial_commas "and" (map quote atps)) ^ "."
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   254
             |> Output.urgent_message
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   255
           else
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   256
             ();
ddff373cf3ad added message when Waldmeister isn't run
blanchet
parents: 42944
diff changeset
   257
           accum)
41256
0e7d45cc005f put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents: 41255
diff changeset
   258
        else
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   259
          launch_provers state
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   260
              (get_facts label is_good_prop atp_relevance_fudge o K atps)
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   261
              (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
   262
      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
   263
        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
   264
          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
   265
        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
   266
          let
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   267
            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
   268
            val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   269
            fun smt_filter facts =
41788
adfd365c7ea4 added a timeout around SMT preprocessing (notably monomorphization)
blanchet
parents: 41773
diff changeset
   270
              (if debug then curry (op o) SOME
adfd365c7ea4 added a timeout around SMT preprocessing (notably monomorphization)
blanchet
parents: 41773
diff changeset
   271
               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
   272
                  (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
   273
          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
   274
            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
   275
                 |> AList.group (op =)
41741
839d1488045f renamed field
blanchet
parents: 41727
diff changeset
   276
                 |> map (launch_provers state (K facts) weight smt_filter o snd)
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
   277
                 |> exists fst |> rpair 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
   278
          end
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   279
      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
   280
      val launch_ueq_atps =
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   281
        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
   282
      fun launch_atps_and_smt_solvers () =
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   283
        [launch_full_atps, launch_ueq_atps, launch_smts]
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
   284
        |> smart_par_list_map (fn f => f (false, state) |> K ())
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   285
        handle ERROR msg => (print ("Error: " ^ msg); error msg)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   286
    in
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   287
      (false, state)
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   288
      |> (if blocking then
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   289
            launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts)
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   290
          else
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42850
diff changeset
   291
            (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
41773
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   292
      handle TimeLimit.TimeOut =>
22d23da89aa5 gracious timeout in "blocking" mode
blanchet
parents: 41746
diff changeset
   293
             (print "Sledgehammer ran out of time."; (false, state))
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   294
    end
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
   295
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   296
end;