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

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

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

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 15:29:18 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 15:29:18 2011 +0200
     4.3 @@ -82,7 +82,8 @@
     4.4     ("type_sys", "smart"),
     4.5     ("relevance_thresholds", "0.45 0.85"),
     4.6     ("max_relevant", "smart"),
     4.7 -   ("monomorphize_limit", "4"),
     4.8 +   ("max_mono_iters", "4"),
     4.9 +   ("max_mono_instances", "500"),
    4.10     ("explicit_apply", "false"),
    4.11     ("isar_proof", "false"),
    4.12     ("isar_shrink_factor", "1"),
    4.13 @@ -103,8 +104,8 @@
    4.14     ("no_slicing", "slicing")]
    4.15  
    4.16  val params_for_minimize =
    4.17 -  ["debug", "verbose", "overlord", "type_sys", "full_types", "isar_proof",
    4.18 -   "isar_shrink_factor", "timeout"]
    4.19 +  ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
    4.20 +   "max_mono_instances", "isar_proof", "isar_shrink_factor", "timeout"]
    4.21  
    4.22  val property_dependent_params = ["provers", "full_types", "timeout"]
    4.23  
    4.24 @@ -245,7 +246,8 @@
    4.25        | s => Dumb_Type_Sys (type_sys_from_string s)
    4.26      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    4.27      val max_relevant = lookup_int_option "max_relevant"
    4.28 -    val monomorphize_limit = lookup_int "monomorphize_limit"
    4.29 +    val max_mono_iters = lookup_int "max_mono_iters"
    4.30 +    val max_mono_instances = lookup_int "max_mono_instances"
    4.31      val explicit_apply = lookup_bool "explicit_apply"
    4.32      val isar_proof = lookup_bool "isar_proof"
    4.33      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    4.34 @@ -255,10 +257,11 @@
    4.35    in
    4.36      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    4.37       provers = provers, relevance_thresholds = relevance_thresholds,
    4.38 -     max_relevant = max_relevant, monomorphize_limit = monomorphize_limit,
    4.39 -     type_sys = type_sys, explicit_apply = explicit_apply,
    4.40 -     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    4.41 -     slicing = slicing, timeout = timeout, expect = expect}
    4.42 +     max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    4.43 +     max_mono_instances = max_mono_instances, type_sys = type_sys,
    4.44 +     explicit_apply = explicit_apply, isar_proof = isar_proof,
    4.45 +     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    4.46 +     timeout = timeout, expect = expect}
    4.47    end
    4.48  
    4.49  fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 12 15:29:18 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 12 15:29:18 2011 +0200
     5.3 @@ -42,8 +42,9 @@
     5.4  
     5.5  fun print silent f = if silent then () else Output.urgent_message (f ())
     5.6  
     5.7 -fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit,
     5.8 -                 type_sys, isar_proof, isar_shrink_factor, ...} : params)
     5.9 +fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
    5.10 +                 max_mono_instances, type_sys, isar_proof, isar_shrink_factor,
    5.11 +                 ...} : params)
    5.12          explicit_apply_opt silent (prover : prover) timeout i n state facts =
    5.13    let
    5.14      val thy = Proof.theory_of state
    5.15 @@ -65,9 +66,9 @@
    5.16        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
    5.17         provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    5.18         relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
    5.19 -       monomorphize_limit = monomorphize_limit, isar_proof = isar_proof,
    5.20 -       isar_shrink_factor = isar_shrink_factor, slicing = false,
    5.21 -       timeout = timeout, expect = ""}
    5.22 +       max_mono_iters = max_mono_iters, max_mono_instances = max_mono_instances,
    5.23 +       isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    5.24 +       slicing = false, timeout = timeout, expect = ""}
    5.25      val facts =
    5.26        facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
    5.27      val problem =

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:18 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:18 2011 +0200
     6.3 @@ -28,7 +28,8 @@
     6.4       type_sys: rich_type_system,
     6.5       relevance_thresholds: real * real,
     6.6       max_relevant: int option,
     6.7 -     monomorphize_limit: int,
     6.8 +     max_mono_iters: int,
     6.9 +     max_mono_instances: int,
    6.10       explicit_apply: bool,
    6.11       isar_proof: bool,
    6.12       isar_shrink_factor: int,
    6.13 @@ -238,7 +239,8 @@
    6.14     type_sys: rich_type_system,
    6.15     relevance_thresholds: real * real,
    6.16     max_relevant: int option,
    6.17 -   monomorphize_limit: int,
    6.18 +   max_mono_iters: int,
    6.19 +   max_mono_instances: int,
    6.20     explicit_apply: bool,
    6.21     isar_proof: bool,
    6.22     isar_shrink_factor: int,
    6.23 @@ -361,12 +363,20 @@
    6.24      |> find_first (if full_types then is_type_sys_virtually_sound else K true)
    6.25      |> the |> adjust_dumb_type_sys formats
    6.26  
    6.27 +fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances
    6.28 +                                 num_facts =
    6.29 +  Config.put SMT_Config.verbose debug
    6.30 +  #> Config.put SMT_Config.monomorph_full false
    6.31 +  #> Config.put SMT_Config.monomorph_limit max_mono_iters
    6.32 +  #> Config.put SMT_Config.monomorph_instances
    6.33 +                (Int.max (max_mono_instances, num_facts))
    6.34 +
    6.35  fun run_atp auto name
    6.36          ({exec, required_execs, arguments, proof_delims, known_failures,
    6.37            conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
    6.38 -        ({debug, verbose, overlord, type_sys, max_relevant, monomorphize_limit,
    6.39 -          explicit_apply, isar_proof, isar_shrink_factor, slicing, timeout, ...}
    6.40 -         : params)
    6.41 +        ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
    6.42 +          max_mono_instances, explicit_apply, isar_proof, isar_shrink_factor,
    6.43 +          slicing, timeout, ...} : params)
    6.44          minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
    6.45    let
    6.46      val thy = Proof.theory_of state
    6.47 @@ -411,10 +421,6 @@
    6.48              val num_actual_slices = length actual_slices
    6.49              fun monomorphize_facts facts =
    6.50                let
    6.51 -                val repair_context =
    6.52 -                  Config.put SMT_Config.verbose debug
    6.53 -                  #> Config.put SMT_Config.monomorph_full false
    6.54 -                  #> Config.put SMT_Config.monomorph_limit monomorphize_limit
    6.55                  val facts = facts |> map untranslated_fact
    6.56                  (* pseudo-theorem involving the same constants as the subgoal *)
    6.57                  val subgoal_th =
    6.58 @@ -423,10 +429,12 @@
    6.59                  val indexed_facts =
    6.60                    (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
    6.61                in
    6.62 -                SMT_Monomorph.monomorph indexed_facts (repair_context ctxt)
    6.63 -                |> fst |> sort (int_ord o pairself fst)
    6.64 -                |> filter_out (curry (op =) ~1 o fst)
    6.65 -                |> map (Untranslated_Fact o apfst (fst o nth facts))
    6.66 +                ctxt |> repair_smt_monomorph_context debug max_mono_iters
    6.67 +                            max_mono_instances (length facts)
    6.68 +                     |> SMT_Monomorph.monomorph indexed_facts
    6.69 +                     |> fst |> sort (int_ord o pairself fst)
    6.70 +                     |> filter_out (curry (op =) ~1 o fst)
    6.71 +                     |> map (Untranslated_Fact o apfst (fst o nth facts))
    6.72                end
    6.73              fun run_slice blacklist (slice, (time_frac, (complete,
    6.74                                         (best_max_relevant, best_type_systems))))
    6.75 @@ -655,28 +663,28 @@
    6.76    Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5)
    6.77  
    6.78  fun smt_filter_loop ctxt name
    6.79 -                    ({debug, verbose, overlord, monomorphize_limit, timeout,
    6.80 -                      slicing, ...} : params)
    6.81 +                    ({debug, verbose, overlord, max_mono_iters,
    6.82 +                      max_mono_instances, timeout, slicing, ...} : params)
    6.83                      state i smt_filter =
    6.84    let
    6.85      val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
    6.86      val repair_context =
    6.87 -      select_smt_solver name
    6.88 -      #> Config.put SMT_Config.verbose debug
    6.89 -      #> (if overlord then
    6.90 -            Config.put SMT_Config.debug_files
    6.91 -                       (overlord_file_location_for_prover name
    6.92 -                        |> (fn (path, name) => path ^ "/" ^ name))
    6.93 -          else
    6.94 -            I)
    6.95 -      #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
    6.96 -      #> Config.put SMT_Config.monomorph_full false
    6.97 -      #> Config.put SMT_Config.monomorph_limit monomorphize_limit
    6.98 +          select_smt_solver name
    6.99 +          #> (if overlord then
   6.100 +                Config.put SMT_Config.debug_files
   6.101 +                           (overlord_file_location_for_prover name
   6.102 +                            |> (fn (path, name) => path ^ "/" ^ name))
   6.103 +              else
   6.104 +                I)
   6.105 +          #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
   6.106      val state = state |> Proof.map_context repair_context
   6.107 -
   6.108      fun do_slice timeout slice outcome0 time_so_far facts =
   6.109        let
   6.110          val timer = Timer.startRealTimer ()
   6.111 +        val state =
   6.112 +          state |> Proof.map_context
   6.113 +                       (repair_smt_monomorph_context debug max_mono_iters
   6.114 +                            max_mono_instances (length facts))
   6.115          val ms = timeout |> Time.toMilliseconds
   6.116          val slice_timeout =
   6.117            if slice < max_slices then