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_minimize_min_facts : int Config.T

    22   val auto_minimize_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

    26     -> ((string * string list) list -> string -> minimize_command)

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

    28 end;

    30 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =

    31 struct

    33 open ATP_Util

    34 open ATP_Translate

    35 open ATP_Reconstruct

    36 open Sledgehammer_Util

    37 open Sledgehammer_Filter

    38 open Sledgehammer_Provers

    39 open Sledgehammer_Minimize

    41 val someN = "some"

    42 val noneN = "none"

    43 val timeoutN = "timeout"

    44 val unknownN = "unknown"

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

    48 fun max_outcome_code codes =

    49   NONE

    50   |> fold (fn candidate =>

    51               fn accum as SOME _ => accum

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

    53                          else NONE)

    54           ordered_outcome_codes

    55   |> the_default unknownN

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

    58                        n goal =

    59   (name,

    60    (if verbose then

    61       " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts

    62     else

    63       "") ^

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

    65    (if blocking then "."

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

    68 val auto_minimize_min_facts =

    69   Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}

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

    71 val auto_minimize_max_time =

    72   Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}

    73                            (K 5.0)

    75 fun adjust_reconstructor_params override_params

    76         ({debug, verbose, overlord, blocking, provers, type_enc, sound,

    77          lam_trans, relevance_thresholds, max_relevant, max_mono_iters,

    78          max_new_mono_instances, isar_proof, isar_shrink_factor, slice, timeout,

    79          preplay_timeout, expect} : params) =

    80   let

    81     fun lookup_override name default_value =

    82       case AList.lookup (op =) override_params name of

    83         SOME [s] => SOME s

    84       | _ => default_value

    85     (* Only those options that reconstructors are interested in are considered

    86        here. *)

    87     val type_enc = lookup_override "type_enc" type_enc

    88     val lam_trans = lookup_override "lam_trans" lam_trans

    89   in

    90     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,

    91      provers = provers, type_enc = type_enc, sound = sound,

    92      lam_trans = lam_trans, max_relevant = max_relevant,

    93      relevance_thresholds = relevance_thresholds,

    94      max_mono_iters = max_mono_iters,

    95      max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,

    96      isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,

    97      preplay_timeout = preplay_timeout, expect = expect}

    98   end

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

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

   102              (result as {outcome, used_facts, run_time, preplay, message,

   103                          message_tail} : prover_result) =

   104   if is_some outcome orelse null used_facts then

   105     result

   106   else

   107     let

   108       val num_facts = length used_facts

   109       val ((minimize, (minimize_name, params)), preplay) =

   110         if mode = Normal then

   111           if num_facts >= Config.get ctxt auto_minimize_min_facts then

   112             ((true, (name, params)), preplay)

   113           else

   114             let

   115               fun can_min_fast_enough time =

   116                 0.001

   117                 * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)

   118                 <= Config.get ctxt auto_minimize_max_time

   119               val prover_fast_enough = can_min_fast_enough run_time

   120             in

   121               if isar_proof then

   122                 ((prover_fast_enough, (name, params)), preplay)

   123               else

   124                 let val preplay = preplay () in

   125                   (case preplay of

   126                      Played (reconstr, timeout) =>

   127                      if can_min_fast_enough timeout then

   128                        (true, extract_reconstructor params reconstr

   129                               ||> (fn override_params =>

   130                                       adjust_reconstructor_params

   131                                           override_params params))

   132                      else

   133                        (prover_fast_enough, (name, params))

   134                    | _ => (prover_fast_enough, (name, params)),

   135                    K preplay)

   136                 end

   137             end

   138         else

   139           ((false, (name, params)), preplay)

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

   141         if minimize then

   142           minimize_facts minimize_name params (not verbose) subgoal

   143                          subgoal_count state

   144                          (filter_used_facts used_facts

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

   146           |>> Option.map (map fst)

   147         else

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

   149     in

   150       case used_facts of

   151         SOME used_facts =>

   152         (if debug andalso not (null used_facts) then

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

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

   155            |> filter_used_facts used_facts

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

   157            |> commas

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

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

   160            |> Output.urgent_message

   161          else

   162            ();

   163          {outcome = NONE, used_facts = used_facts, run_time = run_time,

   164           preplay = preplay, message = message, message_tail = message_tail})

   165       | NONE => result

   166     end

   168 fun get_minimizing_prover ctxt mode name params minimize_command problem =

   169   get_prover ctxt mode name params minimize_command problem

   170   |> minimize ctxt mode name params problem

   172 fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true

   173   | is_induction_fact _ = false

   175 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,

   176                               timeout, expect, ...})

   177         mode minimize_command only

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

   179   let

   180     val ctxt = Proof.context_of state

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

   182     val birth_time = Time.now ()

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

   184     val max_relevant =

   185       max_relevant

   186       |> the_default (default_max_relevant_for_prover ctxt slice name)

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

   188     fun desc () =

   189       prover_description ctxt params name num_facts subgoal subgoal_count goal

   190     val problem =

   191       let

   192         val filter_induction = filter_out is_induction_fact

   193       in {state = state, goal = goal, subgoal = subgoal,

   194          subgoal_count = subgoal_count, facts =

   195           ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction)

   196             facts

   197           |> take num_facts,

   198          smt_filter = smt_filter}

   199       end

   200     fun really_go () =

   201       problem

   202       |> get_minimizing_prover ctxt mode name params minimize_command

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

   204              (if outcome = SOME ATP_Proof.TimedOut then timeoutN

   205               else if is_some outcome then noneN

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

   207     fun go () =

   208       let

   209         val (outcome_code, message) =

   210           if debug then

   211             really_go ()

   212           else

   213             (really_go ()

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

   215                   | exn =>

   216                     if Exn.is_interrupt exn then

   217                       reraise exn

   218                     else

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

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

   221         val _ =

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

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

   224              machine. *)

   225           if expect = "" orelse outcome_code = expect orelse

   226              not (is_prover_installed ctxt name) then

   227             ()

   228           else if blocking then

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

   230           else

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

   232       in (outcome_code, message) end

   233   in

   234     if mode = Auto_Try then

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

   236         (outcome_code,

   237          state

   238          |> outcome_code = someN

   239             ? Proof.goal_message (fn () =>

   240                   [Pretty.str "",

   241                    Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))]

   242                   |> Pretty.chunks))

   243       end

   244     else if blocking then

   245       let

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

   247       in

   248         (if outcome_code = someN orelse mode = Normal then

   249            quote name ^ ": " ^ message ()

   250          else

   251            "")

   252         |> Async_Manager.break_into_chunks

   253         |> List.app Output.urgent_message;

   254         (outcome_code, state)

   255       end

   256     else

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

   258                             ((fn (outcome_code, message) =>

   259                                  (verbose orelse outcome_code = someN,

   260                                   message ())) o go);

   261        (unknownN, state))

   262   end

   264 fun class_of_smt_solver ctxt name =

   265   ctxt |> select_smt_solver name

   266        |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class

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

   269    well. *)

   270 fun smart_par_list_map _ [] = []

   271   | smart_par_list_map f [x] = [f x]

   272   | smart_par_list_map f xs = Par_List.map f xs

   274 fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p

   275   | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"

   277 val auto_try_max_relevant_divisor = 2 (* FUDGE *)

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

   280                                  relevance_thresholds, max_relevant, slice,

   281                                  timeout, ...})

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

   283   if null provers then

   284     error "No prover is set."

   285   else case subgoal_count state of

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

   287   | n =>

   288     let

   289       val _ = Proof.assert_backward state

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

   291       val state =

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

   293       val ctxt = Proof.context_of state

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

   295       val chained_ths = chained_ths |> normalize_chained_theorems

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

   297       val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers

   298       val facts =

   299         nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts

   300                          concl_t

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

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

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

   304               | NONE => ()

   305       val _ = print "Sledgehammering..."

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

   307         provers |> List.partition (is_smt_prover ctxt)

   308                 ||> List.partition (is_unit_equational_atp ctxt)

   309       fun launch_provers state get_facts translate maybe_smt_filter provers =

   310         let

   311           val facts = get_facts ()

   312           val num_facts = length facts

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

   314                       |> map (translate num_facts)

   315           val problem =

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

   317              facts = facts,

   318              smt_filter = maybe_smt_filter

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

   320           val launch = launch_prover params mode minimize_command only

   321         in

   322           if mode = Auto_Try orelse mode = Try then

   323             (unknownN, state)

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

   325                         if outcome_code = someN then accum

   326                         else launch problem prover)

   327                     provers

   328           else

   329             provers

   330             |> (if blocking then smart_par_list_map else map)

   331                    (launch problem #> fst)

   332             |> max_outcome_code |> rpair state

   333         end

   334       fun get_facts label is_appropriate_prop relevance_fudge provers =

   335         let

   336           val max_max_relevant =

   337             case max_relevant of

   338               SOME n => n

   339             | NONE =>

   340               0 |> fold (Integer.max

   341                          o default_max_relevant_for_prover ctxt slice)

   342                         provers

   343                 |> mode = Auto_Try

   344                    ? (fn n => n div auto_try_max_relevant_divisor)

   345           val is_built_in_const =

   346             is_built_in_const_for_prover ctxt (hd provers)

   347         in

   348           facts

   349           |> (case is_appropriate_prop of

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

   351               | NONE => I)

   352           |> relevant_facts ctxt relevance_thresholds max_max_relevant

   353                             is_built_in_const relevance_fudge relevance_override

   354                             chained_ths hyp_ts concl_t

   355           |> tap (fn facts =>

   356                      if debug then

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

   358                        (if null facts then

   359                           "Found no relevant facts."

   360                         else

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

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

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

   364                        |> print

   365                      else

   366                        ())

   367         end

   368       fun launch_atps label is_appropriate_prop atps accum =

   369         if null atps then

   370           accum

   371         else if is_some is_appropriate_prop andalso

   372                 not (the is_appropriate_prop concl_t) then

   373           (if verbose orelse length atps = length provers then

   374              "Goal outside the scope of " ^

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

   376              |> Output.urgent_message

   377            else

   378              ();

   379            accum)

   380         else

   381           launch_provers state

   382               (get_facts label is_appropriate_prop atp_relevance_fudge o K atps)

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

   384       fun launch_smts accum =

   385         if null smts then

   386           accum

   387         else

   388           let

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

   390             val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt

   391             fun smt_filter facts =

   392               (if debug then curry (op o) SOME

   393                else TimeLimit.timeLimit timeout o try)

   394                   (SMT_Solver.smt_filter_preprocess state (facts ()))

   395           in

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

   397                  |> AList.group (op =)

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

   399                              #> fst)

   400                  |> max_outcome_code |> rpair state

   401           end

   402       val launch_full_atps = launch_atps "ATP" NONE full_atps

   403       val launch_ueq_atps =

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

   405       fun launch_atps_and_smt_solvers () =

   406         [launch_full_atps, launch_smts, launch_ueq_atps]

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

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

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

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

   411     in

   412       (unknownN, state)

   413       |> (if blocking then

   414             launch_full_atps

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

   416           else

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

   418       handle TimeLimit.TimeOut =>

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

   420     end

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

   423 end;

author	blanchet
	Thu, 01 Dec 2011 13:34:13 +0100
changeset 46577	418846ea4f99
parent 46537	d83797ef0d2d
child 46578	6bf7eec9b153
permissions	-rw-r--r--