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