took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
1.1 --- a/src/HOL/TPTP/MaSh_Export.thy Mon Jul 23 09:28:03 2012 +0200
1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Mon Jul 23 15:32:30 2012 +0200
1.3 @@ -11,7 +11,7 @@
1.4
1.5 sledgehammer_params
1.6 [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
1.7 - lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
1.8 + lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize]
1.9
1.10 ML {*
1.11 open MaSh_Export
1.12 @@ -66,5 +66,4 @@
1.13 ()
1.14 *}
1.15
1.16 -
1.17 end
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 09:28:03 2012 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jul 23 15:32:30 2012 +0200
2.3 @@ -226,7 +226,7 @@
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 E first. *)
2.6 fun default_provers_param_value ctxt =
2.7 - [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N]
2.8 + [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN]
2.9 |> map_filter (remotify_prover_if_not_installed ctxt)
2.10 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
2.11 max_default_remote_threads)
2.12 @@ -404,11 +404,11 @@
2.13 else
2.14 ();
2.15 mash_learn ctxt (get_params Normal ctxt
2.16 - (("timeout",
2.17 - [string_of_real default_learn_atp_timeout]) ::
2.18 + ([("timeout",
2.19 + [string_of_real default_learn_atp_timeout]),
2.20 + ("slice", ["false"])] @
2.21 override_params @
2.22 - [("slice", ["false"]),
2.23 - ("minimize", ["true"]),
2.24 + [("minimize", ["true"]),
2.25 ("preplay_timeout", ["0"])]))
2.26 fact_override (#facts (Proof.goal state))
2.27 (subcommand = learn_atpN orelse subcommand = relearn_atpN))