--- 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