added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option

--- a/NEWS	Thu May 12 15:29:18 2011 +0200
+++ b/NEWS	Thu May 12 15:29:18 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" and "monomorphize_limit" options.
+  - Added "type_sys", "max_mono_iters", and "max_mono_instances" options.
 
 * "try":
   - Added "simp:", "intro:", and "elim:" options.

--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu May 12 15:29:18 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu May 12 15:29:18 2011 +0200
@@ -390,6 +390,7 @@
 \item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or
 \textit{smart}.
 \item[$\bullet$] \qtybf{int\/}: An integer.
+%\item[$\bullet$] \qtybf{float\/}: A floating-point number (e.g., 2.5).
 \item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers
 (e.g., 0.6 0.95).
 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
@@ -647,11 +648,16 @@
 
 For SMT solvers and ToFoF-E, the type system is always \textit{simple\_types}.
 
-\opdefault{monomorphize\_limit}{int}{\upshape 4}
+\opdefault{max\_mono\_iters}{int}{\upshape 4}
 Specifies the maximum number of iterations for the monomorphization fixpoint
 construction. The higher this limit is, the more monomorphic instances are
 potentially generated. Whether monomorphization takes place depends on the
 type system used.
+
+\opdefault{max\_mono\_instances}{int}{\upshape 500}
+Specifies the maximum number of monomorphic instances to generate as a soft
+limit. The higher this limit is, the more monomorphic instances are potentially
+generated. Whether monomorphization takes place depends on the type system used.
 \end{enum}
 
 \subsection{Relevance Filter}

--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:18 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:18 2011 +0200
@@ -169,7 +169,7 @@
       | keep (c :: cs) = c :: keep cs
   in String.explode #> rev #> keep #> rev #> String.implode end
 
-val max_readable_name_size = 24
+val max_readable_name_size = 20
 
 (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
    problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 15:29:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 15:29:18 2011 +0200
@@ -82,7 +82,8 @@
    ("type_sys", "smart"),
    ("relevance_thresholds", "0.45 0.85"),
    ("max_relevant", "smart"),
-   ("monomorphize_limit", "4"),
+   ("max_mono_iters", "4"),
+   ("max_mono_instances", "500"),
    ("explicit_apply", "false"),
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1"),
@@ -103,8 +104,8 @@
    ("no_slicing", "slicing")]
 
 val params_for_minimize =
-  ["debug", "verbose", "overlord", "type_sys", "full_types", "isar_proof",
-   "isar_shrink_factor", "timeout"]
+  ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
+   "max_mono_instances", "isar_proof", "isar_shrink_factor", "timeout"]
 
 val property_dependent_params = ["provers", "full_types", "timeout"]
 
@@ -245,7 +246,8 @@
       | s => Dumb_Type_Sys (type_sys_from_string s)
     val relevance_thresholds = lookup_real_pair "relevance_thresholds"
     val max_relevant = lookup_int_option "max_relevant"
-    val monomorphize_limit = lookup_int "monomorphize_limit"
+    val max_mono_iters = lookup_int "max_mono_iters"
+    val max_mono_instances = lookup_int "max_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")
@@ -255,10 +257,11 @@
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
      provers = provers, relevance_thresholds = relevance_thresholds,
-     max_relevant = max_relevant, monomorphize_limit = monomorphize_limit,
-     type_sys = type_sys, explicit_apply = explicit_apply,
-     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
-     slicing = slicing, timeout = timeout, expect = expect}
+     max_relevant = max_relevant, max_mono_iters = max_mono_iters,
+     max_mono_instances = max_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}
   end
 
 fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 12 15:29:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 12 15:29:18 2011 +0200
@@ -42,8 +42,9 @@
 
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
-fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit,
-                 type_sys, isar_proof, isar_shrink_factor, ...} : params)
+fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
+                 max_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
@@ -65,9 +66,9 @@
       {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,
-       monomorphize_limit = monomorphize_limit, isar_proof = isar_proof,
-       isar_shrink_factor = isar_shrink_factor, slicing = false,
-       timeout = timeout, expect = ""}
+       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 = ""}
     val facts =
       facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
     val problem =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:18 2011 +0200
