src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Thu Apr 03 16:57:19 2014 +0200 (2014-04-03)
changeset 56378 8fb4515818f7
parent 54802 9ce867291c76
child 56379 d8ecce5d51cd
permissions -rw-r--r--
updated Z3 TPTP to 4.3.1+
     1 (*  Title:      HOL/Tools/ATP/atp_systems.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Setup for supported ATPs.
     6 *)
     7 
     8 signature ATP_SYSTEMS =
     9 sig
    10   type term_order = ATP_Problem.term_order
    11   type atp_format = ATP_Problem.atp_format
    12   type atp_formula_role = ATP_Problem.atp_formula_role
    13   type atp_failure = ATP_Proof.atp_failure
    14 
    15   type slice_spec = (int * string) * atp_format * string * string * bool
    16   type atp_config =
    17     {exec : 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 : (atp_failure * string) list,
    24      prem_role : atp_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_pirateN : 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     -> (atp_failure * string) list -> atp_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 : (atp_failure * string) list,
   106    prem_role : atp_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_pirateN = "spass_pirate"
   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)
   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)
   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)
   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_TPTP_HOME"], ["z3_tptp"]),
   623    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   624      "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
   625    proof_delims = [],
   626    known_failures = known_szs_status_failures,
   627    prem_role = Hypothesis,
   628    best_slices =
   629      (* FUDGE *)
   630      K [(0.5, (((250, meshN), z3_tff0, "mono_native", combsN, false), "")),
   631         (0.25, (((125, mepoN), z3_tff0, "mono_native", combsN, false), "")),
   632         (0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")),
   633         (0.125, (((31, meshN), z3_tff0, "mono_native", combsN, false), ""))],
   634    best_max_mono_iters = default_max_mono_iters,
   635    best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
   636 
   637 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
   638 
   639 
   640 (* Not really a prover: Experimental Polymorphic THF and DFG output *)
   641 
   642 fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
   643   {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
   644    arguments = K (K (K (K (K (K ""))))),
   645    proof_delims = [],
   646    known_failures = known_szs_status_failures,
   647    prem_role = prem_role,
   648    best_slices =
   649      K [(1.0, (((200, ""), format, type_enc,
   650                 if is_format_higher_order format then keep_lamsN
   651                 else combsN, uncurried_aliases), ""))],
   652    best_max_mono_iters = default_max_mono_iters,
   653    best_max_new_mono_instances = default_max_new_mono_instances}
   654 
   655 val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
   656 val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
   657 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
   658 
   659 val spass_pirate_format = DFG Polymorphic
   660 val remote_spass_pirate_config : atp_config =
   661   {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]),
   662    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   663      string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   664    proof_delims = [("Involved clauses:", "Involved clauses:")],
   665    known_failures = known_szs_status_failures,
   666    prem_role = #prem_role spass_config,
   667    best_slices = K [(1.0, (((200, ""), spass_pirate_format, "tc_native", combsN, true), ""))],
   668    best_max_mono_iters = default_max_mono_iters,
   669    best_max_new_mono_instances = default_max_new_mono_instances}
   670 val remote_spass_pirate = (remote_prefix ^ spass_pirateN, fn () => remote_spass_pirate_config)
   671 
   672 
   673 (* Remote ATP invocation via SystemOnTPTP *)
   674 
   675 val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
   676 
   677 fun get_remote_systems () =
   678   TimeLimit.timeLimit (seconds 10.0)
   679     (fn () =>
   680         case Isabelle_System.bash_output
   681             "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
   682           (output, 0) => split_lines output
   683         | (output, _) =>
   684           (warning (case extract_known_atp_failure known_perl_failures output of
   685                       SOME failure => string_of_atp_failure failure
   686                     | NONE => trim_line output ^ "."); [])) ()
   687   handle TimeLimit.TimeOut => []
   688 
   689 fun find_remote_system name [] systems =
   690     find_first (String.isPrefix (name ^ "---")) systems
   691   | find_remote_system name (version :: versions) systems =
   692     case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
   693       NONE => find_remote_system name versions systems
   694     | res => res
   695 
   696 fun get_remote_system name versions =
   697   Synchronized.change_result remote_systems
   698       (fn systems => (if null systems then get_remote_systems () else systems)
   699                      |> `(`(find_remote_system name versions)))
   700 
   701 fun the_remote_system name versions =
   702   (case get_remote_system name versions of
   703     (SOME sys, _) => sys
   704   | (NONE, []) => error "SystemOnTPTP is not available."
   705   | (NONE, syss) =>
   706     (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of
   707       [] => error "SystemOnTPTP is currently not available."
   708     | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg ^ ".")
   709     | syss =>
   710       error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^
   711         commas_quote syss ^ ".)")))
   712 
   713 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   714 
   715 fun remote_config system_name system_versions proof_delims known_failures
   716                   prem_role best_slice : atp_config =
   717   {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
   718    arguments = fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
   719      (if command <> "" then "-c " ^ quote command ^ " " else "") ^
   720      "-s " ^ the_remote_system system_name system_versions ^ " " ^
   721      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
   722      " " ^ file_name,
   723    proof_delims = union (op =) tstp_proof_delims proof_delims,
   724    known_failures = known_failures @ known_perl_failures @ known_says_failures,
   725    prem_role = prem_role,
   726    best_slices = fn ctxt => [(1.0, best_slice ctxt)],
   727    best_max_mono_iters = default_max_mono_iters,
   728    best_max_new_mono_instances = default_max_new_mono_instances}
   729 
   730 fun remotify_config system_name system_versions best_slice
   731         ({proof_delims, known_failures, prem_role, ...} : atp_config)
   732         : atp_config =
   733   remote_config system_name system_versions proof_delims known_failures
   734                 prem_role best_slice
   735 
   736 fun remote_atp name system_name system_versions proof_delims known_failures
   737                prem_role best_slice =
   738   (remote_prefix ^ name,
   739    fn () => remote_config system_name system_versions proof_delims
   740                           known_failures prem_role best_slice)
   741 fun remotify_atp (name, config) system_name system_versions best_slice =
   742   (remote_prefix ^ name,
   743    remotify_config system_name system_versions best_slice o config)
   744 
   745 val explicit_tff0 = TFF Monomorphic
   746 
   747 val remote_agsyhol =
   748   remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
   749       (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
   750 val remote_e =
   751   remotify_atp e "EP" ["1.7", "1.6", "1.5", "1"]
   752       (K (((750, ""), FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
   753 val remote_iprover =
   754   remotify_atp iprover "iProver" ["0.99"]
   755       (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
   756 val remote_iprover_eq =
   757   remotify_atp iprover_eq "iProver-Eq" ["0.8"]
   758       (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
   759 val remote_leo2 =
   760   remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
   761       (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
   762 val remote_satallax =
   763   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
   764       (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
   765 val remote_vampire =
   766   remotify_atp vampire "Vampire" ["3.0", "2.6", "2.5", "1.8"]
   767       (K (((250, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
   768 val remote_e_sine =
   769   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
   770       (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
   771 val remote_snark =
   772   remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
   773       [("refutation.", "end_refutation.")] [] Hypothesis
   774       (K (((100, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
   775 val remote_e_tofof =
   776   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
   777       (K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
   778 val remote_waldmeister =
   779   remote_atp waldmeisterN "Waldmeister" ["710"]
   780       [("#START OF PROOF", "Proved Goals:")]
   781       [(OutOfResources, "Too many function symbols"),
   782        (Inappropriate, "****  Unexpected end of file."),
   783        (Crashed, "Unrecoverable Segmentation Fault")]
   784       Hypothesis
   785       (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
   786 
   787 
   788 (* Setup *)
   789 
   790 fun add_atp (name, config) thy =
   791   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   792   handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   793 
   794 fun get_atp thy name =
   795   fst (the (Symtab.lookup (Data.get thy) name))
   796   handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
   797 
   798 val supported_atps = Symtab.keys o Data.get
   799 
   800 fun is_atp_installed thy name =
   801   let val {exec, ...} = get_atp thy name () in
   802     exists (fn var => getenv var <> "") (fst (exec ()))
   803   end
   804 
   805 fun refresh_systems_on_tptp () =
   806   Synchronized.change remote_systems (fn _ => get_remote_systems ())
   807 
   808 fun effective_term_order ctxt atp =
   809   let val ord = Config.get ctxt term_order in
   810     if ord = smartN then
   811       {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN),
   812        gen_simp = String.isSuffix spass_pirateN atp}
   813     else
   814       let val is_lpo = String.isSubstring lpoN ord in
   815         {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
   816          gen_prec = String.isSubstring xprecN ord, 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, spass, vampire,
   822    z3_tptp, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof, remote_iprover,
   823    remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
   824    remote_spass_pirate, remote_waldmeister]
   825 
   826 val setup = fold add_atp atps
   827 
   828 end;