augment Satallax unsat cores with all definitions
authorblanchet
Wed May 23 21:19:48 2012 +0200 (2012-05-23)
changeset 479739af7e5caf16f
parent 47972 96c9b8381909
child 47974 08d2dcc2dab9
augment Satallax unsat cores with all definitions
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed May 23 21:19:48 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed May 23 21:19:48 2012 +0200
     1.3 @@ -199,8 +199,17 @@
     1.4      isa_ext
     1.5  
     1.6  fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) =
     1.7 -    (if rule = leo2_ext orelse rule = satallax_unsat_coreN then
     1.8 +    (if rule = leo2_ext then
     1.9         insert (op =) (ext_name ctxt, (Global, General))
    1.10 +     else if rule = satallax_unsat_coreN then
    1.11 +       (fn [] =>
    1.12 +           (* Satallax doesn't include definitions in its unsatisfiable cores,
    1.13 +              so we assume the worst and include them all here. *)
    1.14 +           Vector.foldl (fn (facts, factss) =>
    1.15 +                            filter (fn (_, (_, status)) => status = Def) facts
    1.16 +                            @ factss)
    1.17 +                        [(ext_name ctxt, (Global, General))] fact_names
    1.18 +         | facts => facts)
    1.19       else
    1.20         I)
    1.21      #> (if null deps then union (op =) (resolve_fact fact_names ss)