src/HOL/Tools/ATP/atp_systems.ML
changeset 57672 6be755147695
parent 57671 dc5e1b1db9ba
child 57707 0242e9578828
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 25 11:26:17 2014 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 25 11:26:19 2014 +0200
     1.3 @@ -261,9 +261,9 @@
     1.4       |> implode) ^
     1.5      "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
     1.6      \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
     1.7 -    \FIFOWeight(PreferProcessed))'"
     1.8 +    \FIFOWeight(PreferProcessed))' "
     1.9    else
    1.10 -    "-xAuto"
    1.11 +    "-xAuto "
    1.12  
    1.13  val e_ord_weights =
    1.14    map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
    1.15 @@ -273,10 +273,8 @@
    1.16  fun e_term_order_info_arguments false false _ = ""
    1.17    | e_term_order_info_arguments gen_weights gen_prec ord_info =
    1.18      let val ord_info = ord_info () in
    1.19 -      (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' "
    1.20 -       else "") ^
    1.21 -      (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' "
    1.22 -       else "")
    1.23 +      (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^
    1.24 +      (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
    1.25      end
    1.26  
    1.27  val e_config : atp_config =
    1.28 @@ -287,8 +285,8 @@
    1.29       fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
    1.30         (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
    1.31         "--tstp-in --tstp-out --silent " ^
    1.32 -       e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
    1.33 -       e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
    1.34 +       e_selection_weight_arguments ctxt heuristic sel_weights ^
    1.35 +       e_term_order_info_arguments gen_weights gen_prec ord_info ^
    1.36         "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
    1.37         "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
    1.38         (if full_proofs orelse not (is_e_at_least_1_8 ()) then