# HG changeset patch # User blanchet # Date 1334999749 -7200 # Node ID 9a9218111085403bd94a123fc15af49ef8890296 # Parent 2cddc27a881f022e7bbe1cf004a6543eadde41d6 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 diff -r 2cddc27a881f -r 9a9218111085 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Sat Apr 21 07:33:47 2012 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Sat Apr 21 11:15:49 2012 +0200 @@ -290,12 +290,12 @@ $[a] = [b] \,\Longrightarrow\, a = b$ \\ Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount] % -Sledgehammer: ``\textit{remote\_satallax\/}'' on goal \\ +Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\ $[a] = [b] \,\Longrightarrow\, a = b$ \\ Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \postw -Sledgehammer ran E, Satallax, SPASS, Vampire, Waldmeister, and Z3 in parallel. +Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel. Depending on which provers are installed and how many processor cores are available, some of the provers might be missing or present with a \textit{remote\_} prefix. Waldmeister is run only for unit equational problems, @@ -913,7 +913,7 @@ with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers. \end{enum} -By default, Sledgehammer runs E, Satallax, SPASS, Vampire, Z3 (or whatever +By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever the SMT module's \textit{smt\_solver} configuration option is set to), and (if appropriate) Waldmeister in parallel---either locally or remotely, depending on the number of processor cores available. For historical reasons, the default diff -r 2cddc27a881f -r 9a9218111085 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 21 07:33:47 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 21 11:15:49 2012 +0200 @@ -215,7 +215,7 @@ (* The first ATP of the list is used by Auto Sledgehammer. Because of the low timeout, it makes sense to put SPASS first. *) fun default_provers_param_value ctxt = - [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, satallaxN, + [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN] |> map_filter (remotify_prover_if_not_installed ctxt) |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),