# HG changeset patch
# User blanchet
# Date 1305793453 -7200
# Node ID de1fe9eaf3f42569e95fc40fe84ea4d44a7c8a65
# Parent  40649ab0ceada11cb5167c48ba1f917763e9d581
tweaked ATP type systems further based on Judgment Day

diff -r 40649ab0cead -r de1fe9eaf3f4 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu May 19 10:24:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 19 10:24:13 2011 +0200
@@ -222,11 +222,12 @@
    best_slices = fn ctxt =>
      (* FUDGE *)
      if effective_e_weight_method ctxt = e_slicesN then
-       [(0.333, (true, (100, ["mangled_preds?"]))) (* sym_offset_weight *),
-        (0.333, (true, (800, ["poly_tags!"]))) (* auto *),
-        (0.334, (true, (200, ["mangled_preds?"]))) (* fun_weight *)]
+       [(0.333, (true, (100, ["poly_preds"]))) (* sym_offset_weight *),
+        (0.333, (true, (800, ["mangled_preds_heavy"]))) (* auto *),
+        (0.334, (true, (200, ["mangled_tags!", "mangled_tags?"])))
+                                                               (* fun_weight *)]
      else
-       [(1.0, (true, (250, ["mangled_preds?"])))]}
+       [(1.0, (true, (200, ["mangled_tags!", "mangled_tags?"])))]}
 
 val e = (eN, e_config)
 
@@ -244,7 +245,7 @@
    arguments = fn ctxt => fn slice => fn timeout => fn _ =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
-     |> (slice = 0 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
+     |> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
      known_perl_failures @
@@ -260,8 +261,9 @@
    formats = [Fof],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.667, (false, (150, ["mangled_preds"]))) (* SOS *),
-      (0.333, (true, (150, ["mangled_preds"]))) (* ~SOS *)]
+     [(0.333, (false, (150, ["mangled_preds_heavy"]))) (* SOS *),
+      (0.333, (false, (150, ["mangled_preds?"]))) (* SOS *),
+      (0.334, (true, (150, ["poly_preds"]))) (* ~SOS *)]
      |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -279,7 +281,7 @@
    arguments = fn ctxt => fn slice => fn timeout => fn _ =>
      "--proof tptp --mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
      " --thanks \"Andrei and Krystof\" --input_file"
-     |> (slice = 0 orelse Config.get ctxt vampire_force_sos)
+     |> (slice < 2 orelse Config.get ctxt vampire_force_sos)
         ? prefix "--sos on ",
    proof_delims =
      [("=========== Refutation ==========",
@@ -301,8 +303,9 @@
    formats = [Fof],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.667, (false, (450, ["mangled_tags!", "mangled_preds?"]))) (* SOS *),
-      (0.333, (true, (450, ["mangled_tags!", "mangled_preds?"]))) (* ~SOS *)]
+     [(0.333, (false, (400, ["mangled_preds_heavy"]))) (* SOS *),
+      (0.333, (false, (400, ["mangled_tags?"]))) (* SOS *),
+      (0.334, (true, (400, ["poly_preds"]))) (* ~SOS *)]
      |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -406,7 +409,7 @@
              Axiom Conjecture [Tff] (K (200, ["simple_types"]) (* FUDGE *))
 val remote_sine_e =
   remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof]
-             (K (500, ["poly_args"]) (* FUDGE *))
+             (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Conjecture
diff -r 40649ab0cead -r de1fe9eaf3f4 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 19 10:24:13 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 19 10:24:13 2011 +0200
@@ -404,8 +404,7 @@
 val atp_important_message_keep_quotient = 10
 
 val fallback_best_type_systems =
-  [Preds (Polymorphic, Const_Arg_Types, Light),
-   Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]
+  [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]
 
 fun adjust_dumb_type_sys formats (Simple_Types level) =
     if member (op =) formats Tff then (Tff, Simple_Types level)