src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Fri Jul 25 11:26:19 2014 +0200 (2014-07-25)
changeset 57672 6be755147695
parent 57671 dc5e1b1db9ba
child 57707 0242e9578828
permissions -rw-r--r--
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 term_order = ATP_Problem.term_order
    11   type atp_format = ATP_Problem.atp_format
    12   type atp_formula_role = ATP_Problem.atp_formula_role
    13   type atp_failure = ATP_Proof.atp_failure
    14 
    15   type slice_spec = (int * string) * atp_format * string * string * bool
    16   type atp_config =
    17     {exec : bool -> string list * string list,
    18      arguments : Proof.context -> bool -> string -> Time.time -> string ->
    19        term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
    20      proof_delims : (string * string) list,
    21      known_failures : (atp_failure * string) list,
    22      prem_role : atp_formula_role,
    23      best_slices : Proof.context -> (real * (slice_spec * string)) list,
    24      best_max_mono_iters : int,
    25      best_max_new_mono_instances : int}
    26 
    27   val default_max_mono_iters : int
    28   val default_max_new_mono_instances : int
    29   val force_sos : bool Config.T
    30   val term_order : string Config.T
    31   val e_smartN : string
    32   val e_autoN : string
    33   val e_fun_weightN : string
    34   val e_sym_offset_weightN : string
    35   val e_selection_heuristic : string Config.T
    36   val e_default_fun_weight : real Config.T
    37   val e_fun_weight_base : real Config.T
    38   val e_fun_weight_span : real Config.T
    39   val e_default_sym_offs_weight : real Config.T
    40   val e_sym_offs_weight_base : real Config.T
    41   val e_sym_offs_weight_span : real Config.T
    42   val spass_H1SOS : string
    43   val spass_H2 : string
    44   val spass_H2LR0LT0 : string
    45   val spass_H2NuVS0 : string
    46   val spass_H2NuVS0Red2 : string
    47   val spass_H2SOS : string
    48   val spass_extra_options : string Config.T
    49   val remote_atp : string -> string -> string list -> (string * string) list ->
    50     (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) ->
    51     string * (unit -> atp_config)
    52   val add_atp : string * (unit -> atp_config) -> theory -> theory
    53   val get_atp : theory -> string -> (unit -> atp_config)
    54   val supported_atps : theory -> string list
    55   val is_atp_installed : theory -> string -> bool
    56   val refresh_systems_on_tptp : unit -> unit
    57   val effective_term_order : Proof.context -> string -> term_order
    58 end;
    59 
    60 structure ATP_Systems : ATP_SYSTEMS =
    61 struct
    62 
    63 open ATP_Problem
    64 open ATP_Proof
    65 open ATP_Problem_Generate
    66 
    67 
    68 (* ATP configuration *)
    69 
    70 val default_max_mono_iters = 3 (* FUDGE *)
    71 val default_max_new_mono_instances = 100 (* FUDGE *)
    72 
    73 type slice_spec = (int * string) * atp_format * string * string * bool
    74 
    75 type atp_config =
    76   {exec : bool -> string list * string list,
    77    arguments : Proof.context -> bool -> string -> Time.time -> string ->
    78      term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
    79    proof_delims : (string * string) list,
    80    known_failures : (atp_failure * string) list,
    81    prem_role : atp_formula_role,
    82    best_slices : Proof.context -> (real * (slice_spec * string)) list,
    83    best_max_mono_iters : int,
    84    best_max_new_mono_instances : int}
    85 
    86 (* "best_slices" must be found empirically, taking a wholistic approach since
    87    the ATPs are run in parallel. Each slice has the format
    88 
    89      (time_frac, ((max_facts, fact_filter), format, type_enc,
    90                   lam_trans, uncurried_aliases), extra)
    91 
    92    where
    93 
    94      time_frac = faction of the time available given to the slice (which should
    95        add up to 1.0)
    96 
    97      extra = extra information to the prover (e.g., SOS or no SOS).
    98 
    99    The last slice should be the most "normal" one, because it will get all the
   100    time available if the other slices fail early and also because it is used if
   101    slicing is disabled (e.g., by the minimizer). *)
   102 
   103 val mepoN = "mepo"
   104 val mashN = "mash"
   105 val meshN = "mesh"
   106 
   107 val tstp_proof_delims =
   108   [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation"),
   109    ("% SZS output start Refutation", "% SZS output end Refutation"),
   110    ("% SZS output start Proof", "% SZS output end Proof")]
   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 structure Data = Theory_Data
   136 (
   137   type T = ((unit -> atp_config) * stamp) Symtab.table
   138   val empty = Symtab.empty
   139   val extend = I
   140   fun merge data : T =
   141     Symtab.merge (eq_snd (op =)) data
   142     handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   143 )
   144 
   145 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
   146 
   147 val sosN = "sos"
   148 val no_sosN = "no_sos"
   149 
   150 val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
   151 
   152 val smartN = "smart"
   153 (* val kboN = "kbo" *)
   154 val lpoN = "lpo"
   155 val xweightsN = "_weights"
   156 val xprecN = "_prec"
   157 val xsimpN = "_simp" (* SPASS-specific *)
   158 
   159 (* Possible values for "atp_term_order":
   160    "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *)
   161 val term_order =
   162   Attrib.setup_config_string @{binding atp_term_order} (K smartN)
   163 
   164 
   165 (* agsyHOL *)
   166 
   167 val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice)
   168 
   169 val agsyhol_config : atp_config =
   170   {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
   171    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   172        "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^
   173        file_name,
   174    proof_delims = tstp_proof_delims,
   175    known_failures = known_szs_status_failures,
   176    prem_role = Hypothesis,
   177    best_slices =
   178      (* FUDGE *)
   179      K [(1.0, (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), ""))],
   180    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
   181    best_max_new_mono_instances = default_max_new_mono_instances}
   182 
   183 val agsyhol = (agsyholN, fn () => agsyhol_config)
   184 
   185 
   186 (* Alt-Ergo *)
   187 
   188 val alt_ergo_config : atp_config =
   189   {exec = K (["WHY3_HOME"], ["why3"]),
   190    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   191        "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^
   192        string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   193    proof_delims = [],
   194    known_failures =
   195      [(ProofMissing, ": Valid"),
   196       (TimedOut, ": Timeout"),
   197       (GaveUp, ": Unknown")],
   198    prem_role = Hypothesis,
   199    best_slices = fn _ =>
   200      (* FUDGE *)
   201      [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))],
   202    best_max_mono_iters = default_max_mono_iters,
   203    best_max_new_mono_instances = default_max_new_mono_instances}
   204 
   205 val alt_ergo = (alt_ergoN, fn () => alt_ergo_config)
   206 
   207 
   208 (* E *)
   209 
   210 fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
   211 
   212 val e_smartN = "smart"
   213 val e_autoN = "auto"
   214 val e_fun_weightN = "fun_weight"
   215 val e_sym_offset_weightN = "sym_offset_weight"
   216 
   217 val e_selection_heuristic =
   218   Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
   219 (* FUDGE *)
   220 val e_default_fun_weight =
   221   Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
   222 val e_fun_weight_base =
   223   Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
   224 val e_fun_weight_span =
   225   Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
   226 val e_default_sym_offs_weight =
   227   Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
   228 val e_sym_offs_weight_base =
   229   Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
   230 val e_sym_offs_weight_span =
   231   Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
   232 
   233 fun e_selection_heuristic_case heuristic fw sow =
   234   if heuristic = e_fun_weightN then fw
   235   else if heuristic = e_sym_offset_weightN then sow
   236   else raise Fail ("unexpected " ^ quote heuristic)
   237 
   238 fun scaled_e_selection_weight ctxt heuristic w =
   239   w * Config.get ctxt (e_selection_heuristic_case heuristic
   240                            e_fun_weight_span e_sym_offs_weight_span)
   241   + Config.get ctxt (e_selection_heuristic_case heuristic
   242                          e_fun_weight_base e_sym_offs_weight_base)
   243   |> Real.ceil |> signed_string_of_int
   244 
   245 fun e_selection_weight_arguments ctxt heuristic sel_weights =
   246   if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then
   247     (* supplied by Stephan Schulz *)
   248     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
   249     \--destructive-er-aggressive --destructive-er --presat-simplify \
   250     \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
   251     \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
   252     e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
   253     "(SimulateSOS," ^
   254     (e_selection_heuristic_case heuristic
   255          e_default_fun_weight e_default_sym_offs_weight
   256      |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
   257     ",20,1.5,1.5,1" ^
   258     (sel_weights ()
   259      |> map (fn (s, w) => "," ^ s ^ ":" ^
   260                           scaled_e_selection_weight ctxt heuristic w)
   261      |> implode) ^
   262     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
   263     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
   264     \FIFOWeight(PreferProcessed))' "
   265   else
   266     "-xAuto "
   267 
   268 val e_ord_weights =
   269   map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
   270 fun e_ord_precedence [_] = ""
   271   | e_ord_precedence info = info |> map fst |> space_implode "<"
   272 
   273 fun e_term_order_info_arguments false false _ = ""
   274   | e_term_order_info_arguments gen_weights gen_prec ord_info =
   275     let val ord_info = ord_info () in
   276       (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^
   277       (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
   278     end
   279 
   280 val e_config : atp_config =
   281   {exec = fn full_proofs => (["E_HOME"],
   282      if full_proofs orelse not (is_e_at_least_1_8 ()) then ["eproof_ram", "eproof"]
   283      else ["eprover"]),
   284    arguments = fn ctxt => fn full_proofs => fn heuristic => fn timeout => fn file_name =>
   285      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
   286        (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
   287        "--tstp-in --tstp-out --silent " ^
   288        e_selection_weight_arguments ctxt heuristic sel_weights ^
   289        e_term_order_info_arguments gen_weights gen_prec ord_info ^
   290        "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
   291        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
   292        (if full_proofs orelse not (is_e_at_least_1_8 ()) then
   293           " --output-level=5 --pcl-shell-level=" ^ (if full_proofs then "0" else "2")
   294         else
   295           " --proof-object=1") ^
   296        " " ^ file_name,
   297    proof_delims =
   298      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
   299      tstp_proof_delims,
   300    known_failures =
   301      [(TimedOut, "Failure: Resource limit exceeded (time)"),
   302       (TimedOut, "time limit exceeded")] @
   303      known_szs_status_failures,
   304    prem_role = Conjecture,
   305    best_slices = fn ctxt =>
   306      let val heuristic = Config.get ctxt e_selection_heuristic in
   307        (* FUDGE *)
   308        if heuristic = e_smartN then
   309          [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
   310           (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)),
   311           (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)),
   312           (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)),
   313           (0.15, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN)),
   314           (0.25, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN))]
   315        else
   316          [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))]
   317      end,
   318    best_max_mono_iters = default_max_mono_iters,
   319    best_max_new_mono_instances = default_max_new_mono_instances}
   320 
   321 val e = (eN, fn () => e_config)
   322 
   323 
   324 (* E-MaLeS *)
   325 
   326 val e_males_config : atp_config =
   327   {exec = K (["E_MALES_HOME"], ["emales.py"]),
   328    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   329        "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name,
   330    proof_delims = tstp_proof_delims,
   331    known_failures = #known_failures e_config,
   332    prem_role = Conjecture,
   333    best_slices =
   334      (* FUDGE *)
   335      K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")),
   336         (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")),
   337         (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")),
   338         (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))],
   339    best_max_mono_iters = default_max_mono_iters,
   340    best_max_new_mono_instances = default_max_new_mono_instances}
   341 
   342 val e_males = (e_malesN, fn () => e_males_config)
   343 
   344 
   345 (* E-Par *)
   346 
   347 val e_par_config : atp_config =
   348   {exec = K (["E_HOME"], ["runepar.pl"]),
   349    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   350        string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^
   351        " 2" (* proofs *),
   352    proof_delims = tstp_proof_delims,
   353    known_failures = #known_failures e_config,
   354    prem_role = Conjecture,
   355    best_slices = #best_slices e_males_config,
   356    best_max_mono_iters = default_max_mono_iters,
   357    best_max_new_mono_instances = default_max_new_mono_instances}
   358 
   359 val e_par = (e_parN, fn () => e_par_config)
   360 
   361 
   362 (* iProver *)
   363 
   364 val iprover_config : atp_config =
   365   {exec = K (["IPROVER_HOME"], ["iprover"]),
   366    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   367        "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^
   368        string_of_real (Time.toReal timeout) ^ " " ^ file_name,
   369    proof_delims = tstp_proof_delims,
   370    known_failures =
   371      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
   372      known_szs_status_failures,
   373    prem_role = Hypothesis,
   374    best_slices =
   375      (* FUDGE *)
   376      K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))],
   377    best_max_mono_iters = default_max_mono_iters,
   378    best_max_new_mono_instances = default_max_new_mono_instances}
   379 
   380 val iprover = (iproverN, fn () => iprover_config)
   381 
   382 
   383 (* iProver-Eq *)
   384 
   385 val iprover_eq_config : atp_config =
   386   {exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]),
   387    arguments = #arguments iprover_config,
   388    proof_delims = #proof_delims iprover_config,
   389    known_failures = #known_failures iprover_config,
   390    prem_role = #prem_role iprover_config,
   391    best_slices = #best_slices iprover_config,
   392    best_max_mono_iters = #best_max_mono_iters iprover_config,
   393    best_max_new_mono_instances = #best_max_new_mono_instances iprover_config}
   394 
   395 val iprover_eq = (iprover_eqN, fn () => iprover_eq_config)
   396 
   397 
   398 (* LEO-II *)
   399 
   400 (* LEO-II supports definitions, but it performs significantly better on our
   401    benchmarks when they are not used. *)
   402 val leo2_thf0 = THF (Monomorphic, THF_Without_Choice)
   403 
   404 val leo2_config : atp_config =
   405   {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
   406    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   407        "--foatp e --atp e=\"$E_HOME\"/eprover \
   408        \--atp epclextract=\"$E_HOME\"/epclextract \
   409        \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
   410        file_name,
   411    proof_delims = tstp_proof_delims,
   412    known_failures =
   413      [(TimedOut, "CPU time limit exceeded, terminating"),
   414       (GaveUp, "No.of.Axioms")] @
   415      known_szs_status_failures,
   416    prem_role = Hypothesis,
   417    best_slices =
   418      (* FUDGE *)
   419      K [(1.0, (((40, ""), leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
   420    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
   421    best_max_new_mono_instances = default_max_new_mono_instances}
   422 
   423 val leo2 = (leo2N, fn () => leo2_config)
   424 
   425 
   426 (* Satallax *)
   427 
   428 (* Choice is disabled until there is proper reconstruction for it. *)
   429 val satallax_thf0 = THF (Monomorphic, THF_Without_Choice)
   430 
   431 val satallax_config : atp_config =
   432   {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
   433    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   434        "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   435    proof_delims =
   436      [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
   437    known_failures = known_szs_status_failures,
   438    prem_role = Hypothesis,
   439    best_slices =
   440      (* FUDGE *)
   441      K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
   442    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
   443    best_max_new_mono_instances = default_max_new_mono_instances}
   444 
   445 val satallax = (satallaxN, fn () => satallax_config)
   446 
   447 
   448 (* SPASS *)
   449 
   450 val spass_H1SOS = "-Heuristic=1 -SOS"
   451 val spass_H2 = "-Heuristic=2"
   452 val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
   453 val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
   454 val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
   455 val spass_H2SOS = "-Heuristic=2 -SOS"
   456 
   457 val spass_extra_options =
   458   Attrib.setup_config_string @{binding atp_spass_extra_options} (K "")
   459 
   460 (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
   461 val spass_config : atp_config =
   462   {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
   463    arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
   464        fn file_name => fn _ =>
   465        "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
   466        "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
   467        |> extra_options <> "" ? prefix (extra_options ^ " "),
   468    proof_delims = [("Here is a proof", "Formulae used in the proof")],
   469    known_failures =
   470      [(GaveUp, "SPASS beiseite: Completion found"),
   471       (TimedOut, "SPASS beiseite: Ran out of time"),
   472       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
   473       (MalformedInput, "Undefined symbol"),
   474       (MalformedInput, "Free Variable"),
   475       (Unprovable, "No formulae and clauses found in input file"),
   476       (InternalError, "Please report this error")] @
   477       known_perl_failures,
   478    prem_role = Conjecture,
   479    best_slices = fn ctxt =>
   480      (* FUDGE *)
   481      [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")),
   482       (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
   483       (0.1666, (((50, meshN), DFG Monomorphic,  "mono_native", liftingN, true), spass_H2LR0LT0)),
   484       (0.1000, (((250, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)),
   485       (0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
   486       (0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
   487       (0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
   488       (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))]
   489      |> (case Config.get ctxt spass_extra_options of
   490            "" => I
   491          | opts => map (apsnd (apsnd (K opts)))),
   492    best_max_mono_iters = default_max_mono_iters,
   493    best_max_new_mono_instances = default_max_new_mono_instances}
   494 
   495 val spass = (spassN, fn () => spass_config)
   496 
   497 
   498 (* Vampire *)
   499 
   500 (* Vampire 1.8 has TFF0 support, but the support was buggy until revision
   501    1435 (or shortly before). *)
   502 fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
   503 fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
   504 
   505 val vampire_tff0 = TFF Monomorphic
   506 
   507 val vampire_config : atp_config =
   508   {exec = K (["VAMPIRE_HOME"], ["vampire"]),
   509    arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name =>
   510        fn _ =>
   511        "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
   512        " --proof tptp --output_axiom_names on" ^
   513        (if is_vampire_at_least_1_8 () then
   514           (* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
   515           (if full_proofs then
   516              " --forced_options splitting=off:equality_proxy=off:general_splitting=off\
   517              \:inequality_splitting=0:naming=0"
   518            else
   519              "")
   520         else
   521           "") ^
   522        " --thanks \"Andrei et al.\" --input_file " ^ file_name
   523        |> sos = sosN ? prefix "--sos on ",
   524    proof_delims =
   525      [("=========== Refutation ==========",
   526        "======= End of refutation =======")] @
   527      tstp_proof_delims,
   528    known_failures =
   529      [(GaveUp, "UNPROVABLE"),
   530       (GaveUp, "CANNOT PROVE"),
   531       (Unprovable, "Satisfiability detected"),
   532       (Unprovable, "Termination reason: Satisfiable"),
   533       (Interrupted, "Aborted by signal SIGINT")] @
   534      known_szs_status_failures,
   535    prem_role = Conjecture,
   536    best_slices = fn ctxt =>
   537      (* FUDGE *)
   538      (if is_vampire_beyond_1_8 () then
   539         [(0.333, (((500, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
   540          (0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
   541          (0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
   542       else
   543         [(0.333, (((150, meshN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
   544          (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)),
   545          (0.334, (((50, meshN), FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))])
   546      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   547          else I),
   548    best_max_mono_iters = default_max_mono_iters,
   549    best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
   550 
   551 val vampire = (vampireN, fn () => vampire_config)
   552 
   553 (* Z3 with TPTP syntax (half experimental, half legacy) *)
   554 
   555 val z3_tff0 = TFF Monomorphic
   556 
   557 val z3_tptp_config : atp_config =
   558   {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
   559    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   560      "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
   561    proof_delims = [("SZS status Theorem", "")],
   562    known_failures = known_szs_status_failures,
   563    prem_role = Hypothesis,
   564    best_slices =
   565      (* FUDGE *)
   566      K [(0.5, (((250, meshN), z3_tff0, "mono_native", combsN, false), "")),
   567         (0.25, (((125, mepoN), z3_tff0, "mono_native", combsN, false), "")),
   568         (0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")),
   569         (0.125, (((31, meshN), z3_tff0, "mono_native", combsN, false), ""))],
   570    best_max_mono_iters = default_max_mono_iters,
   571    best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
   572 
   573 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
   574 
   575 
   576 (* Zipperposition*)
   577 
   578 val zipperposition_config : atp_config =
   579   {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
   580    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   581        "-print none -proof tstp -print-types -timeout " ^
   582        string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   583    proof_delims = tstp_proof_delims,
   584    known_failures = known_szs_status_failures,
   585    prem_role = Hypothesis,
   586    best_slices = fn _ =>
   587      (* FUDGE *)
   588      [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))],
   589    best_max_mono_iters = default_max_mono_iters,
   590    best_max_new_mono_instances = default_max_new_mono_instances}
   591 
   592 val zipperposition = (zipperpositionN, fn () => zipperposition_config)
   593 
   594 
   595 (* Not really a prover: Experimental Polymorphic THF and DFG output *)
   596 
   597 fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
   598   {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
   599    arguments = K (K (K (K (K (K ""))))),
   600    proof_delims = [],
   601    known_failures = known_szs_status_failures,
   602    prem_role = prem_role,
   603    best_slices =
   604      K [(1.0, (((200, ""), format, type_enc,
   605                 if is_format_higher_order format then keep_lamsN
   606                 else combsN, uncurried_aliases), ""))],
   607    best_max_mono_iters = default_max_mono_iters,
   608    best_max_new_mono_instances = default_max_new_mono_instances}
   609 
   610 val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
   611 
   612 val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
   613 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
   614 
   615 val dummy_thf_ml_config = dummy_config Hypothesis dummy_thf_format "ml_poly_native_higher" false
   616 val dummy_thf_ml = (dummy_thf_mlN, fn () => dummy_thf_ml_config)
   617 
   618 val spass_pirate_format = DFG Polymorphic
   619 val remote_spass_pirate_config : atp_config =
   620   {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]),
   621    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   622      string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   623    proof_delims = [("Involved clauses:", "Involved clauses:")],
   624    known_failures = known_szs_status_failures,
   625    prem_role = #prem_role spass_config,
   626    best_slices = K [(1.0, (((200, ""), spass_pirate_format, "tc_native", combsN, true), ""))],
   627    best_max_mono_iters = default_max_mono_iters,
   628    best_max_new_mono_instances = default_max_new_mono_instances}
   629 val remote_spass_pirate = (remote_prefix ^ spass_pirateN, fn () => remote_spass_pirate_config)
   630 
   631 
   632 (* Remote ATP invocation via SystemOnTPTP *)
   633 
   634 val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
   635 
   636 fun get_remote_systems () =
   637   TimeLimit.timeLimit (seconds 10.0)
   638     (fn () =>
   639         case Isabelle_System.bash_output
   640             "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
   641           (output, 0) => split_lines output
   642         | (output, _) =>
   643           (warning (case extract_known_atp_failure known_perl_failures output of
   644                       SOME failure => string_of_atp_failure failure
   645                     | NONE => trim_line output ^ "."); [])) ()
   646   handle TimeLimit.TimeOut => []
   647 
   648 fun find_remote_system name [] systems =
   649     find_first (String.isPrefix (name ^ "---")) systems
   650   | find_remote_system name (version :: versions) systems =
   651     case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
   652       NONE => find_remote_system name versions systems
   653     | res => res
   654 
   655 fun get_remote_system name versions =
   656   Synchronized.change_result remote_systems
   657       (fn systems => (if null systems then get_remote_systems () else systems)
   658                      |> `(`(find_remote_system name versions)))
   659 
   660 fun the_remote_system name versions =
   661   (case get_remote_system name versions of
   662     (SOME sys, _) => sys
   663   | (NONE, []) => error "SystemOnTPTP is not available."
   664   | (NONE, syss) =>
   665     (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of
   666       [] => error "SystemOnTPTP is currently not available."
   667     | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg ^ ".")
   668     | syss =>
   669       error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^
   670         commas_quote syss ^ ".)")))
   671 
   672 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   673 
   674 fun remote_config system_name system_versions proof_delims known_failures
   675                   prem_role best_slice : atp_config =
   676   {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
   677    arguments = fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
   678      (if command <> "" then "-c " ^ quote command ^ " " else "") ^
   679      "-s " ^ the_remote_system system_name system_versions ^ " " ^
   680      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
   681      " " ^ file_name,
   682    proof_delims = union (op =) tstp_proof_delims proof_delims,
   683    known_failures = known_failures @ known_perl_failures @ known_says_failures,
   684    prem_role = prem_role,
   685    best_slices = fn ctxt => [(1.0, best_slice ctxt)],
   686    best_max_mono_iters = default_max_mono_iters,
   687    best_max_new_mono_instances = default_max_new_mono_instances}
   688 
   689 fun remotify_config system_name system_versions best_slice
   690         ({proof_delims, known_failures, prem_role, ...} : atp_config)
   691         : atp_config =
   692   remote_config system_name system_versions proof_delims known_failures
   693                 prem_role best_slice
   694 
   695 fun remote_atp name system_name system_versions proof_delims known_failures
   696                prem_role best_slice =
   697   (remote_prefix ^ name,
   698    fn () => remote_config system_name system_versions proof_delims
   699                           known_failures prem_role best_slice)
   700 fun remotify_atp (name, config) system_name system_versions best_slice =
   701   (remote_prefix ^ name,
   702    remotify_config system_name system_versions best_slice o config)
   703 
   704 fun gen_remote_waldmeister name type_enc =
   705   remote_atp name "Waldmeister" ["710"] tstp_proof_delims
   706     ([(OutOfResources, "Too many function symbols"),
   707       (Inappropriate, "****  Unexpected end of file."),
   708       (Crashed, "Unrecoverable Segmentation Fault")]
   709      @ known_szs_status_failures)
   710     Hypothesis
   711     (K (((50, ""), CNF_UEQ, type_enc, combsN, false), "") (* FUDGE *))
   712 
   713 val explicit_tff0 = TFF Monomorphic
   714 
   715 val remote_agsyhol =
   716   remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
   717       (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
   718 val remote_e =
   719   remotify_atp e "EP" ["1.7", "1.6", "1.5", "1"]
   720       (K (((750, ""), FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
   721 val remote_iprover =
   722   remotify_atp iprover "iProver" ["0.99"]
   723       (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
   724 val remote_iprover_eq =
   725   remotify_atp iprover_eq "iProver-Eq" ["0.8"]
   726       (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
   727 val remote_leo2 =
   728   remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
   729       (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
   730 val remote_satallax =
   731   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
   732       (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
   733 val remote_vampire =
   734   remotify_atp vampire "Vampire" ["3.0", "2.6", "2.5", "1.8"]
   735       (K (((250, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
   736 val remote_e_sine =
   737   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
   738       (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
   739 val remote_snark =
   740   remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
   741       [("refutation.", "end_refutation.")] [] Hypothesis
   742       (K (((100, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
   743 val remote_e_tofof =
   744   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
   745       (K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
   746 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
   747 val remote_waldmeister_new = gen_remote_waldmeister waldmeister_newN "mono_args"
   748 
   749 
   750 (* Setup *)
   751 
   752 fun add_atp (name, config) thy =
   753   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   754   handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   755 
   756 fun get_atp thy name =
   757   fst (the (Symtab.lookup (Data.get thy) name))
   758   handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
   759 
   760 val supported_atps = Symtab.keys o Data.get
   761 
   762 fun is_atp_installed thy name =
   763   let val {exec, ...} = get_atp thy name () in
   764     exists (fn var => getenv var <> "") (fst (exec false))
   765   end
   766 
   767 fun refresh_systems_on_tptp () =
   768   Synchronized.change remote_systems (fn _ => get_remote_systems ())
   769 
   770 fun effective_term_order ctxt atp =
   771   let val ord = Config.get ctxt term_order in
   772     if ord = smartN then
   773       {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN),
   774        gen_simp = String.isSuffix spass_pirateN atp}
   775     else
   776       let val is_lpo = String.isSubstring lpoN ord in
   777         {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
   778          gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord}
   779       end
   780   end
   781 
   782 val atps =
   783   [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
   784    z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
   785    remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
   786    remote_snark, remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
   787 
   788 val _ = Theory.setup (fold add_atp atps)
   789 
   790 end;