src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Tue Sep 06 18:13:36 2011 +0200 (2011-09-06)
changeset 44754 265174356212
parent 44596 2621046c550a
child 44768 a7bc1bdb8bb4
permissions -rw-r--r--
added dummy polymorphic THF system
     1 (*  Title:      HOL/Tools/ATP/atp_systems.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Setup for supported ATPs.
     6 *)
     7 
     8 signature ATP_SYSTEMS =
     9 sig
    10   type tptp_format = ATP_Problem.tptp_format
    11   type formula_kind = ATP_Problem.formula_kind
    12   type failure = ATP_Proof.failure
    13 
    14   type atp_config =
    15     {exec : string * string,
    16      required_execs : (string * string) list,
    17      arguments :
    18        Proof.context -> bool -> string -> Time.time
    19        -> (unit -> (string * real) list) -> string,
    20      proof_delims : (string * string) list,
    21      known_failures : (failure * string) list,
    22      conj_sym_kind : formula_kind,
    23      prem_kind : formula_kind,
    24      best_slices :
    25        Proof.context
    26        -> (real * (bool * (int * tptp_format * string * string))) list}
    27 
    28   val force_sos : bool Config.T
    29   val e_smartN : string
    30   val e_autoN : string
    31   val e_fun_weightN : string
    32   val e_sym_offset_weightN : string
    33   val e_weight_method : string Config.T
    34   val e_default_fun_weight : real Config.T
    35   val e_fun_weight_base : real Config.T
    36   val e_fun_weight_span : real Config.T
    37   val e_default_sym_offs_weight : real Config.T
    38   val e_sym_offs_weight_base : real Config.T
    39   val e_sym_offs_weight_span : real Config.T
    40   val eN : string
    41   val e_sineN : string
    42   val e_tofofN : string
    43   val leo2N : string
    44   val pffN : string
    45   val phfN : string
    46   val satallaxN : string
    47   val snarkN : string
    48   val spassN : string
    49   val vampireN : string
    50   val waldmeisterN : string
    51   val z3_tptpN : string
    52   val remote_prefix : string
    53   val remote_atp :
    54     string -> string -> string list -> (string * string) list
    55     -> (failure * string) list -> formula_kind -> formula_kind
    56     -> (Proof.context -> int * tptp_format * string) -> string * atp_config
    57   val add_atp : string * atp_config -> theory -> theory
    58   val get_atp : theory -> string -> atp_config
    59   val supported_atps : theory -> string list
    60   val is_atp_installed : theory -> string -> bool
    61   val refresh_systems_on_tptp : unit -> unit
    62   val setup : theory -> theory
    63 end;
    64 
    65 structure ATP_Systems : ATP_SYSTEMS =
    66 struct
    67 
    68 open ATP_Problem
    69 open ATP_Proof
    70 
    71 (* ATP configuration *)
    72 
    73 type atp_config =
    74   {exec : string * string,
    75    required_execs : (string * string) list,
    76    arguments :
    77      Proof.context -> bool -> string -> Time.time
    78      -> (unit -> (string * real) list) -> string,
    79    proof_delims : (string * string) list,
    80    known_failures : (failure * string) list,
    81    conj_sym_kind : formula_kind,
    82    prem_kind : formula_kind,
    83    best_slices :
    84      Proof.context
    85      -> (real * (bool * (int * tptp_format * string * string))) list}
    86 
    87 (* "best_slices" must be found empirically, taking a wholistic approach since
    88    the ATPs are run in parallel. The "real" components give the faction of the
    89    time available given to the slice and should add up to 1.0. The "bool"
    90    component indicates whether the slice's strategy is complete; the "int", the
    91    preferred number of facts to pass; the first "string", the preferred type
    92    system (which should be sound or quasi-sound); the second "string", extra
    93    information to the prover (e.g., SOS or no SOS).
    94 
    95    The last slice should be the most "normal" one, because it will get all the
    96    time available if the other slices fail early and also because it is used if
    97    slicing is disabled (e.g., by the minimizer). *)
    98 
    99 val known_perl_failures =
   100   [(CantConnect, "HTTP error"),
   101    (NoPerl, "env: perl"),
   102    (NoLibwwwPerl, "Can't locate HTTP")]
   103 
   104 (* named ATPs *)
   105 
   106 val eN = "e"
   107 val e_sineN = "e_sine"
   108 val e_tofofN = "e_tofof"
   109 val leo2N = "leo2"
   110 val pffN = "pff"
   111 val phfN = "phf"
   112 val satallaxN = "satallax"
   113 val snarkN = "snark"
   114 val spassN = "spass"
   115 val vampireN = "vampire"
   116 val waldmeisterN = "waldmeister"
   117 val z3_tptpN = "z3_tptp"
   118 val remote_prefix = "remote_"
   119 
   120 structure Data = Theory_Data
   121 (
   122   type T = (atp_config * stamp) Symtab.table
   123   val empty = Symtab.empty
   124   val extend = I
   125   fun merge data : T = Symtab.merge (eq_snd op =) data
   126     handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   127 )
   128 
   129 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
   130 
   131 val sosN = "sos"
   132 val no_sosN = "no_sos"
   133 
   134 val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
   135 
   136 
   137 (* E *)
   138 
   139 fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
   140 
   141 val tstp_proof_delims =
   142   [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
   143    ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
   144 
   145 val e_smartN = "smart"
   146 val e_autoN = "auto"
   147 val e_fun_weightN = "fun_weight"
   148 val e_sym_offset_weightN = "sym_offset_weight"
   149 
   150 val e_weight_method =
   151   Attrib.setup_config_string @{binding atp_e_weight_method} (K e_smartN)
   152 (* FUDGE *)
   153 val e_default_fun_weight =
   154   Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
   155 val e_fun_weight_base =
   156   Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
   157 val e_fun_weight_span =
   158   Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
   159 val e_default_sym_offs_weight =
   160   Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
   161 val e_sym_offs_weight_base =
   162   Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
   163 val e_sym_offs_weight_span =
   164   Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
   165 
   166 fun e_weight_method_case method fw sow =
   167   if method = e_fun_weightN then fw
   168   else if method = e_sym_offset_weightN then sow
   169   else raise Fail ("unexpected " ^ quote method)
   170 
   171 fun scaled_e_weight ctxt method w =
   172   w * Config.get ctxt
   173           (e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
   174   + Config.get ctxt
   175         (e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
   176   |> Real.ceil |> signed_string_of_int
   177 
   178 fun e_weight_arguments ctxt method weights =
   179   if method = e_autoN then
   180     "-xAutoDev"
   181   else
   182     (* supplied by Stephan Schulz *)
   183     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
   184     \--destructive-er-aggressive --destructive-er --presat-simplify \
   185     \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
   186     \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
   187     \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
   188     "(SimulateSOS, " ^
   189     (e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
   190      |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
   191     ",20,1.5,1.5,1" ^
   192     (weights ()
   193      |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
   194      |> implode) ^
   195     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
   196     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
   197     \FIFOWeight(PreferProcessed))'"
   198 
   199 fun effective_e_weight_method ctxt =
   200   if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
   201 
   202 val e_config : atp_config =
   203   {exec = ("E_HOME", "eproof"),
   204    required_execs = [],
   205    arguments =
   206      fn ctxt => fn _ => fn method => fn timeout => fn weights =>
   207         "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
   208         " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
   209    proof_delims = tstp_proof_delims,
   210    known_failures =
   211      [(Unprovable, "SZS status: CounterSatisfiable"),
   212       (Unprovable, "SZS status CounterSatisfiable"),
   213       (ProofMissing, "SZS status Theorem"),
   214       (TimedOut, "Failure: Resource limit exceeded (time)"),
   215       (TimedOut, "time limit exceeded"),
   216       (OutOfResources, "# Cannot determine problem status"),
   217       (OutOfResources, "SZS status: ResourceOut"),
   218       (OutOfResources, "SZS status ResourceOut")],
   219    conj_sym_kind = Hypothesis,
   220    prem_kind = Conjecture,
   221    best_slices = fn ctxt =>
   222      let val method = effective_e_weight_method ctxt in
   223        (* FUDGE *)
   224        if method = e_smartN then
   225          [(0.333, (true, (500, FOF, "mono_tags?", e_fun_weightN))),
   226           (0.334, (true, (50, FOF, "mono_guards?", e_fun_weightN))),
   227           (0.333, (true, (1000, FOF, "mono_tags?", e_sym_offset_weightN)))]
   228        else
   229          [(1.0, (true, (500, FOF, "mono_tags?", method)))]
   230      end}
   231 
   232 val e = (eN, e_config)
   233 
   234 
   235 (* LEO-II *)
   236 
   237 val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
   238 
   239 val leo2_config : atp_config =
   240   {exec = ("LEO2_HOME", "leo"),
   241    required_execs = [],
   242    arguments =
   243      fn _ => fn _ => fn sos => fn timeout => fn _ =>
   244         "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
   245         |> sos = sosN ? prefix "--sos ",
   246    proof_delims = tstp_proof_delims,
   247    known_failures = [],
   248    conj_sym_kind = Axiom,
   249    prem_kind = Hypothesis,
   250    best_slices = fn ctxt =>
   251      (* FUDGE *)
   252      [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))),
   253       (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))]
   254      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   255          else I)}
   256 
   257 val leo2 = (leo2N, leo2_config)
   258 
   259 
   260 (* Satallax *)
   261 
   262 val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
   263 
   264 val satallax_config : atp_config =
   265   {exec = ("SATALLAX_HOME", "satallax"),
   266    required_execs = [],
   267    arguments =
   268      fn _ => fn _ => fn _ => fn timeout => fn _ =>
   269         "-t " ^ string_of_int (to_secs 1 timeout),
   270    proof_delims = tstp_proof_delims,
   271    known_failures = [(ProofMissing, "SZS status Theorem")],
   272    conj_sym_kind = Axiom,
   273    prem_kind = Hypothesis,
   274    best_slices =
   275      (* FUDGE *)
   276      K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]}
   277 
   278 val satallax = (satallaxN, satallax_config)
   279 
   280 
   281 (* SPASS *)
   282 
   283 (* The "-VarWeight=3" option helps the higher-order problems, probably by
   284    counteracting the presence of explicit application operators. *)
   285 val spass_config : atp_config =
   286   {exec = ("ISABELLE_ATP", "scripts/spass"),
   287    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
   288    arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
   289      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   290       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
   291      |> sos = sosN ? prefix "-SOS=1 ",
   292    proof_delims = [("Here is a proof", "Formulae used in the proof")],
   293    known_failures =
   294      known_perl_failures @
   295      [(GaveUp, "SPASS beiseite: Completion found"),
   296       (TimedOut, "SPASS beiseite: Ran out of time"),
   297       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
   298       (MalformedInput, "Undefined symbol"),
   299       (MalformedInput, "Free Variable"),
   300       (Unprovable, "No formulae and clauses found in input file"),
   301       (SpassTooOld, "tptp2dfg"),
   302       (InternalError, "Please report this error")],
   303    conj_sym_kind = Hypothesis,
   304    prem_kind = Conjecture,
   305    best_slices = fn ctxt =>
   306      (* FUDGE *)
   307      [(0.333, (false, (150, FOF, "mono_tags", sosN))),
   308       (0.333, (false, (300, FOF, "poly_tags?", sosN))),
   309       (0.334, (true, (50, FOF, "mono_tags?", no_sosN)))]
   310      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   311          else I)}
   312 
   313 val spass = (spassN, spass_config)
   314 
   315 
   316 (* Vampire *)
   317 
   318 (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on
   319    SystemOnTPTP. *)
   320 fun is_old_vampire_version () =
   321   string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
   322 
   323 val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
   324 
   325 val vampire_config : atp_config =
   326   {exec = ("VAMPIRE_HOME", "vampire"),
   327    required_execs = [],
   328    arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
   329      "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
   330      " --proof tptp --output_axiom_names on \
   331      \ --thanks \"Andrei and Krystof\" --input_file"
   332      |> sos = sosN ? prefix "--sos on ",
   333    proof_delims =
   334      [("=========== Refutation ==========",
   335        "======= End of refutation ======="),
   336       ("% SZS output start Refutation", "% SZS output end Refutation"),
   337       ("% SZS output start Proof", "% SZS output end Proof")],
   338    known_failures =
   339      [(GaveUp, "UNPROVABLE"),
   340       (GaveUp, "CANNOT PROVE"),
   341       (GaveUp, "SZS status GaveUp"),
   342       (TimedOut, "SZS status Timeout"),
   343       (Unprovable, "Satisfiability detected"),
   344       (Unprovable, "Termination reason: Satisfiable"),
   345       (VampireTooOld, "not a valid option"),
   346       (Interrupted, "Aborted by signal SIGINT")],
   347    conj_sym_kind = Conjecture,
   348    prem_kind = Conjecture,
   349    best_slices = fn ctxt =>
   350      (* FUDGE *)
   351      (if is_old_vampire_version () then
   352         [(0.333, (false, (150, FOF, "poly_guards", sosN))),
   353          (0.333, (false, (500, FOF, "mono_tags?", sosN))),
   354          (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
   355       else
   356         [(0.333, (false, (150, vampire_tff0, "poly_guards", sosN))),
   357          (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
   358          (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
   359      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   360          else I)}
   361 
   362 val vampire = (vampireN, vampire_config)
   363 
   364 
   365 (* Z3 with TPTP syntax *)
   366 
   367 val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
   368 
   369 val z3_tptp_config : atp_config =
   370   {exec = ("Z3_HOME", "z3"),
   371    required_execs = [],
   372    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
   373      "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
   374    proof_delims = [],
   375    known_failures =
   376      [(GaveUp, "SZS status Satisfiable"),
   377       (GaveUp, "SZS status CounterSatisfiable"),
   378       (GaveUp, "SZS status GaveUp"),
   379       (GaveUp, "SZS status Unknown"),
   380       (ProofMissing, "SZS status Unsatisfiable"),
   381       (ProofMissing, "SZS status Theorem")],
   382    conj_sym_kind = Hypothesis,
   383    prem_kind = Hypothesis,
   384    best_slices =
   385      (* FUDGE *)
   386      K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))),
   387         (0.25, (false, (125, z3_tff0, "mono_simple", ""))),
   388         (0.125, (false, (62, z3_tff0, "mono_simple", ""))),
   389         (0.125, (false, (31, z3_tff0, "mono_simple", "")))]}
   390 
   391 val z3_tptp = (z3_tptpN, z3_tptp_config)
   392 
   393 
   394 (* Not really a prover: Experimental Polymorphic TFF and THF output *)
   395 
   396 fun dummy_config format type_enc : atp_config =
   397   {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
   398    required_execs = [],
   399    arguments = K (K (K (K (K "")))),
   400    proof_delims = [],
   401    known_failures = [(GaveUp, "SZS status Unknown")],
   402    conj_sym_kind = Hypothesis,
   403    prem_kind = Hypothesis,
   404    best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
   405 
   406 val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
   407 val pff_config = dummy_config pff_format "poly_simple"
   408 val pff = (pffN, pff_config)
   409 
   410 val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
   411 val phf_config = dummy_config phf_format "poly_simple_higher"
   412 val phf = (phfN, phf_config)
   413 
   414 
   415 (* Remote ATP invocation via SystemOnTPTP *)
   416 
   417 val systems = Synchronized.var "atp_systems" ([] : string list)
   418 
   419 fun get_systems () =
   420   case Isabelle_System.bash_output
   421            "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
   422     (output, 0) => split_lines output
   423   | (output, _) =>
   424     error (case extract_known_failure known_perl_failures output of
   425              SOME failure => string_for_failure failure
   426            | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
   427 
   428 fun find_system name [] systems =
   429     find_first (String.isPrefix (name ^ "---")) systems
   430   | find_system name (version :: versions) systems =
   431     case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
   432       NONE => find_system name versions systems
   433     | res => res
   434 
   435 fun get_system name versions =
   436   Synchronized.change_result systems
   437       (fn systems => (if null systems then get_systems () else systems)
   438                      |> `(`(find_system name versions)))
   439 
   440 fun the_system name versions =
   441   case get_system name versions of
   442     (SOME sys, _) => sys
   443   | (NONE, []) => error ("SystemOnTPTP is currently not available.")
   444   | (NONE, syss) =>
   445     error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
   446            "(Available systems: " ^ commas_quote syss ^ ".)")
   447 
   448 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   449 
   450 fun remote_config system_name system_versions proof_delims known_failures
   451                   conj_sym_kind prem_kind best_slice : atp_config =
   452   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
   453    required_execs = [],
   454    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
   455      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
   456      ^ " -s " ^ the_system system_name system_versions,
   457    proof_delims = union (op =) tstp_proof_delims proof_delims,
   458    known_failures = known_failures @ known_perl_failures @
   459      [(Unprovable, "says Satisfiable"),
   460       (Unprovable, "says CounterSatisfiable"),
   461       (GaveUp, "says Unknown"),
   462       (GaveUp, "says GaveUp"),
   463       (ProofMissing, "says Theorem"),
   464       (ProofMissing, "says Unsatisfiable"),
   465       (TimedOut, "says Timeout"),
   466       (Inappropriate, "says Inappropriate")],
   467    conj_sym_kind = conj_sym_kind,
   468    prem_kind = prem_kind,
   469    best_slices = fn ctxt =>
   470      let val (max_relevant, format, type_enc) = best_slice ctxt in
   471        [(1.0, (false, (max_relevant, format, type_enc, "")))]
   472      end}
   473 
   474 fun remotify_config system_name system_versions best_slice
   475         ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
   476          : atp_config) : atp_config =
   477   remote_config system_name system_versions proof_delims known_failures
   478                 conj_sym_kind prem_kind best_slice
   479 
   480 fun remote_atp name system_name system_versions proof_delims known_failures
   481                conj_sym_kind prem_kind best_slice =
   482   (remote_prefix ^ name,
   483    remote_config system_name system_versions proof_delims known_failures
   484                  conj_sym_kind prem_kind best_slice)
   485 fun remotify_atp (name, config) system_name system_versions best_slice =
   486   (remote_prefix ^ name,
   487    remotify_config system_name system_versions best_slice config)
   488 
   489 val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
   490 
   491 val remote_e =
   492   remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   493                (K (750, FOF, "mono_tags?") (* FUDGE *))
   494 val remote_leo2 =
   495   remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
   496                (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
   497 val remote_satallax =
   498   remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
   499                (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
   500 val remote_vampire =
   501   remotify_atp vampire "Vampire" ["1.8"]
   502                (K (250, FOF, "mono_guards?") (* FUDGE *))
   503 val remote_z3_tptp =
   504   remotify_atp z3_tptp "Z3" ["3.0"]
   505                (K (250, z3_tff0, "mono_simple") (* FUDGE *))
   506 val remote_e_sine =
   507   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
   508              Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
   509 val remote_snark =
   510   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
   511              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
   512              (K (100, explicit_tff0, "mono_simple") (* FUDGE *))
   513 val remote_e_tofof =
   514   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
   515              Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *))
   516 val remote_waldmeister =
   517   remote_atp waldmeisterN "Waldmeister" ["710"]
   518              [("#START OF PROOF", "Proved Goals:")]
   519              [(OutOfResources, "Too many function symbols"),
   520               (Crashed, "Unrecoverable Segmentation Fault")]
   521              Hypothesis Hypothesis
   522              (K (50, CNF_UEQ, "mono_tags?") (* FUDGE *))
   523 
   524 (* Setup *)
   525 
   526 fun add_atp (name, config) thy =
   527   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   528   handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   529 
   530 fun get_atp thy name =
   531   the (Symtab.lookup (Data.get thy) name) |> fst
   532   handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
   533 
   534 val supported_atps = Symtab.keys o Data.get
   535 
   536 fun is_atp_installed thy name =
   537   let val {exec, required_execs, ...} = get_atp thy name in
   538     forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
   539   end
   540 
   541 fun refresh_systems_on_tptp () =
   542   Synchronized.change systems (fn _ => get_systems ())
   543 
   544 val atps =
   545   [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
   546    remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
   547    remote_e_tofof, remote_waldmeister]
   548 val setup = fold add_atp atps
   549 
   550 end;