# HG changeset patch
# User blanchet
# Date 1284474866 -7200
# Node ID f58fbb959826cefe9dcad212b231d7c2d6bcaf7f
# Parent  9cab71c20613c6725e70a1e0ee17f073afb44d65
handle relevance filter corner cases more gracefully;
e.g. the minimizer selects 15 facts but "max_relevant = 14"

diff -r 9cab71c20613 -r f58fbb959826 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 14 16:33:38 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 14 16:34:26 2010 +0200
@@ -357,7 +357,8 @@
           relevance_override chained_ths hyp_ts concl_t
     val problem =
       {state = st', goal = goal, subgoal = i,
-       axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms}
+       axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms,
+       only = true}
     val time_limit =
       (case hard_timeout of
         NONE => I
diff -r 9cab71c20613 -r f58fbb959826 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Sep 14 16:33:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Sep 14 16:34:26 2010 +0200
@@ -31,7 +31,8 @@
     {state: Proof.state,
      goal: thm,
      subgoal: int,
-     axioms: (term * ((string * locality) * fol_formula) option) list}
+     axioms: (term * ((string * locality) * fol_formula) option) list,
+     only: bool}
   type prover_result =
     {outcome: failure option,
      message: string,
@@ -100,7 +101,8 @@
   {state: Proof.state,
    goal: thm,
    subgoal: int,
-   axioms: (term * ((string * locality) * fol_formula) option) list}
+   axioms: (term * ((string * locality) * fol_formula) option) list,
+   only: bool}
 
 type prover_result =
   {outcome: failure option,
@@ -236,12 +238,12 @@
          use_conjecture_for_hypotheses}
         ({debug, verbose, overlord, full_types, explicit_apply,
           max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
-        minimize_command ({state, goal, subgoal, axioms} : problem) =
+        minimize_command ({state, goal, subgoal, axioms, only} : problem) =
   let
     val ctxt = Proof.context_of state
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
-    val max_relevant = the_default default_max_relevant max_relevant
-    val axioms = take max_relevant axioms
+    val axioms = axioms |> not only
+                          ? take (the_default default_max_relevant max_relevant)
     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
                        else Config.get ctxt dest_dir
     val the_problem_prefix = Config.get ctxt problem_prefix
@@ -431,7 +433,8 @@
 
 fun run_sledgehammer (params as {blocking, verbose, atps, full_types,
                                  relevance_thresholds, max_relevant, ...})
-                     auto i relevance_override minimize_command state =
+                     auto i (relevance_override as {only, ...}) minimize_command
+                     state =
   if null atps then
     error "No ATP is set."
   else case subgoal_count state of
@@ -460,7 +463,7 @@
                            hyp_ts concl_t
           val problem =
             {state = state, goal = goal, subgoal = i,
-             axioms = map (prepare_axiom ctxt) axioms}
+             axioms = map (prepare_axiom ctxt) axioms, only = only}
           val run_prover = run_prover params auto i n minimize_command problem
         in
           if auto then
diff -r 9cab71c20613 -r f58fbb959826 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Sep 14 16:33:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Sep 14 16:34:26 2010 +0200
@@ -817,10 +817,11 @@
   in
     trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
                         " theorems");
-    (if threshold0 > 1.0 orelse threshold0 > threshold1 then
+    (if only orelse threshold1 < 0.0 then
+       axioms
+     else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
+             max_relevant = 0 then
        []
-     else if threshold0 < 0.0 then
-       axioms
      else
        relevance_filter ctxt threshold0 decay max_relevant relevance_override
                         axioms (concl_t :: hyp_ts))
diff -r 9cab71c20613 -r f58fbb959826 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Sep 14 16:33:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Sep 14 16:34:26 2010 +0200
@@ -61,7 +61,7 @@
     val {context = ctxt, goal, ...} = Proof.goal state
     val problem =
       {state = state, goal = goal, subgoal = subgoal,
-       axioms = map (prepare_axiom ctxt) axioms}
+       axioms = map (prepare_axiom ctxt) axioms, only = true}
     val result as {outcome, used_thm_names, ...} = prover params (K "") problem
   in
     priority (case outcome of