src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 43351 b19d95b4d736
parent 43306 03e6da81aee6
child 43590 0940a64beca2
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jun 09 23:30:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jun 10 12:01:15 2011 +0200
     1.3 @@ -260,6 +260,8 @@
     1.4        val {facts = chained_ths, goal, ...} = Proof.goal state
     1.5        val chained_ths = chained_ths |> normalize_chained_theorems
     1.6        val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
     1.7 +      val facts = nearly_all_facts ctxt relevance_override chained_ths hyp_ts
     1.8 +                                   concl_t
     1.9        val _ = () |> not blocking ? kill_provers
    1.10        val _ = case find_first (not o is_prover_supported ctxt) provers of
    1.11                  SOME name => error ("No such prover: " ^ name ^ ".")
    1.12 @@ -307,9 +309,13 @@
    1.13            val is_built_in_const =
    1.14              is_built_in_const_for_prover ctxt (hd provers)
    1.15          in
    1.16 -          relevant_facts ctxt relevance_thresholds max_max_relevant
    1.17 -                         is_appropriate_prop is_built_in_const relevance_fudge
    1.18 -                         relevance_override chained_ths hyp_ts concl_t
    1.19 +          facts
    1.20 +          |> (case is_appropriate_prop of
    1.21 +                SOME is_app => filter (is_app o prop_of o snd)
    1.22 +              | NONE => I)
    1.23 +          |> relevant_facts ctxt relevance_thresholds max_max_relevant
    1.24 +                            is_built_in_const relevance_fudge relevance_override
    1.25 +                            chained_ths hyp_ts concl_t
    1.26            |> tap (fn facts =>
    1.27                       if debug then
    1.28                         label ^ plural_s (length provers) ^ ": " ^
    1.29 @@ -326,7 +332,8 @@
    1.30        fun launch_atps label is_appropriate_prop atps accum =
    1.31          if null atps then
    1.32            accum
    1.33 -        else if not (is_appropriate_prop concl_t) then
    1.34 +        else if is_some is_appropriate_prop andalso
    1.35 +                not (the is_appropriate_prop concl_t) then
    1.36            (if verbose orelse length atps = length provers then
    1.37               "Goal outside the scope of " ^
    1.38               space_implode " " (serial_commas "and" (map quote atps)) ^ "."
    1.39 @@ -343,7 +350,7 @@
    1.40            accum
    1.41          else
    1.42            let
    1.43 -            val facts = get_facts "SMT solver" (K true) smt_relevance_fudge smts
    1.44 +            val facts = get_facts "SMT solver" NONE smt_relevance_fudge smts
    1.45              val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
    1.46              fun smt_filter facts =
    1.47                (if debug then curry (op o) SOME
    1.48 @@ -356,9 +363,9 @@
    1.49                               #> fst)
    1.50                   |> max_outcome_code |> rpair state
    1.51            end
    1.52 -      val launch_full_atps = launch_atps "ATP" (K true) full_atps
    1.53 +      val launch_full_atps = launch_atps "ATP" NONE full_atps
    1.54        val launch_ueq_atps =
    1.55 -        launch_atps "Unit equational provers" is_unit_equality ueq_atps
    1.56 +        launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps
    1.57        fun launch_atps_and_smt_solvers () =
    1.58          [launch_full_atps, launch_smts, launch_ueq_atps]
    1.59          |> smart_par_list_map (fn f => ignore (f (unknownN, state)))