# HG changeset patch # User blanchet # Date 1342593844 -7200 # Node ID 3ee5b558940249cbf648acbe7acdb82acae0591c # Parent 7b5f7ca25d17317c5f8fdd7b9e0b6c04365951d9 speed up tautology/metaness check diff -r 7b5f7ca25d17 -r 3ee5b5589402 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200 @@ -113,14 +113,12 @@ handle TYPE _ => @{prop True} end -fun all_non_tautological_facts_of ctxt prover thy css_table = +fun all_non_tautological_facts_of thy css_table = Sledgehammer_Fact.all_facts_of thy css_table - |> filter_out ((Sledgehammer_Filter_MaSh.is_likely_tautology ctxt prover orf - Sledgehammer_Filter_MaSh.is_too_meta) o snd) + |> filter_out (Sledgehammer_Filter_MaSh.is_likely_tautology_or_too_meta o snd) fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = let - val atp = atp_for_format format val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val type_enc = type_enc |> type_enc_from_string Strict @@ -128,7 +126,7 @@ val mono = not (is_type_enc_polymorphic type_enc) val path = file_name |> Path.explode val _ = File.write path "" - val facts = all_non_tautological_facts_of ctxt atp thy css_table + val facts = all_non_tautological_facts_of thy css_table val atp_problem = facts |> map (fn ((_, loc), th) => diff -r 7b5f7ca25d17 -r 3ee5b5589402 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 @@ -26,8 +26,8 @@ val max_facts_slack = 2 -fun all_names ctxt prover = - filter_out (is_likely_tautology ctxt prover orf is_too_meta) +val all_names = + filter_out (is_likely_tautology_or_too_meta) #> map (rpair () o Thm.get_name_hint) #> Symtab.make fun evaluate_mash_suggestions ctxt params thy file_name = @@ -40,7 +40,7 @@ val lines = path |> File.read_lines val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = all_facts_of thy css_table - val all_names = all_names ctxt prover (facts |> map snd) + val all_names = all_names (facts |> map snd) val iter_ok = Unsynchronized.ref 0 val mash_ok = Unsynchronized.ref 0 val mesh_ok = Unsynchronized.ref 0 diff -r 7b5f7ca25d17 -r 3ee5b5589402 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200 @@ -13,7 +13,7 @@ val generate_features : Proof.context -> string -> theory -> bool -> string -> unit val generate_isa_dependencies : - Proof.context -> string -> theory -> bool -> string -> unit + theory -> bool -> string -> unit val generate_prover_dependencies : Proof.context -> params -> theory -> bool -> string -> unit val generate_commands : Proof.context -> string -> theory -> string -> unit @@ -49,8 +49,8 @@ val thy_name_of_fact = hd o Long_Name.explode fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact -fun all_names ctxt prover = - filter_out (is_likely_tautology ctxt prover orf is_too_meta) +val all_names = + filter_out (is_likely_tautology_or_too_meta) #> map (rpair () o Thm.get_name_hint) #> Symtab.make fun generate_accessibility thy include_thy file_name = @@ -90,7 +90,7 @@ in File.append path s end in List.app do_fact facts end -fun generate_isa_dependencies ctxt prover thy include_thy file_name = +fun generate_isa_dependencies thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" @@ -98,7 +98,7 @@ all_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) |> map snd - val all_names = all_names ctxt prover ths + val all_names = all_names ths fun do_thm th = let val name = Thm.get_name_hint th @@ -117,7 +117,7 @@ all_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) val ths = facts |> map snd - val all_names = all_names ctxt prover ths + val all_names = all_names ths fun is_dep dep (_, th) = Thm.get_name_hint th = dep fun add_isa_dep facts dep accum = if exists (is_dep dep) accum then @@ -165,7 +165,7 @@ facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) val ths = facts |> map snd - val all_names = all_names ctxt prover ths + val all_names = all_names ths fun do_fact ((_, (_, status)), th) prevs = let val name = Thm.get_name_hint th diff -r 7b5f7ca25d17 -r 3ee5b5589402 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 18 08:44:04 2012 +0200 @@ -87,6 +87,7 @@ val new_skolem_var_name_from_const : string -> string val atp_logical_consts : string list val atp_irrelevant_consts : string list + val atp_widely_irrelevant_consts : string list val atp_schematic_consts_of : term -> typ list Symtab.table val is_type_enc_higher_order : type_enc -> bool val is_type_enc_polymorphic : type_enc -> bool diff -r 7b5f7ca25d17 -r 3ee5b5589402 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 @@ -28,8 +28,7 @@ val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list val mesh_facts : int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list - val is_likely_tautology : Proof.context -> string -> thm -> bool - val is_too_meta : thm -> bool + val is_likely_tautology_or_too_meta : thm -> bool val theory_ord : theory * theory -> order val thm_ord : thm * thm -> order val features_of : @@ -201,6 +200,37 @@ end +fun is_likely_tautology_or_too_meta th = + let + val is_boring_const = member (op =) atp_widely_irrelevant_consts + fun is_boring_bool t = + not (exists_Const (not o is_boring_const o fst) t) orelse + exists_type (exists_subtype (curry (op =) @{typ prop})) t + fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t + | is_boring_prop (@{const "==>"} $ t $ u) = + is_boring_prop t andalso is_boring_prop u + | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) = + is_boring_prop t andalso is_boring_prop u + | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) = + is_boring_bool t andalso is_boring_bool u + | is_boring_prop _ = true + in + is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) + end + +fun theory_ord p = + if Theory.eq_thy p then + EQUAL + else if Theory.subthy p then + LESS + else if Theory.subthy (swap p) then + GREATER + else case int_ord (pairself (length o Theory.ancestors_of) p) of + EQUAL => string_ord (pairself Context.theory_name p) + | order => order + +val thm_ord = theory_ord o pairself theory_of_thm + fun interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth ts = let @@ -243,28 +273,6 @@ end in [] |> fold add_patterns ts |> sort string_ord end -fun is_likely_tautology ctxt prover th = - null (interesting_terms_types_and_classes ctxt prover 0 ~1 [prop_of th]) - andalso not (Thm.eq_thm_prop (@{thm ext}, th)) - -(* ### FIXME: optimize *) -fun is_too_meta th = - fastype_of (Object_Logic.atomize_term (theory_of_thm th) (prop_of th)) - <> @{typ bool} - -fun theory_ord p = - if Theory.eq_thy p then - EQUAL - else if Theory.subthy p then - LESS - else if Theory.subthy (swap p) then - GREATER - else case int_ord (pairself (length o Theory.ancestors_of) p) of - EQUAL => string_ord (pairself Context.theory_name p) - | order => order - -val thm_ord = theory_ord o pairself theory_of_thm - fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) val term_max_depth = 1 @@ -545,13 +553,18 @@ facts = let val timer = Timer.startRealTimer () +fun check_timer s = + tracing ("*** " ^ s ^ " " ^ PolyML.makestring (Timer.checkRealTimer timer)) val prover = hd provers fun timed_out frac = Time.> (Timer.checkRealTimer timer, time_mult frac timeout) +val _ = check_timer "begin" (*###*) val {fact_graph, ...} = mash_get ctxt +val _ = check_timer " got" (*###*) val new_facts = facts |> filter_out (is_fact_in_graph fact_graph) |> sort (thm_ord o pairself snd) +val _ = check_timer " new facts" (*###*) in if null new_facts then "" @@ -559,9 +572,10 @@ let val ths = facts |> map snd val all_names = - ths |> filter_out (is_likely_tautology ctxt prover orf is_too_meta) + ths |> filter_out is_likely_tautology_or_too_meta |> map (rpair () o Thm.get_name_hint) |> Symtab.make +val _ = check_timer " all names" (*###*) fun do_fact _ (accum as (_, true)) = accum | do_fact ((_, (_, status)), th) ((parents, upds), false) = let @@ -571,8 +585,10 @@ val upd = (name, parents, feats, deps) in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end val parents = parents_wrt_facts ctxt facts fact_graph +val _ = check_timer " parents" (*###*) val ((_, upds), _) = ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev +val _ = check_timer " did facts" (*###*) val n = length upds fun trans {thys, fact_graph} = let @@ -580,8 +596,10 @@ if Graph.is_empty fact_graph then mash_INIT else mash_ADD val (upds, fact_graph) = ([], fact_graph) |> fold (update_fact_graph ctxt) upds +val _ = check_timer " updated" (*###*) in (mash_INIT_or_ADD ctxt overlord (rev upds); +check_timer " inited/added" (*###*); {thys = thys |> add_thys_for thy, fact_graph = fact_graph}) end