compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
authorblanchet
Fri Jun 10 12:01:15 2011 +0200 (2011-06-10)
changeset 43351b19d95b4d736
parent 43345 165188299a25
child 43352 597f31069e18
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/ex/atp_export.ML
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jun 09 23:30:18 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jun 10 12:01:15 2011 +0200
     1.3 @@ -408,10 +408,13 @@
     1.4          val _ = if is_appropriate_prop concl_t then ()
     1.5                  else raise Fail "inappropriate"
     1.6          val facts =
     1.7 -          Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
     1.8 -              (the_default default_max_relevant max_relevant)
     1.9 -              is_appropriate_prop is_built_in_const relevance_fudge
    1.10 -              relevance_override chained_ths hyp_ts concl_t
    1.11 +          Sledgehammer_Filter.nearly_all_facts ctxt relevance_override
    1.12 +                                               chained_ths hyp_ts concl_t
    1.13 +          |> filter (is_appropriate_prop o prop_of o snd)
    1.14 +          |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    1.15 +                 (the_default default_max_relevant max_relevant)
    1.16 +                 is_built_in_const relevance_fudge relevance_override
    1.17 +                 chained_ths hyp_ts concl_t
    1.18          val problem =
    1.19            {state = st', goal = goal, subgoal = i,
    1.20             subgoal_count = Sledgehammer_Util.subgoal_count st,
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Jun 09 23:30:18 2011 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jun 10 12:01:15 2011 +0200
     2.3 @@ -110,7 +110,7 @@
     2.4      (case Prooftab.lookup (!proof_table) (line_num, col_num) of
     2.5         SOME proofs =>
     2.6         let
     2.7 -         val {context = ctxt, facts, goal} = Proof.goal pre
     2.8 +         val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
     2.9           val prover = AList.lookup (op =) args "prover"
    2.10                        |> the_default default_prover
    2.11           val {relevance_thresholds, max_relevant, slicing, ...} =
    2.12 @@ -130,10 +130,13 @@
    2.13           val subgoal = 1
    2.14           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
    2.15           val facts =
    2.16 -           Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    2.17 -               (the_default default_max_relevant max_relevant)
    2.18 -               is_appropriate_prop is_built_in_const relevance_fudge
    2.19 -               relevance_override facts hyp_ts concl_t
    2.20 +          Sledgehammer_Filter.nearly_all_facts ctxt relevance_override
    2.21 +                                               chained_ths hyp_ts concl_t
    2.22 +          |> filter (is_appropriate_prop o prop_of o snd)
    2.23 +          |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    2.24 +                 (the_default default_max_relevant max_relevant)
    2.25 +                 is_built_in_const relevance_fudge relevance_override
    2.26 +                 chained_ths hyp_ts concl_t
    2.27             |> map (fst o fst)
    2.28           val (found_facts, lost_facts) =
    2.29             flat proofs |> sort_distinct string_ord
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jun 09 23:30:18 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Jun 10 12:01:15 2011 +0200
     3.3 @@ -39,19 +39,23 @@
     3.4    val new_monomorphizer : bool Config.T
     3.5    val ignore_no_atp : bool Config.T
     3.6    val instantiate_inducts : bool Config.T
     3.7 +  val const_names_in_fact :
     3.8 +    theory -> (string * typ -> term list -> bool * term list) -> term
     3.9 +    -> string list
    3.10    val fact_from_ref :
    3.11      Proof.context -> unit Symtab.table -> thm list
    3.12      -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
    3.13    val all_facts :
    3.14 -    Proof.context -> 'a Symtab.table -> bool -> (term -> bool) -> thm list
    3.15 -    -> thm list -> (((unit -> string) * locality) * thm) list
    3.16 -  val const_names_in_fact :
    3.17 -    theory -> (string * typ -> term list -> bool * term list) -> term
    3.18 -    -> string list
    3.19 +    Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list
    3.20 +    -> (((unit -> string) * locality) * thm) list
    3.21 +  val nearly_all_facts :
    3.22 +    Proof.context -> relevance_override -> thm list -> term list -> term
    3.23 +    -> (((unit -> string) * locality) * thm) list
    3.24    val relevant_facts :
    3.25 -    Proof.context -> real * real -> int -> (term -> bool)
    3.26 +    Proof.context -> real * real -> int
    3.27      -> (string * typ -> term list -> bool * term list) -> relevance_fudge
    3.28      -> relevance_override -> thm list -> term list -> term
    3.29 +    -> (((unit -> string) * locality) * thm) list
    3.30      -> ((string * locality) * thm) list
    3.31  end;
    3.32  
    3.33 @@ -778,12 +782,11 @@
    3.34  (**** Predicates to detect unwanted facts (prolific or likely to cause
    3.35        unsoundness) ****)
    3.36  
    3.37 -fun is_theorem_bad_for_atps is_appropriate_prop thm =
    3.38 +fun is_theorem_bad_for_atps thm =
    3.39    let val t = prop_of thm in
    3.40 -    not (is_appropriate_prop t) orelse is_formula_too_complex t orelse
    3.41 -    exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse
    3.42 -    exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
    3.43 -    is_that_fact thm
    3.44 +    is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
    3.45 +    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    3.46 +    is_metastrange_theorem thm orelse is_that_fact thm
    3.47    end
    3.48  
    3.49  fun meta_equify (@{const Trueprop}
    3.50 @@ -810,7 +813,7 @@
    3.51                    |> add Simp normalize_simp_prop snd simps
    3.52    end
    3.53  
    3.54 -fun all_facts ctxt reserved really_all is_appropriate_prop add_ths chained_ths =
    3.55 +fun all_facts ctxt reserved really_all add_ths chained_ths =
    3.56    let
    3.57      val thy = Proof_Context.theory_of ctxt
    3.58      val global_facts = Global_Theory.facts_of thy
    3.59 @@ -860,7 +863,7 @@
    3.60              #> fold (fn th => fn (j, (multis, unis)) =>
    3.61                          (j + 1,
    3.62                           if not (member Thm.eq_thm_prop add_ths th) andalso
    3.63 -                            is_theorem_bad_for_atps is_appropriate_prop th then
    3.64 +                            is_theorem_bad_for_atps th then
    3.65                             (multis, unis)
    3.66                           else
    3.67                             let
    3.68 @@ -894,30 +897,36 @@
    3.69  fun external_frees t =
    3.70    [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
    3.71  
    3.72 +fun nearly_all_facts ctxt ({add, only, ...} : relevance_override) chained_ths
    3.73 +                     hyp_ts concl_t =
    3.74 +  let
    3.75 +    val thy = Proof_Context.theory_of ctxt
    3.76 +    val reserved = reserved_isar_keyword_table ()
    3.77 +    val add_ths = Attrib.eval_thms ctxt add
    3.78 +    val ind_stmt =
    3.79 +      Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
    3.80 +      |> Object_Logic.atomize_term thy
    3.81 +    val ind_stmt_xs = external_frees ind_stmt
    3.82 +  in
    3.83 +    (if only then
    3.84 +       maps (map (fn ((name, loc), th) => ((K name, loc), th))
    3.85 +             o fact_from_ref ctxt reserved chained_ths) add
    3.86 +     else
    3.87 +       all_facts ctxt reserved false add_ths chained_ths)
    3.88 +    |> Config.get ctxt instantiate_inducts
    3.89 +       ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
    3.90 +    |> (not (Config.get ctxt ignore_no_atp) andalso not only)
    3.91 +       ? filter_out (No_ATPs.member ctxt o snd)
    3.92 +    |> uniquify
    3.93 +  end
    3.94 +
    3.95  fun relevant_facts ctxt (threshold0, threshold1) max_relevant
    3.96 -        is_appropriate_prop is_built_in_const fudge
    3.97 -        (override as {add, only, ...}) chained_ths hyp_ts concl_t =
    3.98 +                   is_built_in_const fudge (override as {only, ...}) chained_ths
    3.99 +                   hyp_ts concl_t facts =
   3.100    let
   3.101      val thy = Proof_Context.theory_of ctxt
   3.102      val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
   3.103                            1.0 / Real.fromInt (max_relevant + 1))
   3.104 -    val add_ths = Attrib.eval_thms ctxt add
   3.105 -    val reserved = reserved_isar_keyword_table ()
   3.106 -    val ind_stmt =
   3.107 -      Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
   3.108 -      |> Object_Logic.atomize_term thy
   3.109 -    val ind_stmt_xs = external_frees ind_stmt
   3.110 -    val facts =
   3.111 -      (if only then
   3.112 -         maps (map (fn ((name, loc), th) => ((K name, loc), th))
   3.113 -               o fact_from_ref ctxt reserved chained_ths) add
   3.114 -       else
   3.115 -         all_facts ctxt reserved false is_appropriate_prop add_ths chained_ths)
   3.116 -      |> Config.get ctxt instantiate_inducts
   3.117 -         ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
   3.118 -      |> (not (Config.get ctxt ignore_no_atp) andalso not only)
   3.119 -         ? filter_out (No_ATPs.member ctxt o snd)
   3.120 -      |> uniquify
   3.121    in
   3.122      trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
   3.123                               " facts");
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jun 09 23:30:18 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jun 10 12:01:15 2011 +0200
     4.3 @@ -260,6 +260,8 @@
     4.4        val {facts = chained_ths, goal, ...} = Proof.goal state
     4.5        val chained_ths = chained_ths |> normalize_chained_theorems
     4.6        val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
     4.7 +      val facts = nearly_all_facts ctxt relevance_override chained_ths hyp_ts
     4.8 +                                   concl_t
     4.9        val _ = () |> not blocking ? kill_provers
    4.10        val _ = case find_first (not o is_prover_supported ctxt) provers of
    4.11                  SOME name => error ("No such prover: " ^ name ^ ".")
    4.12 @@ -307,9 +309,13 @@
    4.13            val is_built_in_const =
    4.14              is_built_in_const_for_prover ctxt (hd provers)
    4.15          in
    4.16 -          relevant_facts ctxt relevance_thresholds max_max_relevant
    4.17 -                         is_appropriate_prop is_built_in_const relevance_fudge
    4.18 -                         relevance_override chained_ths hyp_ts concl_t
    4.19 +          facts
    4.20 +          |> (case is_appropriate_prop of
    4.21 +                SOME is_app => filter (is_app o prop_of o snd)
    4.22 +              | NONE => I)
    4.23 +          |> relevant_facts ctxt relevance_thresholds max_max_relevant
    4.24 +                            is_built_in_const relevance_fudge relevance_override
    4.25 +                            chained_ths hyp_ts concl_t
    4.26            |> tap (fn facts =>
    4.27                       if debug then
    4.28                         label ^ plural_s (length provers) ^ ": " ^
    4.29 @@ -326,7 +332,8 @@
    4.30        fun launch_atps label is_appropriate_prop atps accum =
    4.31          if null atps then
    4.32            accum
    4.33 -        else if not (is_appropriate_prop concl_t) then
    4.34 +        else if is_some is_appropriate_prop andalso
    4.35 +                not (the is_appropriate_prop concl_t) then
    4.36            (if verbose orelse length atps = length provers then
    4.37               "Goal outside the scope of " ^
    4.38               space_implode " " (serial_commas "and" (map quote atps)) ^ "."
    4.39 @@ -343,7 +350,7 @@
    4.40            accum
    4.41          else
    4.42            let
    4.43 -            val facts = get_facts "SMT solver" (K true) smt_relevance_fudge smts
    4.44 +            val facts = get_facts "SMT solver" NONE smt_relevance_fudge smts
    4.45              val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
    4.46              fun smt_filter facts =
    4.47                (if debug then curry (op o) SOME
    4.48 @@ -356,9 +363,9 @@
    4.49                               #> fst)
    4.50                   |> max_outcome_code |> rpair state
    4.51            end
    4.52 -      val launch_full_atps = launch_atps "ATP" (K true) full_atps
    4.53 +      val launch_full_atps = launch_atps "ATP" NONE full_atps
    4.54        val launch_ueq_atps =
    4.55 -        launch_atps "Unit equational provers" is_unit_equality ueq_atps
    4.56 +        launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps
    4.57        fun launch_atps_and_smt_solvers () =
    4.58          [launch_full_atps, launch_smts, launch_ueq_atps]
    4.59          |> smart_par_list_map (fn f => ignore (f (unknownN, state)))
     5.1 --- a/src/HOL/ex/atp_export.ML	Thu Jun 09 23:30:18 2011 +0200
     5.2 +++ b/src/HOL/ex/atp_export.ML	Fri Jun 10 12:01:15 2011 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4  
     5.5  fun facts_of thy =
     5.6    Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
     5.7 -                                true (K true) [] []
     5.8 +                                true [] []
     5.9  
    5.10  fun fold_body_thms f =
    5.11    let
     6.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Jun 09 23:30:18 2011 +0200
     6.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Fri Jun 10 12:01:15 2011 +0200
     6.3 @@ -34,10 +34,11 @@
     6.4      val relevance_override = {add = [], del = [], only = false}
     6.5      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
     6.6      val facts =
     6.7 -      Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
     6.8 -          (the_default default_max_relevant max_relevant) (K true)
     6.9 -          is_built_in_const relevance_fudge relevance_override chained_ths
    6.10 -          hyp_ts concl_t
    6.11 +      Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
    6.12 +                                           hyp_ts concl_t
    6.13 +      |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    6.14 +             (the_default default_max_relevant max_relevant) is_built_in_const
    6.15 +             relevance_fudge relevance_override chained_ths hyp_ts concl_t
    6.16      val problem =
    6.17        {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    6.18         facts = map Sledgehammer_Provers.Untranslated_Fact facts,