1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Mar 21 16:53:24 2012 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Mar 21 16:53:24 2012 +0100
1.3 @@ -60,7 +60,7 @@
1.4 val remote_atp :
1.5 string -> string -> string list -> (string * string) list
1.6 -> (failure * string) list -> formula_kind -> formula_kind
1.7 - -> (Proof.context -> slice_spec) -> string * atp_config
1.8 + -> (Proof.context -> slice_spec * string) -> string * atp_config
1.9 val add_atp : string * atp_config -> theory -> theory
1.10 val get_atp : theory -> string -> atp_config
1.11 val supported_atps : theory -> string list
1.12 @@ -574,14 +574,15 @@
1.13 conj_sym_kind prem_kind best_slice : atp_config =
1.14 {exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
1.15 required_vars = [],
1.16 - arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
1.17 - "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
1.18 - " -s " ^ the_system system_name system_versions,
1.19 + arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
1.20 + (if command <> "" then "-c " ^ quote command ^ " " else "") ^
1.21 + "-s " ^ the_system system_name system_versions ^ " " ^
1.22 + "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
1.23 proof_delims = union (op =) tstp_proof_delims proof_delims,
1.24 known_failures = known_failures @ known_perl_failures @ known_says_failures,
1.25 conj_sym_kind = conj_sym_kind,
1.26 prem_kind = prem_kind,
1.27 - best_slices = fn ctxt => [(1.0, (false, (best_slice ctxt, "")))]}
1.28 + best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]}
1.29
1.30 fun remotify_config system_name system_versions best_slice
1.31 ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
1.32 @@ -602,44 +603,43 @@
1.33
1.34 val remote_e =
1.35 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
1.36 - (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *))
1.37 + (K ((750, FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
1.38 val remote_leo2 =
1.39 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
1.40 - (K (100, leo2_thf0, "mono_native_higher", liftingN, false) (* FUDGE *))
1.41 + (K ((100, leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
1.42 val remote_satallax =
1.43 - remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
1.44 - (K (100, satallax_thf0, "mono_native_higher", keep_lamsN, false)
1.45 - (* FUDGE *))
1.46 + remotify_atp satallax "Satallax" ["2.3", "2.2", "2"]
1.47 + (K ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "satallax.opt -p hocore -t %d %s") (* FUDGE *))
1.48 val remote_vampire =
1.49 remotify_atp vampire "Vampire" ["1.8"]
1.50 - (K (250, vampire_tff0, "mono_native", combs_or_liftingN, false) (* FUDGE *))
1.51 + (K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
1.52 val remote_z3_tptp =
1.53 remotify_atp z3_tptp "Z3" ["3.0"]
1.54 - (K (250, z3_tff0, "mono_native", combsN, false) (* FUDGE *))
1.55 + (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
1.56 val remote_e_sine =
1.57 - remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
1.58 - Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *))
1.59 + remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom Conjecture
1.60 + (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
1.61 val remote_iprover =
1.62 remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
1.63 - (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
1.64 + (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
1.65 val remote_iprover_eq =
1.66 remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
1.67 - (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
1.68 + (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
1.69 val remote_snark =
1.70 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
1.71 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
1.72 - (K (100, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *))
1.73 + (K ((100, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
1.74 val remote_e_tofof =
1.75 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
1.76 Hypothesis
1.77 - (K (150, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *))
1.78 + (K ((150, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
1.79 val remote_waldmeister =
1.80 remote_atp waldmeisterN "Waldmeister" ["710"]
1.81 [("#START OF PROOF", "Proved Goals:")]
1.82 [(OutOfResources, "Too many function symbols"),
1.83 (Crashed, "Unrecoverable Segmentation Fault")]
1.84 Hypothesis Hypothesis
1.85 - (K (50, CNF_UEQ, "mono_tags??", combsN, false) (* FUDGE *))
1.86 + (K ((50, CNF_UEQ, "mono_tags??", combsN, false), "") (* FUDGE *))
1.87
1.88 (* Setup *)
1.89
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 21 16:53:24 2012 +0100
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 21 16:53:24 2012 +0100
2.3 @@ -215,7 +215,8 @@
2.4 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
2.5 timeout, it makes sense to put SPASS first. *)
2.6 fun default_provers_param_value ctxt =
2.7 - [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN]
2.8 + [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, satallaxN,
2.9 + waldmeisterN]
2.10 |> map_filter (remotify_prover_if_not_installed ctxt)
2.11 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
2.12 max_default_remote_threads)