added formats to the slice and use TFF for remote Vampire

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 07:14:09 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 14:44:19 2011 +0200
@@ -21,9 +21,8 @@
      known_failures : (failure * string) list,
      conj_sym_kind : formula_kind,
      prem_kind : formula_kind,
-     formats : format list,
      best_slices :
-       Proof.context -> (real * (bool * (int * string * string))) list}
+       Proof.context -> (real * (bool * (int * format * string * string))) list}
 
   val force_sos : bool Config.T
   val e_smartN : string
@@ -50,8 +49,8 @@
   val remote_prefix : string
   val remote_atp :
     string -> string -> string list -> (string * string) list
-    -> (failure * string) list -> formula_kind -> formula_kind -> format list
-    -> (Proof.context -> int * string) -> string * atp_config
+    -> (failure * string) list -> formula_kind -> formula_kind
+    -> (Proof.context -> int * format * string) -> string * atp_config
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val supported_atps : theory -> string list
@@ -78,9 +77,8 @@
    known_failures : (failure * string) list,
    conj_sym_kind : formula_kind,
    prem_kind : formula_kind,
-   formats : format list,
    best_slices :
-     Proof.context -> (real * (bool * (int * string * string))) list}
+     Proof.context -> (real * (bool * (int * format * string * string))) list}
 
 (* "best_slices" must be found empirically, taking a wholistic approach since
    the ATPs are run in parallel. The "real" components give the faction of the
@@ -214,16 +212,15 @@
       (OutOfResources, "SZS status ResourceOut")],
    conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
-   formats = [FOF],
    best_slices = fn ctxt =>
      let val method = effective_e_weight_method ctxt in
        (* FUDGE *)
        if method = e_smartN then
-         [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))),
-          (0.334, (true, (50, "mangled_guards?", e_fun_weightN))),
-          (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
+         [(0.333, (true, (500, FOF, "mangled_tags?", e_fun_weightN))),
+          (0.334, (true, (50, FOF, "mangled_guards?", e_fun_weightN))),
+          (0.333, (true, (1000, FOF, "mangled_tags?", e_sym_offset_weightN)))]
        else
-         [(1.0, (true, (500, "mangled_tags?", method)))]
+         [(1.0, (true, (500, FOF, "mangled_tags?", method)))]
      end}
 
 val e = (eN, e_config)
@@ -242,11 +239,10 @@
    known_failures = [],
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
-   formats = [THF Without_Choice, FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.667, (false, (150, "simple_higher", sosN))),
-      (0.333, (true, (50, "simple_higher", no_sosN)))]
+     [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))),
+      (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -265,8 +261,8 @@
    known_failures = [(ProofMissing, "SZS status Theorem")],
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
-   formats = [THF With_Choice],
-   best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
+   best_slices =
+     K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)}
 
 val satallax = (satallaxN, satallax_config)
 
@@ -295,12 +291,11 @@
       (InternalError, "Please report this error")],
    conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
