# HG changeset patch # User blanchet # Date 1307437509 -7200 # Node ID 9d717505595f24b20bb0fe0c4e4799ba23297c9a # Parent 2749c357f865f2a74b687f8f9828956d0b433ad7# Parent dabf6e3112136174a22851b1495249b4d3101b3f merged diff -r 2749c357f865 -r 9d717505595f src/HOL/SMT.thy --- a/src/HOL/SMT.thy Tue Jun 07 11:04:17 2011 +0200 +++ b/src/HOL/SMT.thy Tue Jun 07 11:05:09 2011 +0200 @@ -245,14 +245,14 @@ construction whose cycles are limited by the following option. *} -declare [[ smt_monomorph_limit = 10 ]] +declare [[ monomorph_max_rounds = 5 ]] text {* In addition, the number of generated monomorphic instances is limited by the following option. *} -declare [[ smt_monomorph_instances = 500 ]] +declare [[ monomorph_max_new_instances = 500 ]] diff -r 2749c357f865 -r 9d717505595f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 11:04:17 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 11:05:09 2011 +0200 @@ -544,7 +544,7 @@ fun repair_monomorph_context max_iters max_new_instances = Config.put Monomorph.max_rounds max_iters #> Config.put Monomorph.max_new_instances max_new_instances - #> Config.put Monomorph.complete_instances false + #> Config.put Monomorph.keep_partial_instances false fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances = (not debug ? Config.put SMT_Config.verbose false) diff -r 2749c357f865 -r 9d717505595f src/HOL/Tools/monomorph.ML --- a/src/HOL/Tools/monomorph.ML Tue Jun 07 11:04:17 2011 +0200 +++ b/src/HOL/Tools/monomorph.ML Tue Jun 07 11:05:09 2011 +0200 @@ -37,7 +37,7 @@ (* configuration options *) val max_rounds: int Config.T val max_new_instances: int Config.T - val complete_instances: bool Config.T + val keep_partial_instances: bool Config.T (* monomorphization *) val monomorph: (term -> typ list Symtab.table) -> (int * thm) list -> @@ -66,8 +66,8 @@ val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5) val max_new_instances = Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300) -val complete_instances = - Attrib.setup_config_bool @{binding monomorph_complete_instances} (K true) +val keep_partial_instances = + Attrib.setup_config_bool @{binding monomorph_keep_partial_instances} (K true) @@ -161,7 +161,7 @@ fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx = let val thy = Proof_Context.theory_of ctxt - val count_partial = Config.get ctxt complete_instances + val count_partial = Config.get ctxt keep_partial_instances fun add_new_ground subst n T = let val T' = Envir.subst_type subst T @@ -287,7 +287,7 @@ in (map inst thm_infos, ctxt) end fun instantiate_all ctxt thm_infos (_, (_, subs, _)) = - if Config.get ctxt complete_instances then + if Config.get ctxt keep_partial_instances then let fun is_refined ((_, _, refined), _) = refined in (Inttab.map (K (filter_out is_refined)) subs, thm_infos)