src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Tue Aug 14 13:20:59 2012 +0200 (2012-08-14 ago)
changeset 48798 9152e66f98da
parent 48407 47fe0ca12fc2
child 49358 0fa351b1bd14
permissions -rw-r--r--
be less aggressive at kicking out chained facts
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@46320
    11
  type minimize_command = ATP_Proof_Reconstruct.minimize_command
blanchet@48292
    12
  type fact_override = Sledgehammer_Fact.fact_override
blanchet@43021
    13
  type mode = Sledgehammer_Provers.mode
blanchet@41087
    14
  type params = Sledgehammer_Provers.params
blanchet@40061
    15
blanchet@43020
    16
  val someN : string
blanchet@43020
    17
  val noneN : string
blanchet@43020
    18
  val timeoutN : string
blanchet@43020
    19
  val unknownN : string
blanchet@38044
    20
  val run_sledgehammer :
blanchet@48292
    21
    params -> mode -> int -> fact_override
blanchet@45520
    22
    -> ((string * string list) list -> string -> minimize_command)
blanchet@43020
    23
    -> Proof.state -> bool * (string * Proof.state)
wenzelm@28477
    24
end;
wenzelm@28477
    25
blanchet@41087
    26
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
wenzelm@28477
    27
struct
wenzelm@28477
    28
blanchet@43085
    29
open ATP_Util
blanchet@46320
    30
open ATP_Problem_Generate
blanchet@46320
    31
open ATP_Proof_Reconstruct
blanchet@38023
    32
open Sledgehammer_Util
blanchet@48250
    33
open Sledgehammer_Fact
blanchet@41087
    34
open Sledgehammer_Provers
blanchet@41091
    35
open Sledgehammer_Minimize
blanchet@48381
    36
open Sledgehammer_MaSh
blanchet@40072
    37
blanchet@43020
    38
val someN = "some"
blanchet@43020
    39
val noneN = "none"
blanchet@43020
    40
val timeoutN = "timeout"
blanchet@43020
    41
val unknownN = "unknown"
blanchet@43020
    42
blanchet@43020
    43
val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
blanchet@43020
    44
blanchet@43020
    45
fun max_outcome_code codes =
blanchet@43020
    46
  NONE
blanchet@43020
    47
  |> fold (fn candidate =>
blanchet@43020
    48
              fn accum as SOME _ => accum
blanchet@43020
    49
               | NONE => if member (op =) codes candidate then SOME candidate
blanchet@43020
    50
                         else NONE)
blanchet@43020
    51
          ordered_outcome_codes
blanchet@43020
    52
  |> the_default unknownN
blanchet@43020
    53
blanchet@41208
    54
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
blanchet@41089
    55
                       n goal =
blanchet@48319
    56
  (quote name,
blanchet@43005
    57
   (if verbose then
blanchet@43005
    58
      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
blanchet@43005
    59
    else
blanchet@43005
    60
      "") ^
blanchet@43005
    61
   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
blanchet@45379
    62
   (if blocking then "."
blanchet@45379
    63
    else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
blanchet@41089
    64
blanchet@48293
    65
fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
blanchet@43059
    66
                              timeout, expect, ...})
blanchet@48407
    67
                  mode minimize_command only learn
blanchet@48407
    68
                  {state, goal, subgoal, subgoal_count, facts} name =
blanchet@41089
    69
  let
blanchet@41089
    70
    val ctxt = Proof.context_of state
blanchet@42850
    71
    val hard_timeout = Time.+ (timeout, timeout)
blanchet@41089
    72
    val birth_time = Time.now ()
blanchet@42850
    73
    val death_time = Time.+ (birth_time, hard_timeout)
blanchet@48293
    74
    val max_facts =
blanchet@48293
    75
      max_facts |> the_default (default_max_facts_for_prover ctxt slice name)
blanchet@48293
    76
    val num_facts = length facts |> not only ? Integer.min max_facts
blanchet@43006
    77
    fun desc () =
blanchet@41089
    78
      prover_description ctxt params name num_facts subgoal subgoal_count goal
blanchet@41089
    79
    val problem =
blanchet@47904
    80
      {state = state, goal = goal, subgoal = subgoal,
blanchet@47904
    81
       subgoal_count = subgoal_count,
blanchet@47904
    82
       facts = facts
blanchet@47904
    83
               |> not (Sledgehammer_Provers.is_ho_atp ctxt name)
blanchet@47904
    84
                  ? filter_out (curry (op =) Induction o snd o snd o fst
blanchet@47904
    85
                                o untranslated_fact)
blanchet@47904
    86
               |> take num_facts}
