src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
author blanchet
Sun May 01 18:37:24 2011 +0200 (2011-05-01)
changeset 42546 8591fcc56c34
parent 42544 75cb06eee990
child 42579 2552c09b1a72
permissions -rw-r--r--
make sure typing fact names are unique (needed e.g. by SNARK)
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_run.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Sledgehammer's heart.
     7 *)
     8 
     9 signature SLEDGEHAMMER_RUN =
    10 sig
    11   type relevance_override = Sledgehammer_Filter.relevance_override
    12   type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
    13   type params = Sledgehammer_Provers.params
    14   type prover = Sledgehammer_Provers.prover
    15 
    16   val auto_minimize_min_facts : int Unsynchronized.ref
    17   val get_minimizing_prover : Proof.context -> bool -> string -> prover
    18   val run_sledgehammer :
    19     params -> bool -> int -> relevance_override -> (string -> minimize_command)
    20     -> Proof.state -> bool * Proof.state
    21 end;
    22 
    23 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
    24 struct
    25 
    26 open Sledgehammer_Util
    27 open Sledgehammer_Filter
    28 open Sledgehammer_ATP_Translate
    29 open Sledgehammer_Provers
    30 open Sledgehammer_Minimize
    31 
    32 fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
    33                        n goal =
    34   quote name ^
    35   (if verbose then
    36      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
    37    else
    38      "") ^
    39   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
    40   (if blocking then
    41      "."
    42    else
    43      ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
    44 
    45 val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
    46 
    47 fun get_minimizing_prover ctxt auto name
    48         (params as {debug, verbose, explicit_apply, ...}) minimize_command
    49         (problem as {state, subgoal, subgoal_count, facts, ...}) =
    50   get_prover ctxt auto name params minimize_command problem
    51   |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
    52          if is_some outcome then
    53            result
    54          else
    55            let
    56              val (used_facts, message) =
    57                if length used_facts >= !auto_minimize_min_facts then
    58                  minimize_facts name params (SOME explicit_apply) (not verbose)
    59                      subgoal subgoal_count state
    60                      (filter_used_facts used_facts
    61                           (map (apsnd single o untranslated_fact) facts))
    62                  |>> Option.map (map fst)
    63                else
    64                  (SOME used_facts, message)
    65            in
    66              case used_facts of
    67                SOME used_facts =>
    68                (if debug andalso not (null used_facts) then
    69                   facts ~~ (0 upto length facts - 1)
    70                   |> map (fn (fact, j) =>
    71                              fact |> untranslated_fact |> apsnd (K j))
    72                   |> filter_used_facts used_facts
    73                   |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
    74                   |> commas
    75                   |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^
    76                               quote name ^ " proof (of " ^
    77                               string_of_int (length facts) ^ "): ") "."
    78                   |> Output.urgent_message
    79                 else
    80                   ();
    81                 {outcome = NONE, used_facts = used_facts,
    82                  run_time_in_msecs = run_time_in_msecs, message = message})
    83              | NONE => result
    84            end)
    85 
    86 fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
    87                               expect, ...})
    88         auto minimize_command only
    89         {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
    90   let
    91     val ctxt = Proof.context_of state
    92     val birth_time = Time.now ()
    93     val death_time = Time.+ (birth_time, timeout)
    94     val max_relevant =
    95       max_relevant
    96       |> the_default (default_max_relevant_for_prover ctxt slicing name)
    97     val num_facts = length facts |> not only ? Integer.min max_relevant
    98     val desc =
    99       prover_description ctxt params name num_facts subgoal subgoal_count goal
   100     val problem =
   101       {state = state, goal = goal, subgoal = subgoal,
   102        subgoal_count = subgoal_count, facts = take num_facts facts,
   103        smt_filter = smt_filter}
   104     fun really_go () =
   105       problem
   106       |> get_minimizing_prover ctxt auto name params (minimize_command name)
   107       |> (fn {outcome, message, ...} =>
   108              (if is_some outcome then "none" else "some" (* sic *), message))
   109     fun go () =
   110       let
   111         val (outcome_code, message) =
   112           if debug then
   113             really_go ()
   114           else
   115             (really_go ()
   116              handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
   117                   | exn =>
   118                     if Exn.is_interrupt exn then
   119                       reraise exn
   120                     else
   121                       ("unknown", "Internal error:\n" ^
   122                                   ML_Compiler.exn_message exn ^ "\n"))
   123         val _ =
   124           (* The "expect" argument is deliberately ignored if the prover is
   125              missing so that the "Metis_Examples" can be processed on any
   126              machine. *)
   127           if expect = "" orelse outcome_code = expect orelse
   128              not (is_prover_installed ctxt name) then
   129             ()
   130           else if blocking then
   131             error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
   132           else
   133             warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
   134       in (outcome_code = "some", message) end
   135   in
   136     if auto then
   137       let val (success, message) = TimeLimit.timeLimit timeout go () in
   138         (success, state |> success ? Proof.goal_message (fn () =>
   139              Pretty.chunks [Pretty.str "",
   140                             Pretty.mark Markup.hilite (Pretty.str message)]))
   141       end
   142     else if blocking then
   143       let val (success, message) = TimeLimit.timeLimit timeout go () in
   144         List.app Output.urgent_message
   145                  (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
   146         (success, state)
   147       end
   148     else
   149       (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
   150        (false, state))
   151   end
   152 
   153 fun class_of_smt_solver ctxt name =
   154   ctxt |> select_smt_solver name
   155        |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
   156 
   157 (* Makes backtraces more transparent and might be more efficient as well. *)
   158 fun smart_par_list_map _ [] = []
   159   | smart_par_list_map f [x] = [f x]
   160   | smart_par_list_map f xs = Par_List.map f xs
   161 
   162 fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
   163   | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
   164 
   165 (* FUDGE *)
   166 val auto_max_relevant_divisor = 2
   167 
   168 fun run_sledgehammer (params as {debug, blocking, provers, monomorphize,
   169                                  type_sys, relevance_thresholds, max_relevant,
   170                                  slicing, timeout, ...})
   171         auto i (relevance_override as {only, ...}) minimize_command state =
   172   if null provers then
   173     error "No prover is set."
   174   else case subgoal_count state of
   175     0 => (Output.urgent_message "No subgoal!"; (false, state))
   176   | n =>
   177     let
   178       val _ = Proof.assert_backward state
   179       val print = if auto then K () else Output.urgent_message
   180       val state =
   181         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
   182       val ctxt = Proof.context_of state
   183       val thy = Proof_Context.theory_of ctxt
   184       val {facts = chained_ths, goal, ...} = Proof.goal state
   185       val (_, hyp_ts, concl_t) = strip_subgoal goal i
   186       val no_dangerous_types = type_system_types_dangerous_types type_sys
   187       val _ = () |> not blocking ? kill_provers
   188       val _ = case find_first (not o is_prover_supported ctxt) provers of
   189                 SOME name => error ("No such prover: " ^ name ^ ".")
   190               | NONE => ()
   191       val _ = print "Sledgehammering..."
   192       val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
   193       fun launch_provers state get_facts translate maybe_smt_filter provers =
   194         let
   195           val facts = get_facts ()
   196           val num_facts = length facts
   197           val facts = facts ~~ (0 upto num_facts - 1)
   198                       |> map (translate num_facts)
   199           val problem =
   200             {state = state, goal = goal, subgoal = i, subgoal_count = n,
   201              facts = facts,
   202              smt_filter = maybe_smt_filter
   203                   (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
   204           val launch = launch_prover params auto minimize_command only
   205         in
   206           if auto then
   207             fold (fn prover => fn (true, state) => (true, state)
   208                                 | (false, _) => launch problem prover)
   209                  provers (false, state)
   210           else
   211             provers
   212             |> (if blocking then smart_par_list_map else map) (launch problem)
   213             |> exists fst |> rpair state
   214         end
   215       fun get_facts label no_dangerous_types relevance_fudge provers =
   216         let
   217           val max_max_relevant =
   218             case max_relevant of
   219               SOME n => n
   220             | NONE =>
   221               0 |> fold (Integer.max
   222                          o default_max_relevant_for_prover ctxt slicing)
   223                         provers
   224                 |> auto ? (fn n => n div auto_max_relevant_divisor)
   225           val is_built_in_const =
   226             is_built_in_const_for_prover ctxt (hd provers)
   227         in
   228           relevant_facts ctxt no_dangerous_types relevance_thresholds
   229                          max_max_relevant is_built_in_const relevance_fudge
   230                          relevance_override chained_ths hyp_ts concl_t
   231           |> tap (fn facts =>
   232                      if debug then
   233                        label ^ plural_s (length provers) ^ ": " ^
   234                        (if null facts then
   235                           "Found no relevant facts."
   236                         else
   237                           "Including (up to) " ^ string_of_int (length facts) ^
   238                           " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
   239                           (facts |> map (fst o fst) |> space_implode " ") ^ ".")
   240                        |> print
   241                      else
   242                        ())
   243         end
   244       fun launch_atps accum =
   245         if null atps then
   246           accum
   247         else
   248           launch_provers state
   249               (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
   250               (if monomorphize then
   251                  K (Untranslated_Fact o fst)
   252                else
   253                  ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
   254               (K (K NONE)) atps
   255       fun launch_smts accum =
   256         if null smts then
   257           accum
   258         else
   259           let
   260             val facts = get_facts "SMT solver" true smt_relevance_fudge smts
   261             val weight = SMT_Weighted_Fact oo weight_smt_fact thy
   262             fun smt_filter facts =
   263               (if debug then curry (op o) SOME
   264                else TimeLimit.timeLimit timeout o try)
   265                   (SMT_Solver.smt_filter_preprocess state (facts ()))
   266           in
   267             smts |> map (`(class_of_smt_solver ctxt))
   268                  |> AList.group (op =)
   269                  |> map (launch_provers state (K facts) weight smt_filter o snd)
   270                  |> exists fst |> rpair state
   271           end
   272       fun launch_atps_and_smt_solvers () =
   273         [launch_atps, launch_smts]
   274         |> smart_par_list_map (fn f => f (false, state) |> K ())
   275         handle ERROR msg => (print ("Error: " ^ msg); error msg)
   276     in
   277       (false, state)
   278       |> (if blocking then launch_atps #> not auto ? launch_smts
   279           else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
   280       handle TimeLimit.TimeOut =>
   281              (print "Sledgehammer ran out of time."; (false, state))
   282     end
   283 
   284 end;