src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Wed, 08 Dec 2010 22:17:52 +0100
changeset 41089 2e69fb6331cb
parent 41088 54eb8e7c7f9b
child 41090 b98fe4de1ecd
permissions -rw-r--r--
moved function to later module
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
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    14
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
    15
  val run_sledgehammer :
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    16
    params -> bool -> int -> relevance_override -> (string -> minimize_command)
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
    17
    -> Proof.state -> bool * Proof.state
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    18
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    19
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    20
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    21
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    22
38023
962b0a7f544b more refactoring
blanchet
parents: 38021
diff changeset
    23
open Sledgehammer_Util
38988
483879af0643 finished renaming
blanchet
parents: 38985
diff changeset
    24
open Sledgehammer_Filter
40068
ed2869dd9bfa renamed modules
blanchet
parents: 40065
diff changeset
    25
open Sledgehammer_ATP_Translate
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41066
diff changeset
    26
open Sledgehammer_Provers
40072
27f2a45b0aab more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents: 40071
diff changeset
    27
41089
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    28
fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    29
                       n goal =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    30
  quote name ^
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    31
  (if verbose then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    32
     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    33
   else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    34
     "") ^
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    35
  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    36
  (if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    37
     ""
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    38
   else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    39
     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    40
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    41
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    42
               auto minimize_command only
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    43
               {state, goal, subgoal, subgoal_count, facts} name =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    44
  let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    45
    val ctxt = Proof.context_of state
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    46
    val birth_time = Time.now ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    47
    val death_time = Time.+ (birth_time, timeout)
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    48
    val max_relevant =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    49
      the_default (default_max_relevant_for_prover ctxt name) max_relevant
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    50
    val num_facts = length facts |> not only ? Integer.min max_relevant
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    51
    val desc =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    52
      prover_description ctxt params name num_facts subgoal subgoal_count goal
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    53
    val prover = get_prover ctxt auto name
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    54
    val problem =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    55
      {state = state, goal = goal, subgoal = subgoal,
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    56
       subgoal_count = subgoal_count, facts = take num_facts facts}
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    57
    fun go () =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    58
      let
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    59
        fun really_go () =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    60
          prover params (minimize_command name) problem
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    61
          |> (fn {outcome, message, ...} =>
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    62
                 (if is_some outcome then "none" else "some", message))
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    63
        val (outcome_code, message) =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    64
          if debug then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    65
            really_go ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    66
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    67
            (really_go ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    68
             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    69
                  | exn =>
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    70
                    if Exn.is_interrupt exn then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    71
                      reraise exn
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    72
                    else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    73
                      ("unknown", "Internal error:\n" ^
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    74
                                  ML_Compiler.exn_message exn ^ "\n"))
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    75
        val _ =
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    76
          if expect = "" orelse outcome_code = expect then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    77
            ()
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    78
          else if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    79
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    80
          else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    81
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    82
      in (outcome_code = "some", message) end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    83
  in
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    84
    if auto then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    85
      let val (success, message) = TimeLimit.timeLimit timeout go () in
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    86
        (success, state |> success ? Proof.goal_message (fn () =>
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    87
             Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    88
                 (Pretty.str message)]))
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    89
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    90
    else if blocking then
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    91
      let val (success, message) = TimeLimit.timeLimit timeout go () in
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    92
        List.app Output.urgent_message
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    93
                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    94
        (success, state)
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    95
      end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    96
    else
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    97
      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    98
       (false, state))
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
    99
  end
2e69fb6331cb moved function to later module
blanchet
parents: 41088
diff changeset
   100
40698
8a3f7ea91370 cosmetics
blanchet
parents: 40693
diff changeset
   101
(* FUDGE *)
8a3f7ea91370 cosmetics
blanchet
parents: 40693
diff changeset
   102
val auto_max_relevant_divisor = 2
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   103
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   104
fun fact_name (Untranslated ((name, _), _)) = SOME name
41088
54eb8e7c7f9b clarified terminology
blanchet
parents: 41087
diff changeset
   105
  | fact_name (ATP_Translated (_, p)) = Option.map (fst o fst) p
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   106
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   107
fun run_sledgehammer (params as {blocking, debug, provers, full_types,
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40068
diff changeset
   108
                                 relevance_thresholds, max_relevant, ...})
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
   109
                     auto i (relevance_override as {only, ...}) minimize_command
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39364
diff changeset
   110
                     state =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   111
  if null provers then
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   112
    error "No prover is set."
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   113
  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
   114
    0 => (Output.urgent_message "No subgoal!"; (false, state))