blanchet@48394
    87
    fun print_used_facts used_facts =
blanchet@48394
    88
      tag_list 1 facts
blanchet@48394
    89
      |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
blanchet@48798
    90
      |> filter_used_facts false used_facts
blanchet@48394
    91
      |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
blanchet@48394
    92
      |> commas
blanchet@48394
    93
      |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
blanchet@48394
    94
                  " proof (of " ^ string_of_int (length facts) ^ "): ") "."
blanchet@48394
    95
      |> Output.urgent_message
blanchet@41255
    96
    fun really_go () =
blanchet@41263
    97
      problem
blanchet@48399
    98
      |> get_minimizing_prover ctxt mode learn name params minimize_command
blanchet@48394
    99
      |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} =>
blanchet@48394
   100
                           print_used_facts used_facts
blanchet@48394
   101
                         | _ => ())
blanchet@43261
   102
      |> (fn {outcome, preplay, message, message_tail, ...} =>
blanchet@43005
   103
             (if outcome = SOME ATP_Proof.TimedOut then timeoutN
blanchet@43005
   104
              else if is_some outcome then noneN
blanchet@43261
   105
              else someN, fn () => message (preplay ()) ^ message_tail))
blanchet@41089
   106
    fun go () =
blanchet@41089
   107
      let
blanchet@41089
   108
        val (outcome_code, message) =
blanchet@41089
   109
          if debug then
blanchet@41089
   110
            really_go ()
blanchet@41089
   111
          else
blanchet@41089
   112
            (really_go ()
blanchet@43052
   113
             handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
blanchet@41089
   114
                  | exn =>
blanchet@41089
   115
                    if Exn.is_interrupt exn then
blanchet@41089
   116
                      reraise exn
blanchet@41089
   117
                    else
blanchet@43052
   118
                      (unknownN, fn () => "Internal error:\n" ^
blanchet@43052
   119
                                          ML_Compiler.exn_message exn ^ "\n"))
blanchet@41089
   120
        val _ =
blanchet@41142
   121
          (* The "expect" argument is deliberately ignored if the prover is
blanchet@41142
   122
             missing so that the "Metis_Examples" can be processed on any
blanchet@41142
   123
             machine. *)
blanchet@41142
   124
          if expect = "" orelse outcome_code = expect orelse
blanchet@41142
   125
             not (is_prover_installed ctxt name) then
blanchet@41089
   126
            ()
blanchet@41089
   127
          else if blocking then
blanchet@41089
   128
            error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
blanchet@41089
   129
          else
blanchet@41089
   130
            warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
blanchet@43005
   131
      in (outcome_code, message) end
blanchet@41089
   132
  in
blanchet@43021
   133
    if mode = Auto_Try then
blanchet@43006
   134
      let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
blanchet@43006
   135
        (outcome_code,
blanchet@43006
   136
         state
blanchet@43006
   137
         |> outcome_code = someN
blanchet@43006
   138
            ? Proof.goal_message (fn () =>
blanchet@43006
   139
                  [Pretty.str "",
wenzelm@45666
   140
                   Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))]
blanchet@43006
   141
                  |> Pretty.chunks))
blanchet@41089
   142
      end
blanchet@41089
   143
    else if blocking then
blanchet@43006
   144
      let
blanchet@43006
   145
        val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
blanchet@43006
   146
      in
blanchet@43058
   147
        (if outcome_code = someN orelse mode = Normal then
blanchet@43058
   148
           quote name ^ ": " ^ message ()
blanchet@43058
   149
         else
blanchet@43058
   150
           "")
blanchet@43005
   151
        |> Async_Manager.break_into_chunks
blanchet@43005
   152
        |> List.app Output.urgent_message;
blanchet@43006
   153
        (outcome_code, state)
blanchet@41089
   154
      end
blanchet@41089
   155
    else
blanchet@48319
   156
      (Async_Manager.launch SledgehammerN birth_time death_time (desc ())
blanchet@43052
   157
                            ((fn (outcome_code, message) =>
blanchet@43059
   158
                                 (verbose orelse outcome_code = someN,
blanchet@43059
   159
                                  message ())) o go);
blanchet@43006
   160
       (unknownN, state))
