# HG changeset patch # User blanchet # Date 1304369535 -7200 # Node ID a7a30721767ad4d3453505d29dc9b26fe397feb0 # Parent 381fdcab0f36e30a11254a876de7ef51138573d5 have each ATP filter out dangerous facts for themselves, based on their type system diff -r 381fdcab0f36 -r a7a30721767a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 02 22:31:46 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 02 22:52:15 2011 +0200 @@ -377,8 +377,6 @@ Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i - val fairly_sound = - Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys val time_limit = (case hard_timeout of NONE => I @@ -388,8 +386,7 @@ time_isa) = time_limit (Mirabelle.cpu_time (fn () => let val facts = - Sledgehammer_Filter.relevant_facts ctxt fairly_sound - relevance_thresholds + Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t val problem = diff -r 381fdcab0f36 -r a7a30721767a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Mon May 02 22:31:46 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Mon May 02 22:52:15 2011 +0200 @@ -125,11 +125,8 @@ val relevance_override = {add = [], del = [], only = false} val subgoal = 1 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal - val fairly_sound = - Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys val facts = - Sledgehammer_Filter.relevant_facts ctxt fairly_sound - relevance_thresholds + Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override facts hyp_ts concl_t |> map (fst o fst) diff -r 381fdcab0f36 -r a7a30721767a src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon May 02 22:31:46 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon May 02 22:52:15 2011 +0200 @@ -41,13 +41,14 @@ Proof.context -> unit Symtab.table -> thm list -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list val all_facts : - Proof.context -> 'a Symtab.table -> bool -> bool -> relevance_fudge - -> thm list -> thm list -> (((unit -> string) * locality) * (bool * thm)) list + Proof.context -> 'a Symtab.table -> bool -> relevance_fudge -> thm list + -> thm list -> (((unit -> string) * locality) * (bool * thm)) list val const_names_in_fact : theory -> (string * typ -> term list -> bool * term list) -> term -> string list + val is_dangerous_term : term -> bool val relevant_facts : - Proof.context -> bool -> real * real -> int + Proof.context -> real * real -> int -> (string * typ -> term list -> bool * term list) -> relevance_fudge -> relevance_override -> thm list -> term list -> term -> ((string * locality) * thm) list @@ -772,24 +773,20 @@ equations like "?x = ()". The resulting clauses will have no type constraint, yielding false proofs. Even "bool" leads to many unsound proofs, though only for higher-order problems. *) -val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}]; +val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}] (* Facts containing variables of type "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types are omitted. *) -fun is_dangerous_term fairly_sound t = - not fairly_sound andalso - let val t = transform_elim_term t in - has_bound_or_var_of_type dangerous_types t orelse - is_exhaustive_finite t - end +val is_dangerous_term = + transform_elim_term + #> has_bound_or_var_of_type dangerous_types orf is_exhaustive_finite -fun is_theorem_bad_for_atps fairly_sound thm = +fun is_theorem_bad_for_atps thm = let val t = prop_of thm in is_formula_too_complex t orelse exists_type type_has_top_sort t orelse - is_dangerous_term fairly_sound t orelse exists_sledgehammer_const t orelse - exists_low_level_class_const t orelse is_metastrange_theorem thm orelse - is_that_fact thm + exists_sledgehammer_const t orelse exists_low_level_class_const t orelse + is_metastrange_theorem thm orelse is_that_fact thm end fun clasimpset_rules_of ctxt = @@ -800,7 +797,7 @@ val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end -fun all_facts ctxt reserved really_all fairly_sound +fun all_facts ctxt reserved really_all ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths chained_ths = let @@ -846,7 +843,7 @@ pair 1 #> fold (fn th => fn (j, rest) => (j + 1, - if is_theorem_bad_for_atps fairly_sound th andalso + if is_theorem_bad_for_atps th andalso not (member Thm.eq_thm add_ths th) then rest else @@ -890,9 +887,9 @@ fun external_frees t = [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) -fun relevant_facts ctxt fairly_sound (threshold0, threshold1) max_relevant - is_built_in_const fudge (override as {add, only, ...}) - chained_ths hyp_ts concl_t = +fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const + fudge (override as {add, only, ...}) chained_ths hyp_ts + concl_t = let val thy = Proof_Context.theory_of ctxt val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), @@ -908,7 +905,7 @@ maps (map (fn ((name, loc), th) => ((K name, loc), (true, th))) o fact_from_ref ctxt reserved chained_ths) add else - all_facts ctxt reserved false fairly_sound fudge add_ths chained_ths) + all_facts ctxt reserved false fudge add_ths chained_ths) |> instantiate_inducts ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) |> rearrange_facts ctxt (respect_no_atp andalso not only) diff -r 381fdcab0f36 -r a7a30721767a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 22:31:46 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 22:52:15 2011 +0200 @@ -68,7 +68,7 @@ val smt_slice_fact_frac : real Unsynchronized.ref val smt_slice_time_frac : real Unsynchronized.ref val smt_slice_min_secs : int Unsynchronized.ref - + (* end *) val das_Tool : string val select_smt_solver : string -> Proof.context -> Proof.context val is_smt_prover : Proof.context -> string -> bool @@ -86,7 +86,6 @@ val weight_smt_fact : theory -> int -> ((string * locality) * thm) * int -> (string * locality) * (int option * thm) - val is_rich_type_sys_fairly_sound : rich_type_system -> bool val untranslated_fact : prover_fact -> (string * locality) * thm val smt_weighted_fact : theory -> int -> prover_fact * int @@ -312,10 +311,6 @@ fun weight_smt_fact thy num_facts ((info, th), j) = (info, (smt_fact_weight j num_facts, th |> Thm.transfer thy)) -fun is_rich_type_sys_fairly_sound (Dumb_Type_Sys type_sys) = - is_type_sys_fairly_sound type_sys - | is_rich_type_sys_fairly_sound (Smart_Type_Sys full_types) = full_types - fun untranslated_fact (Untranslated_Fact p) = p | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th) fun atp_translated_fact ctxt fact = @@ -432,8 +427,12 @@ val num_facts = length facts |> is_none max_relevant ? Integer.min default_max_relevant + val fairly_sound = is_type_sys_fairly_sound type_sys val facts = - facts |> take num_facts + facts |> fairly_sound + ? filter_out (is_dangerous_term o prop_of o snd + o untranslated_fact) + |> take num_facts |> not (null blacklist) ? filter_out (member (op =) blacklist o fst o untranslated_fact) @@ -718,7 +717,7 @@ " fact" ^ plural_s num_facts ^ ": " ^ string_for_failure (failure_from_smt_failure (the outcome)) ^ " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^ - plural_s new_num_facts + plural_s new_num_facts ^ "..." |> Output.urgent_message else () diff -r 381fdcab0f36 -r a7a30721767a src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 02 22:31:46 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 02 22:52:15 2011 +0200 @@ -99,7 +99,7 @@ prover_description ctxt params name num_facts subgoal subgoal_count goal val problem = {state = state, goal = goal, subgoal = subgoal, - subgoal_count = subgoal_count, facts = take num_facts facts, + subgoal_count = subgoal_count, facts = facts |> take num_facts, smt_filter = smt_filter} fun really_go () = problem @@ -182,7 +182,6 @@ val thy = Proof_Context.theory_of ctxt val {facts = chained_ths, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i - val fairly_sound = is_rich_type_sys_fairly_sound type_sys val _ = () |> not blocking ? kill_provers val _ = case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") @@ -211,7 +210,7 @@ |> (if blocking then smart_par_list_map else map) (launch problem) |> exists fst |> rpair state end - fun get_facts label fairly_sound relevance_fudge provers = + fun get_facts label relevance_fudge provers = let val max_max_relevant = case max_relevant of @@ -224,7 +223,7 @@ val is_built_in_const = is_built_in_const_for_prover ctxt (hd provers) in - relevant_facts ctxt fairly_sound relevance_thresholds max_max_relevant + relevant_facts ctxt relevance_thresholds max_max_relevant is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t |> tap (fn facts => @@ -244,15 +243,14 @@ if null atps then accum else - launch_provers state - (get_facts "ATP" fairly_sound atp_relevance_fudge o K atps) - (K (Untranslated_Fact o fst)) (K (K NONE)) atps + launch_provers state (get_facts "ATP" atp_relevance_fudge o K atps) + (K (Untranslated_Fact o fst)) (K (K NONE)) atps fun launch_smts accum = if null smts then accum else let - val facts = get_facts "SMT solver" true smt_relevance_fudge smts + val facts = get_facts "SMT solver" smt_relevance_fudge smts val weight = SMT_Weighted_Fact oo weight_smt_fact thy fun smt_filter facts = (if debug then curry (op o) SOME diff -r 381fdcab0f36 -r a7a30721767a src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Mon May 02 22:31:46 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Mon May 02 22:52:15 2011 +0200 @@ -32,10 +32,8 @@ Sledgehammer_Provers.relevance_fudge_for_prover ctxt name val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i - val fairly_sound = - Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys val facts = - Sledgehammer_Filter.relevant_facts ctxt fairly_sound relevance_thresholds + Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t val problem = diff -r 381fdcab0f36 -r a7a30721767a src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Mon May 02 22:31:46 2011 +0200 +++ b/src/HOL/ex/tptp_export.ML Mon May 02 22:52:15 2011 +0200 @@ -22,7 +22,7 @@ val fact_name_of = prefix Sledgehammer_ATP_Translate.fact_prefix o ascii_of fun facts_of thy = - Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty true + Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty true Sledgehammer_Provers.atp_relevance_fudge [] [] fun fold_body_thms f =