src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Fri May 27 10:30:07 2011 +0200 (2011-05-27 ago)
changeset 43005 c96f06bffd90
parent 43004 20e9caff1f86
child 43006 ff631c45797e
permissions -rw-r--r--
merge timeout messages from several ATPs into one message to avoid clutter
blanchet@41087
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_run.ML
wenzelm@28477
     2
    Author:     Fabian Immler, TU Muenchen
wenzelm@32996
     3
    Author:     Makarius
blanchet@35969
     4
    Author:     Jasmin Blanchette, TU Muenchen
wenzelm@28477
     5
blanchet@38021
     6
Sledgehammer's heart.
wenzelm@28477
     7
*)
wenzelm@28477
     8
blanchet@41087
     9
signature SLEDGEHAMMER_RUN =
wenzelm@28477
    10
sig
blanchet@38988
    11
  type relevance_override = Sledgehammer_Filter.relevance_override
blanchet@40068
    12
  type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
blanchet@41087
    13
  type params = Sledgehammer_Provers.params
blanchet@41263
    14
  type prover = Sledgehammer_Provers.prover
blanchet@40061
    15
blanchet@42646
    16
  val auto_minimize_min_facts : int Config.T
blanchet@42444
    17
  val get_minimizing_prover : Proof.context -> bool -> string -> prover
blanchet@38044
    18
  val run_sledgehammer :
blanchet@42444
    19
    params -> bool -> int -> relevance_override -> (string -> minimize_command)
blanchet@42444
    20
    -> Proof.state -> bool * Proof.state
wenzelm@28477
    21
end;
wenzelm@28477
    22
blanchet@41087
    23
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
wenzelm@28477
    24
struct
wenzelm@28477
    25
blanchet@38023
    26
open Sledgehammer_Util
blanchet@38988
    27
open Sledgehammer_Filter
blanchet@40068
    28
open Sledgehammer_ATP_Translate
blanchet@41087
    29
open Sledgehammer_Provers
blanchet@41091
    30
open Sledgehammer_Minimize
blanchet@40072
    31
blanchet@41208
    32
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
blanchet@41089
    33
                       n goal =
blanchet@43005
    34
  (name,
blanchet@43005
    35
   (if verbose then
blanchet@43005
    36
      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
blanchet@43005
    37
    else
blanchet@43005
    38
      "") ^
blanchet@43005
    39
   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
blanchet@43005
    40
   (if blocking then
blanchet@43005
    41
      "."
blanchet@43005
    42
    else
blanchet@43005
    43
      ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
blanchet@41089
    44
blanchet@42646
    45
val auto_minimize_min_facts =
blanchet@42646
    46
  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
blanchet@42968
    47
      (fn generic => Config.get_generic generic binary_min_facts)
blanchet@41091
    48
blanchet@42444
    49
fun get_minimizing_prover ctxt auto name
blanchet@41742
    50
        (params as {debug, verbose, explicit_apply, ...}) minimize_command
blanchet@41263
    51
        (problem as {state, subgoal, subgoal_count, facts, ...}) =
blanchet@42444
    52
  get_prover ctxt auto name params minimize_command problem
blanchet@41263
    53
  |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
blanchet@41263
    54
         if is_some outcome then
blanchet@41263
    55
           result
blanchet@41263
    56
         else
blanchet@41263
    57
           let
blanchet@41263
    58
             val (used_facts, message) =
blanchet@42646
    59
               if length used_facts
blanchet@42646
    60
                  >= Config.get ctxt auto_minimize_min_facts then
blanchet@41742
    61
                 minimize_facts name params (SOME explicit_apply) (not verbose)
blanchet@41742
    62
                     subgoal subgoal_count state
blanchet@41263
    63
                     (filter_used_facts used_facts
blanchet@41263
    64
                          (map (apsnd single o untranslated_fact) facts))
blanchet@41263
    65
                 |>> Option.map (map fst)
blanchet@41263
    66
               else
blanchet@41263
    67
                 (SOME used_facts, message)
blanchet@41263
    68
           in
blanchet@41263
    69
             case used_facts of
blanchet@41263
    70
               SOME used_facts =>
blanchet@41263
    71
               (if debug andalso not (null used_facts) then
blanchet@41263
    72
                  facts ~~ (0 upto length facts - 1)
blanchet@41263
    73
                  |> map (fn (fact, j) =>
blanchet@41263
    74
                             fact |> untranslated_fact |> apsnd (K j))
blanchet@41263
    75
                  |> filter_used_facts used_facts
blanchet@41263
    76
                  |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
blanchet@41263
    77
                  |> commas
blanchet@41263
    78
                  |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^
blanchet@41263
    79
                              quote name ^ " proof (of " ^
blanchet@41263
    80
                              string_of_int (length facts) ^ "): ") "."
blanchet@41263
    81
                  |> Output.urgent_message
blanchet@41263
    82
                else
blanchet@41263
    83
                  ();
blanchet@41263
    84
                {outcome = NONE, used_facts = used_facts,
blanchet@41263
    85
                 run_time_in_msecs = run_time_in_msecs, message = message})
blanchet@41263
    86
             | NONE => result
blanchet@41263
    87
           end)
