# HG changeset patch
# User desharna
# Date 1634223362 -7200
# Node ID dc1a7c10565b489f8d505826de6299df3dc91ed1
# Parent  2c093a3167d1cb619522335710865acc9ffe50c1
tuned Vampire configuration to use TFX in Sledgehammer

diff -r 2c093a3167d1 -r dc1a7c10565b src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Oct 18 11:15:59 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Oct 14 16:56:02 2021 +0200
@@ -467,7 +467,7 @@
 
 val vampire_config : atp_config =
   let
-    val format = TFF (With_FOOL, Monomorphic)
+    val format = TFF (With_FOOL, Polymorphic)
   in
     {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
@@ -488,9 +488,9 @@
      prem_role = Hypothesis,
      best_slices = fn ctxt =>
        (* FUDGE *)
-       [(0.333, (((500, meshN), format, "mono_native", combs_or_liftingN, false), sosN)),
-        (0.333, (((150, meshN), format, "poly_tags??", combs_or_liftingN, false), sosN)),
-        (0.334, (((50, meshN), format, "mono_native", combs_or_liftingN, false), no_sosN))]
+       [(0.333, (((500, meshN), format, "mono_native_fool", combs_or_liftingN, false), sosN)),
+        (0.333, (((150, meshN), format, "poly_native_fool", combs_or_liftingN, false), sosN)),
+        (0.334, (((50, meshN), format, "mono_native_fool", combs_or_liftingN, false), no_sosN))]
        |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
      best_max_mono_iters = default_max_mono_iters,
      best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}