wneuper/isa: src/HOL/Mirabelle/Tools/mirabelle

     1 (*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

     2     Author:     Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich

     3 *)

     5 structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =

     6 struct

     8 val proverK = "prover"

     9 val prover_timeoutK = "prover_timeout"

    10 val keepK = "keep"

    11 val full_typesK = "full_types"

    12 val type_sysK = "type_sys"

    13 val slicingK = "slicing"

    14 val e_weight_methodK = "e_weight_method"

    15 val spass_force_sosK = "spass_force_sos"

    16 val vampire_force_sosK = "vampire_force_sos"

    17 val max_relevantK = "max_relevant"

    18 val minimizeK = "minimize"

    19 val minimize_timeoutK = "minimize_timeout"

    20 val metis_ftK = "metis_ft"

    21 val reconstructorK = "reconstructor"

    23 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "

    24 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "

    25 fun reconstructor_tag reconstructor id =

    26   "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): "

    28 val separator = "-----"

    31 datatype sh_data = ShData of {

    32   calls: int,

    33   success: int,

    34   nontriv_calls: int,

    35   nontriv_success: int,

    36   lemmas: int,

    37   max_lems: int,

    38   time_isa: int,

    39   time_prover: int,

    40   time_prover_fail: int}

    42 datatype re_data = ReData of {

    43   calls: int,

    44   success: int,

    45   nontriv_calls: int,

    46   nontriv_success: int,

    47   proofs: int,

    48   time: int,

    49   timeout: int,

    50   lemmas: int * int * int,

    51   posns: (Position.T * bool) list

    52   }

    54 datatype min_data = MinData of {

    55   succs: int,

    56   ab_ratios: int

    57   }

    59 fun make_sh_data

    60       (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa,

    61        time_prover,time_prover_fail) =

    62   ShData{calls=calls, success=success, nontriv_calls=nontriv_calls,

    63          nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems,

    64          time_isa=time_isa, time_prover=time_prover,

    65          time_prover_fail=time_prover_fail}

    67 fun make_min_data (succs, ab_ratios) =

    68   MinData{succs=succs, ab_ratios=ab_ratios}

    70 fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time,

    71                   timeout,lemmas,posns) =

    72   ReData{calls=calls, success=success, nontriv_calls=nontriv_calls,

    73          nontriv_success=nontriv_success, proofs=proofs, time=time,

    74          timeout=timeout, lemmas=lemmas, posns=posns}

    76 val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0)

    77 val empty_min_data = make_min_data (0, 0)

    78 val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), [])

    80 fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success,

    81                               lemmas, max_lems, time_isa,

    82   time_prover, time_prover_fail}) = (calls, success, nontriv_calls,

    83   nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)

    85 fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)

    87 fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success,

    88   proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,

    89   nontriv_success, proofs, time, timeout, lemmas, posns)

    92 datatype reconstructor_mode =

    93   Unminimized | Minimized | UnminimizedFT | MinimizedFT

    95 datatype data = Data of {

    96   sh: sh_data,

    97   min: min_data,

    98   re_u: re_data, (* reconstructor with unminimized set of lemmas *)

    99   re_m: re_data, (* reconstructor with minimized set of lemmas *)

   100   re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *)

   101   re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *)

   102   mini: bool   (* with minimization *)

   103   }

   105 fun make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) =

   106   Data {sh=sh, min=min, re_u=re_u, re_m=re_m, re_uft=re_uft, re_mft=re_mft,

   107     mini=mini}

   109 val empty_data = make_data (empty_sh_data, empty_min_data,

   110   empty_re_data, empty_re_data, empty_re_data, empty_re_data, false)

   112 fun map_sh_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =

   113   let val sh' = make_sh_data (f (tuple_of_sh_data sh))

   114   in make_data (sh', min, re_u, re_m, re_uft, re_mft, mini) end

   116 fun map_min_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =

   117   let val min' = make_min_data (f (tuple_of_min_data min))

   118   in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end

   120 fun map_re_data f m (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =

   121   let

   122     fun map_me g Unminimized   (u, m, uft, mft) = (g u, m, uft, mft)

   123       | map_me g Minimized     (u, m, uft, mft) = (u, g m, uft, mft)

   124       | map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft)

   125       | map_me g MinimizedFT   (u, m, uft, mft) = (u, m, uft, g mft)

   127     val f' = make_re_data o f o tuple_of_re_data

   129     val (re_u', re_m', re_uft', re_mft') =

   130       map_me f' m (re_u, re_m, re_uft, re_mft)

   131   in make_data (sh, min, re_u', re_m', re_uft', re_mft', mini) end

   133 fun set_mini mini (Data {sh, min, re_u, re_m, re_uft, re_mft, ...}) =

   134   make_data (sh, min, re_u, re_m, re_uft, re_mft, mini)

   136 fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));

   138 val inc_sh_calls =  map_sh_data

   139   (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)

   140     => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))

   142 val inc_sh_success = map_sh_data

   143   (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)

   144     => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail))

   146 val inc_sh_nontriv_calls =  map_sh_data

   147   (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)

   148     => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))

   150 val inc_sh_nontriv_success = map_sh_data

   151   (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)

   152     => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail))

   154 fun inc_sh_lemmas n = map_sh_data

   155   (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)

   156     => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail))

   158 fun inc_sh_max_lems n = map_sh_data

   159   (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)

   160     => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail))

   162 fun inc_sh_time_isa t = map_sh_data

   163   (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)

   164     => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail))

   166 fun inc_sh_time_prover t = map_sh_data

   167   (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)

   168     => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail))

   170 fun inc_sh_time_prover_fail t = map_sh_data

   171   (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)

   172     => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t))

   174 val inc_min_succs = map_min_data

   175   (fn (succs,ab_ratios) => (succs+1, ab_ratios))

   177 fun inc_min_ab_ratios r = map_min_data

   178   (fn (succs, ab_ratios) => (succs, ab_ratios+r))

   180 val inc_reconstructor_calls = map_re_data

   181   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   182     => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))

   184 val inc_reconstructor_success = map_re_data

   185   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   186     => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))

   188 val inc_reconstructor_nontriv_calls = map_re_data

   189   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   190     => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns))

   192 val inc_reconstructor_nontriv_success = map_re_data

   193   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   194     => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns))

   196 val inc_reconstructor_proofs = map_re_data

   197   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   198     => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns))

   200 fun inc_reconstructor_time m t = map_re_data

   201  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   202   => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m

   204 val inc_reconstructor_timeout = map_re_data

   205   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   206     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns))

   208 fun inc_reconstructor_lemmas m n = map_re_data

   209   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   210     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m

   212 fun inc_reconstructor_posns m pos = map_re_data

   213   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   214     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m

   216 local

   218 val str = string_of_int

   219 val str3 = Real.fmt (StringCvt.FIX (SOME 3))

   220 fun percentage a b = string_of_int (a * 100 div b)

   221 fun time t = Real.fromInt t / 1000.0

   222 fun avg_time t n =

   223   if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0

   225 fun log_sh_data log

   226     (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) =

   227  (log ("Total number of sledgehammer calls: " ^ str calls);

   228   log ("Number of successful sledgehammer calls: " ^ str success);

   229   log ("Number of sledgehammer lemmas: " ^ str lemmas);

   230   log ("Max number of sledgehammer lemmas: " ^ str max_lems);

   231   log ("Success rate: " ^ percentage success calls ^ "%");

   232   log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls);

   233   log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success);

   234   log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa));

   235   log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover));

   236   log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail));

   237   log ("Average time for sledgehammer calls (Isabelle): " ^

   238     str3 (avg_time time_isa calls));

   239   log ("Average time for successful sledgehammer calls (ATP): " ^

   240     str3 (avg_time time_prover success));

   241   log ("Average time for failed sledgehammer calls (ATP): " ^

   242     str3 (avg_time time_prover_fail (calls - success)))

   243   )

   246 fun str_of_pos (pos, triv) =

   247   let val str0 = string_of_int o the_default 0

   248   in

   249     str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) ^

   250     (if triv then "[T]" else "")

   251   end

   253 fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,

   254      re_nontriv_success, re_proofs, re_time, re_timeout,

   255     (lemmas, lems_sos, lems_max), re_posns) =

   256  (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls);

   257   log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^

   258     " (proof: " ^ str re_proofs ^ ")");

   259   log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout);

   260   log ("Success rate: " ^ percentage re_success sh_calls ^ "%");

   261   log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls);

   262   log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^

   263     " (proof: " ^ str re_proofs ^ ")");

   264   log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas);

   265   log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos);

   266   log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max);

   267   log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time));

   268   log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^

   269     str3 (avg_time re_time re_success));

   270   if tag=""

   271   then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns))

   272   else ()

   273  )

   275 fun log_min_data log (succs, ab_ratios) =

   276   (log ("Number of successful minimizations: " ^ string_of_int succs);

   277    log ("After/before ratios: " ^ string_of_int ab_ratios)

   278   )

   280 in

   282 fun log_data id log (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =

   283   let

   284     val ShData {calls=sh_calls, ...} = sh

   286     fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else ()

   287     fun log_re tag m =

   288       log_re_data log tag sh_calls (tuple_of_re_data m)

   289     fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () =>

   290       (log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2)))

   291   in

   292     if sh_calls > 0

   293     then

   294      (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");

   295       log_sh_data log (tuple_of_sh_data sh);

   296       log "";

   297       if not mini

   298       then log_reconstructor ("", re_u) ("fully-typed ", re_uft)

   299       else

   300         app_if re_u (fn () =>

   301          (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);

   302           log "";

   303           app_if re_m (fn () =>

   304             (log_min_data log (tuple_of_min_data min); log "";

   305              log_reconstructor ("", re_m) ("fully-typed ", re_mft))))))

   306     else ()

   307   end

   309 end

   312 (* Warning: we implicitly assume single-threaded execution here! *)

   313 val data = Unsynchronized.ref ([] : (int * data) list)

   315 fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy)

   316 fun done id ({log, ...}: Mirabelle.done_args) =

   317   AList.lookup (op =) (!data) id

   318   |> Option.map (log_data id log)

   319   |> K ()

   321 fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())

   324 fun get_prover ctxt args =

   325   let

   326     fun default_prover_name () =

   327       hd (#provers (Sledgehammer_Isar.default_params ctxt []))

   328       handle Empty => error "No ATP available."

   329     fun get_prover name =

   330       (name, Sledgehammer_Run.get_minimizing_prover ctxt

   331                 Sledgehammer_Provers.Normal name)

   332   in

   333     (case AList.lookup (op =) args proverK of

   334       SOME name => get_prover name

   335     | NONE => get_prover (default_prover_name ()))

   336   end

   338 type locality = ATP_Translate.locality

   340 (* hack *)

   341 fun reconstructor_from_msg args msg =

   342   (case AList.lookup (op =) args reconstructorK of

   343     SOME name => name

   344   | NONE =>

   345     if String.isSubstring "metisFT" msg then "metisFT"

   346     else if String.isSubstring "metis" msg then "metis"

   347     else "smt")

   349 local

   351 datatype sh_result =

   352   SH_OK of int * int * (string * locality) list |

   353   SH_FAIL of int * int |

   354   SH_ERROR

   356 fun run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos

   357       vampire_force_sos hard_timeout timeout dir st =

   358   let

   359     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st

   360     val i = 1

   361     fun change_dir (SOME dir) =

   362         Config.put Sledgehammer_Provers.dest_dir dir

   363         #> Config.put SMT_Config.debug_files

   364           (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"

   365           ^ serial_string ())

   366       | change_dir NONE = I

   367     val st' =

   368       st |> Proof.map_context

   369                 (change_dir dir

   370                  #> (Option.map (Config.put ATP_Systems.e_weight_method)

   371                        e_weight_method |> the_default I)

   372                  #> (Option.map (Config.put ATP_Systems.spass_force_sos)

   373                        spass_force_sos |> the_default I)

   374                  #> (Option.map (Config.put ATP_Systems.vampire_force_sos)

   375                        vampire_force_sos |> the_default I)

   376                  #> Config.put Sledgehammer_Provers.measure_run_time true)

   377     val params as {relevance_thresholds, max_relevant, slicing, ...} =

   378       Sledgehammer_Isar.default_params ctxt

   379           [("verbose", "true"),

   380            ("type_sys", type_sys),

   381            ("max_relevant", max_relevant),

   382            ("slicing", slicing),

   383            ("timeout", string_of_int timeout)]

   384     val default_max_relevant =

   385       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing

   386         prover_name

   387     val is_appropriate_prop =

   388       Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name

   389     val is_built_in_const =

   390       Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name

   391     val relevance_fudge =

   392       Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name

   393     val relevance_override = {add = [], del = [], only = false}

   394     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i

   395     val time_limit =

   396       (case hard_timeout of

   397         NONE => I

   398       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))

   399     fun failed failure =

   400       ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,

   401         preplay = K ATP_Reconstruct.Failed_to_Play,

   402         message = K ""}, ~1)

   403     val ({outcome, used_facts, run_time_in_msecs, preplay, message}

   404          : Sledgehammer_Provers.prover_result,

   405         time_isa) = time_limit (Mirabelle.cpu_time (fn () =>

   406       let

   407         val _ = if is_appropriate_prop concl_t then ()

   408                 else raise Fail "inappropriate"

   409         val facts =

   410           Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds

   411               (the_default default_max_relevant max_relevant)

   412               is_appropriate_prop is_built_in_const relevance_fudge

   413               relevance_override chained_ths hyp_ts concl_t

   414         val problem =

   415           {state = st', goal = goal, subgoal = i,

   416            subgoal_count = Sledgehammer_Util.subgoal_count st,

   417            facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,

   418            smt_filter = NONE}

   419       in prover params (K (K "")) problem end)) ()

   420       handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut

   421            | Fail "inappropriate" => failed ATP_Proof.Inappropriate

   422     val time_prover = run_time_in_msecs |> the_default ~1

   423     val msg = message (preplay ())

   424   in

   425     case outcome of

   426       NONE => (msg, SH_OK (time_isa, time_prover, used_facts))

   427     | SOME _ => (msg, SH_FAIL (time_isa, time_prover))

   428   end

   429   handle ERROR msg => ("error: " ^ msg, SH_ERROR)

   431 fun thms_of_name ctxt name =

   432   let

   433     val lex = Keyword.get_lexicons

   434     val get = maps (Proof_Context.get_fact ctxt o fst)

   435   in

   436     Source.of_string name

   437     |> Symbol.source

   438     |> Token.source {do_recover=SOME false} lex Position.start

   439     |> Token.source_proper

   440     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE

   441     |> Source.exhaust

   442   end

   444 in

   446 fun run_sledgehammer trivial args reconstructor named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =

   447   let

   448     val triv_str = if trivial then "[T] " else ""

   449     val _ = change_data id inc_sh_calls

   450     val _ = if trivial then () else change_data id inc_sh_nontriv_calls

   451     val (prover_name, prover) = get_prover (Proof.context_of st) args

   452     val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"

   453     val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"

   454     val slicing = AList.lookup (op =) args slicingK |> the_default "true"

   455     val e_weight_method = AList.lookup (op =) args e_weight_methodK

   456     val spass_force_sos = AList.lookup (op =) args spass_force_sosK

   457       |> Option.map (curry (op <>) "false")

   458     val vampire_force_sos = AList.lookup (op =) args vampire_force_sosK

   459       |> Option.map (curry (op <>) "false")

   460     val dir = AList.lookup (op =) args keepK

   461     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)

   462     (* always use a hard timeout, but give some slack so that the automatic

   463        minimizer has a chance to do its magic *)

   464     val hard_timeout = SOME (2 * timeout)

   465     val (msg, result) =

   466       run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos

   467         vampire_force_sos hard_timeout timeout dir st

   468   in

   469     case result of

   470       SH_OK (time_isa, time_prover, names) =>

   471         let

   472           fun get_thms (_, ATP_Translate.Chained) = NONE

   473             | get_thms (name, loc) =

   474               SOME ((name, loc), thms_of_name (Proof.context_of st) name)

   475         in

   476           change_data id inc_sh_success;

   477           if trivial then () else change_data id inc_sh_nontriv_success;

   478           change_data id (inc_sh_lemmas (length names));

   479           change_data id (inc_sh_max_lems (length names));

   480           change_data id (inc_sh_time_isa time_isa);

   481           change_data id (inc_sh_time_prover time_prover);

   482           reconstructor := reconstructor_from_msg args msg;

   483           named_thms := SOME (map_filter get_thms names);

   484           log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^

   485             string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)

   486         end

   487     | SH_FAIL (time_isa, time_prover) =>

   488         let

   489           val _ = change_data id (inc_sh_time_isa time_isa)

   490           val _ = change_data id (inc_sh_time_prover_fail time_prover)

   491         in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end

   492     | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)

   493   end

   495 end

   497 fun run_minimize args reconstructor named_thms id

   498         ({pre=st, log, ...}: Mirabelle.run_args) =

   499   let

   500     val ctxt = Proof.context_of st

   501     val n0 = length (these (!named_thms))

   502     val (prover_name, _) = get_prover ctxt args

   503     val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"

   504     val timeout =

   505       AList.lookup (op =) args minimize_timeoutK

   506       |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)

   507       |> the_default 5

   508     val params = Sledgehammer_Isar.default_params ctxt

   509       [("provers", prover_name),

   510        ("verbose", "true"),

   511        ("type_sys", type_sys),

   512        ("timeout", string_of_int timeout)]

   513     val minimize =

   514       Sledgehammer_Minimize.minimize_facts prover_name params

   515           true 1 (Sledgehammer_Util.subgoal_count st)

   516     val _ = log separator

   517     val (used_facts, (preplay, message)) = minimize st (these (!named_thms))

   518     val msg = message (preplay ())

   519   in

   520     case used_facts of

   521       SOME named_thms' =>

   522         (change_data id inc_min_succs;

   523          change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));

   524          if length named_thms' = n0

   525          then log (minimize_tag id ^ "already minimal")

   526          else (reconstructor := reconstructor_from_msg args msg;

   527                named_thms := SOME named_thms';

   528                log (minimize_tag id ^ "succeeded:\n" ^ msg))

   529         )

   530     | NONE => log (minimize_tag id ^ "failed: " ^ msg)

   531   end

   534 fun run_reconstructor trivial full m name reconstructor named_thms id

   535     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =

   536   let

   537     fun do_reconstructor thms ctxt =

   538       (if !reconstructor = "sledgehammer_tac" then

   539          (fn ctxt => fn thms =>

   540             Method.insert_tac thms THEN'

   541             Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)

   542        else if !reconstructor = "smt" then

   543          SMT_Solver.smt_tac

   544        else if full orelse !reconstructor = "metisFT" then

   545          Metis_Tactics.metisFT_tac

   546        else

   547          Metis_Tactics.metis_tac) ctxt thms

   548     fun apply_reconstructor thms =

   549       Mirabelle.can_apply timeout (do_reconstructor thms) st

   551     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"

   552       | with_time (true, t) = (change_data id (inc_reconstructor_success m);

   553           if trivial then ()

   554           else change_data id (inc_reconstructor_nontriv_success m);

   555           change_data id (inc_reconstructor_lemmas m (length named_thms));

   556           change_data id (inc_reconstructor_time m t);

   557           change_data id (inc_reconstructor_posns m (pos, trivial));

   558           if name = "proof" then change_data id (inc_reconstructor_proofs m)

   559           else ();

   560           "succeeded (" ^ string_of_int t ^ ")")

   561     fun timed_reconstructor thms =

   562       (with_time (Mirabelle.cpu_time apply_reconstructor thms), true)

   563       handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m);

   564                ("timeout", false))

   565            | ERROR msg => ("error: " ^ msg, false)

   567     val _ = log separator

   568     val _ = change_data id (inc_reconstructor_calls m)

   569     val _ = if trivial then ()

   570             else change_data id (inc_reconstructor_nontriv_calls m)

   571   in

   572     maps snd named_thms

   573     |> timed_reconstructor

   574     |>> log o prefix (reconstructor_tag reconstructor id)

   575     |> snd

   576   end

   578 val try_timeout = seconds 5.0

   580 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =

   581   let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in

   582     if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal

   583     then () else

   584     let

   585       val reconstructor = Unsynchronized.ref ""

   586       val named_thms =

   587         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)

   588       val minimize = AList.defined (op =) args minimizeK

   589       val metis_ft = AList.defined (op =) args metis_ftK

   590       val trivial =

   591         Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre

   592         handle TimeLimit.TimeOut => false

   593       fun apply_reconstructor m1 m2 =

   594         if metis_ft

   595         then

   596           if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false

   597               (run_reconstructor trivial false m1 name reconstructor

   598                    (these (!named_thms))) id st)

   599           then

   600             (Mirabelle.catch_result (reconstructor_tag reconstructor) false

   601               (run_reconstructor trivial true m2 name reconstructor

   602                    (these (!named_thms))) id st; ())

   603           else ()

   604         else

   605           (Mirabelle.catch_result (reconstructor_tag reconstructor) false

   606             (run_reconstructor trivial false m1 name reconstructor

   607                  (these (!named_thms))) id st; ())

   608     in

   609       change_data id (set_mini minimize);

   610       Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor

   611                                                named_thms) id st;

   612       if is_some (!named_thms)

   613       then

   614        (apply_reconstructor Unminimized UnminimizedFT;

   615         if minimize andalso not (null (these (!named_thms)))

   616         then

   617          (Mirabelle.catch minimize_tag

   618               (run_minimize args reconstructor named_thms) id st;

   619           apply_reconstructor Minimized MinimizedFT)

   620         else ())

   621       else ()

   622     end

   623   end

   625 fun invoke args =

   626   let

   627     val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK

   628   in Mirabelle.register (init, sledgehammer_action args, done) end

   630 end

author	blanchet
	Tue, 31 May 2011 16:38:36 +0200
changeset 43929	0a97f3295642
parent 43905	b6e61d22fa61
child 44007	68e3cd19fee8
permissions	-rw-r--r--