LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover
authorblanchet
Sun May 13 16:31:01 2012 +0200 (2012-05-13)
changeset 4791494f37848b7c9
parent 47913 b12e1fa43ad1
child 47915 5b1a737777c9
LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 13 16:31:01 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 13 16:31:01 2012 +0200
     1.3 @@ -325,20 +325,16 @@
     1.4     required_vars = [],
     1.5     arguments =
     1.6       fn _ => fn _ => fn sos => fn timeout => fn _ =>
     1.7 -        "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout)
     1.8 -        |> sos = sosN ? prefix "--sos ",
     1.9 +        "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
    1.10     proof_delims = tstp_proof_delims,
    1.11     known_failures =
    1.12       known_szs_status_failures @
    1.13       [(TimedOut, "CPU time limit exceeded, terminating"),
    1.14        (GaveUp, "No.of.Axioms")],
    1.15     prem_kind = Hypothesis,
    1.16 -   best_slices = fn ctxt =>
    1.17 +   best_slices =
    1.18       (* FUDGE *)
    1.19 -     [(0.667, (false, ((100, leo2_thf0, "mono_native_higher", keep_lamsN, false), sosN))),
    1.20 -      (0.333, (true, ((50, leo2_thf0, "mono_native_higher", keep_lamsN, false), no_sosN)))]
    1.21 -     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    1.22 -         else I)}
    1.23 +     K [(1.0, (true, ((20, leo2_thf0, "mono_native_higher", keep_lamsN, false), "")))]}
    1.24  
    1.25  val leo2 = (leo2N, fn () => leo2_config)
    1.26  
    1.27 @@ -359,7 +355,7 @@
    1.28     prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
    1.29     best_slices =
    1.30       (* FUDGE *)
    1.31 -     K [(1.0, (true, ((75, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]}
    1.32 +     K [(1.0, (true, ((120, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]}
    1.33  
    1.34  val satallax = (satallaxN, fn () => satallax_config)
    1.35