-   formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, "mangled_tags", sosN))),
-      (0.333, (false, (300, "poly_tags?", sosN))),
-      (0.334, (true, (50, "mangled_tags?", no_sosN)))]
+     [(0.333, (false, (150, FOF, "mangled_tags", sosN))),
+      (0.333, (false, (300, FOF, "poly_tags?", sosN))),
+      (0.334, (true, (50, FOF, "mangled_tags?", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -333,12 +328,11 @@
       (Interrupted, "Aborted by signal SIGINT")],
    conj_sym_kind = Conjecture,
    prem_kind = Conjecture,
-   formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, "poly_guards", sosN))),
-      (0.334, (true, (50, "mangled_guards?", no_sosN))),
-      (0.333, (false, (500, "mangled_tags?", sosN)))]
+     [(0.333, (false, (150, TFF, "poly_guards", sosN))),
+      (0.334, (true, (50, TFF, "mangled_guards?", no_sosN))),
+      (0.333, (false, (500, TFF, "mangled_tags?", sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -361,13 +355,12 @@
       (ProofMissing, "SZS status Unsatisfiable")],
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
-   formats = [FOF],
    best_slices =
      (* FUDGE (FIXME) *)
-     K [(0.5, (false, (250, "mangled_guards?", ""))),
-        (0.25, (false, (125, "mangled_guards?", ""))),
-        (0.125, (false, (62, "mangled_guards?", ""))),
-        (0.125, (false, (31, "mangled_guards?", "")))]}
+     K [(0.5, (false, (250, FOF, "mangled_guards?", ""))),
+        (0.25, (false, (125, FOF, "mangled_guards?", ""))),
+        (0.125, (false, (62, FOF, "mangled_guards?", ""))),
+        (0.125, (false, (31, FOF, "mangled_guards?", "")))]}
 
 val z3_atp = (z3_atpN, z3_atp_config)
 
@@ -407,7 +400,7 @@
 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
 
 fun remote_config system_name system_versions proof_delims known_failures
-                  conj_sym_kind prem_kind formats best_slice : atp_config =
+                  conj_sym_kind prem_kind best_slice : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
@@ -425,58 +418,58 @@
       (Inappropriate, "says Inappropriate")],
    conj_sym_kind = conj_sym_kind,
    prem_kind = prem_kind,
-   formats = formats,
    best_slices = fn ctxt =>
-     let val (max_relevant, type_enc) = best_slice ctxt in
-       [(1.0, (false, (max_relevant, type_enc, "")))]
+     let val (max_relevant, format, type_enc) = best_slice ctxt in
+       [(1.0, (false, (max_relevant, format, type_enc, "")))]
      end}
 
 fun remotify_config system_name system_versions best_slice
-        ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, ...}
+        ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
          : atp_config) : atp_config =
   remote_config system_name system_versions proof_delims known_failures
-                conj_sym_kind prem_kind formats best_slice
+                conj_sym_kind prem_kind best_slice
 
 fun remote_atp name system_name system_versions proof_delims known_failures
-        conj_sym_kind prem_kind formats best_slice =
+               conj_sym_kind prem_kind best_slice =
   (remote_prefix ^ name,
    remote_config system_name system_versions proof_delims known_failures
-                 conj_sym_kind prem_kind formats best_slice)
+                 conj_sym_kind prem_kind best_slice)
 fun remotify_atp (name, config) system_name system_versions best_slice =
   (remote_prefix ^ name,
    remotify_config system_name system_versions best_slice config)
 
 val remote_e =
   remotify_atp e "EP" ["1.0", "1.1", "1.2"]
-               (K (750, "mangled_tags?") (* FUDGE *))
+               (K (750, FOF, "mangled_tags?") (* FUDGE *))
 val remote_leo2 =
   remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
