swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations
1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Sat Apr 21 07:33:47 2012 +0200
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Sat Apr 21 11:15:49 2012 +0200
1.3 @@ -290,12 +290,12 @@
1.4 $[a] = [b] \,\Longrightarrow\, a = b$ \\
1.5 Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
1.6 %
1.7 -Sledgehammer: ``\textit{remote\_satallax\/}'' on goal \\
1.8 +Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\
1.9 $[a] = [b] \,\Longrightarrow\, a = b$ \\
1.10 Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
1.11 \postw
1.12
1.13 -Sledgehammer ran E, Satallax, SPASS, Vampire, Waldmeister, and Z3 in parallel.
1.14 +Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
1.15 Depending on which provers are installed and how many processor cores are
1.16 available, some of the provers might be missing or present with a
1.17 \textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
1.18 @@ -913,7 +913,7 @@
1.19 with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
1.20 \end{enum}
1.21
1.22 -By default, Sledgehammer runs E, Satallax, SPASS, Vampire, Z3 (or whatever
1.23 +By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
1.24 the SMT module's \textit{smt\_solver} configuration option is set to), and (if
1.25 appropriate) Waldmeister in parallel---either locally or remotely, depending on
1.26 the number of processor cores available. For historical reasons, the default
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 21 07:33:47 2012 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 21 11:15:49 2012 +0200
2.3 @@ -215,7 +215,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 SPASS first. *)
2.6 fun default_provers_param_value ctxt =
2.7 - [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, satallaxN,
2.8 + [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN,
2.9 waldmeisterN]
2.10 |> map_filter (remotify_prover_if_not_installed ctxt)
2.11 |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),