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