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