1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Tue Mar 20 18:42:45 2012 +0100
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Tue Mar 20 18:42:45 2012 +0100
     1.3 @@ -117,14 +117,14 @@
     1.4  fun run_some_atp ctxt format problem =
     1.5    let
     1.6      val thy = Proof_Context.theory_of ctxt
     1.7 -    val prob_file = File.tmp_path (Path.explode "prob.tptp")
     1.8 +    val prob_file = File.tmp_path (Path.explode "prob")
     1.9      val atp = case format of DFG _ => spass_newN | _ => eN
    1.10      val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp
    1.11      val ord = effective_term_order ctxt atp
    1.12      val _ = problem |> lines_for_atp_problem format ord (K [])
    1.13                      |> File.write_list prob_file
    1.14      val command =
    1.15 -      File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
    1.16 +      File.shell_path (Path.explode (getenv (hd (fst exec)) ^ "/" ^ snd exec)) ^
    1.17        " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^
    1.18        File.shell_path prob_file
    1.19    in

     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 18:42:45 2012 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 18:42:45 2012 +0100
     2.3 @@ -14,8 +14,8 @@
     2.4  
     2.5    type slice_spec = int * atp_format * string * string * bool
     2.6    type atp_config =
     2.7 -    {exec : string * string,
     2.8 -     required_execs : (string * string) list,
     2.9 +    {exec : string list * string,
    2.10 +     required_vars : string list list,
    2.11       arguments :
    2.12         Proof.context -> bool -> string -> Time.time
    2.13         -> term_order * (unit -> (string * int) list)
    2.14 @@ -51,12 +51,12 @@
    2.15    val satallaxN : string
    2.16    val snarkN : string
    2.17    val spassN : string
    2.18 +  val spass_oldN : string
    2.19    val spass_newN : string
    2.20    val vampireN : string
    2.21    val waldmeisterN : string
    2.22    val z3_tptpN : string
    2.23    val remote_prefix : string
    2.24 -  val effective_term_order : Proof.context -> string -> term_order
    2.25    val remote_atp :
    2.26      string -> string -> string list -> (string * string) list
    2.27      -> (failure * string) list -> formula_kind -> formula_kind
    2.28 @@ -66,6 +66,7 @@
    2.29    val supported_atps : theory -> string list
    2.30    val is_atp_installed : theory -> string -> bool
    2.31    val refresh_systems_on_tptp : unit -> unit
    2.32 +  val effective_term_order : Proof.context -> string -> term_order
    2.33    val setup : theory -> theory
    2.34  end;
    2.35  
    2.36 @@ -81,8 +82,8 @@
    2.37  type slice_spec = int * atp_format * string * string * bool
    2.38  
    2.39  type atp_config =
    2.40 -  {exec : string * string,
    2.41 -   required_execs : (string * string) list,
    2.42 +  {exec : string list * string,
    2.43 +   required_vars : string list list,
    2.44     arguments :
    2.45       Proof.context -> bool -> string -> Time.time
    2.46       -> term_order * (unit -> (string * int) list)
    2.47 @@ -133,7 +134,7 @@
    2.48  (* named ATPs *)
    2.49  
    2.50  val alt_ergoN = "alt_ergo"
    2.51 -val dummy_thfN = "dummy_thf" (* experimental *)
    2.52 +val dummy_thfN = "dummy_thf" (* for experiments *)
    2.53  val eN = "e"
    2.54  val e_sineN = "e_sine"
    2.55  val e_tofofN = "e_tofof"
    2.56 @@ -143,7 +144,8 @@
    2.57  val satallaxN = "satallax"
    2.58  val snarkN = "snark"
    2.59  val spassN = "spass"
    2.60 -val spass_newN = "spass_new" (* experimental *)
    2.61 +val spass_oldN = "spass_old" (* for experiments *)
    2.62 +val spass_newN = "spass_new" (* for experiments *)
    2.63  val vampireN = "vampire"
    2.64  val waldmeisterN = "waldmeister"
    2.65  val z3_tptpN = "z3_tptp"
    2.66 @@ -178,30 +180,13 @@
    2.67  val term_order =
    2.68    Attrib.setup_config_string @{binding atp_term_order} (K smartN)
    2.69  
    2.70 -fun effective_term_order ctxt atp =
    2.71 -  let val ord = Config.get ctxt term_order in
    2.72 -    if ord = smartN then
    2.73 -      if atp = spass_newN then
    2.74 -        {is_lpo = false, gen_weights = true, gen_prec = false, gen_simp = true}
    2.75 -      else
    2.76 -        {is_lpo = false, gen_weights = false, gen_prec = false,
    2.77 -         gen_simp = false}
    2.78 -    else
    2.79 -      let val is_lpo = String.isSubstring lpoN ord in
    2.80 -        {is_lpo = is_lpo,
    2.81 -         gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
    2.82 -         gen_prec = String.isSubstring xprecN ord,
    2.83 -         gen_simp = String.isSubstring xsimpN ord}
    2.84 -      end
    2.85 -  end
    2.86 -
    2.87  (* Alt-Ergo *)
    2.88  
    2.89  val alt_ergo_tff1 = TFF (TPTP_Polymorphic, TPTP_Explicit)
    2.90  
    2.91  val alt_ergo_config : atp_config =
    2.92 -  {exec = ("WHY3_HOME", "why3"),
    2.93 -   required_execs = [],
    2.94 +  {exec = (["WHY3_HOME"], "why3"),
    2.95 +   required_vars = [],
    2.96     arguments =
    2.97       fn _ => fn _ => fn _ => fn timeout => fn _ =>
    2.98          "--format tff1 --prover alt-ergo --timelimit " ^
    2.99 @@ -222,7 +207,7 @@
   2.100  
   2.101  (* E *)
   2.102  
   2.103 -fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.3") = LESS)
   2.104 +fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.2") = GREATER)
   2.105  
   2.106  val tstp_proof_delims =
   2.107    [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
   2.108 @@ -300,11 +285,11 @@
   2.109      end
   2.110  
   2.111  fun effective_e_selection_heuristic ctxt =
   2.112 -  if is_old_e_version () then e_autoN else Config.get ctxt e_selection_heuristic
   2.113 +  if is_new_e_version () then Config.get ctxt e_selection_heuristic else e_autoN
   2.114  
   2.115  val e_config : atp_config =
   2.116 -  {exec = ("E_HOME", "eproof"),
   2.117 -   required_execs = [],
   2.118 +  {exec = (["E_HOME"], "eproof"),
   2.119 +   required_vars = [],
   2.120     arguments =
   2.121       fn ctxt => fn _ => fn heuristic => fn timeout =>
   2.122          fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
   2.123 @@ -340,8 +325,8 @@
   2.124  val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
   2.125  
   2.126  val leo2_config : atp_config =
   2.127 -  {exec = ("LEO2_HOME", "leo"),
   2.128 -   required_execs = [],
   2.129 +  {exec = (["LEO2_HOME"], "leo"),
   2.130 +   required_vars = [],
   2.131     arguments =
   2.132       fn _ => fn _ => fn sos => fn timeout => fn _ =>
   2.133          "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout)
   2.134 @@ -368,8 +353,8 @@
   2.135  val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
   2.136  
   2.137  val satallax_config : atp_config =
   2.138 -  {exec = ("SATALLAX_HOME", "satallax"),
   2.139 -   required_execs = [],
   2.140 +  {exec = (["SATALLAX_HOME"], "satallax"),
   2.141 +   required_vars = [],
   2.142     arguments =
   2.143       fn _ => fn _ => fn _ => fn timeout => fn _ =>
   2.144          "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
   2.145 @@ -387,11 +372,15 @@
   2.146  
   2.147  (* SPASS *)
   2.148  
   2.149 -(* The "-VarWeight=3" option helps the higher-order problems, probably by
   2.150 -   counteracting the presence of explicit application operators. *)
   2.151 -val spass_config : atp_config =
   2.152 -  {exec = ("ISABELLE_ATP", "scripts/spass"),
   2.153 -   required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
   2.154 +fun is_new_spass_version () =
   2.155 +  string_ord (getenv "SPASS_VERSION", "3.7") = GREATER orelse
   2.156 +  getenv "SPASS_NEW_HOME" <> ""
   2.157 +
   2.158 +(* TODO: Legacy: Remove after planned Isabelle2012 release (and don't forget
   2.159 +   "required_vars" and "script/spass"). *)
   2.160 +val spass_old_config : atp_config =
   2.161 +  {exec = (["ISABELLE_ATP"], "scripts/spass"),
   2.162 +   required_vars = [["SPASS_OLD_HOME", "SPASS_HOME"]],
   2.163     arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
   2.164       ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   2.165        \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
   2.166 @@ -415,7 +404,7 @@
   2.167        (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))]
   2.168       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)}
   2.169  
   2.170 -val spass = (spassN, spass_config)
   2.171 +val spass_old = (spass_oldN, spass_old_config)
   2.172  
   2.173  val spass_new_H2 = "-Heuristic=2"
   2.174  val spass_new_H2SOS = "-Heuristic=2 -SOS"
   2.175 @@ -423,17 +412,16 @@
   2.176  val spass_new_H2NuVS0Red2 =
   2.177    "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
   2.178  
   2.179 -(* Experimental *)
   2.180  val spass_new_config : atp_config =
   2.181 -  {exec = ("SPASS_NEW_HOME", "SPASS"),
   2.182 -   required_execs = [],
   2.183 +  {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"),
   2.184 +   required_vars = [],
   2.185     arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
   2.186       ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
   2.187       |> extra_options <> "" ? prefix (extra_options ^ " "),
   2.188 -   proof_delims = #proof_delims spass_config,
   2.189 -   known_failures = #known_failures spass_config,
   2.190 -   conj_sym_kind = #conj_sym_kind spass_config,
   2.191 -   prem_kind = #prem_kind spass_config,
   2.192 +   proof_delims = #proof_delims spass_old_config,
   2.193 +   known_failures = #known_failures spass_old_config,
   2.194 +   conj_sym_kind = #conj_sym_kind spass_old_config,
   2.195 +   prem_kind = #prem_kind spass_old_config,
   2.196     best_slices = fn _ =>
   2.197       (* FUDGE *)
   2.198       [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
   2.199 @@ -447,19 +435,22 @@
   2.200  
   2.201  val spass_new = (spass_newN, spass_new_config)
   2.202  
   2.203 +fun spass () =
   2.204 +  (spassN, if is_new_spass_version () then spass_new_config
   2.205 +           else spass_old_config)
   2.206  
   2.207  (* Vampire *)
   2.208  
   2.209  (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on
   2.210     SystemOnTPTP. *)
   2.211 -fun is_old_vampire_version () =
   2.212 -  string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
   2.213 +fun is_new_vampire_version () =
   2.214 +  string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
   2.215  
   2.216  val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
   2.217  
   2.218  val vampire_config : atp_config =
   2.219 -  {exec = ("VAMPIRE_HOME", "vampire"),
   2.220 -   required_execs = [],
   2.221 +  {exec = (["VAMPIRE_HOME"], "vampire"),
   2.222 +   required_vars = [],
   2.223     arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
   2.224       "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
   2.225       " --proof tptp --output_axiom_names on\
   2.226 @@ -482,14 +473,14 @@
   2.227     prem_kind = Conjecture,
   2.228     best_slices = fn ctxt =>
   2.229       (* FUDGE *)
   2.230 -     (if is_old_vampire_version () then
   2.231 +     (if is_new_vampire_version () then
   2.232 +        [(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))),
   2.233 +         (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))),
   2.234 +         (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))]
   2.235 +      else
   2.236          [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN))),
   2.237           (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN))),
   2.238 -         (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))]
   2.239 -      else
   2.240 -        [(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))),
   2.241 -         (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))),
   2.242 -         (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))])
   2.243 +         (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))])
   2.244       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   2.245           else I)}
   2.246  
   2.247 @@ -501,8 +492,8 @@
   2.248  val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
   2.249  
   2.250  val z3_tptp_config : atp_config =
   2.251 -  {exec = ("Z3_HOME", "z3"),
   2.252 -   required_execs = [],
   2.253 +  {exec = (["Z3_HOME"], "z3"),
   2.254 +   required_vars = [],
   2.255     arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
   2.256       "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
   2.257     proof_delims = [],
   2.258 @@ -522,8 +513,8 @@
   2.259  (* Not really a prover: Experimental Polymorphic TFF and THF output *)
   2.260  
   2.261  fun dummy_config format type_enc : atp_config =
   2.262 -  {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
   2.263 -   required_execs = [],
   2.264 +  {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"),
   2.265 +   required_vars = [],
   2.266     arguments = K (K (K (K (K "")))),
   2.267     proof_delims = [],
   2.268     known_failures = known_szs_status_failures,
   2.269 @@ -581,8 +572,8 @@
   2.270  
   2.271  fun remote_config system_name system_versions proof_delims known_failures
   2.272                    conj_sym_kind prem_kind best_slice : atp_config =
   2.273 -  {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
   2.274 -   required_execs = [],
   2.275 +  {exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
   2.276 +   required_vars = [],
   2.277     arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
   2.278       "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
   2.279       " -s " ^ the_system system_name system_versions,
   2.280 @@ -663,18 +654,37 @@
   2.281  val supported_atps = Symtab.keys o Data.get
   2.282  
   2.283  fun is_atp_installed thy name =
   2.284 -  let val {exec, required_execs, ...} = get_atp thy name in
   2.285 -    forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
   2.286 +  let val {exec, required_vars, ...} = get_atp thy name in
   2.287 +    forall (exists (fn var => getenv var <> "")) (fst exec :: required_vars)
   2.288    end
   2.289  
   2.290  fun refresh_systems_on_tptp () =
   2.291    Synchronized.change systems (fn _ => get_systems ())
   2.292  
   2.293 -val atps =
   2.294 -  [alt_ergo, e, leo2, dummy_thf, satallax, spass, spass_new, vampire, z3_tptp,
   2.295 -   remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
   2.296 -   remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
   2.297 -   remote_waldmeister]
   2.298 -val setup = fold add_atp atps
   2.299 +fun effective_term_order ctxt atp =
   2.300 +  let val ord = Config.get ctxt term_order in
   2.301 +    if ord = smartN then
   2.302 +      if atp = spass_newN orelse
   2.303 +         (atp = spassN andalso is_new_spass_version ()) then
   2.304 +        {is_lpo = false, gen_weights = true, gen_prec = false, gen_simp = true}
   2.305 +      else
   2.306 +        {is_lpo = false, gen_weights = false, gen_prec = false,
   2.307 +         gen_simp = false}
   2.308 +    else
   2.309 +      let val is_lpo = String.isSubstring lpoN ord in
   2.310 +        {is_lpo = is_lpo,
   2.311 +         gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
   2.312 +         gen_prec = String.isSubstring xprecN ord,
   2.313 +         gen_simp = String.isSubstring xsimpN ord}
   2.314 +      end
   2.315 +  end
   2.316 +
   2.317 +fun atps () =
   2.318 +  [alt_ergo, e, leo2, dummy_thf, satallax, spass_old, spass_new, spass (),
   2.319 +   vampire, z3_tptp, remote_e, remote_e_sine, remote_e_tofof, remote_iprover,
   2.320 +   remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
   2.321 +   remote_z3_tptp, remote_snark, remote_waldmeister]
   2.322 +
   2.323 +fun setup thy = fold add_atp (atps ()) thy
   2.324  
   2.325  end;

     3.1 --- a/src/HOL/Tools/ATP/scripts/spass	Tue Mar 20 18:42:45 2012 +0100
     3.2 +++ b/src/HOL/Tools/ATP/scripts/spass	Tue Mar 20 18:42:45 2012 +0100
     3.3 @@ -7,12 +7,13 @@
     3.4  
     3.5  options=${@:1:$(($#-1))}
     3.6  name=${@:$(($#)):1}
     3.7 +home=${SPASS_OLD_HOME:-$SPASS_HOME}
     3.8  
     3.9 -"$SPASS_HOME/SPASS" -Flotter "$name" \
    3.10 +"$home/SPASS" -Flotter "$name" \
    3.11      | sed 's/description({$/description({*/' \
    3.12      | sed 's/set_ClauseFormulaRelation()\.//' \
    3.13      > $name.cnf
    3.14  cat $name.cnf
    3.15 -"$SPASS_HOME/SPASS" $options "$name.cnf" \
    3.16 +"$home/SPASS" $options "$name.cnf" \
    3.17      | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
    3.18  rm -f "$name.cnf"

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Mar 20 18:42:45 2012 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Mar 20 18:42:45 2012 +0100
     4.3 @@ -215,8 +215,7 @@
     4.4  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
     4.5     timeout, it makes sense to put SPASS first. *)
     4.6  fun default_provers_param_value ctxt =
     4.7 -  [spassN, spass_newN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN,
     4.8 -   waldmeisterN]
     4.9 +  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN]
    4.10    |> map_filter (remotify_prover_if_not_installed ctxt)
    4.11    |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
    4.12                                    max_default_remote_threads)

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Mar 20 18:42:45 2012 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Mar 20 18:42:45 2012 +0100
     5.3 @@ -580,7 +580,7 @@
     5.4  val atp_timeout_slack = seconds 1.0
     5.5  
     5.6  fun run_atp mode name
     5.7 -        ({exec, required_execs, arguments, proof_delims, known_failures,
     5.8 +        ({exec, required_vars, arguments, proof_delims, known_failures,
     5.9            conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
    5.10          (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
    5.11                      uncurried_aliases, max_relevant, max_mono_iters,
    5.12 @@ -605,7 +605,11 @@
    5.13          Path.append (Path.explode dest_dir) problem_file_name
    5.14        else
    5.15          error ("No such directory: " ^ quote dest_dir ^ ".")
    5.16 -    val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
    5.17 +    val command =
    5.18 +      case find_first (fn var => getenv var <> "") (fst exec) of
    5.19 +        SOME var => Path.explode (getenv var ^ "/" ^ snd exec)
    5.20 +      | NONE => error ("The environment variable " ^ quote (hd (fst exec)) ^
    5.21 +                       " is not set.")
    5.22      fun split_time s =
    5.23        let
    5.24          val split = String.tokens (fn c => str c = "\n")
    5.25 @@ -622,10 +626,12 @@
    5.26           as_time t |> Time.fromMilliseconds)
    5.27        end
    5.28      fun run_on prob_file =
    5.29 -      case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
    5.30 -        (home_var, _) :: _ =>
    5.31 -        error ("The environment variable " ^ quote home_var ^ " is not set.")
    5.32 -      | [] =>
    5.33 +      case find_first (forall (fn var => getenv var = ""))
    5.34 +                      (fst exec :: required_vars) of
    5.35 +        SOME home_vars =>
    5.36 +        error ("The environment variable " ^ quote (hd home_vars) ^
    5.37 +               " is not set.")
    5.38 +      | NONE =>
    5.39          if File.exists command then
    5.40            let
    5.41              (* If slicing is disabled, we expand the last slice to fill the