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