src/HOL/Tools/ATP_Manager/atp_systems.ML
changeset 38023 962b0a7f544b
parent 38022 d9c4d87838f3
child 38032 54448f5d151f
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:58:30 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 18:33:10 2010 +0200
     1.3 @@ -7,9 +7,23 @@
     1.4  
     1.5  signature ATP_SYSTEMS =
     1.6  sig
     1.7 -  val dest_dir : string Config.T
     1.8 -  val problem_prefix : string Config.T
     1.9 -  val measure_runtime : bool Config.T
    1.10 +  datatype failure =
    1.11 +    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
    1.12 +    OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
    1.13 +
    1.14 +  type prover_config =
    1.15 +    {home_var: string,
    1.16 +     executable: string,
    1.17 +     arguments: bool -> Time.time -> string,
    1.18 +     proof_delims: (string * string) list,
    1.19 +     known_failures: (failure * string) list,
    1.20 +     max_new_relevant_facts_per_iter: int,
    1.21 +     prefers_theory_relevant: bool,
    1.22 +     explicit_forall: bool}
    1.23 +
    1.24 +  val add_prover: string * prover_config -> theory -> theory
    1.25 +  val get_prover: theory -> string -> prover_config
    1.26 +  val available_atps: theory -> unit
    1.27    val refresh_systems_on_tptp : unit -> unit
    1.28    val default_atps_param_value : unit -> string
    1.29    val setup : theory -> theory
    1.30 @@ -18,28 +32,11 @@
    1.31  structure ATP_Systems : ATP_SYSTEMS =
    1.32  struct
    1.33  
    1.34 -open Metis_Clauses
    1.35 -open Sledgehammer_Util
    1.36 -open Sledgehammer_Fact_Filter
    1.37 -open ATP_Problem
    1.38 -open Sledgehammer_Proof_Reconstruct
    1.39 -open Sledgehammer
    1.40 -
    1.41 -(** generic ATP **)
    1.42 -
    1.43 -(* external problem files *)
    1.44 +(* prover configuration *)
    1.45  
    1.46 -val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K "");
    1.47 -  (*Empty string means create files in Isabelle's temporary files directory.*)
    1.48 -
    1.49 -val (problem_prefix, problem_prefix_setup) =
    1.50 -  Attrib.config_string "atp_problem_prefix" (K "prob");
    1.51 -
    1.52 -val (measure_runtime, measure_runtime_setup) =
    1.53 -  Attrib.config_bool "atp_measure_runtime" (K false);
    1.54 -
    1.55 -
    1.56 -(* prover configuration *)
    1.57 +datatype failure =
    1.58 +  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
    1.59 +  OldSpass | MalformedInput | MalformedOutput | UnknownError
    1.60  
    1.61  type prover_config =
    1.62    {home_var: string,
    1.63 @@ -52,728 +49,32 @@
    1.64     explicit_forall: bool}
    1.65  
    1.66  
    1.67 -(* basic template *)
    1.68 -
    1.69 -val remotify = prefix "remote_"
    1.70 -
    1.71 -fun with_path cleanup after f path =
    1.72 -  Exn.capture f path
    1.73 -  |> tap (fn _ => cleanup path)
    1.74 -  |> Exn.release
    1.75 -  |> tap (after path)
    1.76 -
    1.77 -(* Splits by the first possible of a list of delimiters. *)
    1.78 -fun extract_proof delims output =
    1.79 -  case pairself (find_first (fn s => String.isSubstring s output))
    1.80 -                (ListPair.unzip delims) of
    1.81 -    (SOME begin_delim, SOME end_delim) =>
    1.82 -    (output |> first_field begin_delim |> the |> snd
    1.83 -            |> first_field end_delim |> the |> fst
    1.84 -            |> first_field "\n" |> the |> snd
    1.85 -     handle Option.Option => "")
    1.86 -  | _ => ""
    1.87 -
    1.88 -fun extract_proof_and_outcome complete res_code proof_delims known_failures
    1.89 -                              output =
    1.90 -  case map_filter (fn (failure, pattern) =>
    1.91 -                      if String.isSubstring pattern output then SOME failure
    1.92 -                      else NONE) known_failures of
    1.93 -    [] => (case extract_proof proof_delims output of
    1.94 -             "" => ("", SOME UnknownError)
    1.95 -           | proof => if res_code = 0 then (proof, NONE)
    1.96 -                      else ("", SOME UnknownError))
    1.97 -  | (failure :: _) =>
    1.98 -    ("", SOME (if failure = IncompleteUnprovable andalso complete then
    1.99 -                 Unprovable
   1.100 -               else
   1.101 -                 failure))
   1.102 -
   1.103 -fun string_for_failure Unprovable = "The ATP problem is unprovable."
   1.104 -  | string_for_failure IncompleteUnprovable =
   1.105 -    "The ATP cannot prove the problem."
   1.106 -  | string_for_failure CantConnect = "Can't connect to remote ATP."
   1.107 -  | string_for_failure TimedOut = "Timed out."
   1.108 -  | string_for_failure OutOfResources = "The ATP ran out of resources."
   1.109 -  | string_for_failure OldSpass =
   1.110 -    (* FIXME: Change the error message below to point to the Isabelle download
   1.111 -       page once the package is there. *)
   1.112 -    "Warning: Sledgehammer requires a more recent version of SPASS with \
   1.113 -    \support for the TPTP syntax. To install it, download and untar the \
   1.114 -    \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
   1.115 -    \\"spass-3.7\" directory's full path to \"" ^
   1.116 -    Path.implode (Path.expand (Path.appends
   1.117 -        (Path.variable "ISABELLE_HOME_USER" ::
   1.118 -         map Path.basic ["etc", "components"]))) ^
   1.119 -    "\" on a line of its own."
   1.120 -  | string_for_failure MalformedInput =
   1.121 -    "Internal Sledgehammer error: The ATP problem is malformed. Please report \
   1.122 -    \this to the Isabelle developers."
   1.123 -  | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
   1.124 -  | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
   1.125 -
   1.126 -
   1.127 -(* Clause preparation *)
   1.128 -
   1.129 -datatype fol_formula =
   1.130 -  FOLFormula of {formula_name: string,
   1.131 -                 kind: kind,
   1.132 -                 combformula: (name, combterm) formula,
   1.133 -                 ctypes_sorts: typ list}
   1.134 -
   1.135 -fun mk_anot phi = AConn (ANot, [phi])
   1.136 -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
   1.137 -fun mk_ahorn [] phi = phi
   1.138 -  | mk_ahorn (phi :: phis) psi =
   1.139 -    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
   1.140 -
   1.141 -(* ### FIXME: reintroduce
   1.142 -fun make_clause_table xs =
   1.143 -  fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
   1.144 -(* Remove existing axiom clauses from the conjecture clauses, as this can
   1.145 -   dramatically boost an ATP's performance (for some reason). *)
   1.146 -fun subtract_cls ax_clauses =
   1.147 -  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
   1.148 -*)
   1.149 -
   1.150 -fun combformula_for_prop thy =
   1.151 -  let
   1.152 -    val do_term = combterm_from_term thy
   1.153 -    fun do_quant bs q s T t' =
   1.154 -      do_formula ((s, T) :: bs) t'
   1.155 -      #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
   1.156 -    and do_conn bs c t1 t2 =
   1.157 -      do_formula bs t1 ##>> do_formula bs t2
   1.158 -      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
   1.159 -    and do_formula bs t =
   1.160 -      case t of
   1.161 -        @{const Not} $ t1 =>
   1.162 -        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
   1.163 -      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   1.164 -        do_quant bs AForall s T t'
   1.165 -      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   1.166 -        do_quant bs AExists s T t'
   1.167 -      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
   1.168 -      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
   1.169 -      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
   1.170 -      | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   1.171 -        do_conn bs AIff t1 t2
   1.172 -      | _ => (fn ts => do_term bs (Envir.eta_contract t)
   1.173 -                       |>> APred ||> union (op =) ts)
   1.174 -  in do_formula [] end
   1.175 -
   1.176 -(* Converts an elim-rule into an equivalent theorem that does not have the
   1.177 -   predicate variable. Leaves other theorems unchanged. We simply instantiate
   1.178 -   the conclusion variable to False. (Cf. "transform_elim_term" in
   1.179 -   "ATP_Systems".) *)
   1.180 -(* FIXME: test! *)
   1.181 -fun transform_elim_term t =
   1.182 -  case Logic.strip_imp_concl t of
   1.183 -    @{const Trueprop} $ Var (z, @{typ bool}) =>
   1.184 -    subst_Vars [(z, @{const True})] t
   1.185 -  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
   1.186 -  | _ => t
   1.187 -
   1.188 -(* Removes the lambdas from an equation of the form "t = (%x. u)".
   1.189 -   (Cf. "extensionalize_theorem" in "Clausifier".) *)
   1.190 -fun extensionalize_term t =
   1.191 -  let
   1.192 -    fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _]))
   1.193 -               $ t2 $ Abs (s, var_T, t')) =
   1.194 -        let val var_t = Var (("x", j), var_T) in
   1.195 -          Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
   1.196 -            $ betapply (t2, var_t) $ subst_bound (var_t, t')
   1.197 -          |> aux (j + 1)
   1.198 -        end
   1.199 -      | aux _ t = t
   1.200 -  in aux (maxidx_of_term t + 1) t end
   1.201 -
   1.202 -(* FIXME: Guarantee freshness *)
   1.203 -fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
   1.204 -fun conceal_bounds Ts t =
   1.205 -  subst_bounds (map (Free o apfst concealed_bound_name)
   1.206 -                    (length Ts - 1 downto 0 ~~ rev Ts), t)
   1.207 -fun reveal_bounds Ts =
   1.208 -  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   1.209 -                    (0 upto length Ts - 1 ~~ Ts))
   1.210 +(* named provers *)
   1.211  
   1.212 -fun introduce_combinators_in_term ctxt kind t =
   1.213 -  let
   1.214 -    val thy = ProofContext.theory_of ctxt
   1.215 -    fun aux Ts t =
   1.216 -      case t of
   1.217 -        @{const Not} $ t1 => @{const Not} $ aux Ts t1
   1.218 -      | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   1.219 -        t0 $ Abs (s, T, aux (T :: Ts) t')
   1.220 -      | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   1.221 -        t0 $ Abs (s, T, aux (T :: Ts) t')
   1.222 -      | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   1.223 -      | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   1.224 -      | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   1.225 -      | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
   1.226 -          $ t1 $ t2 =>
   1.227 -        t0 $ aux Ts t1 $ aux Ts t2
   1.228 -      | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   1.229 -               t
   1.230 -             else
   1.231 -               let
   1.232 -                 val t = t |> conceal_bounds Ts
   1.233 -                           |> Envir.eta_contract
   1.234 -                 val ([t], ctxt') = Variable.import_terms true [t] ctxt
   1.235 -               in
   1.236 -                 t |> cterm_of thy
   1.237 -                   |> Clausifier.introduce_combinators_in_cterm
   1.238 -                   |> singleton (Variable.export ctxt' ctxt)
   1.239 -                   |> prop_of |> Logic.dest_equals |> snd
   1.240 -                   |> reveal_bounds Ts
   1.241 -               end
   1.242 -  in t |> not (Meson.is_fol_term thy t) ? aux [] end
   1.243 -  handle THM _ =>
   1.244 -         (* A type variable of sort "{}" will make abstraction fail. *)
   1.245 -         case kind of
   1.246 -           Axiom => HOLogic.true_const
   1.247 -         | Conjecture => HOLogic.false_const
   1.248 -
   1.249 -(* making axiom and conjecture clauses *)
   1.250 -fun make_clause ctxt (formula_name, kind, t) =
   1.251 -  let
   1.252 -    val thy = ProofContext.theory_of ctxt
   1.253 -    (* ### FIXME: perform other transformations previously done by
   1.254 -       "Clausifier.to_nnf", e.g. "HOL.If" *)
   1.255 -    val t = t |> transform_elim_term
   1.256 -              |> Object_Logic.atomize_term thy
   1.257 -              |> extensionalize_term
   1.258 -              |> introduce_combinators_in_term ctxt kind
   1.259 -    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   1.260 -  in
   1.261 -    FOLFormula {formula_name = formula_name, combformula = combformula,
   1.262 -                kind = kind, ctypes_sorts = ctypes_sorts}
   1.263 -  end
   1.264 -
   1.265 -fun make_axiom_clause ctxt (name, th) =
   1.266 -  (name, make_clause ctxt (name, Axiom, prop_of th))
   1.267 -fun make_conjecture_clauses ctxt ts =
   1.268 -  map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
   1.269 -       (0 upto length ts - 1) ts
   1.270 -
   1.271 -(** Helper clauses **)
   1.272 -
   1.273 -fun count_combterm (CombConst ((s, _), _, _)) =
   1.274 -    Symtab.map_entry s (Integer.add 1)
   1.275 -  | count_combterm (CombVar _) = I
   1.276 -  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
   1.277 -fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   1.278 -  | count_combformula (AConn (_, phis)) = fold count_combformula phis
   1.279 -  | count_combformula (APred tm) = count_combterm tm
   1.280 -fun count_fol_formula (FOLFormula {combformula, ...}) =
   1.281 -  count_combformula combformula
   1.282 -
   1.283 -val optional_helpers =
   1.284 -  [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
   1.285 -   (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
   1.286 -   (["c_COMBS"], @{thms COMBS_def})]
   1.287 -val optional_typed_helpers =
   1.288 -  [(["c_True", "c_False"], @{thms True_or_False}),
   1.289 -   (["c_If"], @{thms if_True if_False True_or_False})]
   1.290 -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   1.291 -
   1.292 -val init_counters =
   1.293 -  Symtab.make (maps (maps (map (rpair 0) o fst))
   1.294 -                    [optional_helpers, optional_typed_helpers])
   1.295 -
   1.296 -fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
   1.297 -  let
   1.298 -    val ct = fold (fold count_fol_formula) [conjectures, axclauses]
   1.299 -                  init_counters
   1.300 -    fun is_needed c = the (Symtab.lookup ct c) > 0
   1.301 -    val cnfs =
   1.302 -      (optional_helpers
   1.303 -       |> full_types ? append optional_typed_helpers
   1.304 -       |> maps (fn (ss, ths) =>
   1.305 -                   if exists is_needed ss then map (`Thm.get_name_hint) ths
   1.306 -                   else [])) @
   1.307 -      (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
   1.308 -  in map (snd o make_axiom_clause ctxt) cnfs end
   1.309 -
   1.310 -fun s_not (@{const Not} $ t) = t
   1.311 -  | s_not t = @{const Not} $ t
   1.312 -
   1.313 -(* prepare for passing to writer,
   1.314 -   create additional clauses based on the information from extra_cls *)
   1.315 -fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
   1.316 -  let
   1.317 -    val thy = ProofContext.theory_of ctxt
   1.318 -    val goal_t = Logic.list_implies (hyp_ts, concl_t)
   1.319 -    val is_FO = Meson.is_fol_term thy goal_t
   1.320 -    val axtms = map (prop_of o snd) extra_cls
   1.321 -    val subs = tfree_classes_of_terms [goal_t]
   1.322 -    val supers = tvar_classes_of_terms axtms
   1.323 -    val tycons = type_consts_of_terms thy (goal_t :: axtms)
   1.324 -    (* TFrees in conjecture clauses; TVars in axiom clauses *)
   1.325 -    val conjectures =
   1.326 -      map (s_not o HOLogic.dest_Trueprop) hyp_ts @
   1.327 -        [HOLogic.dest_Trueprop concl_t]
   1.328 -      |> make_conjecture_clauses ctxt
   1.329 -    val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
   1.330 -    val (clnames, axiom_clauses) =
   1.331 -      ListPair.unzip (map (make_axiom_clause ctxt) axcls)
   1.332 -    (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
   1.333 -       "get_helper_clauses" call? *)
   1.334 -    val helper_clauses =
   1.335 -      get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
   1.336 -    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   1.337 -    val class_rel_clauses = make_class_rel_clauses thy subs supers'
   1.338 -  in
   1.339 -    (Vector.fromList clnames,
   1.340 -      (conjectures, axiom_clauses, extra_clauses, helper_clauses,
   1.341 -       class_rel_clauses, arity_clauses))
   1.342 -  end
   1.343 -
   1.344 -val axiom_prefix = "ax_"
   1.345 -val conjecture_prefix = "conj_"
   1.346 -val arity_clause_prefix = "clsarity_"
   1.347 -val tfrees_name = "tfrees"
   1.348 -
   1.349 -fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
   1.350 -
   1.351 -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   1.352 -  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   1.353 -  | fo_term_for_combtyp (CombType (name, tys)) =
   1.354 -    ATerm (name, map fo_term_for_combtyp tys)
   1.355 -
   1.356 -fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   1.357 -    (true, ATerm (class, [ATerm (name, [])]))
   1.358 -  | fo_literal_for_type_literal (TyLitFree (class, name)) =
   1.359 -    (true, ATerm (class, [ATerm (name, [])]))
   1.360 -
   1.361 -fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
   1.362 -
   1.363 -fun fo_term_for_combterm full_types =
   1.364 -  let
   1.365 -    fun aux top_level u =
   1.366 -      let
   1.367 -        val (head, args) = strip_combterm_comb u
   1.368 -        val (x, ty_args) =
   1.369 -          case head of
   1.370 -            CombConst (name, _, ty_args) =>
   1.371 -            if fst name = "equal" then
   1.372 -              (if top_level andalso length args = 2 then name
   1.373 -               else ("c_fequal", @{const_name fequal}), [])
   1.374 -            else
   1.375 -              (name, if full_types then [] else ty_args)
   1.376 -          | CombVar (name, _) => (name, [])
   1.377 -          | CombApp _ => raise Fail "impossible \"CombApp\""
   1.378 -        val t = ATerm (x, map fo_term_for_combtyp ty_args @
   1.379 -                          map (aux false) args)
   1.380 -    in
   1.381 -      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
   1.382 -    end
   1.383 -  in aux true end
   1.384 -
   1.385 -fun formula_for_combformula full_types =
   1.386 -  let
   1.387 -    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   1.388 -      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   1.389 -      | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
   1.390 -  in aux end
   1.391 -
   1.392 -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
   1.393 -  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   1.394 -                (type_literals_for_types ctypes_sorts))
   1.395 -           (formula_for_combformula full_types combformula)
   1.396 -
   1.397 -fun problem_line_for_axiom full_types
   1.398 -        (formula as FOLFormula {formula_name, kind, ...}) =
   1.399 -  Fof (axiom_prefix ^ ascii_of formula_name, kind,
   1.400 -       formula_for_axiom full_types formula)
   1.401 -
   1.402 -fun problem_line_for_class_rel_clause
   1.403 -        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
   1.404 -  let val ty_arg = ATerm (("T", "T"), []) in
   1.405 -    Fof (ascii_of axiom_name, Axiom,
   1.406 -         AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
   1.407 -                           APred (ATerm (superclass, [ty_arg]))]))
   1.408 -  end
   1.409 -
   1.410 -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   1.411 -    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   1.412 -  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   1.413 -    (false, ATerm (c, [ATerm (sort, [])]))
   1.414 -
   1.415 -fun problem_line_for_arity_clause
   1.416 -        (ArityClause {axiom_name, conclLit, premLits, ...}) =
   1.417 -  Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
   1.418 -       mk_ahorn (map (formula_for_fo_literal o apfst not
   1.419 -                      o fo_literal_for_arity_literal) premLits)
   1.420 -                (formula_for_fo_literal
   1.421 -                     (fo_literal_for_arity_literal conclLit)))
   1.422 -
   1.423 -fun problem_line_for_conjecture full_types
   1.424 -        (FOLFormula {formula_name, kind, combformula, ...}) =
   1.425 -  Fof (conjecture_prefix ^ formula_name, kind,
   1.426 -       formula_for_combformula full_types combformula)
   1.427 +structure Data = Theory_Data
   1.428 +(
   1.429 +  type T = (prover_config * stamp) Symtab.table
   1.430 +  val empty = Symtab.empty
   1.431 +  val extend = I
   1.432 +  fun merge data : T = Symtab.merge (eq_snd op =) data
   1.433 +    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   1.434 +)
   1.435  
   1.436 -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
   1.437 -  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   1.438 -
   1.439 -fun problem_line_for_free_type lit =
   1.440 -  Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
   1.441 -fun problem_lines_for_free_types conjectures =
   1.442 -  let
   1.443 -    val litss = map free_type_literals_for_conjecture conjectures
   1.444 -    val lits = fold (union (op =)) litss []
   1.445 -  in map problem_line_for_free_type lits end
   1.446 -
   1.447 -(** "hBOOL" and "hAPP" **)
   1.448 -
   1.449 -type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   1.450 -
   1.451 -fun consider_term top_level (ATerm ((s, _), ts)) =
   1.452 -  (if is_tptp_variable s then
   1.453 -     I
   1.454 -   else
   1.455 -     let val n = length ts in
   1.456 -       Symtab.map_default
   1.457 -           (s, {min_arity = n, max_arity = 0, sub_level = false})
   1.458 -           (fn {min_arity, max_arity, sub_level} =>
   1.459 -               {min_arity = Int.min (n, min_arity),
   1.460 -                max_arity = Int.max (n, max_arity),
   1.461 -                sub_level = sub_level orelse not top_level})
   1.462 -     end)
   1.463 -  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
   1.464 -fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   1.465 -  | consider_formula (AConn (_, phis)) = fold consider_formula phis
   1.466 -  | consider_formula (APred tm) = consider_term true tm
   1.467 -
   1.468 -fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
   1.469 -fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   1.470 -
   1.471 -fun const_table_for_problem explicit_apply problem =
   1.472 -  if explicit_apply then NONE
   1.473 -  else SOME (Symtab.empty |> consider_problem problem)
   1.474 -
   1.475 -val tc_fun = make_fixed_type_const @{type_name fun}
   1.476 -
   1.477 -fun min_arity_of thy full_types NONE s =
   1.478 -    (if s = "equal" orelse s = type_wrapper_name orelse
   1.479 -        String.isPrefix type_const_prefix s orelse
   1.480 -        String.isPrefix class_prefix s then
   1.481 -       16383 (* large number *)
   1.482 -     else if full_types then
   1.483 -       0
   1.484 -     else case strip_prefix_and_undo_ascii const_prefix s of
   1.485 -       SOME s' => num_type_args thy (invert_const s')
   1.486 -     | NONE => 0)
   1.487 -  | min_arity_of _ _ (SOME the_const_tab) s =
   1.488 -    case Symtab.lookup the_const_tab s of
   1.489 -      SOME ({min_arity, ...} : const_info) => min_arity
   1.490 -    | NONE => 0
   1.491 -
   1.492 -fun full_type_of (ATerm ((s, _), [ty, _])) =
   1.493 -    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
   1.494 -  | full_type_of _ = raise Fail "expected type wrapper"
   1.495 -
   1.496 -fun list_hAPP_rev _ t1 [] = t1
   1.497 -  | list_hAPP_rev NONE t1 (t2 :: ts2) =
   1.498 -    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   1.499 -  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   1.500 -    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   1.501 -                         [full_type_of t2, ty]) in
   1.502 -      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   1.503 -    end
   1.504 -
   1.505 -fun repair_applications_in_term thy full_types const_tab =
   1.506 -  let
   1.507 -    fun aux opt_ty (ATerm (name as (s, _), ts)) =
   1.508 -      if s = type_wrapper_name then
   1.509 -        case ts of
   1.510 -          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   1.511 -        | _ => raise Fail "malformed type wrapper"
   1.512 -      else
   1.513 -        let
   1.514 -          val ts = map (aux NONE) ts
   1.515 -          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
   1.516 -        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   1.517 -  in aux NONE end
   1.518 -
   1.519 -fun boolify t = ATerm (`I "hBOOL", [t])
   1.520 +fun add_prover (name, config) thy =
   1.521 +  Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   1.522 +  handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   1.523  
   1.524 -(* True if the constant ever appears outside of the top-level position in
   1.525 -   literals, or if it appears with different arities (e.g., because of different
   1.526 -   type instantiations). If false, the constant always receives all of its
   1.527 -   arguments and is used as a predicate. *)
   1.528 -fun is_predicate NONE s =
   1.529 -    s = "equal" orelse String.isPrefix type_const_prefix s orelse
   1.530 -    String.isPrefix class_prefix s
   1.531 -  | is_predicate (SOME the_const_tab) s =
   1.532 -    case Symtab.lookup the_const_tab s of
   1.533 -      SOME {min_arity, max_arity, sub_level} =>
   1.534 -      not sub_level andalso min_arity = max_arity
   1.535 -    | NONE => false
   1.536 -
   1.537 -fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
   1.538 -  if s = type_wrapper_name then
   1.539 -    case ts of
   1.540 -      [_, t' as ATerm ((s', _), _)] =>
   1.541 -      if is_predicate const_tab s' then t' else boolify t
   1.542 -    | _ => raise Fail "malformed type wrapper"
   1.543 -  else
   1.544 -    t |> not (is_predicate const_tab s) ? boolify
   1.545 -
   1.546 -fun close_universally phi =
   1.547 -  let
   1.548 -    fun term_vars bounds (ATerm (name as (s, _), tms)) =
   1.549 -        (is_tptp_variable s andalso not (member (op =) bounds name))
   1.550 -          ? insert (op =) name
   1.551 -        #> fold (term_vars bounds) tms
   1.552 -    fun formula_vars bounds (AQuant (q, xs, phi)) =
   1.553 -        formula_vars (xs @ bounds) phi
   1.554 -      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   1.555 -      | formula_vars bounds (APred tm) = term_vars bounds tm
   1.556 -  in
   1.557 -    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   1.558 -  end
   1.559 -
   1.560 -fun repair_formula thy explicit_forall full_types const_tab =
   1.561 -  let
   1.562 -    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   1.563 -      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   1.564 -      | aux (APred tm) =
   1.565 -        APred (tm |> repair_applications_in_term thy full_types const_tab
   1.566 -                  |> repair_predicates_in_term const_tab)
   1.567 -  in aux #> explicit_forall ? close_universally end
   1.568 -
   1.569 -fun repair_problem_line thy explicit_forall full_types const_tab
   1.570 -                        (Fof (ident, kind, phi)) =
   1.571 -  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
   1.572 -fun repair_problem_with_const_table thy =
   1.573 -  map o apsnd o map ooo repair_problem_line thy
   1.574 -
   1.575 -fun repair_problem thy explicit_forall full_types explicit_apply problem =
   1.576 -  repair_problem_with_const_table thy explicit_forall full_types
   1.577 -      (const_table_for_problem explicit_apply problem) problem
   1.578 -
   1.579 -fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
   1.580 -                    file (conjectures, axiom_clauses, extra_clauses,
   1.581 -                          helper_clauses, class_rel_clauses, arity_clauses) =
   1.582 -  let
   1.583 -    val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
   1.584 -    val class_rel_lines =
   1.585 -      map problem_line_for_class_rel_clause class_rel_clauses
   1.586 -    val arity_lines = map problem_line_for_arity_clause arity_clauses
   1.587 -    val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
   1.588 -    val conjecture_lines =
   1.589 -      map (problem_line_for_conjecture full_types) conjectures
   1.590 -    val tfree_lines = problem_lines_for_free_types conjectures
   1.591 -    (* Reordering these might or might not confuse the proof reconstruction
   1.592 -       code or the SPASS Flotter hack. *)
   1.593 -    val problem =
   1.594 -      [("Relevant facts", axiom_lines),
   1.595 -       ("Class relationships", class_rel_lines),
   1.596 -       ("Arity declarations", arity_lines),
   1.597 -       ("Helper facts", helper_lines),
   1.598 -       ("Conjectures", conjecture_lines),
   1.599 -       ("Type variables", tfree_lines)]
   1.600 -      |> repair_problem thy explicit_forall full_types explicit_apply
   1.601 -    val (problem, pool) = nice_tptp_problem readable_names problem
   1.602 -    val conjecture_offset =
   1.603 -      length axiom_lines + length class_rel_lines + length arity_lines
   1.604 -      + length helper_lines
   1.605 -    val _ = File.write_list file (strings_for_tptp_problem problem)
   1.606 -  in
   1.607 -    (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   1.608 -     conjecture_offset)
   1.609 -  end
   1.610 -
   1.611 -fun extract_clause_sequence output =
   1.612 -  let
   1.613 -    val tokens_of = String.tokens (not o Char.isAlphaNum)
   1.614 -    fun extract_num ("clause" :: (ss as _ :: _)) =
   1.615 -    Int.fromString (List.last ss)
   1.616 -      | extract_num _ = NONE
   1.617 -  in output |> split_lines |> map_filter (extract_num o tokens_of) end
   1.618 +fun get_prover thy name =
   1.619 +  the (Symtab.lookup (Data.get thy) name) |> fst
   1.620 +  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
   1.621  
   1.622 -val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
   1.623 -
   1.624 -val parse_clause_formula_pair =
   1.625 -  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
   1.626 -  --| Scan.option ($$ ",")
   1.627 -val parse_clause_formula_relation =
   1.628 -  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
   1.629 -  |-- Scan.repeat parse_clause_formula_pair
   1.630 -val extract_clause_formula_relation =
   1.631 -  Substring.full
   1.632 -  #> Substring.position set_ClauseFormulaRelationN
   1.633 -  #> snd #> Substring.string #> strip_spaces #> explode
   1.634 -  #> parse_clause_formula_relation #> fst
   1.635 -
   1.636 -fun repair_conjecture_shape_and_theorem_names output conjecture_shape
   1.637 -                                              thm_names =
   1.638 -  if String.isSubstring set_ClauseFormulaRelationN output then
   1.639 -    (* This is a hack required for keeping track of axioms after they have been
   1.640 -       clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
   1.641 -       of this hack. *)
   1.642 -    let
   1.643 -      val j0 = hd conjecture_shape
   1.644 -      val seq = extract_clause_sequence output
   1.645 -      val name_map = extract_clause_formula_relation output
   1.646 -      fun renumber_conjecture j =
   1.647 -        AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
   1.648 -        |> the_single
   1.649 -        |> (fn s => find_index (curry (op =) s) seq + 1)
   1.650 -    in
   1.651 -      (conjecture_shape |> map renumber_conjecture,
   1.652 -       seq |> map (the o AList.lookup (op =) name_map)
   1.653 -           |> map (fn s => case try (unprefix axiom_prefix) s of
   1.654 -                             SOME s' => undo_ascii_of s'
   1.655 -                           | NONE => "")
   1.656 -           |> Vector.fromList)
   1.657 -    end
   1.658 -  else
   1.659 -    (conjecture_shape, thm_names)
   1.660 -
   1.661 -
   1.662 -(* generic TPTP-based provers *)
   1.663 -
   1.664 -fun generic_tptp_prover
   1.665 -        (name, {home_var, executable, arguments, proof_delims, known_failures,
   1.666 -                max_new_relevant_facts_per_iter, prefers_theory_relevant,
   1.667 -                explicit_forall})
   1.668 -        ({debug, overlord, full_types, explicit_apply, relevance_threshold,
   1.669 -          relevance_convergence, theory_relevant, defs_relevant, isar_proof,
   1.670 -          isar_shrink_factor, ...} : params)
   1.671 -        minimize_command timeout
   1.672 -        ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
   1.673 -         : problem) =
   1.674 -  let
   1.675 -    (* get clauses and prepare them for writing *)
   1.676 -    val (ctxt, (_, th)) = goal;
   1.677 -    val thy = ProofContext.theory_of ctxt
   1.678 -    (* ### FIXME: (1) preprocessing for "if" etc. *)
   1.679 -    val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
   1.680 -    val the_filtered_clauses =
   1.681 -      case filtered_clauses of
   1.682 -        SOME fcls => fcls
   1.683 -      | NONE => relevant_facts full_types relevance_threshold
   1.684 -                    relevance_convergence defs_relevant
   1.685 -                    max_new_relevant_facts_per_iter
   1.686 -                    (the_default prefers_theory_relevant theory_relevant)
   1.687 -                    relevance_override goal hyp_ts concl_t
   1.688 -    val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
   1.689 -    val (internal_thm_names, clauses) =
   1.690 -      prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
   1.691 -                      the_filtered_clauses
   1.692 -
   1.693 -    (* path to unique problem file *)
   1.694 -    val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   1.695 -                       else Config.get ctxt dest_dir;
   1.696 -    val the_problem_prefix = Config.get ctxt problem_prefix;
   1.697 -    fun prob_pathname nr =
   1.698 -      let
   1.699 -        val probfile =
   1.700 -          Path.basic ((if overlord then "prob_" ^ name
   1.701 -                       else the_problem_prefix ^ serial_string ())
   1.702 -                      ^ "_" ^ string_of_int nr)
   1.703 -      in
   1.704 -        if the_dest_dir = "" then File.tmp_path probfile
   1.705 -        else if File.exists (Path.explode the_dest_dir)
   1.706 -        then Path.append (Path.explode the_dest_dir) probfile
   1.707 -        else error ("No such directory: " ^ the_dest_dir ^ ".")
   1.708 -      end;
   1.709 +fun available_atps thy =
   1.710 +  priority ("Available ATPs: " ^
   1.711 +            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
   1.712  
   1.713 -    val home = getenv home_var
   1.714 -    val command = Path.explode (home ^ "/" ^ executable)
   1.715 -    (* write out problem file and call prover *)
   1.716 -    fun command_line complete probfile =
   1.717 -      let
   1.718 -        val core = File.shell_path command ^ " " ^ arguments complete timeout ^
   1.719 -                   " " ^ File.shell_path probfile
   1.720 -      in
   1.721 -        (if Config.get ctxt measure_runtime then
   1.722 -           "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
   1.723 -         else
   1.724 -           "exec " ^ core) ^ " 2>&1"
   1.725 -      end
   1.726 -    fun split_time s =
   1.727 -      let
   1.728 -        val split = String.tokens (fn c => str c = "\n");
   1.729 -        val (output, t) = s |> split |> split_last |> apfst cat_lines;
   1.730 -        fun as_num f = f >> (fst o read_int);
   1.731 -        val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   1.732 -        val digit = Scan.one Symbol.is_ascii_digit;
   1.733 -        val num3 = as_num (digit ::: digit ::: (digit >> single));
   1.734 -        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   1.735 -        val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
   1.736 -      in (output, as_time t) end;
   1.737 -    fun run_on probfile =
   1.738 -      if home = "" then
   1.739 -        error ("The environment variable " ^ quote home_var ^ " is not set.")
   1.740 -      else if File.exists command then
   1.741 -        let
   1.742 -          fun do_run complete =
   1.743 -            let
   1.744 -              val command = command_line complete probfile
   1.745 -              val ((output, msecs), res_code) =
   1.746 -                bash_output command
   1.747 -                |>> (if overlord then
   1.748 -                       prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   1.749 -                     else
   1.750 -                       I)
   1.751 -                |>> (if Config.get ctxt measure_runtime then split_time
   1.752 -                     else rpair 0)
   1.753 -              val (proof, outcome) =
   1.754 -                extract_proof_and_outcome complete res_code proof_delims
   1.755 -                                          known_failures output
   1.756 -            in (output, msecs, proof, outcome) end
   1.757 -          val readable_names = debug andalso overlord
   1.758 -          val (pool, conjecture_offset) =
   1.759 -            write_tptp_file thy readable_names explicit_forall full_types
   1.760 -                            explicit_apply probfile clauses
   1.761 -          val conjecture_shape =
   1.762 -            conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   1.763 -          val result =
   1.764 -            do_run false
   1.765 -            |> (fn (_, msecs0, _, SOME _) =>
   1.766 -                   do_run true
   1.767 -                   |> (fn (output, msecs, proof, outcome) =>
   1.768 -                          (output, msecs0 + msecs, proof, outcome))
   1.769 -                 | result => result)
   1.770 -        in ((pool, conjecture_shape), result) end
   1.771 -      else
   1.772 -        error ("Bad executable: " ^ Path.implode command ^ ".");
   1.773 -
   1.774 -    (* If the problem file has not been exported, remove it; otherwise, export
   1.775 -       the proof file too. *)
   1.776 -    fun cleanup probfile =
   1.777 -      if the_dest_dir = "" then try File.rm probfile else NONE
   1.778 -    fun export probfile (_, (output, _, _, _)) =
   1.779 -      if the_dest_dir = "" then
   1.780 -        ()
   1.781 -      else
   1.782 -        File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   1.783 -
   1.784 -    val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
   1.785 -      with_path cleanup export run_on (prob_pathname subgoal)
   1.786 -    val (conjecture_shape, internal_thm_names) =
   1.787 -      repair_conjecture_shape_and_theorem_names output conjecture_shape
   1.788 -                                                internal_thm_names
   1.789 -
   1.790 -    val (message, used_thm_names) =
   1.791 -      case outcome of
   1.792 -        NONE =>
   1.793 -        proof_text isar_proof
   1.794 -            (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   1.795 -            (full_types, minimize_command, proof, internal_thm_names, th,
   1.796 -             subgoal)
   1.797 -      | SOME failure => (string_for_failure failure ^ "\n", [])
   1.798 -  in
   1.799 -    {outcome = outcome, message = message, pool = pool,
   1.800 -     used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
   1.801 -     output = output, proof = proof, internal_thm_names = internal_thm_names,
   1.802 -     conjecture_shape = conjecture_shape,
   1.803 -     filtered_clauses = the_filtered_clauses}
   1.804 -  end
   1.805 -
   1.806 -fun tptp_prover name p = (name, generic_tptp_prover (name, p));
   1.807 +fun available_atps thy =
   1.808 +  priority ("Available ATPs: " ^
   1.809 +            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
   1.810  
   1.811  fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
   1.812  
   1.813 @@ -801,7 +102,7 @@
   1.814     max_new_relevant_facts_per_iter = 80 (* FIXME *),
   1.815     prefers_theory_relevant = false,
   1.816     explicit_forall = false}
   1.817 -val e = tptp_prover "e" e_config
   1.818 +val e = ("e", e_config)
   1.819  
   1.820  
   1.821  (* The "-VarWeight=3" option helps the higher-order problems, probably by
   1.822 @@ -826,7 +127,7 @@
   1.823     max_new_relevant_facts_per_iter = 26 (* FIXME *),
   1.824     prefers_theory_relevant = true,
   1.825     explicit_forall = true}
   1.826 -val spass = tptp_prover "spass" spass_config
   1.827 +val spass = ("spass", spass_config)
   1.828  
   1.829  (* Vampire *)
   1.830  
   1.831 @@ -848,11 +149,11 @@
   1.832     max_new_relevant_facts_per_iter = 40 (* FIXME *),
   1.833     prefers_theory_relevant = false,
   1.834     explicit_forall = false}
   1.835 -val vampire = tptp_prover "vampire" vampire_config
   1.836 +val vampire = ("vampire", vampire_config)
   1.837  
   1.838  (* Remote prover invocation via SystemOnTPTP *)
   1.839  
   1.840 -val systems = Synchronized.var "atp_systems" ([]: string list);
   1.841 +val systems = Synchronized.var "atp_systems" ([]: string list)
   1.842  
   1.843  fun get_systems () =
   1.844    case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
   1.845 @@ -893,27 +194,23 @@
   1.846     prefers_theory_relevant = prefers_theory_relevant,
   1.847     explicit_forall = explicit_forall}
   1.848  
   1.849 -fun remote_tptp_prover prover atp_prefix args config =
   1.850 -  tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config)
   1.851 +val remote_name = prefix "remote_"
   1.852  
   1.853 -val remote_e = remote_tptp_prover e "EP---" "" e_config
   1.854 -val remote_spass = remote_tptp_prover spass "SPASS---" "-x" spass_config
   1.855 -val remote_vampire = remote_tptp_prover vampire "Vampire---9" "" vampire_config
   1.856 +fun remote_prover prover atp_prefix args config =
   1.857 +  (remote_name (fst prover), remote_config atp_prefix args config)
   1.858 +
   1.859 +val remote_e = remote_prover e "EP---" "" e_config
   1.860 +val remote_spass = remote_prover spass "SPASS---" "-x" spass_config
   1.861 +val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config
   1.862  
   1.863  fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
   1.864 -  name |> getenv home_var = "" ? remotify
   1.865 +  name |> getenv home_var = "" ? remote_name
   1.866  
   1.867  fun default_atps_param_value () =
   1.868    space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
   1.869 -                     remotify (fst vampire)]
   1.870 +                     remote_name (fst vampire)]
   1.871  
   1.872  val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
   1.873 -val prover_setup = fold add_prover provers
   1.874 -
   1.875 -val setup =
   1.876 -  dest_dir_setup
   1.877 -  #> problem_prefix_setup
   1.878 -  #> measure_runtime_setup
   1.879 -  #> prover_setup
   1.880 +val setup = fold add_prover provers
   1.881  
   1.882  end;