blanchet@41089
   161
  end
blanchet@41089
   162
blanchet@41242
   163
fun class_of_smt_solver ctxt name =
blanchet@41242
   164
  ctxt |> select_smt_solver name
blanchet@41242
   165
       |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
blanchet@41242
   166
blanchet@48293
   167
val auto_try_max_facts_divisor = 2 (* FUDGE *)
blanchet@40060
   168
blanchet@48293
   169
fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts,
blanchet@48293
   170
                                 slice, ...})
blanchet@48292
   171
        mode i (fact_override as {only, ...}) minimize_command state =
blanchet@40059
   172
  if null provers then
blanchet@40059
   173
    error "No prover is set."
blanchet@39318
   174
  else case subgoal_count state of
blanchet@43020
   175
    0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state)))
blanchet@39318
   176
  | n =>
blanchet@39318
   177
    let
blanchet@39364
   178
      val _ = Proof.assert_backward state
blanchet@43021
   179
      val print = if mode = Normal then Output.urgent_message else K ()
blanchet@41242
   180
      val state =
blanchet@41242
   181
        state |> Proof.map_context (Config.put SMT_Config.verbose debug)
blanchet@40200
   182
      val ctxt = Proof.context_of state
blanchet@48396
   183
      val {facts = chained, goal, ...} = Proof.goal state
blanchet@43004
   184
      val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
blanchet@44625
   185
      val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
blanchet@48299
   186
      val reserved = reserved_isar_keyword_table ()
blanchet@48396
   187
      val css = clasimpset_rule_table_of ctxt
blanchet@48407
   188
      val all_facts =
blanchet@48396
   189
        nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
blanchet@48396
   190
                         concl_t
nik@44586
   191
      val _ = () |> not blocking ? kill_provers
blanchet@41727
   192
      val _ = case find_first (not o is_prover_supported ctxt) provers of
blanchet@40941
   193
                SOME name => error ("No such prover: " ^ name ^ ".")
blanchet@40941
   194
              | NONE => ()
blanchet@41773
   195
      val _ = print "Sledgehammering..."
blanchet@42944
   196
      val (smts, (ueq_atps, full_atps)) =
blanchet@42944
   197
        provers |> List.partition (is_smt_prover ctxt)
blanchet@42944
   198
                ||> List.partition (is_unit_equational_atp ctxt)
blanchet@47531
   199
      fun launch_provers state get_facts translate provers =
blanchet@41256
   200
        let
blanchet@41256
   201
          val facts = get_facts ()
blanchet@41256
   202
          val num_facts = length facts
blanchet@41256
   203
          val facts = facts ~~ (0 upto num_facts - 1)
blanchet@41256
   204
                      |> map (translate num_facts)
blanchet@41256
   205
          val problem =
blanchet@41256
   206
            {state = state, goal = goal, subgoal = i, subgoal_count = n,
blanchet@47531
   207
             facts = facts}
blanchet@48407
   208
          fun learn prover =
blanchet@48407
   209
            mash_learn_proof ctxt params prover (prop_of goal) all_facts
blanchet@48407
   210
          val launch = launch_prover params mode minimize_command only learn
blanchet@41256
   211
        in
blanchet@43021
   212
          if mode = Auto_Try orelse mode = Try then
blanchet@43020
   213
            (unknownN, state)
blanchet@43021
   214
            |> fold (fn prover => fn accum as (outcome_code, _) =>
blanchet@43020
   215
                        if outcome_code = someN then accum
blanchet@43020
   216
                        else launch problem prover)
blanchet@43020
   217
                    provers
blanchet@41256
   218
          else
blanchet@41256
   219
            provers
wenzelm@46892
   220
            |> (if blocking then Par_List.map else map)
