contain exponential explosion of term patterns
authorblanchet
Mon Dec 17 22:06:28 2012 +0100 (2012-12-17)
changeset 50585306c7b807e13
parent 50584 4fff0898cc0e
child 50586 e31ee2076db1
contain exponential explosion of term patterns
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 17 22:06:28 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 17 22:06:28 2012 +0100
     1.3 @@ -519,7 +519,9 @@
     1.4  val logical_consts =
     1.5    [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
     1.6  
     1.7 -fun interesting_terms_types_and_classes ctxt thy_name prover term_max_depth
     1.8 +val max_pattern_breadth = 10
     1.9 +
    1.10 +fun interesting_terms_types_and_classes ctxt prover thy_name term_max_depth
    1.11                                          type_max_depth ts =
    1.12    let
    1.13      val thy = Proof_Context.theory_of ctxt
    1.14 @@ -552,8 +554,10 @@
    1.15            []
    1.16        | patternify_term args depth (t $ u) =
    1.17          let
    1.18 -          val ps = patternify_term (u :: args) depth t
    1.19 -          val qs = "" :: patternify_term [] (depth - 1) u
    1.20 +          val ps =
    1.21 +            take max_pattern_breadth (patternify_term (u :: args) depth t)
    1.22 +          val qs =
    1.23 +            take max_pattern_breadth ("" :: patternify_term [] (depth - 1) u)
    1.24          in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end
    1.25        | patternify_term _ _ _ = []
    1.26      fun add_term_pattern feature_of =
    1.27 @@ -584,7 +588,7 @@
    1.28  fun features_of ctxt prover thy (scope, status) ts =
    1.29    let val thy_name = Context.theory_name thy in
    1.30      thy_feature_of thy_name ::
    1.31 -    interesting_terms_types_and_classes ctxt thy_name prover term_max_depth
    1.32 +    interesting_terms_types_and_classes ctxt prover thy_name term_max_depth
    1.33          type_max_depth ts
    1.34      |> status <> General ? cons (status_feature_of status)
    1.35      |> scope <> Global ? cons local_feature