--- a/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 02 15:34:55 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 02 16:17:52 2012 +0200
@@ -203,10 +203,10 @@
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
\texttt{leo}, \texttt{satallax}, \texttt{SPASS}, or \texttt{vampire} executable.
Sledgehammer has been tested with E 1.0 to 1.4, LEO-II 1.3.4, Satallax 2.2, 2.3,
-and 2.4, SPASS 3.8ds, and Vampire 0.6, 1.0, and 1.8.%
+and 2.4, SPASS 3.8ds, and Vampire 0.6 to 2.6.%
\footnote{Following the rewrite of Vampire, the counter for version numbers was
-reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
-than 9.0 or 11.5.}%
+reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, and 2.6 are more
+recent than 9.0 or 11.5.}%
Since the ATPs' output formats are neither documented nor stable, other
versions might not work well with Sledgehammer. Ideally,
you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
@@ -859,7 +859,13 @@
variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
executable and \texttt{E\_VERSION} to the version number (e.g., ``1.4''), or
install the prebuilt E package from \download. Sledgehammer has been tested with
-versions 1.0 to 1.4.
+versions 1.0 to 1.6.
+
+\item[\labelitemi] \textbf{\textit{e\_males}:} E-MaLeS is a metaprover developed
+by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use
+E-MaLeS, set the environment variable \texttt{E\_MALES\_HOME} to the directory
+that contains the \texttt{emales.py} script. Sledgehammer has been tested with
+version 1.1.
\item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
@@ -867,7 +873,7 @@
the environment variable \texttt{LEO2\_HOME} to the directory that contains the
\texttt{leo} executable. Sledgehammer requires version 1.2.9 or above.
-\item[\labelitemi] \textbf{\textit{metis}:} Although it is much less powerful than
+\item[\labelitemi] \textbf{\textit{metis}:} Although it is less powerful than
the external provers, Metis itself can be used for proof search.
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
@@ -877,7 +883,8 @@
\texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the
-current settings (usually:\ Z3 with proof reconstruction).
+current settings (usually:\ Z3 with proof reconstruction) can be used for proof
+search.
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
@@ -886,14 +893,14 @@
version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from
\download. Sledgehammer requires version 3.8ds or above.
-\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution
-prover developed by Andrei Voronkov and his colleagues
+\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order
+resolution prover developed by Andrei Voronkov and his colleagues
\cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g.,
-``1.8rev1435''). Sledgehammer has been tested with versions 0.6, 1.0, and 1.8.
-Versions strictly above 1.8 (e.g., ``1.8rev1435'') support the TPTP typed
-first-order format (TFF0).
+``1.8rev1435'', ``2.6''). Sledgehammer has been tested with versions 0.6, 1.0,
+and 1.8. Versions strictly above 1.8 (e.g., ``1.8rev1435'') support the TPTP
+typed first-order format (TFF0).
\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
SRI \cite{yices}. To use Yices, set the environment variable
@@ -911,8 +918,7 @@
an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
formats (FOF and TFF0). It is included for experimental purposes. Sledgehammer
requires version 4.0 or above. To use it, set the environment variable
-\texttt{Z3\_HOME} to the directory that contains the \texttt{z3}
-executable.
+\texttt{Z3\_HOME} to the directory that contains the \texttt{z3} executable.
\end{enum}
The following remote provers are supported:
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 02 15:34:55 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 02 16:17:52 2012 +0200
@@ -45,6 +45,7 @@
val alt_ergoN : string
val dummy_thfN : string
val eN : string
+ val e_malesN : string
val e_sineN : string
val e_tofofN : string
val iproverN : string
@@ -140,6 +141,7 @@
val alt_ergoN = "alt_ergo"
val dummy_thfN = "dummy_thf" (* for experiments *)
val eN = "e"
+val e_malesN = "e_males"
val e_sineN = "e_sine"
val e_tofofN = "e_tofof"
val iproverN = "iprover"
@@ -189,10 +191,9 @@
val alt_ergo_config : atp_config =
{exec = (["WHY3_HOME"], ["why3"]),
- arguments =
- fn _ => fn _ => fn _ => fn timeout => fn _ =>
- "--format tff1 --prover alt-ergo --timelimit " ^
- string_of_int (to_secs 1 timeout),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ "--format tff1 --prover alt-ergo --timelimit " ^
+ string_of_int (to_secs 1 timeout),
proof_delims = [],
known_failures =
[(ProofMissing, ": Valid"),
@@ -210,8 +211,8 @@
(* E *)
-fun is_recent_e_version () = (string_ord (getenv "E_VERSION", "1.3") <> LESS)
-fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.6") <> LESS)
+fun is_e_at_least_1_3 () = (string_ord (getenv "E_VERSION", "1.3") <> LESS)
+fun is_e_at_least_1_6 () = (string_ord (getenv "E_VERSION", "1.6") <> LESS)
val tstp_proof_delims =
[("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
@@ -288,28 +289,27 @@
end
fun e_shell_level_argument full_proof =
- if is_new_e_version () then
+ if is_e_at_least_1_6 () then
" --pcl-shell-level=" ^ (if full_proof then "0" else "2")
else
""
fun effective_e_selection_heuristic ctxt =
- if is_recent_e_version () then Config.get ctxt e_selection_heuristic
+ if is_e_at_least_1_3 () then Config.get ctxt e_selection_heuristic
else e_autoN
-fun e_kbo () = if is_recent_e_version () then "KBO6" else "KBO"
+fun e_kbo () = if is_e_at_least_1_3 () then "KBO6" else "KBO"
val e_config : atp_config =
{exec = (["E_HOME"], ["eproof_ram", "eproof"]),
- arguments =
- fn ctxt => fn full_proof => fn heuristic => fn timeout =>
- fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
- "--tstp-in --tstp-out --output-level=5 --silent " ^
- e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
- e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
- "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
- "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
- e_shell_level_argument full_proof,
+ arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout =>
+ fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
+ "--tstp-in --tstp-out --output-level=5 --silent " ^
+ e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
+ e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
+ "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
+ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
+ e_shell_level_argument full_proof,
proof_delims = tstp_proof_delims,
known_failures =
[(TimedOut, "Failure: Resource limit exceeded (time)"),
@@ -332,6 +332,24 @@
val e = (eN, fn () => e_config)
+(* E-MaLeS *)
+
+val e_males_config : atp_config =
+ {exec = (["E_MALES_HOME"], ["emales.py"]),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p",
+ proof_delims = tstp_proof_delims,
+ known_failures = #known_failures e_config,
+ prem_role = Conjecture,
+ best_slices =
+ (* FUDGE *)
+ K [(1.0, (true, ((1000, FOF, "mono_tags??", combsN, false), "")))],
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = default_max_new_mono_instances}
+
+val e_males = (e_malesN, fn () => e_males_config)
+
+
(* LEO-II *)
(* LEO-II supports definitions, but it performs significantly better on our
@@ -341,12 +359,10 @@
val leo2_config : atp_config =
{exec = (["LEO2_HOME"], ["leo"]),
- arguments =
- fn _ => fn _ => fn _ => fn timeout => fn _ =>
- "--foatp e --atp e=\"$E_HOME\"/eprover \
- \--atp epclextract=\"$E_HOME\"/epclextract \
- \--proofoutput 1 --timeout " ^
- string_of_int (to_secs 1 timeout),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ "--foatp e --atp e=\"$E_HOME\"/eprover \
+ \--atp epclextract=\"$E_HOME\"/epclextract \
+ \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
proof_delims = tstp_proof_delims,
known_failures =
[(TimedOut, "CPU time limit exceeded, terminating"),
@@ -369,9 +385,8 @@
val satallax_config : atp_config =
{exec = (["SATALLAX_HOME"], ["satallax"]),
- arguments =
- fn _ => fn _ => fn _ => fn timeout => fn _ =>
- "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
proof_delims =
[("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
known_failures = known_szs_status_failures,
@@ -397,8 +412,8 @@
val spass_config : atp_config =
{exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
- ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
- |> extra_options <> "" ? prefix (extra_options ^ " "),
+ ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
+ |> extra_options <> "" ? prefix (extra_options ^ " "),
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
[(OldSPASS, "Unrecognized option Isabelle"),
@@ -430,7 +445,9 @@
(* Vampire 1.8 has TFF support, but the support was buggy until revision
1435 (or shortly before). *)
-fun is_new_vampire_version () =
+fun is_vampire_at_least_1_8 () =
+ string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
+fun is_vampire_beyond_1_8 () =
string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
@@ -438,11 +455,14 @@
val vampire_config : atp_config =
{exec = (["VAMPIRE_HOME"], ["vampire"]),
arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
- "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
- " --proof tptp --output_axiom_names on\
- \ --forced_options propositional_to_bdd=off\
- \ --thanks \"Andrei and Krystof\" --input_file"
- |> sos = sosN ? prefix "--sos on ",
+ "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
+ " --proof tptp --output_axiom_names on" ^
+ (if is_vampire_at_least_1_8 () then
+ " --forced_options propositional_to_bdd=off"
+ else
+ "") ^
+ " --thanks \"Andrei and Krystof\" --input_file"
+ |> sos = sosN ? prefix "--sos on ",
proof_delims =
[("=========== Refutation ==========",
"======= End of refutation ======="),
@@ -458,7 +478,7 @@
prem_role = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- (if is_new_vampire_version () then
+ (if is_vampire_beyond_1_8 () then
[(0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))),
(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))),
(0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))]
@@ -481,8 +501,8 @@
val z3_tptp_config : atp_config =
{exec = (["Z3_HOME"], ["z3"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
- "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
- string_of_int (to_secs 1 timeout),
+ "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
+ string_of_int (to_secs 1 timeout),
proof_delims = [("\ncore(", ").")],
known_failures = known_szs_status_failures,
prem_role = Hypothesis,
@@ -566,9 +586,9 @@
prem_role best_slice : atp_config =
{exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
- (if command <> "" then "-c " ^ quote command ^ " " else "") ^
- "-s " ^ the_system system_name system_versions ^ " " ^
- "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
+ (if command <> "" then "-c " ^ quote command ^ " " else "") ^
+ "-s " ^ the_system system_name system_versions ^ " " ^
+ "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
proof_delims = union (op =) tstp_proof_delims proof_delims,
known_failures = known_failures @ known_perl_failures @ known_says_failures,
prem_role = prem_role,
@@ -671,10 +691,10 @@
end
val atps=
- [alt_ergo, e, leo2, satallax, spass, spass_poly, vampire, z3_tptp, dummy_thf,
- remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
- remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
- remote_waldmeister]
+ [alt_ergo, e, e_males, leo2, satallax, spass, spass_poly, vampire, z3_tptp,
+ dummy_thf, remote_e, remote_e_sine, remote_e_tofof, remote_iprover,
+ remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
+ remote_z3_tptp, remote_snark, remote_waldmeister]
val setup = fold add_atp atps