use E 1.8's auto scheduler option
authorblanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 5700810f68b83b474
parent 57007 d3eed0518882
child 57009 8cb6a5f1ae84
use E 1.8's auto scheduler option
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 19 23:43:53 2014 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 19 23:43:53 2014 +0200
     1.3 @@ -338,10 +338,10 @@
     1.4  
     1.5  val e_config : atp_config =
     1.6    {exec = (fn () => (["E_HOME"],
     1.7 -       if is_e_at_least_1_8 () then ["eprover"] else ["eproof_ram", "eproof"])),
     1.8 -   arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout =>
     1.9 -       fn file_name =>
    1.10 -       fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
    1.11 +     if is_e_at_least_1_8 () then ["eprover"] else ["eproof_ram", "eproof"])),
    1.12 +   arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout => fn file_name =>
    1.13 +     fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
    1.14 +       (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
    1.15         "--tstp-in --tstp-out --silent " ^
    1.16         e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
    1.17         e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
    1.18 @@ -351,10 +351,8 @@
    1.19            " --proof-object=1"
    1.20          else
    1.21            " --output-level=5" ^
    1.22 -          (if is_e_at_least_1_6 () then
    1.23 -             " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
    1.24 -           else
    1.25 -             "")) ^
    1.26 +          (if is_e_at_least_1_6 () then " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
    1.27 +           else "")) ^
    1.28         " " ^ file_name,
    1.29     proof_delims =
    1.30       [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @