# HG changeset patch
# User blanchet
# Date 1378885848 -7200
# Node ID f5b678b155f667ef9bfd2db75f911b69ad4ca766
# Parent  fa5b34ffe4a400a674ac5d89b98cb3b9b1fdc7da
adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)

diff -r fa5b34ffe4a4 -r f5b678b155f6 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 10 16:02:02 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 11 09:50:48 2013 +0200
@@ -91,7 +91,7 @@
 (* ATP configuration *)
 
 val default_max_mono_iters = 3 (* FUDGE *)
-val default_max_new_mono_instances = 200 (* FUDGE *)
+val default_max_new_mono_instances = 100 (* FUDGE *)
 
 type slice_spec = (int * string) * atp_format * string * string * bool
 
@@ -225,7 +225,7 @@
      (* FUDGE *)
      K [(1.0, (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
-   best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
+   best_max_new_mono_instances = default_max_new_mono_instances}
 
 val agsyhol = (agsyholN, fn () => agsyhol_config)
 
@@ -480,7 +480,7 @@
      (* FUDGE *)
      K [(1.0, (((40, ""), leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
-   best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
+   best_max_new_mono_instances = default_max_new_mono_instances}
 
 val leo2 = (leo2N, fn () => leo2_config)
 
@@ -502,7 +502,7 @@
      (* FUDGE *)
      K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
-   best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
+   best_max_new_mono_instances = default_max_new_mono_instances}
 
 val satallax = (satallaxN, fn () => satallax_config)
 
@@ -609,7 +609,7 @@
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I),
    best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = default_max_new_mono_instances}
+   best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
 
 val vampire = (vampireN, fn () => vampire_config)
 
@@ -633,7 +633,7 @@
         (0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")),
         (0.125, (((31, meshN), z3_tff0, "mono_native", combsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = default_max_new_mono_instances}
+   best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
 
 val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)