src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Wed Sep 11 09:50:48 2013 +0200 (2013-09-11)
changeset 53515 f5b678b155f6
parent 53225 16235bb41881
child 53586 bd5fa6425993
permissions -rw-r--r--
adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
     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 : unit -> 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 = 100 (* FUDGE *)
    95 
    96 type slice_spec = (int * string) * atp_format * string * string * bool
    97 
    98 type atp_config =
    99   {exec : unit -> 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 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
   215 
   216 val agsyhol_config : atp_config =
   217   {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
   218    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   219        "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^
   220        file_name,
   221    proof_delims = tstp_proof_delims,
   222    known_failures = known_szs_status_failures,
   223    prem_role = Hypothesis,
   224    best_slices =
   225      (* FUDGE *)
   226      K [(1.0, (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), ""))],
   227    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
   228    best_max_new_mono_instances = default_max_new_mono_instances}
   229 
   230 val agsyhol = (agsyholN, fn () => agsyhol_config)
   231 
   232 
   233 (* Alt-Ergo *)
   234 
   235 val alt_ergo_tff1 = TFF Polymorphic
   236 
   237 val alt_ergo_config : atp_config =
   238   {exec = K (["WHY3_HOME"], ["why3"]),
   239    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   240        "--format tptp --prover 'Alt-Ergo,0.95,' --timelimit " ^
   241        string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   242    proof_delims = [],
   243    known_failures =
   244      [(ProofMissing, ": Valid"),
   245       (TimedOut, ": Timeout"),
   246       (GaveUp, ": Unknown")],
   247    prem_role = Hypothesis,
   248    best_slices = fn _ =>
   249      (* FUDGE *)
   250      [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))],
   251    best_max_mono_iters = default_max_mono_iters,
   252    best_max_new_mono_instances = default_max_new_mono_instances}
   253 
   254 val alt_ergo = (alt_ergoN, fn () => alt_ergo_config)
   255 
   256 
   257 (* E *)
   258 
   259 fun is_e_at_least_1_3 () = string_ord (getenv "E_VERSION", "1.3") <> LESS
   260 fun is_e_at_least_1_6 () = string_ord (getenv "E_VERSION", "1.6") <> LESS
   261 fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> 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 effective_e_selection_heuristic ctxt =
   334   if is_e_at_least_1_3 () then Config.get ctxt e_selection_heuristic
   335   else e_autoN
   336 
   337 fun e_kbo () = if is_e_at_least_1_3 () then "KBO6" else "KBO"
   338 
   339 val e_config : atp_config =
   340   {exec = (fn () => (["E_HOME"],
   341        if is_e_at_least_1_8 () then ["eprover"] else ["eproof_ram", "eproof"])),
   342    arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout =>
   343        fn file_name =>
   344        fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
   345        "--tstp-in --tstp-out --silent " ^
   346        e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
   347        e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
   348        "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
   349        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
   350        (if is_e_at_least_1_8 () then
   351           " --proof-object=1"
   352         else
   353           " --output-level=5" ^
   354           (if is_e_at_least_1_6 () then
   355              " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
   356            else
   357              "")) ^
   358        " " ^ file_name,
   359    proof_delims =
   360      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
   361      tstp_proof_delims,
   362    known_failures =
   363      [(TimedOut, "Failure: Resource limit exceeded (time)"),
   364       (TimedOut, "time limit exceeded")] @
   365      known_szs_status_failures,
   366    prem_role = Conjecture,
   367    best_slices = fn ctxt =>
   368      let val heuristic = effective_e_selection_heuristic ctxt in
   369        (* FUDGE *)
   370        if heuristic = e_smartN then
   371          [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
   372           (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)),
   373           (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)),
   374           (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)),
   375           (0.15, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN)),
   376           (0.25, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN))]
   377        else
   378          [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))]
   379      end,
   380    best_max_mono_iters = default_max_mono_iters,
   381    best_max_new_mono_instances = default_max_new_mono_instances}
   382 
   383 val e = (eN, fn () => e_config)
   384 
   385 
   386 (* E-MaLeS *)
   387 
   388 val e_males_config : atp_config =
   389   {exec = K (["E_MALES_HOME"], ["emales.py"]),
   390    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   391        "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name,
   392    proof_delims = tstp_proof_delims,
   393    known_failures = #known_failures e_config,
   394    prem_role = Conjecture,
   395    best_slices =
   396      (* FUDGE *)
   397      K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")),
   398         (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")),
   399         (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")),
   400         (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))],
   401    best_max_mono_iters = default_max_mono_iters,
   402    best_max_new_mono_instances = default_max_new_mono_instances}
   403 
   404 val e_males = (e_malesN, fn () => e_males_config)
   405 
   406 
   407 (* E-Par *)
   408 
   409 val e_par_config : atp_config =
   410   {exec = K (["E_HOME"], ["runepar.pl"]),
   411    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   412        string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^
   413        " 2" (* proofs *),
   414    proof_delims = tstp_proof_delims,
   415    known_failures = #known_failures e_config,
   416    prem_role = Conjecture,
   417    best_slices = #best_slices e_males_config,
   418    best_max_mono_iters = default_max_mono_iters,
   419    best_max_new_mono_instances = default_max_new_mono_instances}
   420 
   421 val e_par = (e_parN, fn () => e_par_config)
   422 
   423 
   424 (* iProver *)
   425 
   426 val iprover_config : atp_config =
   427   {exec = K (["IPROVER_HOME"], ["iprover"]),
   428    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   429        "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^
   430        string_of_real (Time.toReal timeout) ^ " " ^ file_name,
   431    proof_delims = tstp_proof_delims,
   432    known_failures =
   433      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
   434      known_szs_status_failures,
   435    prem_role = Hypothesis,
   436    best_slices =
   437      (* FUDGE *)
   438      K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))],
   439    best_max_mono_iters = default_max_mono_iters,
   440    best_max_new_mono_instances = default_max_new_mono_instances}
   441 
   442 val iprover = (iproverN, fn () => iprover_config)
   443 
   444 
   445 (* iProver-Eq *)
   446 
   447 val iprover_eq_config : atp_config =
   448   {exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]),
   449    arguments = #arguments iprover_config,
   450    proof_delims = #proof_delims iprover_config,
   451    known_failures = #known_failures iprover_config,
   452    prem_role = #prem_role iprover_config,
   453    best_slices = #best_slices iprover_config,
   454    best_max_mono_iters = #best_max_mono_iters iprover_config,
   455    best_max_new_mono_instances = #best_max_new_mono_instances iprover_config}
   456 
   457 val iprover_eq = (iprover_eqN, fn () => iprover_eq_config)
   458 
   459 
   460 (* LEO-II *)
   461 
   462 (* LEO-II supports definitions, but it performs significantly better on our
   463    benchmarks when they are not used. *)
   464 val leo2_thf0 = THF (Monomorphic, THF_Without_Choice, THF_Without_Defs)
   465 
   466 val leo2_config : atp_config =
   467   {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
   468    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   469        "--foatp e --atp e=\"$E_HOME\"/eprover \
   470        \--atp epclextract=\"$E_HOME\"/epclextract \
   471        \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
   472        file_name,
   473    proof_delims = tstp_proof_delims,
   474    known_failures =
   475      [(TimedOut, "CPU time limit exceeded, terminating"),
   476       (GaveUp, "No.of.Axioms")] @
   477      known_szs_status_failures,
   478    prem_role = Hypothesis,
   479    best_slices =
   480      (* FUDGE *)
   481      K [(1.0, (((40, ""), leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
   482    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
   483    best_max_new_mono_instances = default_max_new_mono_instances}
   484 
   485 val leo2 = (leo2N, fn () => leo2_config)
   486 
   487 
   488 (* Satallax *)
   489 
   490 (* Choice is disabled until there is proper reconstruction for it. *)
   491 val satallax_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
   492 
   493 val satallax_config : atp_config =
   494   {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
   495    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   496        "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   497    proof_delims =
   498      [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
   499    known_failures = known_szs_status_failures,
   500    prem_role = Hypothesis,
   501    best_slices =
   502      (* FUDGE *)
   503      K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
   504    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
   505    best_max_new_mono_instances = default_max_new_mono_instances}
   506 
   507 val satallax = (satallaxN, fn () => satallax_config)
   508 
   509 
   510 (* SPASS *)
   511 
   512 val spass_H1SOS = "-Heuristic=1 -SOS"
   513 val spass_H2 = "-Heuristic=2"
   514 val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
   515 val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
   516 val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
   517 val spass_H2SOS = "-Heuristic=2 -SOS"
   518 
   519 val spass_extra_options =
   520   Attrib.setup_config_string @{binding atp_spass_extra_options} (K "")
   521 
   522 (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
   523 val spass_config : atp_config =
   524   {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
   525    arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
   526        fn file_name => fn _ =>
   527        "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
   528        "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
   529        |> extra_options <> "" ? prefix (extra_options ^ " "),
   530    proof_delims = [("Here is a proof", "Formulae used in the proof")],
   531    known_failures =
   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
   568 
   569 val vampire_config : atp_config =
   570   {exec = K (["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 = 2 * default_max_new_mono_instances (* FUDGE *)}
   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
   620 
   621 val z3_tptp_config : atp_config =
   622   {exec = K (["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 = 2 * default_max_new_mono_instances (* FUDGE *)}
   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 = K (["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 = THF (Polymorphic, THF_With_Choice, THF_With_Defs)
   657 val dummy_thf_config =
   658   dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
   659 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
   660 
   661 val spass_poly_format = DFG Polymorphic
   662 val spass_poly_config =
   663   dummy_config (#prem_role spass_config) spass_poly_format "tc_native" true
   664 val spass_poly = (spass_polyN, fn () => spass_poly_config)
   665 
   666 
   667 (* Remote ATP invocation via SystemOnTPTP *)
   668 
   669 val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
   670 
   671 fun get_remote_systems () =
   672   TimeLimit.timeLimit (seconds 10.0)
   673     (fn () =>
   674         case Isabelle_System.bash_output
   675             "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
   676           (output, 0) => split_lines output
   677         | (output, _) =>
   678           (warning (case extract_known_failure known_perl_failures output of
   679                       SOME failure => string_of_failure failure
   680                     | NONE => trim_line output ^ "."); [])) ()
   681   handle TimeLimit.TimeOut => []
   682 
   683 fun find_remote_system name [] systems =
   684     find_first (String.isPrefix (name ^ "---")) systems
   685   | find_remote_system name (version :: versions) systems =
   686     case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
   687       NONE => find_remote_system name versions systems
   688     | res => res
   689 
   690 fun get_remote_system name versions =
   691   Synchronized.change_result remote_systems
   692       (fn systems => (if null systems then get_remote_systems () else systems)
   693                      |> `(`(find_remote_system name versions)))
   694 
   695 fun the_remote_system name versions =
   696   case get_remote_system name versions of
   697     (SOME sys, _) => sys
   698   | (NONE, []) => error ("SystemOnTPTP is not available.")
   699   | (NONE, syss) =>
   700     case syss |> filter_out (String.isPrefix "%")
   701               |> filter_out (curry (op =) "") of
   702       [] => error ("SystemOnTPTP is currently not available.")
   703     | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg ^ ".")
   704     | syss =>
   705       error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
   706              "(Available systems: " ^ commas_quote syss ^ ".)")
   707 
   708 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   709 
   710 fun remote_config system_name system_versions proof_delims known_failures
   711                   prem_role best_slice : atp_config =
   712   {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
   713    arguments = fn _ => fn _ => fn command => fn timeout => fn file_name =>
   714        fn _ =>
   715        (if command <> "" then "-c " ^ quote command ^ " " else "") ^
   716        "-s " ^ the_remote_system system_name system_versions ^ " " ^
   717        "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
   718        " " ^ file_name,
   719    proof_delims = union (op =) tstp_proof_delims proof_delims,
   720    known_failures = known_failures @ known_perl_failures @ known_says_failures,
   721    prem_role = prem_role,
   722    best_slices = fn ctxt => [(1.0, best_slice ctxt)],
   723    best_max_mono_iters = default_max_mono_iters,
   724    best_max_new_mono_instances = default_max_new_mono_instances}
   725 
   726 fun remotify_config system_name system_versions best_slice
   727         ({proof_delims, known_failures, prem_role, ...} : atp_config)
   728         : atp_config =
   729   remote_config system_name system_versions proof_delims known_failures
   730                 prem_role best_slice
   731 
   732 fun remote_atp name system_name system_versions proof_delims known_failures
   733                prem_role best_slice =
   734   (remote_prefix ^ name,
   735    fn () => remote_config system_name system_versions proof_delims
   736                           known_failures prem_role best_slice)
   737 fun remotify_atp (name, config) system_name system_versions best_slice =
   738   (remote_prefix ^ name,
   739    remotify_config system_name system_versions best_slice o config)
   740 
   741 val explicit_tff0 = TFF Monomorphic
   742 
   743 val remote_agsyhol =
   744   remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
   745       (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
   746 val remote_e =
   747   remotify_atp e "EP" ["1.7", "1.6", "1.5", "1"]
   748       (K (((750, ""), FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
   749 val remote_iprover =
   750   remotify_atp iprover "iProver" ["0.99"]
   751       (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
   752 val remote_iprover_eq =
   753   remotify_atp iprover_eq "iProver-Eq" ["0.8"]
   754       (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
   755 val remote_leo2 =
   756   remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
   757       (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
   758 val remote_satallax =
   759   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
   760       (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
   761 val remote_vampire =
   762   remotify_atp vampire "Vampire" ["3.0", "2.6", "2.5", "1.8"]
   763       (K (((250, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
   764 val remote_e_sine =
   765   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
   766       (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
   767 val remote_snark =
   768   remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
   769       [("refutation.", "end_refutation.")] [] Hypothesis
   770       (K (((100, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
   771 val remote_e_tofof =
   772   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
   773       (K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
   774 val remote_waldmeister =
   775   remote_atp waldmeisterN "Waldmeister" ["710"]
   776       [("#START OF PROOF", "Proved Goals:")]
   777       [(OutOfResources, "Too many function symbols"),
   778        (Inappropriate, "****  Unexpected end of file."),
   779        (Crashed, "Unrecoverable Segmentation Fault")]
   780       Hypothesis
   781       (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
   782 
   783 
   784 (* Setup *)
   785 
   786 fun add_atp (name, config) thy =
   787   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   788   handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   789 
   790 fun get_atp thy name =
   791   the (Symtab.lookup (Data.get thy) name) |> fst
   792   handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
   793 
   794 val supported_atps = Symtab.keys o Data.get
   795 
   796 fun is_atp_installed thy name =
   797   let val {exec, ...} = get_atp thy name () in
   798     exists (fn var => getenv var <> "") (fst (exec ()))
   799   end
   800 
   801 fun refresh_systems_on_tptp () =
   802   Synchronized.change remote_systems (fn _ => get_remote_systems ())
   803 
   804 fun effective_term_order ctxt atp =
   805   let val ord = Config.get ctxt term_order in
   806     if ord = smartN then
   807       let val is_spass = (atp = spassN orelse atp = spass_polyN) in
   808         {is_lpo = false, gen_weights = is_spass, gen_prec = is_spass,
   809          gen_simp = false}
   810       end
   811     else
   812       let val is_lpo = String.isSubstring lpoN ord in
   813         {is_lpo = is_lpo,
   814          gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
   815          gen_prec = String.isSubstring xprecN ord,
   816          gen_simp = String.isSubstring xsimpN ord}
   817       end
   818   end
   819 
   820 val atps =
   821   [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax,
   822    spass, spass_poly, vampire, z3_tptp, dummy_thf, remote_agsyhol, remote_e,
   823    remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
   824    remote_leo2, remote_satallax, remote_vampire, remote_snark,
   825    remote_waldmeister]
   826 
   827 val setup = fold add_atp atps
   828 
   829 end;