src/HOL/Tools/ATP/atp_systems.ML

 sig
   type atp_format = ATP_Problem.atp_format
   type formula_kind = ATP_Problem.formula_kind
   type failure = ATP_Proof.failure
 
+  type slice_spec = int * atp_format * string * string * bool
   type atp_config =
     {exec : string * string,
      required_execs : (string * string) list,
      arguments :
        Proof.context -> bool -> string -> Time.time

      proof_delims : (string * string) list,
      known_failures : (failure * string) list,
      conj_sym_kind : formula_kind,
      prem_kind : formula_kind,
      best_slices :
-       Proof.context
-       -> (real * (bool * ((int * atp_format * string * string) * string)))
-            list}
+       Proof.context -> (real * (bool * (slice_spec * string))) list}
 
   val force_sos : bool Config.T
   val e_smartN : string
   val e_autoN : string
   val e_fun_weightN : string

   val z3_tptpN : string
   val remote_prefix : string
   val remote_atp :
     string -> string -> string list -> (string * string) list
     -> (failure * string) list -> formula_kind -> formula_kind
-    -> (Proof.context -> int * atp_format * string * string)
-    -> string * atp_config
+    -> (Proof.context -> slice_spec) -> string * atp_config
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val supported_atps : theory -> string list
   val is_atp_installed : theory -> string -> bool
   val refresh_systems_on_tptp : unit -> unit

 open ATP_Problem
 open ATP_Proof
 open ATP_Problem_Generate
 
 (* ATP configuration *)
+
+type slice_spec = int * atp_format * string * string * bool
 
 type atp_config =
   {exec : string * string,
    required_execs : (string * string) list,
    arguments :

      -> (unit -> (string * real) list) -> string,
    proof_delims : (string * string) list,
    known_failures : (failure * string) list,
    conj_sym_kind : formula_kind,
    prem_kind : formula_kind,
-   best_slices :
-     Proof.context
-     -> (real * (bool * ((int * atp_format * string * string) * string))) list}
+   best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
 
 (* "best_slices" must be found empirically, taking a wholistic approach since
    the ATPs are run in parallel. The "real" component gives the faction of the
-   time available given to the slice and should add up to 1.0. The "bool"
+   time available given to the slice and should add up to 1.0. The first "bool"
    component indicates whether the slice's strategy is complete; the "int", the
    preferred number of facts to pass; the first "string", the preferred type
    system (which should be sound or quasi-sound); the second "string", the
-   preferred lambda translation scheme; the third "string", extra information to
+   preferred lambda translation scheme; the second "bool", whether uncurried
+   aliased should be generated; the third "string", extra information to
    the prover (e.g., SOS or no SOS).
 
    The last slice should be the most "normal" one, because it will get all the
    time available if the other slices fail early and also because it is used if
    slicing is disabled (e.g., by the minimizer). *)

    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      let val method = effective_e_weight_method ctxt in
        (* FUDGE *)
        if method = e_smartN then
-         [(0.333, (true, ((500, FOF, "mono_tags??", combsN), e_fun_weightN))),
-          (0.334, (true, ((50, FOF, "mono_guards??", combsN), e_fun_weightN))),
-          (0.333, (true, ((1000, FOF, "mono_tags??", combsN),
+         [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false),
+                          e_fun_weightN))),
+          (0.334, (true, ((50, FOF, "mono_guards??", combsN, false),
+                          e_fun_weightN))),
+          (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false),
                           e_sym_offset_weightN)))]
        else
-         [(1.0, (true, ((500, FOF, "mono_tags??", combsN), method)))]
+         [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))]
      end}
 
 val e = (eN, e_config)
 
 

      [(TimedOut, "CPU time limit exceeded, terminating")],
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN),
+     [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN, false),
                        sosN))),
-      (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN),
+      (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN, false),
                       no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
 val leo2 = (leo2N, leo2_config)

    known_failures = known_szs_status_failures,
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN),
-                      "")))]}
+     K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN,
+                       false), "")))]}
 
 val satallax = (satallaxN, satallax_config)
 
 
 (* SPASS *)

       (InternalError, "Please report this error")],
    conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN),
+     [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
                        sosN))),
-      (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN),
+      (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false),
                        sosN))),
-      (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN),
+      (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
                        no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
 val spass = (spassN, spass_config)
 
-val spass_new_macro_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN)
-val spass_new_macro_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN)
-val spass_new_macro_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN)
+val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN, true)
+val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN, true)
+val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN, true)
 
 (* Experimental *)
 val spass_new_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass_new"),
    required_execs =

    known_failures = #known_failures spass_config,
    conj_sym_kind = #conj_sym_kind spass_config,
    prem_kind = #prem_kind spass_config,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(0.300, (true, (spass_new_macro_slice_1, ""))),
