src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Fri Dec 17 21:31:19 2010 +0100 (2010-12-17 ago)
changeset 41256 0e7d45cc005f
parent 41255 a80024d7b71b
child 41260 ff38ea43aada
permissions -rw-r--r--
put the SMT weights back where they belong, so that they're also used by Mirabelle
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@40061
    14
blanchet@41245
    15
  (* for experimentation purposes -- do not use in production code *)
blanchet@41255
    16
  val show_facts_in_proofs : bool Unsynchronized.ref
blanchet@41245
    17
blanchet@38044
    18
  val run_sledgehammer :
blanchet@39318
    19
    params -> bool -> int -> relevance_override -> (string -> minimize_command)
blanchet@39318
    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@41089
    34
  quote name ^
blanchet@41089
    35
  (if verbose then
blanchet@41089
    36
     " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
blanchet@41089
    37
   else
blanchet@41089
    38
     "") ^
blanchet@41089
    39
  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
blanchet@41089
    40
  (if blocking then
blanchet@41089
    41
     ""
blanchet@41089
    42
   else
blanchet@41089
    43
     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
blanchet@41089
    44
blanchet@41255
    45
val show_facts_in_proofs = Unsynchronized.ref false
blanchet@41255
    46
blanchet@41091
    47
val implicit_minimization_threshold = 50
blanchet@41091
    48
blanchet@41208
    49
fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...})
blanchet@41089
    50
               auto minimize_command only
blanchet@41242
    51
               {state, goal, subgoal, subgoal_count, facts, smt_head} name =
blanchet@41089
    52
  let
blanchet@41089
    53
    val ctxt = Proof.context_of state
blanchet@41089
    54
    val birth_time = Time.now ()
blanchet@41089
    55
    val death_time = Time.+ (birth_time, timeout)
blanchet@41089
    56
    val max_relevant =
blanchet@41089
    57
      the_default (default_max_relevant_for_prover ctxt name) max_relevant
blanchet@41089
    58
    val num_facts = length facts |> not only ? Integer.min max_relevant
blanchet@41089
    59
    val desc =
blanchet@41089
    60
      prover_description ctxt params name num_facts subgoal subgoal_count goal
blanchet@41089
    61
    val prover = get_prover ctxt auto name
blanchet@41089
    62
    val problem =
blanchet@41089
    63
      {state = state, goal = goal, subgoal = subgoal,
blanchet@41242
    64
       subgoal_count = subgoal_count, facts = take num_facts facts,
blanchet@41242
    65
       smt_head = smt_head}
blanchet@41255
    66
    fun really_go () =
blanchet@41255
    67
      prover params (minimize_command name) problem
blanchet@41255
    68
      |> (fn {outcome, used_facts, message, ...} =>
blanchet@41255
    69
             if is_some outcome then
blanchet@41255
    70
               ("none", message)
blanchet@41255
    71
             else
blanchet@41255
    72
               let
blanchet@41255
    73
                 val (used_facts, message) =
blanchet@41255
    74
                   if length used_facts >= implicit_minimization_threshold then
blanchet@41255
    75
                     minimize_facts params true subgoal subgoal_count state
blanchet@41255
    76
                         (filter_used_facts used_facts
blanchet@41255
    77
                              (map (apsnd single o untranslated_fact) facts))
blanchet@41255
    78
                     |>> Option.map (map fst)
blanchet@41255
    79
                   else
blanchet@41255
    80
                     (SOME used_facts, message)
blanchet@41255
    81
                 val _ =
blanchet@41255
    82
                   case (debug orelse !show_facts_in_proofs, used_facts) of
blanchet@41255
    83
                     (true, SOME (used_facts as _ :: _)) =>
blanchet@41255
    84
                     facts ~~ (0 upto length facts - 1)
blanchet@41255
    85
                     |> map (fn (fact, j) =>
blanchet@41255
    86
                                fact |> untranslated_fact |> apsnd (K j))
blanchet@41255
    87
                     |> filter_used_facts used_facts
blanchet@41255
    88
                     |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
blanchet@41255
    89
                     |> commas
blanchet@41255
    90
                     |> enclose ("Fact" ^ plural_s num_facts ^ " in " ^
blanchet@41255
    91
                                 quote name ^ " proof (of " ^
blanchet@41255
    92
                                 string_of_int num_facts ^ "): ") "."
blanchet@41255
    93
                     |> Output.urgent_message
blanchet@41255
    94
                   | _ => ()
blanchet@41255
    95
               in ("some", message) end)
blanchet@41089
    96
    fun go () =
blanchet@41089
    97
      let
blanchet@41089
    98
        val (outcome_code, message) =
blanchet@41089
    99
          if debug then
blanchet@41089
   100
            really_go ()
blanchet@41089
   101
          else
