# HG changeset patch
# User blanchet
# Date 1343895029 -7200
# Node ID fb461f81e76e73692e8d4e5c5e00752d96212564
# Parent  053cc8dfde355ec9aa073ce4814005d2cdbe3ac2
added E-MaLeS to list of provers for testing

diff -r 053cc8dfde35 -r fb461f81e76e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 01 22:12:29 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 02 10:10:29 2012 +0200
@@ -45,6 +45,7 @@
   val alt_ergoN : string
   val dummy_thfN : string
   val eN : string
+  val e_malesN : string
   val e_sineN : string
   val e_tofofN : string
   val iproverN : string
@@ -140,6 +141,7 @@
 val alt_ergoN = "alt_ergo"
 val dummy_thfN = "dummy_thf" (* for experiments *)
 val eN = "e"
+val e_malesN = "e_males"
 val e_sineN = "e_sine"
 val e_tofofN = "e_tofof"
 val iproverN = "iprover"
@@ -189,10 +191,9 @@
 
 val alt_ergo_config : atp_config =
   {exec = (["WHY3_HOME"], ["why3"]),
-   arguments =
-     fn _ => fn _ => fn _ => fn timeout => fn _ =>
-        "--format tff1 --prover alt-ergo --timelimit " ^
-        string_of_int (to_secs 1 timeout),
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+       "--format tff1 --prover alt-ergo --timelimit " ^
+       string_of_int (to_secs 1 timeout),
    proof_delims = [],
    known_failures =
      [(ProofMissing, ": Valid"),
@@ -301,15 +302,14 @@
 
 val e_config : atp_config =
   {exec = (["E_HOME"], ["eproof_ram", "eproof"]),
-   arguments =
-     fn ctxt => fn full_proof => fn heuristic => fn timeout =>
-        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,
+   arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout =>
+       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,
    proof_delims = tstp_proof_delims,
    known_failures =
      [(TimedOut, "Failure: Resource limit exceeded (time)"),
@@ -332,6 +332,24 @@
 val e = (eN, fn () => e_config)
 
 
+(* E-MaLeS *)
+
+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",
+   proof_delims = tstp_proof_delims,
+   known_failures = #known_failures e_config,
+   prem_role = Conjecture,
+   best_slices =
+     (* FUDGE *)
+     K [(1.0, (true, ((1000, FOF, "mono_tags??", 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)
+
+
 (* LEO-II *)
 
 (* LEO-II supports definitions, but it performs significantly better on our
@@ -341,12 +359,10 @@
 
 val leo2_config : atp_config =
   {exec = (["LEO2_HOME"], ["leo"]),
-   arguments =
-     fn _ => fn _ => fn _ => fn timeout => fn _ =>
-        "--foatp e --atp e=\"$E_HOME\"/eprover \
-        \--atp epclextract=\"$E_HOME\"/epclextract \
-        \--proofoutput 1 --timeout " ^
-        string_of_int (to_secs 1 timeout),
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+       "--foatp e --atp e=\"$E_HOME\"/eprover \
+       \--atp epclextract=\"$E_HOME\"/epclextract \
+       \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
      [(TimedOut, "CPU time limit exceeded, terminating"),
@@ -369,9 +385,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 _ =>
+       "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
    proof_delims =
      [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
    known_failures = known_szs_status_failures,
@@ -397,8 +412,8 @@
 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 ^ " "),
+       ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
+       |> extra_options <> "" ? prefix (extra_options ^ " "),
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
      [(OldSPASS, "Unrecognized option Isabelle"),
@@ -438,11 +453,11 @@
 val vampire_config : atp_config =
   {exec = (["VAMPIRE_HOME"], ["vampire"]),
    arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
-     "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
-     " --proof tptp --output_axiom_names on\
-     \ --forced_options propositional_to_bdd=off\
-     \ --thanks \"Andrei and Krystof\" --input_file"
-     |> sos = sosN ? prefix "--sos on ",
+       "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
+       " --proof tptp --output_axiom_names on\
+       \ --forced_options propositional_to_bdd=off\
+       \ --thanks \"Andrei and Krystof\" --input_file"
+       |> sos = sosN ? prefix "--sos on ",
    proof_delims =
      [("=========== Refutation ==========",
        "======= End of refutation ======="),
@@ -481,8 +496,8 @@
 val z3_tptp_config : atp_config =
   {exec = (["Z3_HOME"], ["z3"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
-     "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
-     string_of_int (to_secs 1 timeout),
+       "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
+       string_of_int (to_secs 1 timeout),
    proof_delims = [("\ncore(", ").")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
@@ -566,9 +581,9 @@
                   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_system system_name system_versions ^ " " ^
-     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
+       (if command <> "" then "-c " ^ quote command ^ " " else "") ^
+       "-s " ^ the_system system_name system_versions ^ " " ^
+       "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @ known_says_failures,
    prem_role = prem_role,
@@ -671,10 +686,10 @@
   end
 
 val atps=
-  [alt_ergo, e, 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_z3_tptp, remote_snark,
-   remote_waldmeister]
+  [alt_ergo, e, e_males, 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_z3_tptp, remote_snark, remote_waldmeister]
 
 val setup = fold add_atp atps