-      (0.333, (true, (spass_new_macro_slice_2, ""))),
-      (0.333, (true, (spass_new_macro_slice_3, "")))]}
+     [(0.300, (true, (spass_new_slice_1, ""))),
+      (0.333, (true, (spass_new_slice_2, ""))),
+      (0.333, (true, (spass_new_slice_3, "")))]}
 
 val spass_new = (spass_newN, spass_new_config)
 
 
 (* Vampire *)

    conj_sym_kind = Conjecture,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
      (if is_old_vampire_version () then
-        [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN),
-                           sosN))),
-         (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN), sosN))),
-         (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN),
+        [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false),
+                          sosN))),
+         (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false),
+                          sosN))),
+         (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false),
                          no_sosN)))]
       else
         [(0.333, (false, ((150, vampire_tff0, "poly_guards??",
-                           combs_or_liftingN), sosN))),
-         (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN),
-                          sosN))),
-         (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN),
-                         no_sosN)))])
+                           combs_or_liftingN, false), sosN))),
+         (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN,
+                           false), sosN))),
+         (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN,
+                          false), no_sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
 val vampire = (vampireN, vampire_config)
 

    known_failures = known_szs_status_failures,
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN), ""))),
-        (0.25, (false, ((125, z3_tff0, "mono_simple", combsN), ""))),
-        (0.125, (false, ((62, z3_tff0, "mono_simple", combsN), ""))),
-        (0.125, (false, ((31, z3_tff0, "mono_simple", combsN), "")))]}
+     K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN, false), ""))),
+        (0.25, (false, ((125, z3_tff0, "mono_simple", combsN, false), ""))),
+        (0.125, (false, ((62, z3_tff0, "mono_simple", combsN, false), ""))),
+        (0.125, (false, ((31, z3_tff0, "mono_simple", combsN, false), "")))]}
 
 val z3_tptp = (z3_tptpN, z3_tptp_config)
 
 
 (* Not really a prover: Experimental Polymorphic TFF and THF output *)

    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =
      K [(1.0, (false, ((200, format, type_enc,
                         if is_format_higher_order format then keep_lamsN
-                        else combsN), "")))]}
+                        else combsN, false), "")))]}
 
 val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
 val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
 val dummy_tff1 = (dummy_tff1N, dummy_tff1_config)
 

 fun remote_config system_name system_versions proof_delims known_failures
                   conj_sym_kind prem_kind best_slice : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
-     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
-     ^ " -s " ^ the_system system_name system_versions,
+     "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
+     " -s " ^ the_system system_name system_versions,
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @ known_says_failures,
    conj_sym_kind = conj_sym_kind,
    prem_kind = prem_kind,
-   best_slices = fn ctxt =>
-     let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in
-       [(1.0, (false, ((max_relevant, format, type_enc, lam_trans), "")))]
-     end}
+   best_slices = fn ctxt => [(1.0, (false, (best_slice ctxt, "")))]}
 
 fun remotify_config system_name system_versions best_slice
         ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
          : atp_config) : atp_config =
   remote_config system_name system_versions proof_delims known_failures

 
 val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
 
 val remote_e =
   remotify_atp e "EP" ["1.0", "1.1", "1.2"]
-      (K (750, FOF, "mono_tags??", combsN) (* FUDGE *))
+      (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *))
 val remote_leo2 =
   remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
-      (K (100, leo2_thf0, "mono_simple_higher", liftingN) (* FUDGE *))
+      (K (100, leo2_thf0, "mono_simple_higher", liftingN, false) (* FUDGE *))
 val remote_satallax =
   remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
-      (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *))
+      (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN, false)
+         (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["1.8"]
-      (K (250, FOF, "mono_guards??", combs_or_liftingN) (* FUDGE *))
+      (K (250, FOF, "mono_guards??", combs_or_liftingN, false) (* FUDGE *))
 val remote_z3_tptp =
   remotify_atp z3_tptp "Z3" ["3.0"]
-      (K (250, z3_tff0, "mono_simple", combsN) (* FUDGE *))
+      (K (250, z3_tff0, "mono_simple", combsN, false) (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
-      Conjecture (K (500, FOF, "mono_guards??", combsN) (* FUDGE *))
+      Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *))
 val remote_iprover =
   remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
-      (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
+      (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
 val remote_iprover_eq =
   remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
-      (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
+      (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
       [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
-      (K (100, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
+      (K (100, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
 val remote_e_tofof =
   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
       Hypothesis
-      (K (150, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
+      (K (150, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
       [("#START OF PROOF", "Proved Goals:")]
       [(OutOfResources, "Too many function symbols"),
        (Crashed, "Unrecoverable Segmentation Fault")]
       Hypothesis Hypothesis
-      (K (50, CNF_UEQ, "mono_tags??", combsN) (* FUDGE *))
+      (K (50, CNF_UEQ, "mono_tags??", combsN, false) (* FUDGE *))
 
 (* Setup *)
 
 fun add_atp (name, config) thy =
   Data.map (Symtab.update_new (name, (config, stamp ()))) thy