# HG changeset patch
# User blanchet
# Date 1361376324 -3600
# Node ID 44f0bfe67b0122f9642b42d3b966693ea0041db4
# Parent  914436eb988bd4d06b9b568b8f0efd800a9e5463
remove needless steps from refutation graph -- these confuse the proof redirection algorithm (and are needless)

diff -r 914436eb988b -r 44f0bfe67b01 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Feb 20 16:21:04 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Feb 20 17:05:24 2013 +0100
@@ -32,7 +32,7 @@
 
   type direct_proof = direct_inference list
 
-  val make_refute_graph : (atom list * atom) list -> refute_graph
+  val make_refute_graph : atom -> (atom list * atom) list -> refute_graph
   val axioms_of_refute_graph : refute_graph -> atom list -> atom list
   val tainted_atoms_of_refute_graph : refute_graph -> atom list -> atom list
   val sequents_of_refute_graph : refute_graph -> ref_sequent list
@@ -72,14 +72,16 @@
 fun direct_sequent_eq ((gamma, c), (delta, d)) =
   clause_eq (gamma, delta) andalso clause_eq (c, d)
 
-fun make_refute_graph infers =
+fun make_refute_graph bot infers =
   let
     fun add_edge to from =
       Atom_Graph.default_node (from, ())
       #> Atom_Graph.default_node (to, ())
       #> Atom_Graph.add_edge_acyclic (from, to)
     fun add_infer (froms, to) = fold (add_edge to) froms
-  in Atom_Graph.empty |> fold add_infer infers end
+    val graph = fold add_infer infers Atom_Graph.empty
+    val reachable = Atom_Graph.all_preds graph [bot]
+  in graph |> Atom_Graph.restrict (member (is_equal o Atom.ord) reachable) end
 
 fun axioms_of_refute_graph refute_graph conjs =
   subtract atom_eq conjs (Atom_Graph.minimals refute_graph)
diff -r 914436eb988b -r 44f0bfe67b01 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 16:21:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 17:05:24 2013 +0100
@@ -678,12 +678,12 @@
                  | _ => NONE)
               | _ => NONE)
         fun dep_of_step (name, _, _, _, from) = SOME (from, name)
+        val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
         val refute_graph =
-          atp_proof |> map_filter dep_of_step |> make_refute_graph
+          atp_proof |> map_filter dep_of_step |> make_refute_graph bot
         val axioms = axioms_of_refute_graph refute_graph conjs
         val tainted = tainted_atoms_of_refute_graph refute_graph conjs
         val is_clause_tainted = exists (member (op =) tainted)
-        val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
         val steps =
           Symtab.empty
           |> fold (fn (name as (s, _), role, t, rule, _) =>