# HG changeset patch # User blanchet # Date 1306485008 -7200 # Node ID 21b6baec55b1ed1834ec155212af7808563ba3c8 # Parent 0dca147765f45fd1d8848f1dc712fde7a7b3d1f7 renamed "metis_timeout" to "preplay_timeout" and continued implementation diff -r 0dca147765f4 -r 21b6baec55b1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200 @@ -88,7 +88,7 @@ ("isar_proof", "false"), ("isar_shrink_factor", "1"), ("slicing", "true"), - ("metis_timeout", "5")] + ("preplay_timeout", "5")] val alias_params = [("prover", "provers"), @@ -107,7 +107,7 @@ val params_for_minimize = ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters", "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout", - "metis_timeout"] + "preplay_timeout"] val property_dependent_params = ["provers", "full_types", "timeout"] @@ -277,8 +277,9 @@ val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") val slicing = not auto andalso lookup_bool "slicing" val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout - val metis_timeout = - if auto then Time.zeroTime else lookup_time "metis_timeout" |> the_timeout + val preplay_timeout = + if auto then Time.zeroTime + else lookup_time "preplay_timeout" |> the_timeout val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, @@ -287,7 +288,7 @@ max_new_mono_instances = max_new_mono_instances, type_sys = type_sys, explicit_apply = explicit_apply, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slicing = slicing, - timeout = timeout, metis_timeout = metis_timeout, expect = expect} + timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params auto ctxt = extract_params auto (default_raw_params ctxt) diff -r 0dca147765f4 -r 21b6baec55b1 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 10:30:08 2011 +0200 @@ -44,7 +44,7 @@ fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, max_new_mono_instances, type_sys, isar_proof, - isar_shrink_factor, metis_timeout, ...} : params) + isar_shrink_factor, preplay_timeout, ...} : params) explicit_apply_opt silent (prover : prover) timeout i n state facts = let val ctxt = Proof.context_of state @@ -70,7 +70,7 @@ max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slicing = false, - timeout = timeout, metis_timeout = metis_timeout, expect = ""} + timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} val facts = facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) val problem = diff -r 0dca147765f4 -r 21b6baec55b1 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200 @@ -35,7 +35,7 @@ isar_shrink_factor: int, slicing: bool, timeout: Time.time, - metis_timeout: Time.time, + preplay_timeout: Time.time, expect: string} datatype prover_fact = @@ -279,7 +279,7 @@ isar_shrink_factor: int, slicing: bool, timeout: Time.time, - metis_timeout: Time.time, + preplay_timeout: Time.time, expect: string} datatype prover_fact = @@ -870,23 +870,32 @@ end in do_slice timeout 1 NONE Time.zeroTime end -(* taken from "Mirabelle" and generalized *) -fun can_apply timeout tac state i = +(* based on "Mirabelle.can_apply" and generalized *) +fun try_apply timeout tac state i = let val {context = ctxt, facts, goal} = Proof.goal state val full_tac = Method.insert_tac facts i THEN tac ctxt i - in - case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of - SOME (SOME _) => true - | _ => false + in try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal end + +fun try_metis debug timeout ths = + try_apply timeout (Config.put Metis_Tactics.verbose debug + #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) + +datatype metis_try = + Preplayed of string * Time.time | + Preplay_Timed_Out | + Preplay_Failed + +fun preplay debug timeout ths state i = + let val timer = Timer.startRealTimer () in + case try_metis debug timeout ths state i of + SOME (SOME _) => Preplayed ("metis", Timer.checkRealTimer timer) + | SOME NONE => Preplay_Failed + | NONE => Preplay_Timed_Out end -fun can_apply_metis debug timeout ths = - can_apply timeout (Config.put Metis_Tactics.verbose debug - #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) - fun run_smt_solver auto name - (params as {debug, verbose, blocking, metis_timeout, ...}) + (params as {debug, verbose, blocking, preplay_timeout, ...}) minimize_command ({state, subgoal, subgoal_count, facts, smt_filter, ...} : prover_problem) = @@ -903,13 +912,13 @@ case outcome of NONE => let - val (method, settings) = - if can_apply_metis debug metis_timeout (map snd used_facts) state - subgoal then - ("metis", "") - else - ("smt", if name = SMT_Solver.solver_name_of ctxt then "" - else "smt_solver = " ^ maybe_quote name) + val (settings, method, time) = + case preplay debug preplay_timeout (map snd used_facts) state + subgoal of + Preplayed (method, time) => (method, "", SOME time) + | _ => (if name = SMT_Solver.solver_name_of ctxt then "" + else "smt_solver = " ^ maybe_quote name, + "smt", NONE) in try_command_line (proof_banner auto blocking name) (apply_on_subgoal settings subgoal subgoal_count ^