# HG changeset patch # User blanchet # Date 1355778388 -3600 # Node ID 306c7b807e136d3c59ccbe45bbf807eae2945ea8 # Parent 4fff0898cc0e4befa53cd1be6f4d17c14016c1db contain exponential explosion of term patterns diff -r 4fff0898cc0e -r 306c7b807e13 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Dec 17 22:06:28 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Dec 17 22:06:28 2012 +0100 @@ -519,7 +519,9 @@ val logical_consts = [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts -fun interesting_terms_types_and_classes ctxt thy_name prover term_max_depth +val max_pattern_breadth = 10 + +fun interesting_terms_types_and_classes ctxt prover thy_name term_max_depth type_max_depth ts = let val thy = Proof_Context.theory_of ctxt @@ -552,8 +554,10 @@ [] | patternify_term args depth (t $ u) = let - val ps = patternify_term (u :: args) depth t - val qs = "" :: patternify_term [] (depth - 1) u + val ps = + take max_pattern_breadth (patternify_term (u :: args) depth t) + val qs = + take max_pattern_breadth ("" :: patternify_term [] (depth - 1) u) in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end | patternify_term _ _ _ = [] fun add_term_pattern feature_of = @@ -584,7 +588,7 @@ fun features_of ctxt prover thy (scope, status) ts = let val thy_name = Context.theory_name thy in thy_feature_of thy_name :: - interesting_terms_types_and_classes ctxt thy_name prover term_max_depth + interesting_terms_types_and_classes ctxt prover thy_name term_max_depth type_max_depth ts |> status <> General ? cons (status_feature_of status) |> scope <> Global ? cons local_feature