# HG changeset patch # User fleury # Date 1406721792 -7200 # Node ID 0242e9578828d6ee14e1c305004ce8c720469c57 # Parent 94476c92f892a24ee39c9e2739fd9ba4a4c53c05 imported patch satallax_proof_support_Sledgehammer diff -r 94476c92f892 -r 0242e9578828 src/HOL/ATP.thy --- a/src/HOL/ATP.thy Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/ATP.thy Wed Jul 30 14:03:12 2014 +0200 @@ -15,6 +15,8 @@ ML_file "Tools/ATP/atp_problem.ML" ML_file "Tools/ATP/atp_proof.ML" ML_file "Tools/ATP/atp_proof_redirect.ML" +ML_file "Tools/ATP/atp_satallax.ML" + subsection {* Higher-order reasoning helpers *} diff -r 94476c92f892 -r 0242e9578828 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 30 14:03:12 2014 +0200 @@ -68,7 +68,6 @@ val remote_prefix : string val agsyhol_core_rule : string - val satallax_core_rule : string val spass_input_rule : string val spass_pre_skolemize_rule : string val spass_skolemize_rule : string @@ -85,10 +84,26 @@ val scan_general_id : string list -> string * string list val parse_formula : string list -> (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list - val atp_proof_of_tstplike_proof : string -> string atp_problem -> string -> string atp_proof val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof + + val skip_term: string list -> string * string list + val parse_thf0_formula :string list -> + ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, + 'c) ATP_Problem.atp_formula * + string list + val dummy_atype : string ATP_Problem.atp_type + val role_of_tptp_string: string -> ATP_Problem.atp_formula_role + val parse_line: string -> ('a * string ATP_Problem.atp_problem_line list) list -> + string list -> ((string * string list) * ATP_Problem.atp_formula_role * + (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, + 'c) ATP_Problem.atp_formula + * string * (string * 'd list) list) list * string list + val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role * + ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list + val vampire_step_name_ord : (string * 'a) * (string * 'a) -> order + val core_of_agsyhol_proof : string -> string list option end; structure ATP_Proof : ATP_PROOF = @@ -123,7 +138,6 @@ val remote_prefix = "remote_" val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *) -val satallax_core_rule = "__satallax_core" (* arbitrary *) val spass_input_rule = "Inp" val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *) val spass_skolemize_rule = "__Sko" (* arbitrary *) @@ -278,7 +292,7 @@ let fun skip _ accum [] = (accum, []) | skip n accum (ss as s :: ss') = - if s = "," andalso n = 0 then + if (s = "," orelse s = ".") andalso n = 0 then (accum, ss) else if member (op =) [")", "]"] s then if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss' @@ -649,10 +663,6 @@ fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, []) -(* Syntax: *) -fun parse_satallax_core_line x = - (scan_general_id --| Scan.option ($$ " ") >> (single o core_inference satallax_core_rule)) x - (* Syntax: SZS core ... *) fun parse_z3_tptp_core_line x = (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id) @@ -660,35 +670,17 @@ fun parse_line local_name problem = if local_name = leo2N then parse_tstp_thf0_line problem - else if local_name = satallaxN then parse_satallax_core_line else if local_name = spassN then parse_spass_line else if local_name = spass_pirateN then parse_spass_pirate_line else if local_name = z3_tptpN then parse_z3_tptp_core_line else parse_tstp_line problem -fun parse_proof local_name problem = - strip_spaces_except_between_idents - #> raw_explode - #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) - (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat))) - #> fst - fun core_of_agsyhol_proof s = (case split_lines s of "The transformed problem consists of the following conjectures:" :: conj :: _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term) | _ => NONE) -fun atp_proof_of_tstplike_proof _ _ "" = [] - | atp_proof_of_tstplike_proof local_prover problem tstp = - (case core_of_agsyhol_proof tstp of - SOME facts => facts |> map (core_inference agsyhol_core_rule) - | NONE => - tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) - |> parse_proof local_prover problem - |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1))) - |> local_prover = zipperpositionN ? rev) - fun clean_up_dependencies _ [] = [] | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) = (name, role, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: diff -r 94476c92f892 -r 0242e9578828 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jul 30 14:03:12 2014 +0200 @@ -498,7 +498,7 @@ val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" fun add_fact ctxt facts ((_, ss), _, _, rule, deps) = - (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule, satallax_core_rule] rule then + (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule then insert (op =) (short_thm_name ctxt ext, (Global, General)) else I) diff -r 94476c92f892 -r 0242e9578828 src/HOL/Tools/ATP/atp_satallax.ML --- a/src/HOL/Tools/ATP/atp_satallax.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_satallax.ML Wed Jul 30 14:03:12 2014 +0200 @@ -170,7 +170,7 @@ | find_assumptions_to_inline ths [] _ _ = ths fun inline_if_needed_and_simplify th assms to_inline no_inline = - (case find_assumptions_to_inline [] assms to_inline no_inline of + (case find_assumptions_to_inline [th] assms to_inline no_inline of [] => ATerm (("$true", [dummy_atype]), []) | l => foldl1 (fn (a, b) => ATerm ((tptp_or, [dummy_atype]), [a, b])) l) @@ -315,7 +315,7 @@ (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat))) #> fst) else - (Scan.error (!! (fn f => raise UNRECOGNIZED_ATP_PROOF ()) + (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line)))) #> fst #> rev diff -r 94476c92f892 -r 0242e9578828 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 30 14:03:12 2014 +0200 @@ -431,9 +431,9 @@ val satallax_config : atp_config = {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => - "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, + "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = - [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")], + [("% SZS output start Proof", "% SZS output end Proof")], known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = diff -r 94476c92f892 -r 0242e9578828 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Jul 30 14:03:12 2014 +0200 @@ -30,6 +30,7 @@ open ATP_Problem_Generate open ATP_Proof_Reconstruct open ATP_Waldmeister +open ATP_Satallax open ATP_Systems open Sledgehammer_Util open Sledgehammer_Proof_Methods