# HG changeset patch # User blanchet # Date 1435228903 -7200 # Node ID a9b71c82647b103076bac6614cc0d465a0d28ddf # Parent 19c277ea65aeea5a5851bfd70520eda19b812901 put E before (typically remote, hence less reliable) Vampire diff -r 19c277ea65ae -r a9b71c82647b src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Wed Jun 24 23:03:55 2015 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Jun 25 12:41:43 2015 +0200 @@ -266,14 +266,14 @@ Sledgehammer: ``\textit{z3\/}'' \\ Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount] % -Sledgehammer: ``\textit{remote\_vampire\/}'' \\ -Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount] -% Sledgehammer: ``\textit{spass\/}'' \\ Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount] +% +Sledgehammer: ``\textit{e\/}'' \\ +Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount] \postw -Sledgehammer ran CVC4, SPASS, Vampire, and Z3 in parallel. Depending on which +Sledgehammer ran CVC4, E, SPASS, 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. diff -r 19c277ea65ae -r a9b71c82647b src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 24 23:03:55 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jun 25 12:41:43 2015 +0200 @@ -181,7 +181,7 @@ (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value mode ctxt = - [cvc4N, vampireN, z3N, spassN, eN, veritN, e_sineN] + [cvc4N, z3N, spassN, eN, vampireN, veritN, e_sineN] |> map_filter (remotify_prover_if_not_installed ctxt) (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))