equal
deleted
inserted
replaced
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 ^ |