blanchet@41089
   102
            (really_go ()
blanchet@41089
   103
             handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
blanchet@41089
   104
                  | exn =>
blanchet@41089
   105
                    if Exn.is_interrupt exn then
blanchet@41089
   106
                      reraise exn
blanchet@41089
   107
                    else
blanchet@41089
   108
                      ("unknown", "Internal error:\n" ^
blanchet@41089
   109
                                  ML_Compiler.exn_message exn ^ "\n"))
blanchet@41089
   110
        val _ =
blanchet@41142
   111
          (* The "expect" argument is deliberately ignored if the prover is
blanchet@41142
   112
             missing so that the "Metis_Examples" can be processed on any
blanchet@41142
   113
             machine. *)
blanchet@41142
   114
          if expect = "" orelse outcome_code = expect orelse
blanchet@41142
   115
             not (is_prover_installed ctxt name) then
blanchet@41089
   116
            ()
blanchet@41089
   117
          else if blocking then
blanchet@41089
   118
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
blanchet@41089
   119
          else
blanchet@41089
   120
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
blanchet@41089
   121
      in (outcome_code = "some", message) end
blanchet@41089
   122
  in
blanchet@41089
   123
    if auto then
blanchet@41089
   124
      let val (success, message) = TimeLimit.timeLimit timeout go () in
blanchet@41089
   125
        (success, state |> success ? Proof.goal_message (fn () =>
blanchet@41091
   126
             Pretty.chunks [Pretty.str "",
blanchet@41091
   127
                            Pretty.mark Markup.hilite (Pretty.str message)]))
blanchet@41089
   128
      end
blanchet@41089
   129
    else if blocking then
blanchet@41089
   130
      let val (success, message) = TimeLimit.timeLimit timeout go () in
blanchet@41089
   131
        List.app Output.urgent_message
blanchet@41089
   132
                 (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
blanchet@41089
   133
        (success, state)
blanchet@41089
   134
      end
blanchet@41089
   135
    else
blanchet@41089
   136
      (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
blanchet@41089
   137
       (false, state))
blanchet@41089
   138
  end
blanchet@41089
   139
blanchet@41242
   140
fun class_of_smt_solver ctxt name =
blanchet@41242
   141
  ctxt |> select_smt_solver name
blanchet@41242
   142
       |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
blanchet@41242
   143
blanchet@41242
   144
(* Makes backtraces more transparent and might be more efficient as well. *)
blanchet@41242
   145
fun smart_par_list_map _ [] = []
blanchet@41242
   146
  | smart_par_list_map f [x] = [f x]
blanchet@41242
   147
  | smart_par_list_map f xs = Par_List.map f xs
blanchet@41242
   148
blanchet@41256
   149
fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
blanchet@41256
   150
  | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
blanchet@41256
   151
blanchet@40698
   152
(* FUDGE *)
blanchet@40698
   153
val auto_max_relevant_divisor = 2
blanchet@40060
   154
blanchet@41208
   155
fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
blanchet@40069
   156
                                 relevance_thresholds, max_relevant, ...})
blanchet@39366
   157
                     auto i (relevance_override as {only, ...}) minimize_command
blanchet@39366
   158
                     state =
blanchet@40059
   159
  if null provers then
blanchet@40059
   160
    error "No prover is set."
blanchet@39318
   161
  else case subgoal_count state of
wenzelm@40132
   162
    0 => (Output.urgent_message "No subgoal!"; (false, state))
blanchet@39318
   163
  | n =>
blanchet@39318
   164
    let
blanchet@39364
   165
      val _ = Proof.assert_backward state
blanchet@41242
   166
      val state =
blanchet@41242
   167
        state |> Proof.map_context (Config.put SMT_Config.verbose debug)
blanchet@40200
   168
      val ctxt = Proof.context_of state
blanchet@41242
   169
      val thy = ProofContext.theory_of ctxt
blanchet@40200
   170
      val {facts = chained_ths, goal, ...} = Proof.goal state
blanchet@40060
   171
      val (_, hyp_ts, concl_t) = strip_subgoal goal i
blanchet@41138
   172
      val no_dangerous_types = types_dangerous_types type_sys
blanchet@40059
   173
      val _ = () |> not blocking ? kill_provers
blanchet@40941
   174
      val _ = case find_first (not o is_prover_available ctxt) provers of
blanchet@40941
   175
                SOME name => error ("No such prover: " ^ name ^ ".")
blanchet@40941
   176
              | NONE => ()
wenzelm@40132
   177
      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
blanchet@40941
   178
      val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
blanchet@41256
   179
      fun run_provers state get_facts translate maybe_smt_head provers =
blanchet@41256
   180
        let
blanchet@41256
   181
          val facts = get_facts ()