39318
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   115
  | n =>
ad9a1f9b0558 implemented Auto Sledgehammer
blanchet
parents: 39263
diff changeset
   116
    let
39364
61f0d36840c5 Sledgehammer should be called in "prove" mode;
blanchet
parents: 39338
diff changeset
   117
      val _ = Proof.assert_backward state
40200
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   118
      val ctxt = Proof.context_of state
870818d2b56b remove needless context argument;
blanchet
parents: 40190
diff changeset
   119
      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
   120
      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
   121
      val _ = () |> not blocking ? kill_provers
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   122
      val _ = case find_first (not o is_prover_available ctxt) provers of
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   123
                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
   124
              | NONE => ()
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40114
diff changeset
   125
      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   126
      val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   127
      fun run_provers label full_types relevance_fudge maybe_translate provers
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   128
                      (res as (success, state)) =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   129
        if success orelse null provers then
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   130
          res
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   131
        else
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   132
          let
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   133
            val max_max_relevant =
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   134
              case max_relevant of
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   135
                SOME n => n
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   136
              | NONE =>
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40723
diff changeset
   137
                0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   138
                          provers
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   139
                  |> auto ? (fn n => n div auto_max_relevant_divisor)
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   140
            val is_built_in_const =
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   141
              is_built_in_const_for_prover ctxt (hd provers)
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40202
diff changeset
   142
            val facts =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   143
              relevant_facts ctxt full_types relevance_thresholds
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40341
diff changeset
   144
                             max_max_relevant is_built_in_const relevance_fudge
40071
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   145
                             relevance_override chained_ths hyp_ts concl_t
40114
blanchet
parents: 40072
diff changeset
   146
              |> map maybe_translate
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   147
            val problem =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   148
              {state = state, goal = goal, subgoal = i, subgoal_count = n,
40983
07526f546680 handle "max_relevant" uniformly
blanchet
parents: 40982
diff changeset
   149
               facts = facts}
07526f546680 handle "max_relevant" uniformly
blanchet
parents: 40982
diff changeset
   150
            val run_prover = run_prover params auto minimize_command only
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   151
          in
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   152
            if debug then
40370
14456fd302f0 cosmetics
blanchet
parents: 40369
diff changeset
   153
              Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   154
                  (if null facts then
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   155
                     "Found no relevant facts."
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   156
                   else
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   157
                     "Including (up to) " ^ string_of_int (length facts) ^
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   158
                     " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   159
                     (facts |> map_filter fact_name
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   160
                            |> space_implode " ") ^ "."))
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   161
            else
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   162
              ();
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   163
            if auto then
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   164
              fold (fn prover => fn (true, state) => (true, state)
40064
db8413d82c3b got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents: 40063
diff changeset
   165
                                  | (false, _) => run_prover problem prover)
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   166
                   provers (false, state)
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   167
            else
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   168
              provers |> (if blocking then Par_List.map else map)
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   169
                             (run_prover problem)
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   170
                      |> exists fst |> rpair state
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   171
          end
40071
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   172
      val run_atps =
40370
14456fd302f0 cosmetics
blanchet
parents: 40369
diff changeset
   173
        run_provers "ATP" full_types atp_relevance_fudge
41088
54eb8e7c7f9b clarified terminology
blanchet
parents: 41087
diff changeset
   174
                    (ATP_Translated o translate_atp_fact ctxt) atps
40071
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   175
      val run_smts =
40370
14456fd302f0 cosmetics
blanchet
parents: 40369
diff changeset
   176
        run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   177
      fun run_atps_and_smt_solvers () =
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   178
        [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   179
    in
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   180
      (false, state)
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   181
      |> (if blocking then run_atps #> not auto ? run_smts
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40064
diff changeset
   182
          else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   183
    end
38044
463177795c49 minor refactoring
blanchet
parents: 38040
diff changeset
   184
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   185
end;