# HG changeset patch # User blanchet # Date 1291632084 -3600 # Node ID 07526f5466806a849ed3d4c4af17a585e2567f61 # Parent d06ffd777f1f841010dc4eb20418fe9b69b27c4c handle "max_relevant" uniformly diff -r d06ffd777f1f -r 07526f546680 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Dec 06 11:26:17 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Dec 06 11:41:24 2010 +0100 @@ -369,7 +369,7 @@ val problem = {state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, - facts = facts |> map Sledgehammer.Untranslated, only = true} + facts = facts |> map Sledgehammer.Untranslated} val time_limit = (case hard_timeout of NONE => I diff -r d06ffd777f1f -r 07526f546680 src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Mon Dec 06 11:26:17 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Mon Dec 06 11:41:24 2010 +0100 @@ -43,8 +43,7 @@ (prop_of goal)) val problem = {state = Proof.init ctxt, goal = goal, subgoal = i, - facts = map Sledgehammer.Untranslated facts, - only = true, subgoal_count = n} + subgoal_count = n, facts = map Sledgehammer.Untranslated facts} in (case prover params (K "") problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME diff -r d06ffd777f1f -r 07526f546680 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Dec 06 11:26:17 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Dec 06 11:41:24 2010 +0100 @@ -39,8 +39,7 @@ goal: thm, subgoal: int, subgoal_count: int, - facts: fact list, - only: bool} + facts: fact list} type prover_result = {outcome: failure option, @@ -224,8 +223,7 @@ goal: thm, subgoal: int, subgoal_count: int, - facts: fact list, - only: bool} + facts: fact list} type prover_result = {outcome: failure option, @@ -287,18 +285,15 @@ fun run_atp auto atp_name {exec, required_execs, arguments, has_incomplete_mode, proof_delims, - known_failures, default_max_relevant, explicit_forall, - use_conjecture_for_hypotheses} - ({debug, verbose, overlord, full_types, explicit_apply, - max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) - minimize_command - ({state, goal, subgoal, facts, only, ...} : prover_problem) = + known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} + ({debug, verbose, overlord, full_types, explicit_apply, isar_proof, + isar_shrink_factor, timeout, ...} : params) + minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = let val ctxt = Proof.context_of state val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal val facts = - facts |> not only ? take (the_default default_max_relevant max_relevant) - |> map (translated_fact ctxt) + facts |> map (translated_fact ctxt) val dest_dir = if overlord then getenv "ISABELLE_HOME_USER" else Config.get ctxt dest_dir val problem_prefix = Config.get ctxt problem_prefix @@ -538,9 +533,8 @@ (Config.put Metis_Tactics.verbose debug #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i -fun run_smt_solver auto name (params as {debug, max_relevant, ...}) - minimize_command - ({state, subgoal, subgoal_count, facts, only, ...} : prover_problem) = +fun run_smt_solver auto name (params as {debug, ...}) minimize_command + ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = let val (remote, suffix) = case try (unprefix remote_prefix) name of @@ -551,13 +545,9 @@ #> Config.put SMT_Config.verbose debug #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit val state = state |> Proof.map_context repair_context - val ctxt = Proof.context_of state val thy = Proof.theory_of state val get_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated - val default_max_relevant = SMT_Solver.default_max_relevant ctxt suffix - val facts = - facts |> map_filter get_fact - |> not only ? take (the_default default_max_relevant max_relevant) + val facts = facts |> map_filter get_fact val {outcome, used_facts, run_time_in_msecs} = smt_filter_loop params remote state subgoal facts val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) @@ -595,19 +585,21 @@ end fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) - auto minimize_command - (problem as {state, goal, subgoal, subgoal_count, facts, ...}) - name = + auto minimize_command only + {state, goal, subgoal, subgoal_count, facts} name = let val ctxt = Proof.context_of state val birth_time = Time.now () val death_time = Time.+ (birth_time, timeout) val max_relevant = the_default (default_max_relevant_for_prover ctxt name) max_relevant - val num_facts = Int.min (length facts, max_relevant) + val num_facts = length facts |> not only ? Integer.min max_relevant val desc = prover_description ctxt params name num_facts subgoal subgoal_count goal val prover = get_prover ctxt auto name + val problem = + {state = state, goal = goal, subgoal = subgoal, + subgoal_count = subgoal_count, facts = take num_facts facts} fun go () = let fun really_go () = @@ -694,8 +686,8 @@ |> map maybe_translate val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - facts = facts, only = only} - val run_prover = run_prover params auto minimize_command + facts = facts} + val run_prover = run_prover params auto minimize_command only in if debug then Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^ diff -r d06ffd777f1f -r 07526f546680 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Dec 06 11:26:17 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Dec 06 11:41:24 2010 +0100 @@ -59,7 +59,7 @@ val {goal, ...} = Proof.goal state val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - facts = facts, only = true} + facts = facts} val result as {outcome, used_facts, ...} = prover params (K "") problem in Output.urgent_message