src/HOL/Tools/ATP/atp_systems.ML
changeset 53515 f5b678b155f6
parent 53225 16235bb41881
child 53586 bd5fa6425993
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 10 16:02:02 2013 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 11 09:50:48 2013 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4  (* ATP configuration *)
     1.5  
     1.6  val default_max_mono_iters = 3 (* FUDGE *)
     1.7 -val default_max_new_mono_instances = 200 (* FUDGE *)
     1.8 +val default_max_new_mono_instances = 100 (* FUDGE *)
     1.9  
    1.10  type slice_spec = (int * string) * atp_format * string * string * bool
    1.11  
    1.12 @@ -225,7 +225,7 @@
    1.13       (* FUDGE *)
    1.14       K [(1.0, (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), ""))],
    1.15     best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    1.16 -   best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
    1.17 +   best_max_new_mono_instances = default_max_new_mono_instances}
    1.18  
    1.19  val agsyhol = (agsyholN, fn () => agsyhol_config)
    1.20  
    1.21 @@ -480,7 +480,7 @@
    1.22       (* FUDGE *)
    1.23       K [(1.0, (((40, ""), leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
    1.24     best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    1.25 -   best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
    1.26 +   best_max_new_mono_instances = default_max_new_mono_instances}
    1.27  
    1.28  val leo2 = (leo2N, fn () => leo2_config)
    1.29  
    1.30 @@ -502,7 +502,7 @@
    1.31       (* FUDGE *)
    1.32       K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
    1.33     best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    1.34 -   best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
    1.35 +   best_max_new_mono_instances = default_max_new_mono_instances}
    1.36  
    1.37  val satallax = (satallaxN, fn () => satallax_config)
    1.38  
    1.39 @@ -609,7 +609,7 @@
    1.40       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
    1.41           else I),
    1.42     best_max_mono_iters = default_max_mono_iters,
    1.43 -   best_max_new_mono_instances = default_max_new_mono_instances}
    1.44 +   best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
    1.45  
    1.46  val vampire = (vampireN, fn () => vampire_config)
    1.47  
    1.48 @@ -633,7 +633,7 @@
    1.49          (0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")),
    1.50          (0.125, (((31, meshN), z3_tff0, "mono_native", combsN, false), ""))],
    1.51     best_max_mono_iters = default_max_mono_iters,
    1.52 -   best_max_new_mono_instances = default_max_new_mono_instances}
    1.53 +   best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
    1.54  
    1.55  val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
    1.56