@@ -28,7 +28,8 @@
      type_sys: rich_type_system,
      relevance_thresholds: real * real,
      max_relevant: int option,
-     monomorphize_limit: int,
+     max_mono_iters: int,
+     max_mono_instances: int,
      explicit_apply: bool,
      isar_proof: bool,
      isar_shrink_factor: int,
@@ -238,7 +239,8 @@
    type_sys: rich_type_system,
    relevance_thresholds: real * real,
    max_relevant: int option,
-   monomorphize_limit: int,
+   max_mono_iters: int,
+   max_mono_instances: int,
    explicit_apply: bool,
    isar_proof: bool,
    isar_shrink_factor: int,
@@ -361,12 +363,20 @@
     |> 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 =
+  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))
+
 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, monomorphize_limit,
-          explicit_apply, isar_proof, isar_shrink_factor, slicing, timeout, ...}
-         : params)
+        ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
+          max_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
@@ -411,10 +421,6 @@
             val num_actual_slices = length actual_slices
             fun monomorphize_facts facts =
               let
-                val repair_context =
-                  Config.put SMT_Config.verbose debug
-                  #> Config.put SMT_Config.monomorph_full false
-                  #> Config.put SMT_Config.monomorph_limit monomorphize_limit
                 val facts = facts |> map untranslated_fact
                 (* pseudo-theorem involving the same constants as the subgoal *)
                 val subgoal_th =
@@ -423,10 +429,12 @@
                 val indexed_facts =
                   (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
               in
-                SMT_Monomorph.monomorph indexed_facts (repair_context ctxt)
-                |> fst |> sort (int_ord o pairself fst)
-                |> filter_out (curry (op =) ~1 o fst)
-                |> map (Untranslated_Fact o apfst (fst o nth facts))
+                ctxt |> repair_smt_monomorph_context debug max_mono_iters
+                            max_mono_instances (length facts)
+                     |> SMT_Monomorph.monomorph indexed_facts
+                     |> fst |> sort (int_ord o pairself fst)
+                     |> filter_out (curry (op =) ~1 o fst)
+                     |> map (Untranslated_Fact o apfst (fst o nth facts))
               end
             fun run_slice blacklist (slice, (time_frac, (complete,
                                        (best_max_relevant, best_type_systems))))
@@ -655,28 +663,28 @@
   Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5)
 
 fun smt_filter_loop ctxt name
-                    ({debug, verbose, overlord, monomorphize_limit, timeout,
-                      slicing, ...} : params)
+                    ({debug, verbose, overlord, max_mono_iters,
+                      max_mono_instances, timeout, slicing, ...} : params)
                     state i smt_filter =
   let
     val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
     val repair_context =
-      select_smt_solver name
-      #> Config.put SMT_Config.verbose debug
-      #> (if overlord then
-            Config.put SMT_Config.debug_files
-                       (overlord_file_location_for_prover name
-                        |> (fn (path, name) => path ^ "/" ^ name))
-          else
-            I)
-      #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
-      #> Config.put SMT_Config.monomorph_full false
-      #> Config.put SMT_Config.monomorph_limit monomorphize_limit
+          select_smt_solver name
+          #> (if overlord then
+                Config.put SMT_Config.debug_files
+                           (overlord_file_location_for_prover name
+                            |> (fn (path, name) => path ^ "/" ^ name))
+              else
+                I)
+          #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
     val state = state |> Proof.map_context repair_context
-
     fun do_slice timeout slice outcome0 time_so_far facts =
       let
         val timer = Timer.startRealTimer ()
+        val state =
+          state |> Proof.map_context
+                       (repair_smt_monomorph_context debug max_mono_iters
+                            max_mono_instances (length facts))
         val ms = timeout |> Time.toMilliseconds
         val slice_timeout =
           if slice < max_slices then