# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 31334a7b109d9a698ecdbf7edaff65bb62c78e4a
# Parent  017e5dac8642727b3bd3c9117398c6fe5743dedd
renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly

diff -r 017e5dac8642 -r 31334a7b109d NEWS
--- a/NEWS	Thu May 12 15:29:19 2011 +0200
+++ b/NEWS	Thu May 12 15:29:19 2011 +0200
@@ -69,7 +69,7 @@
     INCOMPATIBILITY.
   - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
     TPTP problems (TFF).
-  - Added "type_sys", "max_mono_iters", and "max_mono_instances" options.
+  - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options.
 
 * "try":
   - Added "simp:", "intro:", and "elim:" options.
diff -r 017e5dac8642 -r 31334a7b109d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 15:29:19 2011 +0200
@@ -82,8 +82,8 @@
    ("type_sys", "smart"),
    ("relevance_thresholds", "0.45 0.85"),
    ("max_relevant", "smart"),
-   ("max_mono_iters", "4"),
-   ("max_mono_instances", "500"),
+   ("max_mono_iters", "5"),
+   ("max_new_mono_instances", "250"),
    ("explicit_apply", "false"),
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1"),
@@ -105,7 +105,7 @@
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
-   "max_mono_instances", "isar_proof", "isar_shrink_factor", "timeout"]
+   "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout"]
 
 val property_dependent_params = ["provers", "full_types", "timeout"]
 
@@ -249,7 +249,7 @@
     val relevance_thresholds = lookup_real_pair "relevance_thresholds"
     val max_relevant = lookup_int_option "max_relevant"
     val max_mono_iters = lookup_int "max_mono_iters"
-    val max_mono_instances = lookup_int "max_mono_instances"
+    val max_new_mono_instances = lookup_int "max_new_mono_instances"
     val explicit_apply = lookup_bool "explicit_apply"
     val isar_proof = lookup_bool "isar_proof"
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
@@ -260,7 +260,7 @@
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
      provers = provers, relevance_thresholds = relevance_thresholds,
      max_relevant = max_relevant, max_mono_iters = max_mono_iters,
-     max_mono_instances = max_mono_instances, type_sys = type_sys,
+     max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
      explicit_apply = explicit_apply, isar_proof = isar_proof,
      isar_shrink_factor = isar_shrink_factor, slicing = slicing,
      timeout = timeout, expect = expect}
diff -r 017e5dac8642 -r 31334a7b109d src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 12 15:29:19 2011 +0200
@@ -43,8 +43,8 @@
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
-                 max_mono_instances, type_sys, isar_proof, isar_shrink_factor,
-                 ...} : params)
+                 max_new_mono_instances, type_sys, isar_proof,
+                 isar_shrink_factor, ...} : params)
         explicit_apply_opt silent (prover : prover) timeout i n state facts =
   let
     val thy = Proof.theory_of state
@@ -66,9 +66,10 @@
       {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
        provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
        relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
-       max_mono_iters = max_mono_iters, max_mono_instances = max_mono_instances,
-       isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
-       slicing = false, timeout = timeout, expect = ""}
+       max_mono_iters = max_mono_iters,
+       max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
+       isar_shrink_factor = isar_shrink_factor, slicing = false,
+       timeout = timeout, expect = ""}
     val facts =
       facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
     val problem =
diff -r 017e5dac8642 -r 31334a7b109d src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
@@ -29,7 +29,7 @@
      relevance_thresholds: real * real,
      max_relevant: int option,
      max_mono_iters: int,
-     max_mono_instances: int,
+     max_new_mono_instances: int,
      explicit_apply: bool,
      isar_proof: bool,
      isar_shrink_factor: int,
@@ -240,7 +240,7 @@
    relevance_thresholds: real * real,
    max_relevant: int option,
    max_mono_iters: int,
-   max_mono_instances: int,
+   max_new_mono_instances: int,
    explicit_apply: bool,
    isar_proof: bool,
    isar_shrink_factor: int,
@@ -419,20 +419,18 @@
     |> find_first (if full_types then is_type_sys_virtually_sound else K true)
     |> the |> adjust_dumb_type_sys formats
 
-fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances
-                                 num_facts =
+fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
   Config.put SMT_Config.verbose debug
   #> Config.put SMT_Config.monomorph_full false
   #> Config.put SMT_Config.monomorph_limit max_mono_iters
-  #> Config.put SMT_Config.monomorph_instances
-                (Int.max (max_mono_instances, num_facts))
+  #> Config.put SMT_Config.monomorph_instances max_mono_instances
 
 fun run_atp auto name
         ({exec, required_execs, arguments, proof_delims, known_failures,
           conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
         ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
-          max_mono_instances, explicit_apply, isar_proof, isar_shrink_factor,
-          slicing, timeout, ...} : params)
+          max_new_mono_instances, explicit_apply, isar_proof,
+          isar_shrink_factor, slicing, timeout, ...} : params)
         minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
@@ -484,12 +482,14 @@
                   |> Skip_Proof.make_thm thy
                 val indexed_facts =
                   (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
+                val max_mono_instances = max_new_mono_instances + length facts
               in
                 ctxt |> repair_smt_monomorph_context debug max_mono_iters
-                            max_mono_instances (length facts)
+                                                     max_mono_instances
                      |> SMT_Monomorph.monomorph indexed_facts
                      |> fst |> sort (int_ord o pairself fst)
                      |> filter_out (curry (op =) ~1 o fst)
+(* FIXME:            |> take max_mono_instances (* just in case *) *)
                      |> map (Untranslated_Fact o apfst (fst o nth facts))
               end
             fun run_slice blacklist (slice, (time_frac, (complete,
@@ -720,7 +720,7 @@
 
 fun smt_filter_loop ctxt name
                     ({debug, verbose, overlord, max_mono_iters,
-                      max_mono_instances, timeout, slicing, ...} : params)
+                      max_new_mono_instances, timeout, slicing, ...} : params)
                     state i smt_filter =
   let
     val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
@@ -740,7 +740,7 @@
         val state =
           state |> Proof.map_context
                        (repair_smt_monomorph_context debug max_mono_iters
-                            max_mono_instances (length facts))
+                            (max_new_mono_instances + length facts))
         val ms = timeout |> Time.toMilliseconds
         val slice_timeout =
           if slice < max_slices then