# HG changeset patch # User blanchet # Date 1276526624 -7200 # Node ID d0cea0796295a3844106c56e58168e9bda3cea02 # Parent e856582fe9c46ce677c8bcf04d8c18a8212f2f46 expect SPASS 3.7, and give a friendly warning if an older version is used diff -r e856582fe9c4 -r d0cea0796295 doc-src/Sledgehammer/sledgehammer.tex --- 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 diff -r e856582fe9c4 -r d0cea0796295 src/HOL/Tools/ATP_Manager/atp_systems.ML --- 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 = diff -r e856582fe9c4 -r d0cea0796295 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- 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 = diff -r e856582fe9c4 -r d0cea0796295 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- 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 = diff -r e856582fe9c4 -r d0cea0796295 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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"