expect SPASS 3.7, and give a friendly warning if an older version is used
authorblanchet
Mon Jun 14 16:43:44 2010 +0200 (2010-06-14)
changeset 37414d0cea0796295
parent 37413 e856582fe9c4
child 37415 521bc1d10445
expect SPASS 3.7, and give a friendly warning if an older version is used
doc-src/Sledgehammer/sledgehammer.tex
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 14 16:17:20 2010 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 14 16:43:44 2010 +0200
     1.3 @@ -338,11 +338,13 @@
     1.4  Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
     1.5  environment variable \texttt{SPASS\_HOME} to the directory that contains the
     1.6  \texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
     1.7 -download page. See \S\ref{installation} for details.
     1.8 +download page. Sledgehammer requires version 3.5 or above. See
     1.9 +\S\ref{installation} for details.
    1.10  
    1.11 -\item[$\bullet$] \textbf{\textit{spass\_tptp}:} Same as the above, except that
    1.12 -Sledgehammer communicates with SPASS using the TPTP syntax rather than the
    1.13 -native DFG syntax. This ATP is provided for experimental purposes.
    1.14 +\item[$\bullet$] \textbf{\textit{spass\_dfg}:} Same as the above, except that
    1.15 +Sledgehammer communicates with SPASS using the native DFG syntax rather than the
    1.16 +TPTP syntax. Sledgehammer requires version 3.0 or above. This ATP is provided
    1.17 +for compatibility reasons.
    1.18  
    1.19  \item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
    1.20  Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 14 16:17:20 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 14 16:43:44 2010 +0200
     2.3 @@ -331,40 +331,29 @@
     2.4  
     2.5  (* The "-VarWeight=3" option helps the higher-order problems, probably by
     2.6     counteracting the presence of "hAPP". *)
     2.7 -val spass_config : prover_config =
     2.8 +fun generic_spass_config dfg : prover_config =
     2.9    {home_var = "SPASS_HOME",
    2.10     executable = "SPASS",
    2.11     arguments = fn timeout =>
    2.12       "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    2.13 -     \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout),
    2.14 +     \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout)
    2.15 +     |> not dfg ? prefix "-TPTP ",
    2.16     proof_delims = [("Here is a proof", "Formulae used in the proof")],
    2.17     known_failures =
    2.18       [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
    2.19        (TimedOut, "SPASS beiseite: Ran out of time"),
    2.20        (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
    2.21        (MalformedInput, "Undefined symbol"),
    2.22 -      (MalformedInput, "Free Variable")],
    2.23 +      (MalformedInput, "Free Variable"),
    2.24 +      (OldSpass, "unrecognized option `-TPTP'"),
    2.25 +      (OldSpass, "Unrecognized option TPTP")],
    2.26     max_axiom_clauses = 40,
    2.27     prefers_theory_relevant = true}
    2.28 -val spass = dfg_prover "spass" spass_config
    2.29 -
    2.30 -(* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0
    2.31 -   supports only the DFG syntax. As soon as all Isabelle repository/snapshot
    2.32 -   users have upgraded to 3.7, we can kill "spass" (and all DFG support in
    2.33 -   Sledgehammer) and rename "spass_tptp" "spass". *)
    2.34 +val spass_dfg_config = generic_spass_config true
    2.35 +val spass_dfg = dfg_prover "spass_dfg" spass_dfg_config
    2.36  
    2.37 -val spass_tptp_config =
    2.38 -  {home_var = #home_var spass_config,
    2.39 -   executable = #executable spass_config,
    2.40 -   arguments = prefix "-TPTP " o #arguments spass_config,
    2.41 -   proof_delims = #proof_delims spass_config,
    2.42 -   known_failures =
    2.43 -     #known_failures spass_config @
    2.44 -     [(OldSpass, "unrecognized option `-TPTP'"),
    2.45 -      (OldSpass, "Unrecognized option TPTP")],
    2.46 -   max_axiom_clauses = #max_axiom_clauses spass_config,
    2.47 -   prefers_theory_relevant = #prefers_theory_relevant spass_config}
    2.48 -val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config
    2.49 +val spass_config = generic_spass_config false
    2.50 +val spass = tptp_prover "spass" spass_config
    2.51  
    2.52  (* remote prover invocation via SystemOnTPTP *)
    2.53  
    2.54 @@ -426,7 +415,7 @@
    2.55                       remotify (fst vampire)]
    2.56  
    2.57  val provers =
    2.58 -  [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e]
    2.59 +  [spass, spass_dfg, vampire, e, remote_vampire, remote_spass, remote_e]
    2.60  val prover_setup = fold add_prover provers
    2.61  
    2.62  val setup =
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Jun 14 16:17:20 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Jun 14 16:43:44 2010 +0200
     3.3 @@ -193,8 +193,7 @@
     3.4        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
     3.5  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
     3.6  
     3.7 -val max_dfg_symbol_length =
     3.8 -  if is_new_spass_version then 1000000 (* arbitrary large number *) else 63
     3.9 +val max_dfg_symbol_length = 63
    3.10  
    3.11  (* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
    3.12  fun controlled_length dfg s =
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Jun 14 16:17:20 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Jun 14 16:43:44 2010 +0200
     4.3 @@ -423,10 +423,13 @@
     4.4      fold (add_literal_decls params) literals decls
     4.5      handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
     4.6  
     4.7 -fun decls_of_clauses params clauses arity_clauses =
     4.8 -  let val functab =
     4.9 -        init_functab |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
    4.10 -                                            ("tc_bool", 0)]
    4.11 +fun decls_of_clauses (params as (full_types, explicit_apply, _, _)) clauses
    4.12 +                     arity_clauses =
    4.13 +  let
    4.14 +    val functab =
    4.15 +      init_functab
    4.16 +      |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
    4.17 +                             ("tc_bool", 0)]
    4.18        val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
    4.19        val (functab, predtab) =
    4.20          (functab, predtab) |> fold (add_clause_decls params) clauses
    4.21 @@ -595,7 +598,8 @@
    4.22      val tfree_preds = map dfg_tfree_predicate tfree_lits
    4.23      val (helper_clauses_strs, pool) =
    4.24        pool_map (apfst fst oo dfg_clause params) helper_clauses pool
    4.25 -    val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
    4.26 +    val (funcs, cl_preds) =
    4.27 +      decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
    4.28      val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
    4.29      val preds = tfree_preds @ cl_preds @ ty_preds
    4.30      val conjecture_offset =
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jun 14 16:17:20 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jun 14 16:43:44 2010 +0200
     5.3 @@ -6,7 +6,6 @@
     5.4  
     5.5  signature SLEDGEHAMMER_UTIL =
     5.6  sig
     5.7 -  val is_new_spass_version : bool
     5.8    val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
     5.9    val plural_s : int -> string
    5.10    val serial_commas : string -> string list -> string list
    5.11 @@ -25,18 +24,6 @@
    5.12  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    5.13  struct
    5.14  
    5.15 -val is_new_spass_version =
    5.16 -  case getenv "SPASS_VERSION" of
    5.17 -    "" => (case getenv "SPASS_HOME" of
    5.18 -             "" => false
    5.19 -           | s =>
    5.20 -             (* Hack: Preliminary versions of the SPASS 3.7 package don't set
    5.21 -                "SPASS_VERSION". *)
    5.22 -             String.isSubstring "/spass-3.7/" s)
    5.23 -  | s => (case s |> space_explode "." |> map Int.fromString of
    5.24 -            SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5)
    5.25 -          | _ => false)
    5.26 -
    5.27  fun pairf f g x = (f x, g x)
    5.28  
    5.29  fun plural_s n = if n = 1 then "" else "s"