-               (K (100, "simple_higher") (* FUDGE *))
+               (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
 val remote_satallax =
   remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
-               (K (100, "simple_higher") (* FUDGE *))
+               (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
 val remote_vampire =
-  remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
-               (K (200, "mangled_guards?") (* FUDGE *))
+  remotify_atp vampire "Vampire" ["1.8"]
+               (K (200, TFF, "mangled_guards?") (* FUDGE *))
 val remote_z3_atp =
-  remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
+  remotify_atp z3_atp "Z3" ["2.18"]
+               (K (250, FOF, "mangled_guards?") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
-             Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
+             Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
-             [TFF, FOF] (K (100, "simple") (* FUDGE *))
+             (K (100, TFF, "simple") (* FUDGE *))
 val remote_e_tofof =
   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
-             Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
+             Axiom Hypothesis (K (150, TFF, "simple") (* 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 [CNF_UEQ]
-             (K (50, "mangled_tags?") (* FUDGE *))
+             Hypothesis Hypothesis
+             (K (50, CNF_UEQ, "mangled_tags?") (* FUDGE *))
 
 (* Setup *)
 

--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 07:14:09 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 14:44:19 2011 +0200
@@ -90,7 +90,7 @@
   val level_of_type_enc : type_enc -> type_level
   val is_type_enc_quasi_sound : type_enc -> bool
   val is_type_enc_fairly_sound : type_enc -> bool
-  val choose_format : format list -> type_enc -> format * type_enc
+  val adjust_type_enc : format -> type_enc -> type_enc
   val mk_aconns :
     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
   val unmangled_const : string -> string * (string, 'b) ho_term list
@@ -611,23 +611,14 @@
   | is_type_level_monotonicity_based Fin_Nonmono_Types = true
   | is_type_level_monotonicity_based _ = false
 
-fun choose_format formats (Simple_Types (order, level)) =
-    (case find_first is_format_thf formats of
-       SOME format => (format, Simple_Types (order, level))
-     | NONE =>
-       if member (op =) formats TFF then
-         (TFF, Simple_Types (First_Order, level))
-       else
-         choose_format formats (Guards (Mangled_Monomorphic, level, Uniform)))
-  | choose_format formats type_enc =
-    (case hd formats of
-       CNF_UEQ =>
-       (CNF_UEQ, case type_enc of
-                   Guards stuff =>
-                   (if is_type_enc_fairly_sound type_enc then Tags else Guards)
-                       stuff
-                 | _ => type_enc)
-     | format => (format, type_enc))
+fun adjust_type_enc (THF _) type_enc = type_enc
+  | adjust_type_enc TFF (Simple_Types (Higher_Order, level)) =
+    Simple_Types (First_Order, level)
+  | adjust_type_enc format (Simple_Types (_, level)) =
+    adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
+  | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
+    (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
+  | adjust_type_enc _ type_enc = type_enc
 
 fun lift_lambdas ctxt type_enc =
   map (close_form o Envir.eta_contract) #> rpair ctxt
@@ -2087,7 +2078,7 @@
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
         lambda_trans readable_names preproc hyp_ts concl_t facts =
   let
-    val (format, type_enc) = choose_format [format] type_enc
+    val type_enc = type_enc |> adjust_type_enc format
     val lambda_trans =
       if lambda_trans = smartN then
         if is_type_enc_higher_order type_enc then lambdasN else combinatorsN

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 23 07:14:09 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 23 14:44:19 2011 +0200
@@ -154,7 +154,9 @@
 fun is_unit_equational_atp ctxt name =
   let val thy = Proof_Context.theory_of ctxt in
     case try (get_atp thy) name of
-      SOME {formats, ...} => member (op =) formats CNF_UEQ
+      SOME {best_slices, ...} =>
+      exists (fn (_, (_, (_, format, _, _))) => format = CNF_UEQ)
+             (best_slices ctxt)
     | NONE => false
   end
 
@@ -512,10 +514,10 @@
    them each time. *)
 val atp_important_message_keep_quotient = 10
 
-fun choose_format_and_type_enc soundness best_type_enc formats =
+fun choose_type_enc soundness best_type_enc format =
   the_default best_type_enc
   #> type_enc_from_string soundness
-  #> choose_format formats
+  #> adjust_type_enc format
 
 val metis_minimize_max_time = seconds 2.0
 
@@ -540,7 +542,7 @@
 
 fun run_atp mode name
         ({exec, required_execs, arguments, proof_delims, known_failures,
-          conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
+          conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
         ({debug, verbose, overlord, type_enc, sound, max_relevant,
           max_mono_iters, max_new_mono_instances, isar_proof,
           isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
@@ -609,7 +611,8 @@
                 |> maps (fn (name, rths) => map (pair name o snd) rths)
               end
             fun run_slice (slice, (time_frac, (complete,
-                                    (best_max_relevant, best_type_enc, extra))))
+                                    (best_max_relevant, format, best_type_enc,
+                                     extra))))
                           time_left =
               let
                 val num_facts =
@@ -623,9 +626,8 @@
                       Sound
                   else
                     Unsound
-                val (format, type_enc) =
-                  choose_format_and_type_enc soundness best_type_enc formats
-                                             type_enc
+                val type_enc =
+                  type_enc |> choose_type_enc soundness best_type_enc format
                 val fairly_sound = is_type_enc_fairly_sound type_enc
                 val facts =
                   facts |> map untranslated_fact