--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 14 16:17:20 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Jun 14 16:43:44 2010 +0200
@@ -338,11 +338,13 @@
Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
environment variable \texttt{SPASS\_HOME} to the directory that contains the
\texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
-download page. See \S\ref{installation} for details.
+download page. Sledgehammer requires version 3.5 or above. See
+\S\ref{installation} for details.
-\item[$\bullet$] \textbf{\textit{spass\_tptp}:} Same as the above, except that
-Sledgehammer communicates with SPASS using the TPTP syntax rather than the
-native DFG syntax. This ATP is provided for experimental purposes.
+\item[$\bullet$] \textbf{\textit{spass\_dfg}:} Same as the above, except that
+Sledgehammer communicates with SPASS using the native DFG syntax rather than the
+TPTP syntax. Sledgehammer requires version 3.0 or above. This ATP is provided
+for compatibility reasons.
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 14 16:17:20 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 14 16:43:44 2010 +0200
@@ -331,40 +331,29 @@
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
-val spass_config : prover_config =
+fun generic_spass_config dfg : prover_config =
{home_var = "SPASS_HOME",
executable = "SPASS",
arguments = fn timeout =>
"-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
- \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout),
+ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout)
+ |> not dfg ? prefix "-TPTP ",
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
[(IncompleteUnprovable, "SPASS beiseite: Completion found"),
(TimedOut, "SPASS beiseite: Ran out of time"),
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
(MalformedInput, "Undefined symbol"),
- (MalformedInput, "Free Variable")],
+ (MalformedInput, "Free Variable"),
+ (OldSpass, "unrecognized option `-TPTP'"),
+ (OldSpass, "Unrecognized option TPTP")],
max_axiom_clauses = 40,
prefers_theory_relevant = true}
-val spass = dfg_prover "spass" spass_config
-
-(* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0
- supports only the DFG syntax. As soon as all Isabelle repository/snapshot
- users have upgraded to 3.7, we can kill "spass" (and all DFG support in
- Sledgehammer) and rename "spass_tptp" "spass". *)
+val spass_dfg_config = generic_spass_config true
+val spass_dfg = dfg_prover "spass_dfg" spass_dfg_config
-val spass_tptp_config =
- {home_var = #home_var spass_config,
- executable = #executable spass_config,
- arguments = prefix "-TPTP " o #arguments spass_config,
- proof_delims = #proof_delims spass_config,
- known_failures =
- #known_failures spass_config @
- [(OldSpass, "unrecognized option `-TPTP'"),
- (OldSpass, "Unrecognized option TPTP")],
- max_axiom_clauses = #max_axiom_clauses spass_config,
- prefers_theory_relevant = #prefers_theory_relevant spass_config}
-val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config
+val spass_config = generic_spass_config false
+val spass = tptp_prover "spass" spass_config
(* remote prover invocation via SystemOnTPTP *)
@@ -426,7 +415,7 @@
remotify (fst vampire)]
val provers =
- [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e]
+ [spass, spass_dfg, vampire, e, remote_vampire, remote_spass, remote_e]
val prover_setup = fold add_prover provers
val setup =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Jun 14 16:17:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Jun 14 16:43:44 2010 +0200
@@ -193,8 +193,7 @@
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
-val max_dfg_symbol_length =
- if is_new_spass_version then 1000000 (* arbitrary large number *) else 63
+val max_dfg_symbol_length = 63
(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
fun controlled_length dfg s =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Jun 14 16:17:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Jun 14 16:43:44 2010 +0200
@@ -423,10 +423,13 @@
fold (add_literal_decls params) literals decls
handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
-fun decls_of_clauses params clauses arity_clauses =
- let val functab =
- init_functab |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
- ("tc_bool", 0)]
+fun decls_of_clauses (params as (full_types, explicit_apply, _, _)) clauses
+ arity_clauses =
+ let
+ val functab =
+ init_functab
+ |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
+ ("tc_bool", 0)]
val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
val (functab, predtab) =
(functab, predtab) |> fold (add_clause_decls params) clauses
@@ -595,7 +598,8 @@
val tfree_preds = map dfg_tfree_predicate tfree_lits
val (helper_clauses_strs, pool) =
pool_map (apfst fst oo dfg_clause params) helper_clauses pool
- val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
+ val (funcs, cl_preds) =
+ decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
val preds = tfree_preds @ cl_preds @ ty_preds
val conjecture_offset =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Jun 14 16:17:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Jun 14 16:43:44 2010 +0200
@@ -6,7 +6,6 @@
signature SLEDGEHAMMER_UTIL =
sig
- val is_new_spass_version : bool
val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
val plural_s : int -> string
val serial_commas : string -> string list -> string list
@@ -25,18 +24,6 @@
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
-val is_new_spass_version =
- case getenv "SPASS_VERSION" of
- "" => (case getenv "SPASS_HOME" of
- "" => false
- | s =>
- (* Hack: Preliminary versions of the SPASS 3.7 package don't set
- "SPASS_VERSION". *)
- String.isSubstring "/spass-3.7/" s)
- | s => (case s |> space_explode "." |> map Int.fromString of
- SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5)
- | _ => false)
-
fun pairf f g x = (f x, g x)
fun plural_s n = if n = 1 then "" else "s"