imported patch satallax_proof_support_Sledgehammer
authorfleury
Wed Jul 30 14:03:12 2014 +0200 (2014-07-30)
changeset 577070242e9578828
parent 57706 94476c92f892
child 57708 4b52c1b319ce
imported patch satallax_proof_support_Sledgehammer
src/HOL/ATP.thy
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/ATP/atp_satallax.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
     1.1 --- a/src/HOL/ATP.thy	Wed Jul 30 14:03:12 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Wed Jul 30 14:03:12 2014 +0200
     1.3 @@ -15,6 +15,8 @@
     1.4  ML_file "Tools/ATP/atp_problem.ML"
     1.5  ML_file "Tools/ATP/atp_proof.ML"
     1.6  ML_file "Tools/ATP/atp_proof_redirect.ML"
     1.7 +ML_file "Tools/ATP/atp_satallax.ML"
     1.8 +
     1.9  
    1.10  subsection {* Higher-order reasoning helpers *}
    1.11  
     2.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:12 2014 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:12 2014 +0200
     2.3 @@ -68,7 +68,6 @@
     2.4    val remote_prefix : string
     2.5  
     2.6    val agsyhol_core_rule : string
     2.7 -  val satallax_core_rule : string
     2.8    val spass_input_rule : string
     2.9    val spass_pre_skolemize_rule : string
    2.10    val spass_skolemize_rule : string
    2.11 @@ -85,10 +84,26 @@
    2.12    val scan_general_id : string list -> string * string list
    2.13    val parse_formula : string list ->
    2.14      (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list
    2.15 -  val atp_proof_of_tstplike_proof : string -> string atp_problem -> string -> string atp_proof
    2.16    val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof
    2.17    val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof
    2.18    val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof
    2.19 +
    2.20 +  val skip_term: string list -> string * string list
    2.21 +  val parse_thf0_formula :string list ->
    2.22 +      ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
    2.23 +       'c) ATP_Problem.atp_formula *
    2.24 +      string list
    2.25 +  val dummy_atype :  string ATP_Problem.atp_type
    2.26 +  val role_of_tptp_string:  string -> ATP_Problem.atp_formula_role
    2.27 +  val parse_line: string -> ('a * string ATP_Problem.atp_problem_line list) list ->
    2.28 +              string list -> ((string * string list) * ATP_Problem.atp_formula_role *
    2.29 +               (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
    2.30 +                'c) ATP_Problem.atp_formula
    2.31 +               * string * (string * 'd list) list) list * string list
    2.32 +  val core_inference :   'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
    2.33 +              ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
    2.34 +  val vampire_step_name_ord : (string * 'a) * (string * 'a) -> order
    2.35 +  val core_of_agsyhol_proof :  string -> string list option
    2.36  end;
    2.37  
    2.38  structure ATP_Proof : ATP_PROOF =
    2.39 @@ -123,7 +138,6 @@
    2.40  val remote_prefix = "remote_"
    2.41  
    2.42  val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
    2.43 -val satallax_core_rule = "__satallax_core" (* arbitrary *)
    2.44  val spass_input_rule = "Inp"
    2.45  val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *)
    2.46  val spass_skolemize_rule = "__Sko" (* arbitrary *)
    2.47 @@ -278,7 +292,7 @@
    2.48    let
    2.49      fun skip _ accum [] = (accum, [])
    2.50        | skip n accum (ss as s :: ss') =
    2.51 -        if s = "," andalso n = 0 then
    2.52 +        if (s = "," orelse s = ".") andalso n = 0 then
    2.53            (accum, ss)
    2.54          else if member (op =) [")", "]"] s then
    2.55            if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss'
    2.56 @@ -649,10 +663,6 @@
    2.57  
    2.58  fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
    2.59  
    2.60 -(* Syntax: <name> *)
    2.61 -fun parse_satallax_core_line x =
    2.62 -  (scan_general_id --| Scan.option ($$ " ") >> (single o core_inference satallax_core_rule)) x
    2.63 -
    2.64  (* Syntax: SZS core <name> ... <name> *)
    2.65  fun parse_z3_tptp_core_line x =
    2.66    (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id)
    2.67 @@ -660,35 +670,17 @@
    2.68  
    2.69  fun parse_line local_name problem =
    2.70    if local_name = leo2N then parse_tstp_thf0_line problem
    2.71 -  else if local_name = satallaxN then parse_satallax_core_line
    2.72    else if local_name = spassN then parse_spass_line
    2.73    else if local_name = spass_pirateN then parse_spass_pirate_line
    2.74    else if local_name = z3_tptpN then parse_z3_tptp_core_line
    2.75    else parse_tstp_line problem
    2.76  
    2.77 -fun parse_proof local_name problem =
    2.78 -  strip_spaces_except_between_idents
    2.79 -  #> raw_explode
    2.80 -  #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
    2.81 -       (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
    2.82 -  #> fst
    2.83 -
    2.84  fun core_of_agsyhol_proof s =
    2.85    (case split_lines s of
    2.86      "The transformed problem consists of the following conjectures:" :: conj ::
    2.87      _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
    2.88    | _ => NONE)
    2.89  
    2.90 -fun atp_proof_of_tstplike_proof _ _ "" = []
    2.91 -  | atp_proof_of_tstplike_proof local_prover problem tstp =
    2.92 -    (case core_of_agsyhol_proof tstp of
    2.93 -      SOME facts => facts |> map (core_inference agsyhol_core_rule)
    2.94 -    | NONE =>
    2.95 -      tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
    2.96 -      |> parse_proof local_prover problem
    2.97 -      |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1)))
    2.98 -      |> local_prover = zipperpositionN ? rev)
    2.99 -
   2.100  fun clean_up_dependencies _ [] = []
   2.101    | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
   2.102      (name, role, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
     3.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:12 2014 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:12 2014 +0200
     3.3 @@ -498,7 +498,7 @@
     3.4  val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
     3.5  
     3.6  fun add_fact ctxt facts ((_, ss), _, _, rule, deps) =
     3.7 -  (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule, satallax_core_rule] rule then
     3.8 +  (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule then
     3.9       insert (op =) (short_thm_name ctxt ext, (Global, General))
    3.10     else
    3.11       I)
     4.1 --- a/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:12 2014 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:12 2014 +0200
     4.3 @@ -170,7 +170,7 @@
     4.4    | find_assumptions_to_inline ths [] _ _ = ths
     4.5  
     4.6  fun inline_if_needed_and_simplify th assms to_inline no_inline =
     4.7 -    (case find_assumptions_to_inline [] assms to_inline no_inline of
     4.8 +    (case find_assumptions_to_inline [th] assms to_inline no_inline of
     4.9        [] => ATerm (("$true", [dummy_atype]), [])
    4.10    | l => foldl1 (fn (a, b) => ATerm ((tptp_or, [dummy_atype]), [a, b])) l)
    4.11  
    4.12 @@ -315,7 +315,7 @@
    4.13            (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
    4.14             #> fst)
    4.15        else
    4.16 -        (Scan.error (!! (fn f => raise UNRECOGNIZED_ATP_PROOF ())
    4.17 +        (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
    4.18            (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line))))
    4.19            #> fst
    4.20            #> rev
     5.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 30 14:03:12 2014 +0200
     5.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 30 14:03:12 2014 +0200
     5.3 @@ -431,9 +431,9 @@
     5.4  val satallax_config : atp_config =
     5.5    {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
     5.6     arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
     5.7 -       "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
     5.8 +       "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
     5.9     proof_delims =
    5.10 -     [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
    5.11 +     [("% SZS output start Proof", "% SZS output end Proof")],
    5.12     known_failures = known_szs_status_failures,
    5.13     prem_role = Hypothesis,
    5.14     best_slices =
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Jul 30 14:03:12 2014 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Jul 30 14:03:12 2014 +0200
     6.3 @@ -30,6 +30,7 @@
     6.4  open ATP_Problem_Generate
     6.5  open ATP_Proof_Reconstruct
     6.6  open ATP_Waldmeister
     6.7 +open ATP_Satallax
     6.8  open ATP_Systems
     6.9  open Sledgehammer_Util
    6.10  open Sledgehammer_Proof_Methods