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 false name)

   331   in

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

   333       SOME name => get_prover name

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

   335   end

   337 type locality = Sledgehammer_Filter.locality

   339 (* hack *)

   340 fun reconstructor_from_msg args msg =

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

   342     SOME name => name

   343   | NONE =>

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

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

   346     else "smt")

   348 local

   350 datatype sh_result =

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

   352   SH_FAIL of int * int |

   353   SH_ERROR

   355 fun run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos

   356       vampire_force_sos hard_timeout timeout dir st =

   357   let

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

   359     val i = 1

   360     fun change_dir (SOME dir) =

   361         Config.put Sledgehammer_Provers.dest_dir dir

   362         #> Config.put SMT_Config.debug_files

   363           (dir ^ "/" ^ Name.desymbolize false (ATP_Problem.timestamp ()) ^ "_"

   364           ^ serial_string ())

   365       | change_dir NONE = I

   366     val st' =

   367       st |> Proof.map_context

   368                 (change_dir dir

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

   370                        e_weight_method |> the_default I)

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

   372                        spass_force_sos |> the_default I)

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

   374                        vampire_force_sos |> the_default I)

   375                  #> Config.put Sledgehammer_Provers.measure_run_time true)

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

   377       Sledgehammer_Isar.default_params ctxt

   378           [("verbose", "true"),

   379            ("type_sys", type_sys),

   380            ("max_relevant", max_relevant),

   381            ("slicing", slicing),

   382            ("timeout", string_of_int timeout)]

   383     val default_max_relevant =

   384       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing

   385         prover_name

   386     val is_appropriate_prop =

   387       Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name

   388     val is_built_in_const =

   389       Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name

   390     val relevance_fudge =

   391       Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name

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

   393     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i

   394     val time_limit =

   395       (case hard_timeout of

   396         NONE => I

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

   398     fun failed failure =

   399       ({outcome = SOME failure, message = "", used_facts = [],

   400         run_time_in_msecs = NONE}, ~1)

   401     val ({outcome, message, used_facts, run_time_in_msecs}

   402          : Sledgehammer_Provers.prover_result,

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

   404       let

   405         val _ = if is_appropriate_prop concl_t then ()

   406                 else raise Fail "inappropriate"

   407         val facts =

   408           Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds

   409               (the_default default_max_relevant max_relevant)

   410               is_appropriate_prop is_built_in_const relevance_fudge

   411               relevance_override chained_ths hyp_ts concl_t

   412         val problem =

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

   414            subgoal_count = Sledgehammer_Util.subgoal_count st,

   415            facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,

   416            smt_filter = NONE}

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

   418       handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut

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

   420     val time_prover = run_time_in_msecs |> the_default ~1

   421   in

   422     case outcome of

   423       NONE => (message, SH_OK (time_isa, time_prover, used_facts))

   424     | SOME _ => (message, SH_FAIL (time_isa, time_prover))

   425   end

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

   428 fun thms_of_name ctxt name =

   429   let

   430     val lex = Keyword.get_lexicons

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

   432   in

   433     Source.of_string name

   434     |> Symbol.source

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

   436     |> Token.source_proper

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

   438     |> Source.exhaust

   439   end

   441 in

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

   444   let

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

   446     val _ = change_data id inc_sh_calls

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

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

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

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

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

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

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

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

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

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

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

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

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

   460        minimizer has a chance to do its magic *)

   461     val hard_timeout = SOME (2 * timeout)

   462     val (msg, result) =

   463       run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos

   464         vampire_force_sos hard_timeout timeout dir st

   465   in

   466     case result of

   467       SH_OK (time_isa, time_prover, names) =>

   468         let

   469           fun get_thms (_, Sledgehammer_Filter.Chained) = NONE

   470             | get_thms (name, loc) =

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

   472         in

   473           change_data id inc_sh_success;

   474           if trivial then () else change_data id inc_sh_nontriv_success;

   475           change_data id (inc_sh_lemmas (length names));

   476           change_data id (inc_sh_max_lems (length names));

   477           change_data id (inc_sh_time_isa time_isa);

   478           change_data id (inc_sh_time_prover time_prover);

   479           reconstructor := reconstructor_from_msg args msg;

   480           named_thms := SOME (map_filter get_thms names);

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

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

   483         end

   484     | SH_FAIL (time_isa, time_prover) =>

   485         let

   486           val _ = change_data id (inc_sh_time_isa time_isa)

   487           val _ = change_data id (inc_sh_time_prover_fail time_prover)

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

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

   490   end

   492 end

   494 fun run_minimize args reconstructor named_thms id

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

   496   let

   497     val ctxt = Proof.context_of st

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

   499     val (prover_name, _) = get_prover ctxt args

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

   501     val timeout =

   502       AList.lookup (op =) args minimize_timeoutK

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

   504       |> the_default 5

   505     val params as {explicit_apply, ...} = Sledgehammer_Isar.default_params ctxt

   506       [("provers", prover_name),

   507        ("verbose", "true"),

   508        ("type_sys", type_sys),

   509        ("timeout", string_of_int timeout)]

   510     val minimize =

   511       Sledgehammer_Minimize.minimize_facts prover_name params

   512           (SOME explicit_apply) true 1 (Sledgehammer_Util.subgoal_count st)

   513     val _ = log separator

   514   in

   515     case minimize st (these (!named_thms)) of

   516       (SOME named_thms', msg) =>

   517         (change_data id inc_min_succs;

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

   519          if length named_thms' = n0

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

   521          else (reconstructor := reconstructor_from_msg args msg;

   522                named_thms := SOME named_thms';

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

   524         )

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

   526   end

   529 fun run_reconstructor trivial full m name reconstructor named_thms id

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

   531   let

   532     fun do_reconstructor thms ctxt =

   533       (if !reconstructor = "sledgehammer_tac" then

   534          (fn ctxt => fn thms =>

   535             Method.insert_tac thms THEN'

   536             Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)

   537        else if !reconstructor = "smt" then

   538          SMT_Solver.smt_tac

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

   540          Metis_Tactics.metisFT_tac

   541        else

   542          Metis_Tactics.metis_tac) ctxt thms

   543     fun apply_reconstructor thms =

   544       Mirabelle.can_apply timeout (do_reconstructor thms) st

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

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

   548           if trivial then ()

   549           else change_data id (inc_reconstructor_nontriv_success m);

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

   551           change_data id (inc_reconstructor_time m t);

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

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

   554           else ();

   555           "succeeded (" ^ string_of_int t ^ ")")

   556     fun timed_reconstructor thms =

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

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

   559                ("timeout", false))

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

   562     val _ = log separator

   563     val _ = change_data id (inc_reconstructor_calls m)

   564     val _ = if trivial then ()

   565             else change_data id (inc_reconstructor_nontriv_calls m)

   566   in

   567     maps snd named_thms

   568     |> timed_reconstructor

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

   570     |> snd

   571   end

   573 val try_timeout = seconds 5.0

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

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

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

   578     then () else

   579     let

   580       val reconstructor = Unsynchronized.ref ""

   581       val named_thms =

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

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

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

   585       val trivial = Try.invoke_try (SOME try_timeout) ([], [], [], []) pre

   586         handle TimeLimit.TimeOut => false

   587       fun apply_reconstructor m1 m2 =

   588         if metis_ft

   589         then

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

   591               (run_reconstructor trivial false m1 name reconstructor

   592                    (these (!named_thms))) id st)

   593           then

   594             (Mirabelle.catch_result (reconstructor_tag reconstructor) false

   595               (run_reconstructor trivial true m2 name reconstructor

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

   597           else ()

   598         else

   599           (Mirabelle.catch_result (reconstructor_tag reconstructor) false

   600             (run_reconstructor trivial false m1 name reconstructor

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

   602     in

   603       change_data id (set_mini minimize);

   604       Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor

   605                                                named_thms) id st;

   606       if is_some (!named_thms)

   607       then

   608        (apply_reconstructor Unminimized UnminimizedFT;

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

   610         then

   611          (Mirabelle.catch minimize_tag

   612               (run_minimize args reconstructor named_thms) id st;

   613           apply_reconstructor Minimized MinimizedFT)

   614         else ())

   615       else ()

   616     end

   617   end

   619 fun invoke args =

   620   let

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

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

   624 end

author	blanchet
	Tue, 24 May 2011 00:01:33 +0200
changeset 43794	26111aafab12
parent 43793	96f62b77748f
child 43845	20e9caff1f86
permissions	-rw-r--r--