src/HOL/Tools/ATP/atp_systems.ML
changeset 67021 41f1f8c4259b
parent 66544 3e838cf5e80c
child 67560 0fa87bd86566
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Nov 07 15:16:40 2017 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Nov 07 15:16:41 2017 +0100
     1.3 @@ -416,6 +416,29 @@
     1.4  val leo2 = (leo2N, fn () => leo2_config)
     1.5  
     1.6  
     1.7 +(* Leo-III *)
     1.8 +
     1.9 +(* include choice? Disabled now since its disabled for satallax as well. *)
    1.10 +val leo3_thf1 = THF (Polymorphic, THF_Without_Choice)
    1.11 +
    1.12 +val leo3_config : atp_config =
    1.13 +  {exec = K (["LEO3_HOME"], ["leo3"]),
    1.14 +   arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
    1.15 +     file_name ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \
    1.16 +     \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
    1.17 +     (if full_proofs then "--nleq --naeq " else ""),
    1.18 +   proof_delims = tstp_proof_delims,
    1.19 +   known_failures = known_szs_status_failures,
    1.20 +   prem_role = Hypothesis,
    1.21 +   best_slices =
    1.22 +     (* FUDGE *)
    1.23 +     K [(1.0, (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), ""))],
    1.24 +   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    1.25 +   best_max_new_mono_instances = default_max_new_mono_instances}
    1.26 +
    1.27 +val leo3 = (leo3N, fn () => leo3_config)
    1.28 +
    1.29 +
    1.30  (* Satallax *)
    1.31  
    1.32  (* Choice is disabled until there is proper reconstruction for it. *)
    1.33 @@ -431,7 +454,7 @@
    1.34     prem_role = Hypothesis,
    1.35     best_slices =
    1.36       (* FUDGE *)
    1.37 -     K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
    1.38 +     K [(1.0, (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
    1.39     best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    1.40     best_max_new_mono_instances = default_max_new_mono_instances}
    1.41  
    1.42 @@ -713,9 +736,12 @@
    1.43  val remote_leo2 =
    1.44    remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
    1.45      (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
    1.46 +val remote_leo3 =
    1.47 +  remotify_atp leo3 "Leo-III" ["1.1"]
    1.48 +    (K (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
    1.49  val remote_satallax =
    1.50    remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
    1.51 -    (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
    1.52 +    (K (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
    1.53  val remote_vampire =
    1.54    remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"]
    1.55      (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
    1.56 @@ -766,10 +792,10 @@
    1.57    end
    1.58  
    1.59  val atps =
    1.60 -  [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
    1.61 +  [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, leo3, satallax, spass, vampire,
    1.62     z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
    1.63 -   remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
    1.64 -   remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
    1.65 +   remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, remote_satallax,
    1.66 +   remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
    1.67  
    1.68  val _ = Theory.setup (fold add_atp atps)
    1.69