313 best_max_new_mono_instances = default_max_new_mono_instances} |
313 best_max_new_mono_instances = default_max_new_mono_instances} |
314 |
314 |
315 val e = (eN, fn () => e_config) |
315 val e = (eN, fn () => e_config) |
316 |
316 |
317 |
317 |
318 (* E-Par *) |
|
319 |
|
320 val e_par_config : atp_config = |
|
321 {exec = K (["E_HOME"], ["runepar.pl"]), |
|
322 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
|
323 string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^ " 2" (* proofs *), |
|
324 proof_delims = tstp_proof_delims, |
|
325 known_failures = #known_failures e_config, |
|
326 prem_role = Conjecture, |
|
327 best_slices = |
|
328 (* FUDGE *) |
|
329 K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")), |
|
330 (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")), |
|
331 (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")), |
|
332 (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))], |
|
333 best_max_mono_iters = default_max_mono_iters, |
|
334 best_max_new_mono_instances = default_max_new_mono_instances} |
|
335 |
|
336 val e_par = (e_parN, fn () => e_par_config) |
|
337 |
|
338 |
|
339 (* iProver *) |
318 (* iProver *) |
340 |
319 |
341 val iprover_config : atp_config = |
320 val iprover_config : atp_config = |
342 {exec = K (["IPROVER_HOME"], ["iproveropt", "iprover"]), |
321 {exec = K (["IPROVER_HOME"], ["iproveropt", "iprover"]), |
343 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
322 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
671 remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] |
650 remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] |
672 (K (((40, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *)) |
651 (K (((40, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *)) |
673 val remote_leo3 = |
652 val remote_leo3 = |
674 remotify_atp leo3 "Leo-III" ["1.1"] |
653 remotify_atp leo3 "Leo-III" ["1.1"] |
675 (K (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) |
654 (K (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) |
676 val remote_snark = |
|
677 remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"] |
|
678 [("refutation.", "end_refutation.")] [] Hypothesis |
|
679 (K (((100, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *)) |
|
680 val remote_vampire = |
655 val remote_vampire = |
681 remotify_atp vampire "Vampire" ["THF-4.4"] |
656 remotify_atp vampire "Vampire" ["THF-4.4"] |
682 (K (((400, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *)) |
657 (K (((400, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *)) |
683 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" |
658 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" |
684 val remote_zipperposition = |
659 val remote_zipperposition = |
717 gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord} |
692 gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord} |
718 end |
693 end |
719 end |
694 end |
720 |
695 |
721 val atps = |
696 val atps = |
722 [agsyhol, alt_ergo, e, e_par, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, |
697 [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, |
723 zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, |
698 remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, |
724 remote_leo3, remote_snark, remote_vampire, remote_waldmeister, remote_zipperposition] |
699 remote_vampire, remote_waldmeister, remote_zipperposition] |
725 |
700 |
726 val _ = Theory.setup (fold add_atp atps) |
701 val _ = Theory.setup (fold add_atp atps) |
727 |
702 |
728 end; |
703 end; |