1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Apr 18 10:53:27 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Apr 18 10:53:28 2012 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4         preplay_timeout = preplay_timeout, expect = ""}
     1.5      val problem =
     1.6        {state = state, goal = goal, subgoal = i, subgoal_count = n,
     1.7 -       facts = facts, smt_filter = NONE}
     1.8 +       facts = facts}
     1.9      val result as {outcome, used_facts, run_time, ...} =
    1.10        prover params (K (K (K ""))) problem
    1.11    in

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Apr 18 10:53:27 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Apr 18 10:53:28 2012 +0200
     2.3 @@ -49,8 +49,7 @@
     2.4       goal: thm,
     2.5       subgoal: int,
     2.6       subgoal_count: int,
     2.7 -     facts: prover_fact list,
     2.8 -     smt_filter: (string * stature) SMT_Solver.smt_filter_data option}
     2.9 +     facts: prover_fact list}
    2.10  
    2.11    type prover_result =
    2.12      {outcome: failure option,
    2.13 @@ -314,8 +313,7 @@
    2.14     goal: thm,
    2.15     subgoal: int,
    2.16     subgoal_count: int,
    2.17 -   facts: prover_fact list,
    2.18 -   smt_filter: (string * stature) SMT_Solver.smt_filter_data option}
    2.19 +   facts: prover_fact list}
    2.20  
    2.21  type prover_result =
    2.22    {outcome: failure option,
    2.23 @@ -900,7 +898,7 @@
    2.24  fun smt_filter_loop ctxt name
    2.25                      ({debug, verbose, overlord, max_mono_iters,
    2.26                        max_new_mono_instances, timeout, slice, ...} : params)
    2.27 -                    state i smt_filter =
    2.28 +                    state i =
    2.29    let
    2.30      val max_slices = if slice then Config.get ctxt smt_max_slices else 1
    2.31      val repair_context =
    2.32 @@ -944,9 +942,7 @@
    2.33          val _ =
    2.34            if debug then Output.urgent_message "Invoking SMT solver..." else ()
    2.35          val (outcome, used_facts) =
    2.36 -          (case (slice, smt_filter) of
    2.37 -             (1, SOME head) => head |> apsnd (apsnd repair_context)
    2.38 -           | _ => SMT_Solver.smt_filter_preprocess state facts i)
    2.39 +          SMT_Solver.smt_filter_preprocess state facts i
    2.40            |> SMT_Solver.smt_filter_apply slice_timeout
    2.41            |> (fn {outcome, used_facts} => (outcome, used_facts))
    2.42            handle exn => if Exn.is_interrupt exn then
    2.43 @@ -995,15 +991,14 @@
    2.44  
    2.45  fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
    2.46          minimize_command
    2.47 -        ({state, subgoal, subgoal_count, facts, smt_filter, ...}
    2.48 -         : prover_problem) =
    2.49 +        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
    2.50    let
    2.51      val ctxt = Proof.context_of state
    2.52      val num_facts = length facts
    2.53      val facts = facts ~~ (0 upto num_facts - 1)
    2.54                  |> map (smt_weighted_fact ctxt num_facts)
    2.55      val {outcome, used_facts = used_pairs, run_time} =
    2.56 -      smt_filter_loop ctxt name params state subgoal smt_filter facts
    2.57 +      smt_filter_loop ctxt name params state subgoal facts
    2.58      val used_facts = used_pairs |> map fst
    2.59      val outcome = outcome |> Option.map failure_from_smt_failure
    2.60      val (preplay, message, message_tail) =

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Apr 18 10:53:27 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Apr 18 10:53:28 2012 +0200
     3.3 @@ -177,8 +177,8 @@
     3.4  
     3.5  fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
     3.6                                timeout, expect, ...})
     3.7 -        mode minimize_command only
     3.8 -        {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
     3.9 +        mode minimize_command only {state, goal, subgoal, subgoal_count, facts}
    3.10 +        name =
    3.11    let
    3.12      val ctxt = Proof.context_of state
    3.13      val hard_timeout = Time.+ (timeout, timeout)
    3.14 @@ -197,8 +197,7 @@
    3.15           subgoal_count = subgoal_count, facts =
    3.16            ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction)
    3.17              facts
    3.18 -          |> take num_facts,
    3.19 -         smt_filter = smt_filter}
    3.20 +          |> take num_facts}
    3.21        end
    3.22      fun really_go () =
    3.23        problem
    3.24 @@ -268,14 +267,11 @@
    3.25    ctxt |> select_smt_solver name
    3.26         |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
    3.27  
    3.28 -fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
    3.29 -  | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
    3.30 -
    3.31  val auto_try_max_relevant_divisor = 2 (* FUDGE *)
    3.32  
    3.33  fun run_sledgehammer (params as {debug, verbose, blocking, provers,
    3.34                                   relevance_thresholds, max_relevant, slice,
    3.35 -                                 timeout, ...})
    3.36 +                                 ...})
    3.37          mode i (relevance_override as {only, ...}) minimize_command state =
    3.38    if null provers then
    3.39      error "No prover is set."
    3.40 @@ -303,7 +299,7 @@
    3.41        val (smts, (ueq_atps, full_atps)) =
    3.42          provers |> List.partition (is_smt_prover ctxt)
    3.43                  ||> List.partition (is_unit_equational_atp ctxt)
    3.44 -      fun launch_provers state get_facts translate maybe_smt_filter provers =
    3.45 +      fun launch_provers state get_facts translate provers =
    3.46          let
    3.47            val facts = get_facts ()
    3.48            val num_facts = length facts
    3.49 @@ -311,9 +307,7 @@
    3.50                        |> map (translate num_facts)
    3.51            val problem =
    3.52              {state = state, goal = goal, subgoal = i, subgoal_count = n,
    3.53 -             facts = facts,
    3.54 -             smt_filter = maybe_smt_filter
    3.55 -                  (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
    3.56 +             facts = facts}
    3.57            val launch = launch_prover params mode minimize_command only
    3.58          in
    3.59            if mode = Auto_Try orelse mode = Try then
    3.60 @@ -377,7 +371,7 @@
    3.61          else
    3.62            launch_provers state
    3.63                (get_facts label is_appropriate_prop atp_relevance_fudge o K atps)
    3.64 -              (K (Untranslated_Fact o fst)) (K (K NONE)) atps
    3.65 +              (K (Untranslated_Fact o fst)) atps
    3.66        fun launch_smts accum =
    3.67          if null smts then
    3.68            accum
    3.69 @@ -385,15 +379,10 @@
    3.70            let
    3.71              val facts = get_facts "SMT solver" NONE smt_relevance_fudge smts
    3.72              val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
    3.73 -            fun smt_filter facts =
    3.74 -              (if debug then curry (op o) SOME
    3.75 -               else TimeLimit.timeLimit timeout o try)
    3.76 -                  (SMT_Solver.smt_filter_preprocess state (facts ()))
    3.77            in
    3.78              smts |> map (`(class_of_smt_solver ctxt))
    3.79                   |> AList.group (op =)
    3.80 -                 |> map (snd #> launch_provers state (K facts) weight smt_filter
    3.81 -                             #> fst)
    3.82 +                 |> map (snd #> launch_provers state (K facts) weight #> fst)
    3.83                   |> max_outcome_code |> rpair state
    3.84            end
    3.85        val launch_full_atps = launch_atps "ATP" NONE full_atps