707 ? monomorphize_facts |
707 ? monomorphize_facts |
708 |> map (apsnd prop_of) |
708 |> map (apsnd prop_of) |
709 |> prepare_atp_problem ctxt format conj_sym_kind prem_kind |
709 |> prepare_atp_problem ctxt format conj_sym_kind prem_kind |
710 type_enc false lam_trans uncurried_aliases |
710 type_enc false lam_trans uncurried_aliases |
711 readable_names true hyp_ts concl_t |
711 readable_names true hyp_ts concl_t |
712 fun rel_weights () = atp_problem_relevance_weights atp_problem |
712 fun sel_weights () = atp_problem_selection_weights atp_problem |
713 fun kbo_weights () = atp_problem_kbo_weights atp_problem |
713 fun ord_weights () = atp_problem_term_order_weights atp_problem |
714 val full_proof = debug orelse isar_proof |
714 val full_proof = debug orelse isar_proof |
715 val command = |
715 val command = |
716 File.shell_path command ^ " " ^ |
716 File.shell_path command ^ " " ^ |
717 arguments ctxt full_proof extra slice_timeout rel_weights ^ |
717 arguments ctxt full_proof extra slice_timeout sel_weights ^ |
718 " " ^ File.shell_path prob_file |
718 " " ^ File.shell_path prob_file |
719 |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" |
719 |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" |
720 val _ = |
720 val _ = |
721 atp_problem |
721 atp_problem |
722 |> lines_for_atp_problem format kbo_weights |
722 |> lines_for_atp_problem format ord_weights |
723 |> cons ("% " ^ command ^ "\n") |
723 |> cons ("% " ^ command ^ "\n") |
724 |> File.write_list prob_file |
724 |> File.write_list prob_file |
725 val ((output, run_time), (atp_proof, outcome)) = |
725 val ((output, run_time), (atp_proof, outcome)) = |
726 TimeLimit.timeLimit generous_slice_timeout |
726 TimeLimit.timeLimit generous_slice_timeout |
727 Isabelle_System.bash_output command |
727 Isabelle_System.bash_output command |