include "ext" in all Satallax proofs
authorblanchet
Mon May 21 11:31:52 2012 +0200 (2012-05-21)
changeset 479477b482cc7473e
parent 47946 33afcfad3f8d
child 47948 0524790d2112
include "ext" in all Satallax proofs
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 21 10:39:32 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 21 11:31:52 2012 +0200
     1.3 @@ -51,6 +51,7 @@
     1.4      -> string * failure option
     1.5    val is_same_atp_step : step_name -> step_name -> bool
     1.6    val scan_general_id : string list -> string * string list
     1.7 +  val satallax_unsat_coreN : string
     1.8    val parse_formula :
     1.9      string list -> (string, 'a, (string, 'a) ho_term) formula * string list
    1.10    val atp_proof_from_tstplike_proof :
    1.11 @@ -465,10 +466,13 @@
    1.12           Inference_Step ((num, resolve_spass_num names spass_names num), u,
    1.13               rule, map (swap o `(resolve_spass_num NONE spass_names)) deps))
    1.14  
    1.15 +val satallax_unsat_coreN = "__satallax_unsat_core" (* arbitrary *)
    1.16 +
    1.17  (* Syntax: <name> *)
    1.18  fun parse_satallax_line x =
    1.19    (scan_general_id --| Scan.option ($$ " ")
    1.20 -   >> (fn s => Inference_Step ((s, [s]), dummy_phi, "", []))) x
    1.21 +   >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_unsat_coreN, [])))
    1.22 +      x
    1.23  
    1.24  fun parse_line problem spass_names =
    1.25    parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line
     2.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 21 10:39:32 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 21 11:31:52 2012 +0200
     2.3 @@ -198,11 +198,13 @@
     2.4    else
     2.5      isa_ext
     2.6  
     2.7 -fun add_fact _ fact_names (Inference_Step ((_, ss), _, _, [])) =
     2.8 -    union (op =) (resolve_fact fact_names ss)
     2.9 -  | add_fact ctxt _ (Inference_Step (_, _, rule, _)) =
    2.10 -    if rule = leo2_ext then insert (op =) (ext_name ctxt, (Global, General))
    2.11 -    else I
    2.12 +fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) =
    2.13 +    (if rule = leo2_ext orelse rule = satallax_unsat_coreN then
    2.14 +       insert (op =) (ext_name ctxt, (Global, General))
    2.15 +     else
    2.16 +       I)
    2.17 +    #> (if null deps then union (op =) (resolve_fact fact_names ss)
    2.18 +        else I)
    2.19    | add_fact _ _ _ = I
    2.20  
    2.21  fun used_facts_in_atp_proof ctxt fact_names atp_proof =