blanchet@43020
   221
                   (launch problem #> fst)
blanchet@43020
   222
            |> max_outcome_code |> rpair state
blanchet@41256
   223
        end
blanchet@48288
   224
      fun get_facts label is_appropriate_prop provers =
blanchet@41242
   225
        let
blanchet@48293
   226
          val max_max_facts =
blanchet@48293
   227
            case max_facts of
blanchet@41242
   228
              SOME n => n
blanchet@41242
   229
            | NONE =>
blanchet@48293
   230
              0 |> fold (Integer.max o default_max_facts_for_prover ctxt slice)
blanchet@41242
   231
                        provers
blanchet@48293
   232
                |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
blanchet@41242
   233
        in
blanchet@48407
   234
          all_facts
blanchet@43351
   235
          |> (case is_appropriate_prop of
blanchet@43351
   236
                SOME is_app => filter (is_app o prop_of o snd)
blanchet@43351
   237
              | NONE => I)
blanchet@48293
   238
          |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
blanchet@48293
   239
                            hyp_ts concl_t
blanchet@48289
   240
          |> map (apfst (apfst (fn name => name ())))
blanchet@41242
   241
          |> tap (fn facts =>
blanchet@48394
   242
                     if verbose then
blanchet@41242
   243
                       label ^ plural_s (length provers) ^ ": " ^
blanchet@41242
   244
                       (if null facts then
blanchet@41242
   245
                          "Found no relevant facts."
blanchet@41242
   246
                        else
blanchet@41242
   247
                          "Including (up to) " ^ string_of_int (length facts) ^
blanchet@41242
   248
                          " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
blanchet@41242
   249
                          (facts |> map (fst o fst) |> space_implode " ") ^ ".")
blanchet@41773
   250
                       |> print
blanchet@41242
   251
                     else
blanchet@41242
   252
                       ())
blanchet@41242
   253
        end
blanchet@42952
   254
      fun launch_atps label is_appropriate_prop atps accum =
blanchet@42946
   255
        if null atps then
blanchet@41256
   256
          accum
blanchet@43351
   257
        else if is_some is_appropriate_prop andalso
blanchet@43351
   258
                not (the is_appropriate_prop concl_t) then
blanchet@42946
   259
          (if verbose orelse length atps = length provers then
blanchet@42946
   260
             "Goal outside the scope of " ^
blanchet@42946
   261
             space_implode " " (serial_commas "and" (map quote atps)) ^ "."
blanchet@42946
   262
             |> Output.urgent_message
blanchet@42946
   263
           else
blanchet@42946
   264
             ();
blanchet@42946
   265
           accum)
blanchet@41256
   266
        else
blanchet@48288
   267
          launch_provers state (get_facts label is_appropriate_prop o K atps)
blanchet@48288
   268
                         (K (Untranslated_Fact o fst)) atps
blanchet@41746
   269
      fun launch_smts accum =
blanchet@41746
   270
        if null smts then
blanchet@41242
   271
          accum
blanchet@41242
   272
        else
blanchet@41242
   273
          let
blanchet@48288
   274
            val facts = get_facts "SMT solver" NONE smts
blanchet@42646
   275
            val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
blanchet@41242
   276
          in
blanchet@41242
   277
            smts |> map (`(class_of_smt_solver ctxt))
blanchet@41242
   278
                 |> AList.group (op =)
blanchet@47531
   279
                 |> map (snd #> launch_provers state (K facts) weight #> fst)
blanchet@43020
   280
                 |> max_outcome_code |> rpair state
blanchet@41242
   281
          end
blanchet@43351
   282
      val launch_full_atps = launch_atps "ATP" NONE full_atps
blanchet@42944
   283
      val launch_ueq_atps =
blanchet@43351
   284
        launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps
blanchet@41262
   285
      fun launch_atps_and_smt_solvers () =
blanchet@43043
   286
        [launch_full_atps, launch_smts, launch_ueq_atps]
wenzelm@46892
   287
        |> Par_List.map (fn f => ignore (f (unknownN, state)))
blanchet@41773
   288
        handle ERROR msg => (print ("Error: " ^ msg); error msg)
blanchet@43021
   289
      fun maybe f (accum as (outcome_code, _)) =
blanchet@43021
   290
        accum |> (mode = Normal orelse outcome_code <> someN) ? f
blanchet@40060
   291
    in
blanchet@43020
   292
      (unknownN, state)
blanchet@42944
   293
      |> (if blocking then
blanchet@43021
   294
            launch_full_atps
blanchet@43021
   295
            #> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts)
blanchet@42944
   296
          else
blanchet@42944
   297
            (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
blanchet@41773
   298
      handle TimeLimit.TimeOut =>
blanchet@43020
   299
             (print "Sledgehammer ran out of time."; (unknownN, state))
blanchet@40060
   300
    end
blanchet@43020
   301
    |> `(fn (outcome_code, _) => outcome_code = someN)
blanchet@38044
   302
wenzelm@28582
   303
end;