# HG changeset patch # User blanchet # Date 1358427705 -3600 # Node ID 31d864d5057acf3ebef9809afc497f0ce6dec722 # Parent c7f910a596add4a3f0fcfb930c0fcea39f5faf85 added E-Par support diff -r c7f910a596ad -r 31d864d5057a src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Thu Jan 17 13:11:44 2013 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Thu Jan 17 14:01:45 2013 +0100 @@ -68,9 +68,9 @@ |> File.write_list prob_file val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = - File.shell_path (Path.explode path) ^ - " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^ - File.shell_path prob_file + File.shell_path (Path.explode path) ^ " " ^ + arguments ctxt false "" (seconds 1.0) (File.shell_path prob_file) + (ord, K [], K []) in TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command |> fst diff -r c7f910a596ad -r 31d864d5057a src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Jan 17 13:11:44 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Jan 17 14:01:45 2013 +0100 @@ -16,7 +16,7 @@ type atp_config = {exec : string list * string list, arguments : - Proof.context -> bool -> string -> Time.time + Proof.context -> bool -> string -> Time.time -> string -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, @@ -45,6 +45,7 @@ val dummy_thfN : string val eN : string val e_malesN : string + val e_parN : string val e_sineN : string val e_tofofN : string val iproverN : string @@ -88,7 +89,7 @@ type atp_config = {exec : string list * string list, arguments : - Proof.context -> bool -> string -> Time.time + Proof.context -> bool -> string -> Time.time -> string -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, @@ -140,6 +141,7 @@ val dummy_thfN = "dummy_thf" (* for experiments *) val eN = "e" val e_malesN = "e_males" +val e_parN = "e_par" val e_sineN = "e_sine" val e_tofofN = "e_tofof" val iproverN = "iprover" @@ -189,9 +191,9 @@ val alt_ergo_config : atp_config = {exec = (["WHY3_HOME"], ["why3"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--format tff1 --prover alt-ergo --timelimit " ^ - string_of_int (to_secs 1 timeout), + string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [], known_failures = [(ProofMissing, ": Valid"), @@ -301,13 +303,14 @@ val e_config : atp_config = {exec = (["E_HOME"], ["eproof_ram", "eproof"]), arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => + fn file_name => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => "--tstp-in --tstp-out --output-level=5 --silent " ^ e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^ e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^ "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ - e_shell_level_argument full_proof, + e_shell_level_argument full_proof ^ " " ^ file_name, proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "Failure: Resource limit exceeded (time)"), @@ -334,27 +337,45 @@ val e_males_config : atp_config = {exec = (["E_MALES_HOME"], ["emales.py"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => - "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p", + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => + "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name, proof_delims = tstp_proof_delims, known_failures = #known_failures e_config, prem_role = Conjecture, best_slices = (* FUDGE *) - K [(1.0, ((1000, FOF, "mono_tags??", combsN, false), ""))], + K [(0.5, ((1000, FOF, "mono_tags??", combsN, false), "")), + (0.5, ((1000, FOF, "mono_guards??", combsN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val e_males = (e_malesN, fn () => e_males_config) +(* E-Par *) + +val e_par_config : atp_config = + {exec = (["E_HOME"], ["runepar.pl"]), + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => + string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^ + " 2" (* proofs *), + proof_delims = tstp_proof_delims, + known_failures = #known_failures e_config, + prem_role = Conjecture, + best_slices = #best_slices e_males_config, + best_max_mono_iters = default_max_mono_iters, + best_max_new_mono_instances = default_max_new_mono_instances} + +val e_par = (e_parN, fn () => e_par_config) + + (* iProver *) val iprover_config : atp_config = {exec = (["IPROVER_HOME"], ["iprover"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^ - string_of_real (Time.toReal timeout), + string_of_real (Time.toReal timeout) ^ " " ^ file_name, proof_delims = tstp_proof_delims, known_failures = [(ProofIncomplete, "% SZS output start CNFRefutation")] @ @@ -393,10 +414,11 @@ val leo2_config : atp_config = {exec = (["LEO2_HOME"], ["leo"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--foatp e --atp e=\"$E_HOME\"/eprover \ \--atp epclextract=\"$E_HOME\"/epclextract \ - \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout), + \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ + file_name, proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "CPU time limit exceeded, terminating"), @@ -419,8 +441,8 @@ val satallax_config : atp_config = {exec = (["SATALLAX_HOME"], ["satallax"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => - "-p hocore -t " ^ string_of_int (to_secs 1 timeout), + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => + "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")], known_failures = known_szs_status_failures, @@ -446,9 +468,11 @@ (* FIXME: Make "SPASS_NEW_HOME" legacy. *) val spass_config : atp_config = {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]), - arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ => - ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) - |> extra_options <> "" ? prefix (extra_options ^ " "), + arguments = + fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ => + "-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ + file_name + |> extra_options <> "" ? prefix (extra_options ^ " "), proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = [(OldSPASS, "Unrecognized option Isabelle"), @@ -489,14 +513,14 @@ val vampire_config : atp_config = {exec = (["VAMPIRE_HOME"], ["vampire"]), - arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => + arguments = fn _ => fn _ => 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 " --forced_options propositional_to_bdd=off" else "") ^ - " --thanks \"Andrei and Krystof\" --input_file" + " --thanks \"Andrei and Krystof\" --input_file " ^ file_name |> sos = sosN ? prefix "--sos on ", proof_delims = [("=========== Refutation ==========", @@ -535,9 +559,9 @@ val z3_tptp_config : atp_config = {exec = (["Z3_HOME"], ["z3"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^ - string_of_int (to_secs 1 timeout), + string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [("\ncore(", ").")], known_failures = known_szs_status_failures, prem_role = Hypothesis, @@ -557,7 +581,7 @@ fun dummy_config format type_enc : atp_config = {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]), - arguments = K (K (K (K (K "")))), + arguments = K (K (K (K (K (K ""))))), proof_delims = [], known_failures = known_szs_status_failures, prem_role = Hypothesis, @@ -623,10 +647,12 @@ fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice : atp_config = {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]), - arguments = fn _ => fn _ => fn command => fn timeout => fn _ => - (if command <> "" then "-c " ^ quote command ^ " " else "") ^ - "-s " ^ the_remote_system system_name system_versions ^ " " ^ - "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)), + arguments = + fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ => + (if command <> "" then "-c " ^ quote command ^ " " else "") ^ + "-s " ^ the_remote_system system_name system_versions ^ " " ^ + "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^ + " " ^ file_name, proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_perl_failures @ known_says_failures, prem_role = prem_role, @@ -726,10 +752,10 @@ end val atps= - [alt_ergo, e, e_males, iprover, iprover_eq, leo2, satallax, spass, spass_poly, - vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, remote_e_tofof, - remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, - remote_vampire, remote_snark, remote_waldmeister] + [alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, + spass_poly, vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, + remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, + remote_satallax, remote_vampire, remote_snark, remote_waldmeister] val setup = fold add_atp atps diff -r c7f910a596ad -r 31d864d5057a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 17 13:11:44 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 17 14:01:45 2013 +0100 @@ -786,12 +786,12 @@ fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name val full_proof = debug orelse isar_proofs - val args = arguments ctxt full_proof extra - (slice_timeout |> the_default one_day) - (ord, ord_info, sel_weights) + val args = + arguments ctxt full_proof extra + (slice_timeout |> the_default one_day) + (File.shell_path prob_path) (ord, ord_info, sel_weights) val command = - "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ - File.shell_path prob_path ^ ")" + "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")" |> enclose "TIMEFORMAT='%3R'; { time " " ; }" val _ = atp_problem