1.1 --- a/NEWS	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/NEWS	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4      INCOMPATIBILITY.
     1.5    - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
     1.6      TPTP problems (TFF).
     1.7 -  - Added "type_sys", "max_mono_iters", and "max_mono_instances" options.
     1.8 +  - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options.
     1.9  
    1.10  * "try":
    1.11    - Added "simp:", "intro:", and "elim:" options.

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 15:29:19 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 15:29:19 2011 +0200
     2.3 @@ -82,8 +82,8 @@
     2.4     ("type_sys", "smart"),
     2.5     ("relevance_thresholds", "0.45 0.85"),
     2.6     ("max_relevant", "smart"),
     2.7 -   ("max_mono_iters", "4"),
     2.8 -   ("max_mono_instances", "500"),
     2.9 +   ("max_mono_iters", "5"),
    2.10 +   ("max_new_mono_instances", "250"),
    2.11     ("explicit_apply", "false"),
    2.12     ("isar_proof", "false"),
    2.13     ("isar_shrink_factor", "1"),
    2.14 @@ -105,7 +105,7 @@
    2.15  
    2.16  val params_for_minimize =
    2.17    ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
    2.18 -   "max_mono_instances", "isar_proof", "isar_shrink_factor", "timeout"]
    2.19 +   "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout"]
    2.20  
    2.21  val property_dependent_params = ["provers", "full_types", "timeout"]
    2.22  
    2.23 @@ -249,7 +249,7 @@
    2.24      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    2.25      val max_relevant = lookup_int_option "max_relevant"
    2.26      val max_mono_iters = lookup_int "max_mono_iters"
    2.27 -    val max_mono_instances = lookup_int "max_mono_instances"
    2.28 +    val max_new_mono_instances = lookup_int "max_new_mono_instances"
    2.29      val explicit_apply = lookup_bool "explicit_apply"
    2.30      val isar_proof = lookup_bool "isar_proof"
    2.31      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    2.32 @@ -260,7 +260,7 @@
    2.33      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    2.34       provers = provers, relevance_thresholds = relevance_thresholds,
    2.35       max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    2.36 -     max_mono_instances = max_mono_instances, type_sys = type_sys,
    2.37 +     max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
    2.38       explicit_apply = explicit_apply, isar_proof = isar_proof,
    2.39       isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    2.40       timeout = timeout, expect = expect}

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 12 15:29:19 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 12 15:29:19 2011 +0200
     3.3 @@ -43,8 +43,8 @@
     3.4  fun print silent f = if silent then () else Output.urgent_message (f ())
     3.5  
     3.6  fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
     3.7 -                 max_mono_instances, type_sys, isar_proof, isar_shrink_factor,
     3.8 -                 ...} : params)
     3.9 +                 max_new_mono_instances, type_sys, isar_proof,
    3.10 +                 isar_shrink_factor, ...} : params)
    3.11          explicit_apply_opt silent (prover : prover) timeout i n state facts =
    3.12    let
    3.13      val thy = Proof.theory_of state
    3.14 @@ -66,9 +66,10 @@
    3.15        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
    3.16         provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    3.17         relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
    3.18 -       max_mono_iters = max_mono_iters, max_mono_instances = max_mono_instances,
    3.19 -       isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    3.20 -       slicing = false, timeout = timeout, expect = ""}
    3.21 +       max_mono_iters = max_mono_iters,
    3.22 +       max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    3.23 +       isar_shrink_factor = isar_shrink_factor, slicing = false,
    3.24 +       timeout = timeout, expect = ""}
    3.25      val facts =
    3.26        facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
    3.27      val problem =

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
     4.3 @@ -29,7 +29,7 @@
     4.4       relevance_thresholds: real * real,
     4.5       max_relevant: int option,
     4.6       max_mono_iters: int,
     4.7 -     max_mono_instances: int,
     4.8 +     max_new_mono_instances: int,
     4.9       explicit_apply: bool,
    4.10       isar_proof: bool,
    4.11       isar_shrink_factor: int,
    4.12 @@ -240,7 +240,7 @@
    4.13     relevance_thresholds: real * real,
    4.14     max_relevant: int option,
    4.15     max_mono_iters: int,
    4.16 -   max_mono_instances: int,
    4.17 +   max_new_mono_instances: int,
    4.18     explicit_apply: bool,
    4.19     isar_proof: bool,
    4.20     isar_shrink_factor: int,
    4.21 @@ -419,20 +419,18 @@
    4.22      |> find_first (if full_types then is_type_sys_virtually_sound else K true)
    4.23      |> the |> adjust_dumb_type_sys formats
    4.24  
    4.25 -fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances
    4.26 -                                 num_facts =
    4.27 +fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
    4.28    Config.put SMT_Config.verbose debug
    4.29    #> Config.put SMT_Config.monomorph_full false
    4.30    #> Config.put SMT_Config.monomorph_limit max_mono_iters
    4.31 -  #> Config.put SMT_Config.monomorph_instances
    4.32 -                (Int.max (max_mono_instances, num_facts))
    4.33 +  #> Config.put SMT_Config.monomorph_instances max_mono_instances
    4.34  
    4.35  fun run_atp auto name
    4.36          ({exec, required_execs, arguments, proof_delims, known_failures,
    4.37            conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
    4.38          ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
    4.39 -          max_mono_instances, explicit_apply, isar_proof, isar_shrink_factor,
    4.40 -          slicing, timeout, ...} : params)
    4.41 +          max_new_mono_instances, explicit_apply, isar_proof,
    4.42 +          isar_shrink_factor, slicing, timeout, ...} : params)
    4.43          minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
    4.44    let
    4.45      val thy = Proof.theory_of state
    4.46 @@ -484,12 +482,14 @@
    4.47                    |> Skip_Proof.make_thm thy
    4.48                  val indexed_facts =
    4.49                    (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
    4.50 +                val max_mono_instances = max_new_mono_instances + length facts
    4.51                in
    4.52                  ctxt |> repair_smt_monomorph_context debug max_mono_iters
    4.53 -                            max_mono_instances (length facts)
    4.54 +                                                     max_mono_instances
    4.55                       |> SMT_Monomorph.monomorph indexed_facts
    4.56                       |> fst |> sort (int_ord o pairself fst)
    4.57                       |> filter_out (curry (op =) ~1 o fst)
    4.58 +(* FIXME:            |> take max_mono_instances (* just in case *) *)
    4.59                       |> map (Untranslated_Fact o apfst (fst o nth facts))
    4.60                end
    4.61              fun run_slice blacklist (slice, (time_frac, (complete,
    4.62 @@ -720,7 +720,7 @@
    4.63  
    4.64  fun smt_filter_loop ctxt name
    4.65                      ({debug, verbose, overlord, max_mono_iters,
    4.66 -                      max_mono_instances, timeout, slicing, ...} : params)
    4.67 +                      max_new_mono_instances, timeout, slicing, ...} : params)
    4.68                      state i smt_filter =
    4.69    let
    4.70      val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
    4.71 @@ -740,7 +740,7 @@
    4.72          val state =
    4.73            state |> Proof.map_context
    4.74                         (repair_smt_monomorph_context debug max_mono_iters
    4.75 -                            max_mono_instances (length facts))
    4.76 +                            (max_new_mono_instances + length facts))
    4.77          val ms = timeout |> Time.toMilliseconds
    4.78          val slice_timeout =
    4.79            if slice < max_slices then