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_Proof_Reconstruct.minimize_command

    12   type relevance_override = Sledgehammer_Filter.relevance_override

    13   type mode = Sledgehammer_Provers.mode

    14   type params = Sledgehammer_Provers.params

    16   val someN : string

    17   val noneN : string

    18   val timeoutN : string

    19   val unknownN : string

    20   val run_sledgehammer :

    21     params -> mode -> int -> relevance_override

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

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

    24 end;

    26 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =

    27 struct

    29 open ATP_Util

    30 open ATP_Problem_Generate

    31 open ATP_Proof_Reconstruct

    32 open Sledgehammer_Util

    33 open Sledgehammer_Fact

    34 open Sledgehammer_Provers

    35 open Sledgehammer_Minimize

    36 open Sledgehammer_Filter

    38 val someN = "some"

    39 val noneN = "none"

    40 val timeoutN = "timeout"

    41 val unknownN = "unknown"

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

    45 fun max_outcome_code codes =

    46   NONE

    47   |> fold (fn candidate =>

    48               fn accum as SOME _ => accum

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

    50                          else NONE)

    51           ordered_outcome_codes

    52   |> the_default unknownN

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

    55                        n goal =

    56   (name,

    57    (if verbose then

    58       " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts

    59     else

    60       "") ^

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

    62    (if blocking then "."

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

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

    66                               timeout, expect, ...})

    67         mode minimize_command only {state, goal, subgoal, subgoal_count, facts}

    68         name =

    69   let

    70     val ctxt = Proof.context_of state

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

    72     val birth_time = Time.now ()

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

    74     val max_relevant =

    75       max_relevant

    76       |> the_default (default_max_relevant_for_prover ctxt slice name)

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

    78     fun desc () =

    79       prover_description ctxt params name num_facts subgoal subgoal_count goal

    80     val problem =

    81       {state = state, goal = goal, subgoal = subgoal,

    82        subgoal_count = subgoal_count,

    83        facts = facts

    84                |> not (Sledgehammer_Provers.is_ho_atp ctxt name)

    85                   ? filter_out (curry (op =) Induction o snd o snd o fst

    86                                 o untranslated_fact)

    87                |> take num_facts}

    88     fun really_go () =

    89       problem

    90       |> get_minimizing_prover ctxt mode name params minimize_command

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

    92              (if outcome = SOME ATP_Proof.TimedOut then timeoutN

    93               else if is_some outcome then noneN

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

    95     fun go () =

    96       let

    97         val (outcome_code, message) =

    98           if debug then

    99             really_go ()

   100           else

   101             (really_go ()

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

   103                   | exn =>

   104                     if Exn.is_interrupt exn then

   105                       reraise exn

   106                     else

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

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

   109         val _ =

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

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

   112              machine. *)

   113           if expect = "" orelse outcome_code = expect orelse

   114              not (is_prover_installed ctxt name) then

   115             ()

   116           else if blocking then

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

   118           else

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

   120       in (outcome_code, message) end

   121   in

   122     if mode = Auto_Try then

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

   124         (outcome_code,

   125          state

   126          |> outcome_code = someN

   127             ? Proof.goal_message (fn () =>

   128                   [Pretty.str "",

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

   130                   |> Pretty.chunks))

   131       end

   132     else if blocking then

   133       let

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

   135       in

   136         (if outcome_code = someN orelse mode = Normal then

   137            quote name ^ ": " ^ message ()

   138          else

   139            "")

   140         |> Async_Manager.break_into_chunks

   141         |> List.app Output.urgent_message;

   142         (outcome_code, state)

   143       end

   144     else

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

   146                             ((fn (outcome_code, message) =>

   147                                  (verbose orelse outcome_code = someN,

   148                                   message ())) o go);

   149        (unknownN, state))

   150   end

   152 fun class_of_smt_solver ctxt name =

   153   ctxt |> select_smt_solver name

   154        |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class

   156 val auto_try_max_relevant_divisor = 2 (* FUDGE *)

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

   159                                  relevance_thresholds, max_relevant, slice,

   160                                  ...})

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

   162   if null provers then

   163     error "No prover is set."

   164   else case subgoal_count state of

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

   166   | n =>

   167     let

   168       val _ = Proof.assert_backward state

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

   170       val state =

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

   172       val ctxt = Proof.context_of state

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

   174       val chained_ths = chained_ths |> normalize_chained_theorems

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

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

   177       val facts =

   178         nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts

   179                          concl_t

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

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

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

   183               | NONE => ()

   184       val _ = print "Sledgehammering..."

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

   186         provers |> List.partition (is_smt_prover ctxt)

   187                 ||> List.partition (is_unit_equational_atp ctxt)

   188       fun launch_provers state get_facts translate provers =

   189         let

   190           val facts = get_facts ()

   191           val num_facts = length facts

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

   193                       |> map (translate num_facts)

   194           val problem =

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

   196              facts = facts}

   197           val launch = launch_prover params mode minimize_command only

   198         in

   199           if mode = Auto_Try orelse mode = Try then

   200             (unknownN, state)

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

   202                         if outcome_code = someN then accum

   203                         else launch problem prover)

   204                     provers

   205           else

   206             provers

   207             |> (if blocking then Par_List.map else map)

   208                    (launch problem #> fst)

   209             |> max_outcome_code |> rpair state

   210         end

   211       fun get_facts label is_appropriate_prop relevance_fudge provers =

   212         let

   213           val max_max_relevant =

   214             case max_relevant of

   215               SOME n => n

   216             | NONE =>

   217               0 |> fold (Integer.max

   218                          o default_max_relevant_for_prover ctxt slice)

   219                         provers

   220                 |> mode = Auto_Try

   221                    ? (fn n => n div auto_try_max_relevant_divisor)

   222           val is_built_in_const =

   223             is_built_in_const_for_prover ctxt (hd provers)

   224         in

   225           facts

   226           |> (case is_appropriate_prop of

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

   228               | NONE => I)

   229           |> relevant_facts ctxt relevance_thresholds max_max_relevant

   230                             is_built_in_const relevance_fudge relevance_override

   231                             chained_ths hyp_ts concl_t

   232           |> tap (fn facts =>

   233                      if debug then

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

   235                        (if null facts then

   236                           "Found no relevant facts."

   237                         else

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

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

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

   241                        |> print

   242                      else

   243                        ())

   244         end

   245       fun launch_atps label is_appropriate_prop atps accum =

   246         if null atps then

   247           accum

   248         else if is_some is_appropriate_prop andalso

   249                 not (the is_appropriate_prop concl_t) then

   250           (if verbose orelse length atps = length provers then

   251              "Goal outside the scope of " ^

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

   253              |> Output.urgent_message

   254            else

   255              ();

   256            accum)

   257         else

   258           launch_provers state

   259               (get_facts label is_appropriate_prop atp_relevance_fudge o K atps)

   260               (K (Untranslated_Fact o fst)) atps

   261       fun launch_smts accum =

   262         if null smts then

   263           accum

   264         else

   265           let

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

   267             val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt

   268           in

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

   270                  |> AList.group (op =)

   271                  |> map (snd #> launch_provers state (K facts) weight #> fst)

   272                  |> max_outcome_code |> rpair state

   273           end

   274       val launch_full_atps = launch_atps "ATP" NONE full_atps

   275       val launch_ueq_atps =

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

   277       fun launch_atps_and_smt_solvers () =

   278         [launch_full_atps, launch_smts, launch_ueq_atps]

   279         |> Par_List.map (fn f => ignore (f (unknownN, state)))

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

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

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

   283     in

   284       (unknownN, state)

   285       |> (if blocking then

   286             launch_full_atps

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

   288           else

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

   290       handle TimeLimit.TimeOut =>

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

   292     end

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

   295 end;

author	blanchet
	Wed, 11 Jul 2012 21:43:19 +0200
changeset 49265	1065c307fafe
parent 48919	67663c968d70
child 49303	255c6e1fd505
permissions	-rw-r--r--