wneuper/isa: src/HOL/Tools/Sledgehammer/sledgehammer

     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_run.ML

     2     Author:     Fabian Immler, TU Muenchen

     3     Author:     Makarius

     4     Author:     Jasmin Blanchette, TU Muenchen

     6 Sledgehammer's heart.

     7 *)

     9 signature SLEDGEHAMMER_RUN =

    10 sig

    11   type minimize_command = ATP_Reconstruct.minimize_command

    12   type relevance_override = Sledgehammer_Filter.relevance_override

    13   type mode = Sledgehammer_Provers.mode

    14   type params = Sledgehammer_Provers.params

    15   type prover = Sledgehammer_Provers.prover

    17   val someN : string

    18   val noneN : string

    19   val timeoutN : string

    20   val unknownN : string

    21   val auto_min_min_facts : int Config.T

    22   val auto_min_max_time : real Config.T

    23   val get_minimizing_prover : Proof.context -> mode -> string -> prover

    24   val run_sledgehammer :

    25     params -> mode -> int -> relevance_override -> (string -> minimize_command)

    26     -> Proof.state -> bool * (string * Proof.state)

    27 end;

    29 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =

    30 struct

    32 open ATP_Util

    33 open ATP_Translate

    34 open ATP_Reconstruct

    35 open Sledgehammer_Util

    36 open Sledgehammer_Filter

    37 open Sledgehammer_Provers

    38 open Sledgehammer_Minimize

    40 val someN = "some"

    41 val noneN = "none"

    42 val timeoutN = "timeout"

    43 val unknownN = "unknown"

    45 val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]

    47 fun max_outcome_code codes =

    48   NONE

    49   |> fold (fn candidate =>

    50               fn accum as SOME _ => accum

    51                | NONE => if member (op =) codes candidate then SOME candidate

    52                          else NONE)

    53           ordered_outcome_codes

    54   |> the_default unknownN

    56 fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i

    57                        n goal =

    58   (name,

    59    (if verbose then

    60       " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts

    61     else

    62       "") ^

    63    " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^

    64    (if blocking then

    65       "."

    66     else

    67       "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))

    69 val auto_min_min_facts =

    70   Attrib.setup_config_int @{binding sledgehammer_auto_min_min_facts}

    71       (fn generic => Config.get_generic generic binary_min_facts)

    72 val auto_min_max_time =

    73   Attrib.setup_config_real @{binding sledgehammer_auto_min_max_time} (K 5.0)

    75 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})

    76              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)

    77              (result as {outcome, used_facts, run_time_in_msecs, preplay,

    78                          message, message_tail} : prover_result) =

    79   if is_some outcome orelse null used_facts then

    80     result

    81   else

    82     let

    83       val num_facts = length used_facts

    84       val ((minimize, minimize_name), preplay) =

    85         if mode = Normal then

    86           if num_facts >= Config.get ctxt auto_min_min_facts then

    87             ((true, name), preplay)

    88           else

    89             let

    90               fun can_min_fast_enough msecs =

    91                 0.001 * Real.fromInt ((num_facts + 2) * msecs)

    92                 <= Config.get ctxt auto_min_max_time

    93               val prover_fast_enough =

    94                 run_time_in_msecs |> Option.map can_min_fast_enough

    95                                   |> the_default false

    96             in

    97               if isar_proof then

    98                 ((prover_fast_enough, name), preplay)

    99               else

   100                 let val preplay = preplay () in

   101                   (case preplay of

   102                      Played (reconstructor, timeout) =>

   103                      if can_min_fast_enough (Time.toMilliseconds timeout) then

   104                        (true, prover_name_for_reconstructor reconstructor

   105                               |> the_default name)

   106                      else

   107                        (prover_fast_enough, name)

   108                    | _ => (prover_fast_enough, name),

   109                    K preplay)

   110                 end

   111             end

   112         else

   113           ((false, name), preplay)

   114       val (used_facts, (preplay, message, _)) =

   115         if minimize then

   116           minimize_facts minimize_name params (not verbose) subgoal

   117                          subgoal_count state

   118                          (filter_used_facts used_facts

   119                               (map (apsnd single o untranslated_fact) facts))

   120           |>> Option.map (map fst)

   121         else

   122           (SOME used_facts, (preplay, message, ""))

   123     in

   124       case used_facts of

   125         SOME used_facts =>

   126         (if debug andalso not (null used_facts) then

   127            facts ~~ (0 upto length facts - 1)

   128            |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j))

   129            |> filter_used_facts used_facts

   130            |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)

   131            |> commas

   132            |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^

   133                        " proof (of " ^ string_of_int (length facts) ^ "): ") "."

   134            |> Output.urgent_message

   135          else

   136            ();

   137          {outcome = NONE, used_facts = used_facts,

   138           run_time_in_msecs = run_time_in_msecs, preplay = preplay,

   139           message = message, message_tail = message_tail})

   140       | NONE => result

   141     end

   143 fun get_minimizing_prover ctxt mode name params minimize_command problem =

   144   get_prover ctxt mode name params minimize_command problem

   145   |> minimize ctxt mode name params problem

   147 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,

   148                               timeout, expect, ...})

   149         mode minimize_command only

   150         {state, goal, subgoal, subgoal_count, facts, smt_filter} name =

   151   let

   152     val ctxt = Proof.context_of state

   153     val hard_timeout = Time.+ (timeout, timeout)

   154     val birth_time = Time.now ()

   155     val death_time = Time.+ (birth_time, hard_timeout)

   156     val max_relevant =

   157       max_relevant

   158       |> the_default (default_max_relevant_for_prover ctxt slicing name)

   159     val num_facts = length facts |> not only ? Integer.min max_relevant

   160     fun desc () =

   161       prover_description ctxt params name num_facts subgoal subgoal_count goal

   162     val problem =

   163       {state = state, goal = goal, subgoal = subgoal,

   164        subgoal_count = subgoal_count, facts = facts |> take num_facts,

   165        smt_filter = smt_filter}

   166     fun really_go () =

   167       problem

   168       |> get_minimizing_prover ctxt mode name params minimize_command

   169       |> (fn {outcome, preplay, message, message_tail, ...} =>

   170              (if outcome = SOME ATP_Proof.TimedOut then timeoutN

   171               else if is_some outcome then noneN

   172               else someN, fn () => message (preplay ()) ^ message_tail))

   173     fun go () =

   174       let

   175         val (outcome_code, message) =

   176           if debug then

   177             really_go ()

   178           else

   179             (really_go ()

   180              handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")

   181                   | exn =>

   182                     if Exn.is_interrupt exn then

   183                       reraise exn

   184                     else

   185                       (unknownN, fn () => "Internal error:\n" ^

   186                                           ML_Compiler.exn_message exn ^ "\n"))

   187         val _ =

   188           (* The "expect" argument is deliberately ignored if the prover is

   189              missing so that the "Metis_Examples" can be processed on any

   190              machine. *)

   191           if expect = "" orelse outcome_code = expect orelse

   192              not (is_prover_installed ctxt name) then

   193             ()

   194           else if blocking then

   195             error ("Unexpected outcome: " ^ quote outcome_code ^ ".")

   196           else

   197             warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");

   198       in (outcome_code, message) end

   199   in

   200     if mode = Auto_Try then

   201       let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in

   202         (outcome_code,

   203          state

   204          |> outcome_code = someN

   205             ? Proof.goal_message (fn () =>

   206                   [Pretty.str "",

   207                    Pretty.mark Markup.hilite (Pretty.str (message ()))]

   208                   |> Pretty.chunks))

   209       end

   210     else if blocking then

   211       let

   212         val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()

   213       in

   214         (if outcome_code = someN orelse mode = Normal then

   215            quote name ^ ": " ^ message ()

   216          else

   217            "")

   218         |> Async_Manager.break_into_chunks

   219         |> List.app Output.urgent_message;

   220         (outcome_code, state)

   221       end

   222     else

   223       (Async_Manager.launch das_tool birth_time death_time (desc ())

   224                             ((fn (outcome_code, message) =>

   225                                  (verbose orelse outcome_code = someN,

   226                                   message ())) o go);

   227        (unknownN, state))

   228   end

   230 fun class_of_smt_solver ctxt name =

   231   ctxt |> select_smt_solver name

   232        |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class

   234 (* Makes backtraces more transparent and might well be more efficient as

   235    well. *)

   236 fun smart_par_list_map _ [] = []

   237   | smart_par_list_map f [x] = [f x]

   238   | smart_par_list_map f xs = Par_List.map f xs

   240 fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p

   241   | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"

   243 val auto_try_max_relevant_divisor = 2 (* FUDGE *)

   245 fun run_sledgehammer (params as {debug, verbose, blocking, provers,

   246                                  relevance_thresholds, max_relevant, slicing,

   247                                  timeout, ...})

   248         mode i (relevance_override as {only, ...}) minimize_command state =

   249   if null provers then

   250     error "No prover is set."

   251   else case subgoal_count state of

   252     0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state)))

   253   | n =>

   254     let

   255       val _ = Proof.assert_backward state

   256       val print = if mode = Normal then Output.urgent_message else K ()

   257       val state =

   258         state |> Proof.map_context (Config.put SMT_Config.verbose debug)

   259       val ctxt = Proof.context_of state

   260       val {facts = chained_ths, goal, ...} = Proof.goal state

   261       val chained_ths = chained_ths |> normalize_chained_theorems

   262       val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i

   263       val facts = nearly_all_facts ctxt relevance_override chained_ths hyp_ts

   264                                    concl_t

   265       val _ = () |> not blocking ? kill_provers

   266       val _ = case find_first (not o is_prover_supported ctxt) provers of

   267                 SOME name => error ("No such prover: " ^ name ^ ".")

   268               | NONE => ()

   269       val _ = print "Sledgehammering..."

   270       val (smts, (ueq_atps, full_atps)) =

   271         provers |> List.partition (is_smt_prover ctxt)

   272                 ||> List.partition (is_unit_equational_atp ctxt)

   273       fun launch_provers state get_facts translate maybe_smt_filter provers =

   274         let

   275           val facts = get_facts ()

   276           val num_facts = length facts

   277           val facts = facts ~~ (0 upto num_facts - 1)

   278                       |> map (translate num_facts)

   279           val problem =

   280             {state = state, goal = goal, subgoal = i, subgoal_count = n,

   281              facts = facts,

   282              smt_filter = maybe_smt_filter

   283                   (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}

   284           val launch = launch_prover params mode minimize_command only

   285         in

   286           if mode = Auto_Try orelse mode = Try then

   287             (unknownN, state)

   288             |> fold (fn prover => fn accum as (outcome_code, _) =>

   289                         if outcome_code = someN then accum

   290                         else launch problem prover)

   291                     provers

   292           else

   293             provers

   294             |> (if blocking then smart_par_list_map else map)

   295                    (launch problem #> fst)

   296             |> max_outcome_code |> rpair state

   297         end

   298       fun get_facts label is_appropriate_prop relevance_fudge provers =

   299         let

   300           val max_max_relevant =

   301             case max_relevant of

   302               SOME n => n

   303             | NONE =>

   304               0 |> fold (Integer.max

   305                          o default_max_relevant_for_prover ctxt slicing)

   306                         provers

   307                 |> mode = Auto_Try

   308                    ? (fn n => n div auto_try_max_relevant_divisor)

   309           val is_built_in_const =

   310             is_built_in_const_for_prover ctxt (hd provers)

   311         in

   312           facts

   313           |> (case is_appropriate_prop of

   314                 SOME is_app => filter (is_app o prop_of o snd)

   315               | NONE => I)

   316           |> relevant_facts ctxt relevance_thresholds max_max_relevant

   317                             is_built_in_const relevance_fudge relevance_override

   318                             chained_ths hyp_ts concl_t

   319           |> tap (fn facts =>

   320                      if debug then

   321                        label ^ plural_s (length provers) ^ ": " ^

   322                        (if null facts then

   323                           "Found no relevant facts."

   324                         else

   325                           "Including (up to) " ^ string_of_int (length facts) ^

   326                           " relevant fact" ^ plural_s (length facts) ^ ":\n" ^

   327                           (facts |> map (fst o fst) |> space_implode " ") ^ ".")

   328                        |> print

   329                      else

   330                        ())

   331         end

   332       fun launch_atps label is_appropriate_prop atps accum =

   333         if null atps then

   334           accum

   335         else if is_some is_appropriate_prop andalso

   336                 not (the is_appropriate_prop concl_t) then

   337           (if verbose orelse length atps = length provers then

   338              "Goal outside the scope of " ^

   339              space_implode " " (serial_commas "and" (map quote atps)) ^ "."

   340              |> Output.urgent_message

   341            else

   342              ();

   343            accum)

   344         else

   345           launch_provers state

   346               (get_facts label is_appropriate_prop atp_relevance_fudge o K atps)

   347               (K (Untranslated_Fact o fst)) (K (K NONE)) atps

   348       fun launch_smts accum =

   349         if null smts then

   350           accum

   351         else

   352           let

   353             val facts = get_facts "SMT solver" NONE smt_relevance_fudge smts

   354             val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt

   355             fun smt_filter facts =

   356               (if debug then curry (op o) SOME

   357                else TimeLimit.timeLimit timeout o try)

   358                   (SMT_Solver.smt_filter_preprocess state (facts ()))

   359           in

   360             smts |> map (`(class_of_smt_solver ctxt))

   361                  |> AList.group (op =)

   362                  |> map (snd #> launch_provers state (K facts) weight smt_filter

   363                              #> fst)

   364                  |> max_outcome_code |> rpair state

   365           end

   366       val launch_full_atps = launch_atps "ATP" NONE full_atps

   367       val launch_ueq_atps =

   368         launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps

   369       fun launch_atps_and_smt_solvers () =

   370         [launch_full_atps, launch_smts, launch_ueq_atps]

   371         |> smart_par_list_map (fn f => ignore (f (unknownN, state)))

   372         handle ERROR msg => (print ("Error: " ^ msg); error msg)

   373       fun maybe f (accum as (outcome_code, _)) =

   374         accum |> (mode = Normal orelse outcome_code <> someN) ? f

   375     in

   376       (unknownN, state)

   377       |> (if blocking then

   378             launch_full_atps

   379             #> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts)

   380           else

   381             (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))

   382       handle TimeLimit.TimeOut =>

   383              (print "Sledgehammer ran out of time."; (unknownN, state))

   384     end

   385     |> `(fn (outcome_code, _) => outcome_code = someN)

   387 end;

author	blanchet
	Tue, 28 Jun 2011 21:06:59 +0200
changeset 44461	0940a64beca2
parent 44217	b19d95b4d736
child 45449	cfe7f4a68e51
permissions	-rw-r--r--