src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Tue Nov 07 15:16:41 2017 +0100 (19 months ago)
changeset 67021 41f1f8c4259b
parent 66544 3e838cf5e80c
child 67560 0fa87bd86566
permissions -rw-r--r--
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
     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 val e_smartN = "smart"
   211 val e_autoN = "auto"
   212 val e_fun_weightN = "fun_weight"
   213 val e_sym_offset_weightN = "sym_offset_weight"
   214 
   215 val e_selection_heuristic =
   216   Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
   217 (* FUDGE *)
   218 val e_default_fun_weight =
   219   Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
   220 val e_fun_weight_base =
   221   Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
   222 val e_fun_weight_span =
   223   Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
   224 val e_default_sym_offs_weight =
   225   Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
   226 val e_sym_offs_weight_base =
   227   Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
   228 val e_sym_offs_weight_span =
   229   Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
   230 
   231 fun e_selection_heuristic_case heuristic fw sow =
   232   if heuristic = e_fun_weightN then fw
   233   else if heuristic = e_sym_offset_weightN then sow
   234   else raise Fail ("unexpected " ^ quote heuristic)
   235 
   236 fun scaled_e_selection_weight ctxt heuristic w =
   237   w * Config.get ctxt (e_selection_heuristic_case heuristic
   238                            e_fun_weight_span e_sym_offs_weight_span)
   239   + Config.get ctxt (e_selection_heuristic_case heuristic
   240                          e_fun_weight_base e_sym_offs_weight_base)
   241   |> Real.ceil |> signed_string_of_int
   242 
   243 fun e_selection_weight_arguments ctxt heuristic sel_weights =
   244   if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then
   245     (* supplied by Stephan Schulz *)
   246     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
   247     \--destructive-er-aggressive --destructive-er --presat-simplify \
   248     \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
   249     \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
   250     e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
   251     "(SimulateSOS," ^
   252     (e_selection_heuristic_case heuristic
   253          e_default_fun_weight e_default_sym_offs_weight
   254      |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
   255     ",20,1.5,1.5,1" ^
   256     (sel_weights ()
   257      |> map (fn (s, w) => "," ^ s ^ ":" ^
   258                           scaled_e_selection_weight ctxt heuristic w)
   259      |> implode) ^
   260     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
   261     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
   262     \FIFOWeight(PreferProcessed))' "
   263   else
   264     "-xAuto "
   265 
   266 val e_ord_weights =
   267   map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
   268 fun e_ord_precedence [_] = ""
   269   | e_ord_precedence info = info |> map fst |> space_implode "<"
   270 
   271 fun e_term_order_info_arguments false false _ = ""
   272   | e_term_order_info_arguments gen_weights gen_prec ord_info =
   273     let val ord_info = ord_info () in
   274       (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^
   275       (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
   276     end
   277 
   278 val e_tff0 = TFF Monomorphic
   279 
   280 val e_config : atp_config =
   281   {exec = fn _ => (["E_HOME"], ["eprover"]),
   282    arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn file_name =>
   283      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
   284        "--auto-schedule --tstp-in --tstp-out --silent " ^
   285        e_selection_weight_arguments ctxt heuristic sel_weights ^
   286        e_term_order_info_arguments gen_weights gen_prec ord_info ^
   287        "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
   288        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
   289        " --proof-object=1 " ^
   290        file_name,
   291    proof_delims =
   292      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
   293      tstp_proof_delims,
   294    known_failures =
   295      [(TimedOut, "Failure: Resource limit exceeded (time)"),
   296       (TimedOut, "time limit exceeded")] @
   297      known_szs_status_failures,
   298    prem_role = Conjecture,
   299    best_slices = fn ctxt =>
   300      let val heuristic = Config.get ctxt e_selection_heuristic in
   301        (* FUDGE *)
   302        if heuristic = e_smartN then
   303          [(0.15, (((128, meshN), e_tff0, "mono_native", combsN, false), e_fun_weightN)),
   304           (0.15, (((128, mashN), e_tff0, "mono_native", combsN, false), e_sym_offset_weightN)),
   305           (0.15, (((91, mepoN), e_tff0, "mono_native", combsN, false), e_autoN)),
   306           (0.15, (((1000, meshN), e_tff0, "poly_guards??", combsN, false), e_sym_offset_weightN)),
   307           (0.15, (((256, mepoN), e_tff0, "mono_native", liftingN, false), e_fun_weightN)),
   308           (0.25, (((64, mashN), e_tff0, "mono_native", combsN, false), e_fun_weightN))]
   309        else
   310          [(1.0, (((500, ""), e_tff0, "mono_native", combsN, false), heuristic))]
   311      end,
   312    best_max_mono_iters = default_max_mono_iters,
   313    best_max_new_mono_instances = default_max_new_mono_instances}
   314 
   315 val e = (eN, fn () => e_config)
   316 
   317 
   318 (* E-MaLeS *)
   319 
   320 val e_males_config : atp_config =
   321   {exec = K (["E_MALES_HOME"], ["emales.py"]),
   322    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   323        "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name,
   324    proof_delims = tstp_proof_delims,
   325    known_failures = #known_failures e_config,
   326    prem_role = Conjecture,
   327    best_slices =
   328      (* FUDGE *)
   329      K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")),
   330         (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")),
   331         (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")),
   332         (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))],
   333    best_max_mono_iters = default_max_mono_iters,
   334    best_max_new_mono_instances = default_max_new_mono_instances}
   335 
   336 val e_males = (e_malesN, fn () => e_males_config)
   337 
   338 
   339 (* E-Par *)
   340 
   341 val e_par_config : atp_config =
   342   {exec = K (["E_HOME"], ["runepar.pl"]),
   343    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   344        string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^
   345        " 2" (* proofs *),
   346    proof_delims = tstp_proof_delims,
   347    known_failures = #known_failures e_config,
   348    prem_role = Conjecture,
   349    best_slices = #best_slices e_males_config,
   350    best_max_mono_iters = default_max_mono_iters,
   351    best_max_new_mono_instances = default_max_new_mono_instances}
   352 
   353 val e_par = (e_parN, fn () => e_par_config)
   354 
   355 
   356 (* iProver *)
   357 
   358 val iprover_config : atp_config =
   359   {exec = K (["IPROVER_HOME"], ["iprover"]),
   360    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   361        "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^
   362        string_of_real (Time.toReal timeout) ^ " " ^ file_name,
   363    proof_delims = tstp_proof_delims,
   364    known_failures =
   365      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
   366      known_szs_status_failures,
   367    prem_role = Hypothesis,
   368    best_slices =
   369      (* FUDGE *)
   370      K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))],
   371    best_max_mono_iters = default_max_mono_iters,
   372    best_max_new_mono_instances = default_max_new_mono_instances}
   373 
   374 val iprover = (iproverN, fn () => iprover_config)
   375 
   376 
   377 (* iProver-Eq *)
   378 
   379 val iprover_eq_config : atp_config =
   380   {exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]),
   381    arguments = #arguments iprover_config,
   382    proof_delims = #proof_delims iprover_config,
   383    known_failures = #known_failures iprover_config,
   384    prem_role = #prem_role iprover_config,
   385    best_slices = #best_slices iprover_config,
   386    best_max_mono_iters = #best_max_mono_iters iprover_config,
   387    best_max_new_mono_instances = #best_max_new_mono_instances iprover_config}
   388 
   389 val iprover_eq = (iprover_eqN, fn () => iprover_eq_config)
   390 
   391 
   392 (* LEO-II *)
   393 
   394 val leo2_thf0 = THF (Monomorphic, THF_Without_Choice)
   395 
   396 val leo2_config : atp_config =
   397   {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
   398    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
   399      "--foatp e --atp e=\"$E_HOME\"/eprover \
   400      \--atp epclextract=\"$E_HOME\"/epclextract \
   401      \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
   402      (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^
   403      file_name,
   404    proof_delims = tstp_proof_delims,
   405    known_failures =
   406      [(TimedOut, "CPU time limit exceeded, terminating"),
   407       (GaveUp, "No.of.Axioms")] @
   408      known_szs_status_failures,
   409    prem_role = Hypothesis,
   410    best_slices =
   411      (* FUDGE *)
   412      K [(1.0, (((40, ""), leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
   413    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
   414    best_max_new_mono_instances = default_max_new_mono_instances}
   415 
   416 val leo2 = (leo2N, fn () => leo2_config)
   417 
   418 
   419 (* Leo-III *)
   420 
   421 (* include choice? Disabled now since its disabled for satallax as well. *)
   422 val leo3_thf1 = THF (Polymorphic, THF_Without_Choice)
   423 
   424 val leo3_config : atp_config =
   425   {exec = K (["LEO3_HOME"], ["leo3"]),
   426    arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
   427      file_name ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \
   428      \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
   429      (if full_proofs then "--nleq --naeq " else ""),
   430    proof_delims = tstp_proof_delims,
   431    known_failures = known_szs_status_failures,
   432    prem_role = Hypothesis,
   433    best_slices =
   434      (* FUDGE *)
   435      K [(1.0, (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), ""))],
   436    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
   437    best_max_new_mono_instances = default_max_new_mono_instances}
   438 
   439 val leo3 = (leo3N, fn () => leo3_config)
   440 
   441 
   442 (* Satallax *)
   443 
   444 (* Choice is disabled until there is proper reconstruction for it. *)
   445 val satallax_thf0 = THF (Monomorphic, THF_Without_Choice)
   446 
   447 val satallax_config : atp_config =
   448   {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
   449    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   450        "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   451    proof_delims =
   452      [("% SZS output start Proof", "% SZS output end Proof")],
   453    known_failures = known_szs_status_failures,
   454    prem_role = Hypothesis,
   455    best_slices =
   456      (* FUDGE *)
   457      K [(1.0, (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
   458    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
   459    best_max_new_mono_instances = default_max_new_mono_instances}
   460 
   461 val satallax = (satallaxN, fn () => satallax_config)
   462 
   463 
   464 (* SPASS *)
   465 
   466 val spass_H1SOS = "-Heuristic=1 -SOS"
   467 val spass_H2 = "-Heuristic=2"
   468 val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
   469 val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
   470 val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
   471 val spass_H2SOS = "-Heuristic=2 -SOS"
   472 
   473 val spass_extra_options =
   474   Attrib.setup_config_string @{binding atp_spass_extra_options} (K "")
   475 
   476 val spass_config : atp_config =
   477   {exec = K (["SPASS_HOME"], ["SPASS"]),
   478    arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
   479        fn file_name => fn _ =>
   480        "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
   481        "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
   482        |> extra_options <> "" ? prefix (extra_options ^ " "),
   483    proof_delims = [("Here is a proof", "Formulae used in the proof")],
   484    known_failures =
   485      [(GaveUp, "SPASS beiseite: Completion found"),
   486       (TimedOut, "SPASS beiseite: Ran out of time"),
   487       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
   488       (MalformedInput, "Undefined symbol"),
   489       (MalformedInput, "Free Variable"),
   490       (Unprovable, "No formulae and clauses found in input file"),
   491       (InternalError, "Please report this error")] @
   492       known_perl_failures,
   493    prem_role = Conjecture,
   494    best_slices = fn ctxt =>
   495      (* FUDGE *)
   496      [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")),
   497       (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
   498       (0.1666, (((50, meshN), DFG Monomorphic,  "mono_native", liftingN, true), spass_H2LR0LT0)),
   499       (0.1000, (((250, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)),
   500       (0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
   501       (0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
   502       (0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
   503       (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))]
   504      |> (case Config.get ctxt spass_extra_options of
   505            "" => I
   506          | opts => map (apsnd (apsnd (K opts)))),
   507    best_max_mono_iters = default_max_mono_iters,
   508    best_max_new_mono_instances = default_max_new_mono_instances}
   509 
   510 val spass = (spassN, fn () => spass_config)
   511 
   512 
   513 (* Vampire *)
   514 
   515 (* Vampire 1.8 has TFF0 support, but the support was buggy until revision
   516    1435 (or shortly before). *)
   517 fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
   518 fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
   519 
   520 val vampire_tff0 = TFF Monomorphic
   521 
   522 val vampire_basic_options = "--proof tptp --output_axiom_names on --mode casc"
   523 
   524 (* cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
   525 val vampire_full_proof_options =
   526   " --forced_options splitting=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:\
   527   \naming=0"
   528 
   529 val remote_vampire_full_proof_command =
   530   "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"
   531 
   532 val vampire_config : atp_config =
   533   {exec = K (["VAMPIRE_HOME"], ["vampire"]),
   534    arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ =>
   535      vampire_basic_options ^
   536      (if is_vampire_at_least_1_8 () andalso full_proofs then " " ^ vampire_full_proof_options
   537       else "") ^
   538      " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ file_name
   539      |> sos = sosN ? prefix "--sos on ",
   540    proof_delims =
   541      [("=========== Refutation ==========",
   542        "======= End of refutation =======")] @
   543      tstp_proof_delims,
   544    known_failures =
   545      [(GaveUp, "UNPROVABLE"),
   546       (GaveUp, "CANNOT PROVE"),
   547       (Unprovable, "Satisfiability detected"),
   548       (Unprovable, "Termination reason: Satisfiable"),
   549       (Interrupted, "Aborted by signal SIGINT")] @
   550      known_szs_status_failures,
   551    prem_role = Hypothesis,
   552    best_slices = fn ctxt =>
   553      (* FUDGE *)
   554      (if is_vampire_beyond_1_8 () then
   555         [(0.333, (((500, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)),
   556          (0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
   557          (0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
   558       else
   559         [(0.333, (((150, meshN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
   560          (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)),
   561          (0.334, (((50, meshN), FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))])
   562      |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
   563    best_max_mono_iters = default_max_mono_iters,
   564    best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
   565 
   566 val vampire = (vampireN, fn () => vampire_config)
   567 
   568 (* Z3 with TPTP syntax (half experimental, half legacy) *)
   569 
   570 val z3_tff0 = TFF Monomorphic
   571 
   572 val z3_tptp_config : atp_config =
   573   {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
   574    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   575      "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
   576    proof_delims = [("SZS status Theorem", "")],
   577    known_failures = known_szs_status_failures,
   578    prem_role = Hypothesis,
   579    best_slices =
   580      (* FUDGE *)
   581      K [(0.5, (((250, meshN), z3_tff0, "mono_native", combsN, false), "")),
   582         (0.25, (((125, mepoN), z3_tff0, "mono_native", combsN, false), "")),
   583         (0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")),
   584         (0.125, (((31, meshN), z3_tff0, "mono_native", combsN, false), ""))],
   585    best_max_mono_iters = default_max_mono_iters,
   586    best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
   587 
   588 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
   589 
   590 
   591 (* Zipperposition*)
   592 
   593 val zipperposition_config : atp_config =
   594   {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
   595    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   596        "-print none -proof tstp -print-types -timeout " ^
   597        string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   598    proof_delims = tstp_proof_delims,
   599    known_failures = known_szs_status_failures,
   600    prem_role = Hypothesis,
   601    best_slices = fn _ =>
   602      (* FUDGE *)
   603      [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))],
   604    best_max_mono_iters = default_max_mono_iters,
   605    best_max_new_mono_instances = default_max_new_mono_instances}
   606 
   607 val zipperposition = (zipperpositionN, fn () => zipperposition_config)
   608 
   609 
   610 (* Not really a prover: Experimental Polymorphic THF and DFG output *)
   611 
   612 fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
   613   {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
   614    arguments = K (K (K (K (K (K ""))))),
   615    proof_delims = [],
   616    known_failures = known_szs_status_failures,
   617    prem_role = prem_role,
   618    best_slices =
   619      K [(1.0, (((200, ""), format, type_enc,
   620                 if is_format_higher_order format then keep_lamsN
   621                 else combsN, uncurried_aliases), ""))],
   622    best_max_mono_iters = default_max_mono_iters,
   623    best_max_new_mono_instances = default_max_new_mono_instances}
   624 
   625 val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
   626 
   627 val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
   628 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
   629 
   630 val dummy_thf_ml_config = dummy_config Hypothesis dummy_thf_format "ml_poly_native_higher" false
   631 val dummy_thf_ml = (dummy_thf_mlN, fn () => dummy_thf_ml_config)
   632 
   633 val pirate_format = DFG Polymorphic
   634 val remote_pirate_config : atp_config =
   635   {exec = K (["ISABELLE_ATP"], ["scripts/remote_pirate"]),
   636    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   637      string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   638    proof_delims = [("Involved clauses:", "Involved clauses:")],
   639    known_failures = known_szs_status_failures,
   640    prem_role = #prem_role spass_config,
   641    best_slices = K [(1.0, (((200, ""), pirate_format, "tc_native", combsN, true), ""))],
   642    best_max_mono_iters = default_max_mono_iters,
   643    best_max_new_mono_instances = default_max_new_mono_instances}
   644 val remote_pirate = (remote_prefix ^ pirateN, fn () => remote_pirate_config)
   645 
   646 
   647 (* Remote ATP invocation via SystemOnTPTP *)
   648 
   649 val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
   650 
   651 fun get_remote_systems () =
   652   Timeout.apply (seconds 10.0) (fn () =>
   653     (case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
   654       (output, 0) => split_lines output
   655     | (output, _) =>
   656       (warning
   657          (case extract_known_atp_failure known_perl_failures output of
   658            SOME failure => string_of_atp_failure failure
   659          | NONE => trim_line output); []))) ()
   660   handle Timeout.TIMEOUT _ => []
   661 
   662 fun find_remote_system name [] systems =
   663     find_first (String.isPrefix (name ^ "---")) systems
   664   | find_remote_system name (version :: versions) systems =
   665     case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
   666       NONE => find_remote_system name versions systems
   667     | res => res
   668 
   669 fun get_remote_system name versions =
   670   Synchronized.change_result remote_systems
   671       (fn systems => (if null systems then get_remote_systems () else systems)
   672                      |> `(`(find_remote_system name versions)))
   673 
   674 fun the_remote_system name versions =
   675   (case get_remote_system name versions of
   676     (SOME sys, _) => sys
   677   | (NONE, []) => error "SystemOnTPTP is currently not available"
   678   | (NONE, syss) =>
   679     (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of
   680       [] => error "SystemOnTPTP is currently not available"
   681     | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg)
   682     | syss =>
   683       error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^
   684         commas_quote syss ^ ".)")))
   685 
   686 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   687 
   688 fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice =
   689   {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
   690    arguments = fn _ => fn full_proofs => fn full_proof_command => fn timeout => fn file_name => fn _ =>
   691      (if full_proofs andalso full_proof_command <> "" then "-c " ^ quote full_proof_command ^ " "
   692       else "") ^
   693      "-s " ^ the_remote_system system_name system_versions ^ " " ^
   694      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
   695      " " ^ file_name,
   696    proof_delims = union (op =) tstp_proof_delims proof_delims,
   697    known_failures = known_failures @ known_perl_failures @ known_says_failures,
   698    prem_role = prem_role,
   699    best_slices = fn ctxt => [(1.0, best_slice ctxt)],
   700    best_max_mono_iters = default_max_mono_iters,
   701    best_max_new_mono_instances = default_max_new_mono_instances} : atp_config
   702 
   703 fun remotify_config system_name system_versions best_slice
   704     ({proof_delims, known_failures, prem_role, ...} : atp_config) =
   705   remote_config system_name system_versions proof_delims known_failures prem_role best_slice
   706 
   707 fun remote_atp name system_name system_versions proof_delims known_failures prem_role best_slice =
   708   (remote_prefix ^ name, fn () =>
   709      remote_config system_name system_versions proof_delims known_failures prem_role best_slice)
   710 fun remotify_atp (name, config) system_name system_versions best_slice =
   711   (remote_prefix ^ name, remotify_config system_name system_versions best_slice o config)
   712 
   713 fun gen_remote_waldmeister name type_enc =
   714   remote_atp name "Waldmeister" ["710"] tstp_proof_delims
   715     ([(OutOfResources, "Too many function symbols"),
   716       (Inappropriate, "****  Unexpected end of file."),
   717       (Crashed, "Unrecoverable Segmentation Fault")]
   718      @ known_szs_status_failures)
   719     Hypothesis
   720     (K (((50, ""), CNF_UEQ, type_enc, combsN, false), "") (* FUDGE *))
   721 
   722 val explicit_tff0 = TFF Monomorphic
   723 
   724 val remote_agsyhol =
   725   remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
   726     (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
   727 val remote_e =
   728   remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
   729     (K (((750, ""), e_tff0, "mono_native", combsN, false), "") (* FUDGE *))
   730 val remote_iprover =
   731   remotify_atp iprover "iProver" ["0.99"]
   732     (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
   733 val remote_iprover_eq =
   734   remotify_atp iprover_eq "iProver-Eq" ["0.8"]
   735     (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
   736 val remote_leo2 =
   737   remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
   738     (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
   739 val remote_leo3 =
   740   remotify_atp leo3 "Leo-III" ["1.1"]
   741     (K (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
   742 val remote_satallax =
   743   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
   744     (K (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
   745 val remote_vampire =
   746   remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"]
   747     (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
   748 val remote_e_sine =
   749   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
   750     (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
   751 val remote_snark =
   752   remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
   753     [("refutation.", "end_refutation.")] [] Hypothesis
   754     (K (((100, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
   755 val remote_e_tofof =
   756   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
   757     (K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
   758 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
   759 val remote_waldmeister_new = gen_remote_waldmeister waldmeister_newN "mono_args"
   760 
   761 
   762 (* Setup *)
   763 
   764 fun add_atp (name, config) thy =
   765   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   766   handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name)
   767 
   768 fun get_atp thy name =
   769   fst (the (Symtab.lookup (Data.get thy) name))
   770   handle Option.Option => error ("Unknown ATP: " ^ name)
   771 
   772 val supported_atps = Symtab.keys o Data.get
   773 
   774 fun is_atp_installed thy name =
   775   let val {exec, ...} = get_atp thy name () in
   776     exists (fn var => getenv var <> "") (fst (exec false))
   777   end
   778 
   779 fun refresh_systems_on_tptp () =
   780   Synchronized.change remote_systems (fn _ => get_remote_systems ())
   781 
   782 fun effective_term_order ctxt atp =
   783   let val ord = Config.get ctxt term_order in
   784     if ord = smartN then
   785       {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN),
   786        gen_simp = String.isSuffix pirateN atp}
   787     else
   788       let val is_lpo = String.isSubstring lpoN ord in
   789         {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
   790          gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord}
   791       end
   792   end
   793 
   794 val atps =
   795   [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, leo3, satallax, spass, vampire,
   796    z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
   797    remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, remote_satallax,
   798    remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
   799 
   800 val _ = Theory.setup (fold add_atp atps)
   801 
   802 end;