# HG changeset patch # User blanchet # Date 1406280377 -7200 # Node ID dc5e1b1db9ba84db31b21858297e3277a06d81ce # Parent d7b15b99f93cdac606bb376e2d1472a2e1e20b3c avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction) diff -r d7b15b99f93c -r dc5e1b1db9ba src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 25 11:26:11 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 25 11:26:17 2014 +0200 @@ -14,11 +14,9 @@ type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = - {exec : unit -> string list * string list, - arguments : - Proof.context -> bool -> string -> Time.time -> string - -> term_order * (unit -> (string * int) list) - * (unit -> (string * real) list) -> string, + {exec : bool -> string list * string list, + arguments : Proof.context -> bool -> string -> Time.time -> string -> + term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, @@ -48,10 +46,9 @@ val spass_H2NuVS0Red2 : string val spass_H2SOS : string val spass_extra_options : string Config.T - val remote_atp : - string -> string -> string list -> (string * string) list - -> (atp_failure * string) list -> atp_formula_role - -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config) + val remote_atp : string -> string -> string list -> (string * string) list -> + (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) -> + string * (unit -> atp_config) val add_atp : string * (unit -> atp_config) -> theory -> theory val get_atp : theory -> string -> (unit -> atp_config) val supported_atps : theory -> string list @@ -76,11 +73,9 @@ type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = - {exec : unit -> string list * string list, - arguments : - Proof.context -> bool -> string -> Time.time -> string - -> term_order * (unit -> (string * int) list) - * (unit -> (string * real) list) -> string, + {exec : bool -> string list * string list, + arguments : Proof.context -> bool -> string -> Time.time -> string -> + term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, @@ -213,7 +208,6 @@ (* E *) fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS -fun is_e_at_least_1_9 () = string_ord (getenv "E_VERSION", "1.9") <> LESS val e_smartN = "smart" val e_autoN = "auto" @@ -286,9 +280,10 @@ end val e_config : atp_config = - {exec = (fn () => (["E_HOME"], - if is_e_at_least_1_9 () then ["eprover"] else ["eproof_ram", "eproof"])), - arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => fn file_name => + {exec = fn full_proofs => (["E_HOME"], + if full_proofs orelse not (is_e_at_least_1_8 ()) then ["eproof_ram", "eproof"] + else ["eprover"]), + arguments = fn ctxt => fn full_proofs => fn heuristic => fn timeout => fn file_name => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^ "--tstp-in --tstp-out --silent " ^ @@ -296,8 +291,10 @@ e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^ "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ - (if is_e_at_least_1_9 () then " --proof-object=3" - else " --output-level=5 --pcl-shell-level=" ^ (if full_proof then "0" else "2")) ^ + (if full_proofs orelse not (is_e_at_least_1_8 ()) then + " --output-level=5 --pcl-shell-level=" ^ (if full_proofs then "0" else "2") + else + " --proof-object=1") ^ " " ^ file_name, proof_delims = [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ @@ -511,20 +508,20 @@ val vampire_config : atp_config = {exec = K (["VAMPIRE_HOME"], ["vampire"]), - arguments = fn _ => fn full_proof => fn sos => fn timeout => fn file_name => + arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ => "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^ " --proof tptp --output_axiom_names on" ^ (if is_vampire_at_least_1_8 () then (* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *) - (if full_proof then + (if full_proofs then " --forced_options splitting=off:equality_proxy=off:general_splitting=off\ \:inequality_splitting=0:naming=0" else "") else "") ^ - " --thanks \"Andrei and Krystof\" --input_file " ^ file_name + " --thanks \"Andrei et al.\" --input_file " ^ file_name |> sos = sosN ? prefix "--sos on ", proof_delims = [("=========== Refutation ==========", @@ -766,7 +763,7 @@ fun is_atp_installed thy name = let val {exec, ...} = get_atp thy name () in - exists (fn var => getenv var <> "") (fst (exec ())) + exists (fn var => getenv var <> "") (fst (exec false)) end fun refresh_systems_on_tptp () = diff -r d7b15b99f93c -r dc5e1b1db9ba src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Jul 25 11:26:11 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Jul 25 11:26:17 2014 +0200 @@ -143,6 +143,7 @@ val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, best_max_new_mono_instances, ...} = get_atp thy name () + val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name val waldmeister_new = (local_name = waldmeister_newN) val spass = (local_name = spassN orelse local_name = spass_pirateN) @@ -162,7 +163,7 @@ Path.append (Path.explode dest_dir) problem_file_name else error ("No such directory: " ^ quote dest_dir ^ ".") - val exec = exec () + val exec = exec full_proofs val command0 = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => @@ -276,9 +277,8 @@ fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name - val full_proof = isar_proofs |> the_default (mode = Minimize) val args = - arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path) + arguments ctxt full_proofs extra slice_timeout (File.shell_path prob_path) (ord, ord_info, sel_weights) val command = "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"