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