blanchet@41256
   182
          val num_facts = length facts
blanchet@41256
   183
          val facts = facts ~~ (0 upto num_facts - 1)
blanchet@41256
   184
                      |> map (translate num_facts)
blanchet@41256
   185
          val problem =
blanchet@41256
   186
            {state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@41256
   187
             facts = facts,
blanchet@41256
   188
             smt_head = maybe_smt_head
blanchet@41256
   189
                  (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
blanchet@41256
   190
          val run_prover = run_prover params auto minimize_command only
blanchet@41256
   191
        in
blanchet@41256
   192
          if auto then
blanchet@41256
   193
            fold (fn prover => fn (true, state) => (true, state)
blanchet@41256
   194
                                | (false, _) => run_prover problem prover)
blanchet@41256
   195
                 provers (false, state)
blanchet@41256
   196
          else
blanchet@41256
   197
            provers
blanchet@41256
   198
            |> (if blocking then smart_par_list_map else map)
blanchet@41256
   199
                   (run_prover problem)
blanchet@41256
   200
            |> exists fst |> rpair state
blanchet@41256
   201
        end
blanchet@41242
   202
      fun get_facts label no_dangerous_types relevance_fudge provers =
blanchet@41242
   203
        let
blanchet@41242
   204
          val max_max_relevant =
blanchet@41242
   205
            case max_relevant of
blanchet@41242
   206
              SOME n => n
blanchet@41242
   207
            | NONE =>
blanchet@41242
   208
              0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
blanchet@41242
   209
                        provers
blanchet@41242
   210
                |> auto ? (fn n => n div auto_max_relevant_divisor)
blanchet@41242
   211
          val is_built_in_const =
blanchet@41242
   212
            is_built_in_const_for_prover ctxt (hd provers)
blanchet@41242
   213
        in
blanchet@41242
   214
          relevant_facts ctxt no_dangerous_types relevance_thresholds
blanchet@41242
   215
                         max_max_relevant is_built_in_const relevance_fudge
blanchet@41242
   216
                         relevance_override chained_ths hyp_ts concl_t
blanchet@41242
   217
          |> tap (fn facts =>
blanchet@41242
   218
                     if debug then
blanchet@41242
   219
                       label ^ plural_s (length provers) ^ ": " ^
blanchet@41242
   220
                       (if null facts then
blanchet@41242
   221
                          "Found no relevant facts."
blanchet@41242
   222
                        else
blanchet@41242
   223
                          "Including (up to) " ^ string_of_int (length facts) ^
blanchet@41242
   224
                          " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
blanchet@41242
   225
                          (facts |> map (fst o fst) |> space_implode " ") ^ ".")
blanchet@41242
   226
                       |> Output.urgent_message
blanchet@41242
   227
                     else
blanchet@41242
   228
                       ())
blanchet@41242
   229
        end
blanchet@41256
   230
      fun run_atps (accum as (success, _)) =
blanchet@41256
   231
        if success orelse null atps then
blanchet@41256
   232
          accum
blanchet@41256
   233
        else
blanchet@41256
   234
          run_provers state
blanchet@41256
   235
              (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
blanchet@41256
   236
              (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
blanchet@41256
   237
              (K (K NONE)) atps
blanchet@41242
   238
      fun run_smts (accum as (success, _)) =
blanchet@41242
   239
        if success orelse null smts then
blanchet@41242
   240
          accum
blanchet@41242
   241
        else
blanchet@41242
   242
          let
blanchet@41242
   243
            val facts = get_facts "SMT solver" true smt_relevance_fudge smts
blanchet@41256
   244
            val weight = SMT_Weighted_Fact oo weight_smt_fact thy
blanchet@41256
   245
            fun smt_head facts =
blanchet@41256
   246
              try (SMT_Solver.smt_filter_head state (facts ()))
blanchet@41242
   247
          in
blanchet@41242
   248
            smts |> map (`(class_of_smt_solver ctxt))
blanchet@41242
   249
                 |> AList.group (op =)
blanchet@41256
   250
                 |> map (run_provers state (K facts) weight smt_head o snd)
blanchet@41242
   251
                 |> exists fst |> rpair state
blanchet@41242
   252
          end
blanchet@40060
   253
      fun run_atps_and_smt_solvers () =
blanchet@41242
   254
        [run_atps, run_smts]
blanchet@41242
   255
        |> smart_par_list_map (fn f => f (false, state) |> K ())
blanchet@41180
   256
        handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
blanchet@40060
   257
    in
blanchet@40065
   258
      (false, state)
blanchet@40065
   259
      |> (if blocking then run_atps #> not auto ? run_smts
blanchet@40065
   260
          else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
blanchet@40060
   261
    end
blanchet@38044
   262
wenzelm@28582
   263
end;