lower the monomorphization thresholds for less scalable provers
authorblanchet
Wed May 23 13:28:20 2012 +0200 (2012-05-23)
changeset 47962137883567114
parent 47958 c5f7be4a1734
child 47963 46c73ad5f7c0
lower the monomorphization thresholds for less scalable provers
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 23 12:02:27 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed May 23 13:28:20 2012 +0200
     1.3 @@ -24,8 +24,12 @@
     1.4       known_failures : (failure * string) list,
     1.5       prem_kind : formula_kind,
     1.6       best_slices :
     1.7 -       Proof.context -> (real * (bool * (slice_spec * string))) list}
     1.8 +       Proof.context -> (real * (bool * (slice_spec * string))) list,
     1.9 +     best_max_mono_iters : int,
    1.10 +     best_max_new_mono_instances : int}
    1.11  
    1.12 +  val default_max_mono_iters : int
    1.13 +  val default_max_new_mono_instances : int
    1.14    val force_sos : bool Config.T
    1.15    val term_order : string Config.T
    1.16    val e_smartN : string
    1.17 @@ -76,6 +80,9 @@
    1.18  
    1.19  (* ATP configuration *)
    1.20  
    1.21 +val default_max_mono_iters = 3 (* FUDGE *)
    1.22 +val default_max_new_mono_instances = 200 (* FUDGE *)
    1.23 +
    1.24  type slice_spec = int * atp_format * string * string * bool
    1.25  
    1.26  type atp_config =
    1.27 @@ -88,7 +95,9 @@
    1.28     proof_delims : (string * string) list,
    1.29     known_failures : (failure * string) list,
    1.30     prem_kind : formula_kind,
    1.31 -   best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
    1.32 +   best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list,
    1.33 +   best_max_mono_iters : int,
    1.34 +   best_max_new_mono_instances : int}
    1.35  
    1.36  (* "best_slices" must be found empirically, taking a wholistic approach since
    1.37     the ATPs are run in parallel. The "real" component gives the faction of the
    1.38 @@ -193,7 +202,9 @@
    1.39     prem_kind = Hypothesis,
    1.40     best_slices = fn _ =>
    1.41       (* FUDGE *)
    1.42 -     [(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))]}
    1.43 +     [(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))],
    1.44 +   best_max_mono_iters = default_max_mono_iters,
    1.45 +   best_max_new_mono_instances = default_max_new_mono_instances}
    1.46  
    1.47  val alt_ergo = (alt_ergoN, fn () => alt_ergo_config)
    1.48  
    1.49 @@ -307,7 +318,9 @@
    1.50            (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN)))]
    1.51         else
    1.52           [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), heuristic)))]
    1.53 -     end}
    1.54 +     end,
    1.55 +   best_max_mono_iters = default_max_mono_iters,
    1.56 +   best_max_new_mono_instances = default_max_new_mono_instances}
    1.57  
    1.58  val e = (eN, fn () => e_config)
    1.59  
    1.60 @@ -330,7 +343,9 @@
    1.61     prem_kind = Hypothesis,
    1.62     best_slices =
    1.63       (* FUDGE *)
    1.64 -     K [(1.0, (true, ((20, leo2_thf0, "mono_native_higher", keep_lamsN, false), "")))]}
    1.65 +     K [(1.0, (true, ((20, leo2_thf0, "mono_native_higher", keep_lamsN, false), "")))],
    1.66 +   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    1.67 +   best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
    1.68  
    1.69  val leo2 = (leo2N, fn () => leo2_config)
    1.70  
    1.71 @@ -351,7 +366,9 @@
    1.72     prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
    1.73     best_slices =
    1.74       (* FUDGE *)
    1.75 -     K [(1.0, (true, ((120, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]}
    1.76 +     K [(1.0, (true, ((120, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))],
    1.77 +   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    1.78 +   best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
    1.79  
    1.80  val satallax = (satallaxN, fn () => satallax_config)
    1.81  
    1.82 @@ -389,7 +406,9 @@
    1.83       [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false), sosN))),
    1.84        (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false), sosN))),
    1.85        (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))]
    1.86 -     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)}
    1.87 +     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I),
    1.88 +   best_max_mono_iters = default_max_mono_iters,
    1.89 +   best_max_new_mono_instances = default_max_new_mono_instances}
    1.90  
    1.91  val spass_new_H1SOS = "-Heuristic=1 -SOS"
    1.92  val spass_new_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
    1.93 @@ -416,7 +435,9 @@
    1.94        (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H1SOS))),
    1.95        (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
    1.96        (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
    1.97 -      (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0)))]}
    1.98 +      (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0)))],
    1.99 +   best_max_mono_iters = default_max_mono_iters,
   1.100 +   best_max_new_mono_instances = default_max_new_mono_instances}
   1.101  
   1.102  val spass =
   1.103    (spassN, fn () => if is_new_spass_version () then spass_new_config
   1.104 @@ -464,7 +485,9 @@
   1.105           (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN))),
   1.106           (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))])
   1.107       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
   1.108 -         else I)}
   1.109 +         else I),
   1.110 +   best_max_mono_iters = default_max_mono_iters,
   1.111 +   best_max_new_mono_instances = default_max_new_mono_instances}
   1.112  
   1.113  val vampire = (vampireN, fn () => vampire_config)
   1.114  
   1.115 @@ -486,7 +509,9 @@
   1.116       K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))),
   1.117          (0.25, (false, ((125, z3_tff0, "mono_native", combsN, false), ""))),
   1.118          (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))),
   1.119 -        (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))]}
   1.120 +        (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))],
   1.121 +   best_max_mono_iters = default_max_mono_iters,
   1.122 +   best_max_new_mono_instances = default_max_new_mono_instances}
   1.123  
   1.124  val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
   1.125  
   1.126 @@ -503,7 +528,9 @@
   1.127     best_slices =
   1.128       K [(1.0, (false, ((200, format, type_enc,
   1.129                          if is_format_higher_order format then keep_lamsN
   1.130 -                        else combsN, false), "")))]}
   1.131 +                        else combsN, false), "")))],
   1.132 +   best_max_mono_iters = default_max_mono_iters,
   1.133 +   best_max_new_mono_instances = default_max_new_mono_instances}
   1.134  
   1.135  val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
   1.136  val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
   1.137 @@ -561,7 +588,9 @@
   1.138     proof_delims = union (op =) tstp_proof_delims proof_delims,
   1.139     known_failures = known_failures @ known_perl_failures @ known_says_failures,
   1.140     prem_kind = prem_kind,
   1.141 -   best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]}
   1.142 +   best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))],
   1.143 +   best_max_mono_iters = default_max_mono_iters,
   1.144 +   best_max_new_mono_instances = default_max_new_mono_instances}
   1.145  
   1.146  fun remotify_config system_name system_versions best_slice
   1.147          ({proof_delims, known_failures, prem_kind, ...} : atp_config)
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed May 23 12:02:27 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed May 23 13:28:20 2012 +0200
     2.3 @@ -88,8 +88,8 @@
     2.4     ("uncurried_aliases", "smart"),
     2.5     ("relevance_thresholds", "0.45 0.85"),
     2.6     ("max_relevant", "smart"),
     2.7 -   ("max_mono_iters", "3"),
     2.8 -   ("max_new_mono_instances", "200"),
     2.9 +   ("max_mono_iters", "smart"),
    2.10 +   ("max_new_mono_instances", "smart"),
    2.11     ("isar_proof", "false"),
    2.12     ("isar_shrink_factor", "1"),
    2.13     ("slice", "true"),
    2.14 @@ -294,8 +294,9 @@
    2.15      val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
    2.16      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    2.17      val max_relevant = lookup_option lookup_int "max_relevant"
    2.18 -    val max_mono_iters = lookup_int "max_mono_iters"
    2.19 -    val max_new_mono_instances = lookup_int "max_new_mono_instances"
    2.20 +    val max_mono_iters = lookup_option lookup_int "max_mono_iters"
    2.21 +    val max_new_mono_instances =
    2.22 +      lookup_option lookup_int "max_new_mono_instances"
    2.23      val isar_proof = lookup_bool "isar_proof"
    2.24      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    2.25      val slice = mode <> Auto_Try andalso lookup_bool "slice"
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 23 12:02:27 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 23 13:28:20 2012 +0200
     3.3 @@ -30,8 +30,8 @@
     3.4       uncurried_aliases: bool option,
     3.5       relevance_thresholds: real * real,
     3.6       max_relevant: int option,
     3.7 -     max_mono_iters: int,
     3.8 -     max_new_mono_instances: int,
     3.9 +     max_mono_iters: int option,
    3.10 +     max_new_mono_instances: int option,
    3.11       isar_proof: bool,
    3.12       isar_shrink_factor: int,
    3.13       slice: bool,
    3.14 @@ -86,7 +86,7 @@
    3.15    val is_reconstructor : string -> bool
    3.16    val is_atp : theory -> string -> bool
    3.17    val is_smt_prover : Proof.context -> string -> bool
    3.18 -  val is_ho_atp: Proof.context -> string -> bool  
    3.19 +  val is_ho_atp: Proof.context -> string -> bool
    3.20    val is_unit_equational_atp : Proof.context -> string -> bool
    3.21    val is_prover_supported : Proof.context -> string -> bool
    3.22    val is_prover_installed : Proof.context -> string -> bool
    3.23 @@ -295,8 +295,8 @@
    3.24     uncurried_aliases: bool option,
    3.25     relevance_thresholds: real * real,
    3.26     max_relevant: int option,
    3.27 -   max_mono_iters: int,
    3.28 -   max_new_mono_instances: int,
    3.29 +   max_mono_iters: int option,
    3.30 +   max_new_mono_instances: int option,
    3.31     isar_proof: bool,
    3.32     isar_shrink_factor: int,
    3.33     slice: bool,
    3.34 @@ -565,9 +565,11 @@
    3.35        | _ => (name, [])
    3.36    in minimize_command override_params name end
    3.37  
    3.38 -fun repair_monomorph_context max_iters max_new_instances =
    3.39 -  Config.put Monomorph.max_rounds max_iters
    3.40 -  #> Config.put Monomorph.max_new_instances max_new_instances
    3.41 +fun repair_monomorph_context max_iters best_max_iters max_new_instances
    3.42 +                             best_max_new_instances =
    3.43 +  Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
    3.44 +  #> Config.put Monomorph.max_new_instances
    3.45 +         (max_new_instances |> the_default best_max_new_instances)
    3.46    #> Config.put Monomorph.keep_partial_instances false
    3.47  
    3.48  fun suffix_for_mode Auto_Try = "_auto_try"
    3.49 @@ -582,7 +584,8 @@
    3.50  
    3.51  fun run_atp mode name
    3.52          ({exec, required_vars, arguments, proof_delims, known_failures,
    3.53 -          prem_kind, best_slices, ...} : atp_config)
    3.54 +          prem_kind, best_slices, best_max_mono_iters,
    3.55 +          best_max_new_mono_instances, ...} : atp_config)
    3.56          (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
    3.57                      uncurried_aliases, max_relevant, max_mono_iters,
    3.58                      max_new_mono_instances, isar_proof, isar_shrink_factor,
    3.59 @@ -644,8 +647,9 @@
    3.60              fun monomorphize_facts facts =
    3.61                let
    3.62                  val ctxt =
    3.63 -                  ctxt |> repair_monomorph_context max_mono_iters
    3.64 -                                                   max_new_mono_instances
    3.65 +                  ctxt
    3.66 +                  |> repair_monomorph_context max_mono_iters best_max_mono_iters
    3.67 +                          max_new_mono_instances best_max_new_mono_instances
    3.68                  (* pseudo-theorem involving the same constants as the subgoal *)
    3.69                  val subgoal_th =
    3.70                    Logic.list_implies (hyp_ts, concl_t)
    3.71 @@ -923,7 +927,8 @@
    3.72          val state =
    3.73            state |> Proof.map_context
    3.74                         (repair_monomorph_context max_mono_iters
    3.75 -                                                 max_new_mono_instances)
    3.76 +                            default_max_mono_iters max_new_mono_instances
    3.77 +                            default_max_new_mono_instances)
    3.78          val ms = timeout |> Time.toMilliseconds
    3.79          val slice_timeout =
    3.80            if slice < max_slices then