src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
changeset 74235 f0d231ead660
parent 74232 34c8cf767fa3
child 74236 6a0e1c14a8c2
equal deleted inserted replaced
74234:b304285fd800 74235:f0d231ead660
   266       (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^
   266       (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^
   267       (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
   267       (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
   268     end
   268     end
   269 
   269 
   270 val e_config : atp_config =
   270 val e_config : atp_config =
   271   {exec = (["E_HOME"], ["eprover"]),
   271   {exec = (["E_HOME"], ["eprover-ho", "eprover"]),
   272    arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn problem =>
   272    arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn problem =>
   273      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
   273      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
   274        ["--auto-schedule --tstp-in --tstp-out --silent " ^
   274        ["--auto-schedule --tstp-in --tstp-out --silent " ^
   275         e_selection_weight_arguments ctxt heuristic sel_weights ^
   275         e_selection_weight_arguments ctxt heuristic sel_weights ^
   276         e_term_order_info_arguments gen_weights gen_prec ord_info ^
   276         e_term_order_info_arguments gen_weights gen_prec ord_info ^