blanchet@41262
    88
blanchet@43005
    89
val someN = "some"
blanchet@43005
    90
val noneN = "none"
blanchet@43005
    91
val timeoutN = "timeout"
blanchet@43005
    92
val unknownN = "unknown"
blanchet@43005
    93
blanchet@42443
    94
fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
blanchet@42443
    95
                              expect, ...})
blanchet@42444
    96
        auto minimize_command only
blanchet@41741
    97
        {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
blanchet@41089
    98
  let
blanchet@41089
    99
    val ctxt = Proof.context_of state
blanchet@42850
   100
    val hard_timeout = Time.+ (timeout, timeout)
blanchet@41089
   101
    val birth_time = Time.now ()
blanchet@42850
   102
    val death_time = Time.+ (birth_time, hard_timeout)
blanchet@41089
   103
    val max_relevant =
blanchet@42443
   104
      max_relevant
blanchet@42443
   105
      |> the_default (default_max_relevant_for_prover ctxt slicing name)
blanchet@41089
   106
    val num_facts = length facts |> not only ? Integer.min max_relevant
blanchet@41089
   107
    val desc =
blanchet@41089
   108
      prover_description ctxt params name num_facts subgoal subgoal_count goal
blanchet@41089
   109
    val problem =
blanchet@41089
   110
      {state = state, goal = goal, subgoal = subgoal,
blanchet@42638
   111
       subgoal_count = subgoal_count, facts = facts |> take num_facts,
blanchet@41741
   112
       smt_filter = smt_filter}
blanchet@41255
   113
    fun really_go () =
blanchet@41263
   114
      problem
blanchet@42444
   115
      |> get_minimizing_prover ctxt auto name params (minimize_command name)
blanchet@41262
   116
      |> (fn {outcome, message, ...} =>
blanchet@43005
   117
             (if outcome = SOME ATP_Proof.TimedOut then timeoutN
blanchet@43005
   118
              else if is_some outcome then noneN
blanchet@43005
   119
              else someN, message))
blanchet@41089
   120
    fun go () =
blanchet@41089
   121
      let
blanchet@41089
   122
        val (outcome_code, message) =
blanchet@41089
   123
          if debug then
blanchet@41089
   124
            really_go ()
blanchet@41089
   125
          else
blanchet@41089
   126
            (really_go ()
blanchet@43005
   127
             handle ERROR message => (unknownN, "Error: " ^ message ^ "\n")
blanchet@41089
   128
                  | exn =>
blanchet@41089
   129
                    if Exn.is_interrupt exn then
blanchet@41089
   130
                      reraise exn
blanchet@41089
   131
                    else
blanchet@43005
   132
                      (unknownN, "Internal error:\n" ^
blanchet@43005
   133
                                ML_Compiler.exn_message exn ^ "\n"))
blanchet@41089
   134
        val _ =
blanchet@41142
   135
          (* The "expect" argument is deliberately ignored if the prover is
blanchet@41142
   136
             missing so that the "Metis_Examples" can be processed on any
blanchet@41142
   137
             machine. *)
blanchet@41142
   138
          if expect = "" orelse outcome_code = expect orelse
blanchet@41142
   139
             not (is_prover_installed ctxt name) then
blanchet@41089
   140
            ()
blanchet@41089
   141
          else if blocking then
blanchet@41089
   142
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
blanchet@41089
   143
          else
blanchet@41089
   144
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
blanchet@43005
   145
      in (outcome_code, message) end
blanchet@41089
   146
  in
blanchet@41089
   147
    if auto then
blanchet@43005
   148
      let
blanchet@43005
   149
        val (outcome_code, message) = TimeLimit.timeLimit timeout go ()
blanchet@43005
   150
        val success = (outcome_code = someN)
blanchet@43005
   151
      in
blanchet@41089
   152
        (success, state |> success ? Proof.goal_message (fn () =>
blanchet@41091
   153
             Pretty.chunks [Pretty.str "",
blanchet@41091
   154
                            Pretty.mark Markup.hilite (Pretty.str message)]))
blanchet@41089
   155
      end
blanchet@41089
   156
    else if blocking then
blanchet@43005
   157
      let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () in
blanchet@43005
   158
        Async_Manager.implode_desc desc ^ "\n" ^ message
blanchet@43005
   159
        |> Async_Manager.break_into_chunks
blanchet@43005
   160
        |> List.app Output.urgent_message;
blanchet@43005
   161
        (outcome_code = someN, state)
blanchet@41089
   162
      end
blanchet@41089
   163
    else
blanchet@43005
   164
      (Async_Manager.launch das_tool birth_time death_time desc
blanchet@43005
   165
                            (apfst (curry (op <>) timeoutN) o go);
blanchet@41089
   166
       (false, state))
blanchet@41089
   167
  end
blanchet@41089
   168
blanchet@41242
   169
fun class_of_smt_solver ctxt name =
blanchet@41242
   170
  ctxt |> select_smt_solver name
blanchet@41242
   171
       |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
blanchet@41242
   172
blanchet@41242
   173
(* Makes backtraces more transparent and might be more efficient as well. *)
blanchet@41242
   174
fun smart_par_list_map _ [] = []
blanchet@41242
   175
  | smart_par_list_map f [x] = [f x]
blanchet@41242
   176
  | smart_par_list_map f xs = Par_List.map f xs
blanchet@41242
   177
blanchet@41256
   178
fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
blanchet@41256
   179
  | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
blanchet@41256
   180
blanchet@42579
   181
val auto_max_relevant_divisor = 2 (* FUDGE *)
blanchet@40060
   182
blanchet@42946
   183
fun run_sledgehammer (params as {debug, verbose, blocking, provers,
blanchet@42946
   184
                                 relevance_thresholds, max_relevant, slicing,
blanchet@42946
   185
                                 timeout, ...})
blanchet@42444
   186
        auto i (relevance_override as {only, ...}) minimize_command state =
blanchet@40059
   187
  if null provers then
blanchet@40059
   188
    error "No prover is set."
blanchet@39318
   189
  else case subgoal_count state of
wenzelm@40132
   190
    0 => (Output.urgent_message "No subgoal!"; (false, state))
blanchet@39318
   191
  | n =>
blanchet@39318
   192
    let
blanchet@39364
   193
      val _ = Proof.assert_backward state
blanchet@41773
   194
      val print = if auto then K () else Output.urgent_message
blanchet@41242
   195
      val state =
blanchet@41242
   196
        state |> Proof.map_context (Config.put SMT_Config.verbose debug)
blanchet@40200
   197
      val ctxt = Proof.context_of state
blanchet@40200
   198
      val {facts = chained_ths, goal, ...} = Proof.goal state
blanchet@43004
   199
      val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
blanchet@40059
   200
      val _ = () |> not blocking ? kill_provers
blanchet@41727
   201
      val _ = case find_first (not o is_prover_supported ctxt) provers of
blanchet@40941
   202
                SOME name => error ("No such prover: " ^ name ^ ".")
blanchet@40941
   203
              | NONE => ()
blanchet@41773
   204
      val _ = print "Sledgehammering..."
blanchet@42944
   205
      val (smts, (ueq_atps, full_atps)) =
blanchet@42944
   206
        provers |> List.partition (is_smt_prover ctxt)
blanchet@42944
   207
                ||> List.partition (is_unit_equational_atp ctxt)
blanchet@41741
   208
      fun launch_provers state get_facts translate maybe_smt_filter provers =
blanchet@41256
   209
        let
blanchet@41256
   210
          val facts = get_facts ()
blanchet@41256
   211
          val num_facts = length facts
blanchet@41256
   212
          val facts = facts ~~ (0 upto num_facts - 1)
blanchet@41256
   213
                      |> map (translate num_facts)
blanchet@41256
   214
          val problem =
blanchet@41256
   215
            {state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@41256
   216
             facts = facts,
blanchet@41741
   217
             smt_filter = maybe_smt_filter
blanchet@41256
   218
                  (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
blanchet@42444
   219
          val launch = launch_prover params auto minimize_command only
blanchet@41256
   220
        in
blanchet@41256
   221
          if auto then
blanchet@41256
   222
            fold (fn prover => fn (true, state) => (true, state)
blanchet@41262
   223
                                | (false, _) => launch problem prover)
blanchet@41256
   224
                 provers (false, state)
blanchet@41256
   225
          else
blanchet@41256
   226
            provers
blanchet@41262
   227
            |> (if blocking then smart_par_list_map else map) (launch problem)
blanchet@41256
   228
            |> exists fst |> rpair state
blanchet@41256
   229
        end
blanchet@42952
   230
      fun get_facts label is_appropriate_prop relevance_fudge provers =
blanchet@41242
   231
        let
blanchet@41242
   232
          val max_max_relevant =
blanchet@41242
   233
            case max_relevant of
blanchet@41242
   234
              SOME n => n
blanchet@41242
   235
            | NONE =>
blanchet@42443
   236
              0 |> fold (Integer.max
blanchet@42443
   237
                         o default_max_relevant_for_prover ctxt slicing)
blanchet@41242
   238
                        provers
blanchet@41242
   239
                |> auto ? (fn n => n div auto_max_relevant_divisor)
blanchet@41242
   240
          val is_built_in_const =
blanchet@41242
   241
            is_built_in_const_for_prover ctxt (hd provers)
blanchet@41242
   242
        in
blanchet@42952
   243
          relevant_facts ctxt relevance_thresholds max_max_relevant
blanchet@42952
   244
                         is_appropriate_prop is_built_in_const relevance_fudge
blanchet@42952
   245
                         relevance_override chained_ths hyp_ts concl_t
blanchet@41242
   246
          |> tap (fn facts =>
blanchet@41242
   247
                     if debug then
blanchet@41242
   248
                       label ^ plural_s (length provers) ^ ": " ^
blanchet@41242
   249
                       (if null facts then
blanchet@41242
   250
                          "Found no relevant facts."
blanchet@41242
   251
                        else
blanchet@41242
   252
                          "Including (up to) " ^ string_of_int (length facts) ^
blanchet@41242
   253
                          " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
blanchet@41242
   254
                          (facts |> map (fst o fst) |> space_implode " ") ^ ".")
blanchet@41773
   255
                       |> print
blanchet@41242
   256
                     else
blanchet@41242
   257
                       ())
blanchet@41242
   258
        end
blanchet@42952
   259
      fun launch_atps label is_appropriate_prop atps accum =
blanchet@42946
   260
        if null atps then
blanchet@41256
   261
          accum
blanchet@42952
   262
        else if not (is_appropriate_prop concl_t) then
blanchet@42946
   263
          (if verbose orelse length atps = length provers then
blanchet@42946
   264
             "Goal outside the scope of " ^
blanchet@42946
   265
             space_implode " " (serial_commas "and" (map quote atps)) ^ "."
blanchet@42946
   266
             |> Output.urgent_message
blanchet@42946
   267
           else
blanchet@42946
   268
             ();
blanchet@42946
   269
           accum)
blanchet@41256
   270
        else
blanchet@42944
   271
          launch_provers state
blanchet@42952
   272
              (get_facts label is_appropriate_prop atp_relevance_fudge o K atps)
blanchet@42944
   273
              (K (Untranslated_Fact o fst)) (K (K NONE)) atps
blanchet@41746
   274
      fun launch_smts accum =
blanchet@41746
   275
        if null smts then
blanchet@41242
   276
          accum
blanchet@41242
   277
        else
blanchet@41242
   278
          let
blanchet@42944
   279
            val facts = get_facts "SMT solver" (K true) smt_relevance_fudge smts
blanchet@42646
   280
            val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
blanchet@41741
   281
            fun smt_filter facts =
blanchet@41788
   282
              (if debug then curry (op o) SOME
blanchet@41788
   283
               else TimeLimit.timeLimit timeout o try)
boehmes@41432
   284
                  (SMT_Solver.smt_filter_preprocess state (facts ()))
blanchet@41242
   285
          in
blanchet@41242
   286
            smts |> map (`(class_of_smt_solver ctxt))
blanchet@41242
   287
                 |> AList.group (op =)
blanchet@41741
   288
                 |> map (launch_provers state (K facts) weight smt_filter o snd)
blanchet@41242
   289
                 |> exists fst |> rpair state
blanchet@41242
   290
          end
blanchet@42944
   291
      val launch_full_atps = launch_atps "ATP" (K true) full_atps
blanchet@42944
   292
      val launch_ueq_atps =
blanchet@42944
   293
        launch_atps "Unit equational provers" is_unit_equality ueq_atps
blanchet@41262
   294
      fun launch_atps_and_smt_solvers () =
blanchet@42944
   295
        [launch_full_atps, launch_ueq_atps, launch_smts]
blanchet@41242
   296
        |> smart_par_list_map (fn f => f (false, state) |> K ())
blanchet@41773
   297
        handle ERROR msg => (print ("Error: " ^ msg); error msg)
blanchet@40060
   298
    in
blanchet@40065
   299
      (false, state)
blanchet@42944
   300
      |> (if blocking then
blanchet@42944
   301
            launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts)
blanchet@42944
   302
          else
blanchet@42944
   303
            (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
blanchet@41773
   304
      handle TimeLimit.TimeOut =>
blanchet@41773
   305
             (print "Sledgehammer ran out of time."; (false, state))
blanchet@40060
   306
    end
blanchet@38044
   307
wenzelm@28582
   308
end;