# HG changeset patch # User blanchet # Date 1301563012 -7200 # Node ID a6c141925a8a3277c8c35889458b39e551643ffd # Parent 24662b614fd425752f279c39b1c004f6601d0cc3 added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default diff -r 24662b614fd4 -r a6c141925a8a NEWS --- a/NEWS Thu Mar 31 11:16:51 2011 +0200 +++ b/NEWS Thu Mar 31 11:16:52 2011 +0200 @@ -49,6 +49,7 @@ * Sledgehammer: - sledgehammer available_provers ~> sledgehammer supported_provers INCOMPATIBILITY. + - Added "monomorphize" and "monomorphize_limit" options. * "try": - Added "simp:", "intro:", and "elim:" options. diff -r 24662b614fd4 -r a6c141925a8a doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Thu Mar 31 11:16:51 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Mar 31 11:16:52 2011 +0200 @@ -555,6 +555,19 @@ filter. If the option is set to \textit{smart}, it is set to a value that was empirically found to be appropriate for the prover. A typical value would be 300. + +\opfalse{monomorphize}{dont\_monomorphize} +Specifies whether the relevant facts should be monomorphized---i.e., whether +their type variables should be instantiated with relevant ground types. +Monomorphization is always performed for SMT solvers, irrespective of this +option. Monomorphization can simplify reasoning but also leads to larger fact +bases, which can slow down the ATPs. + +\opdefault{monomorphize\_limit}{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. + \end{enum} \subsection{Output Format} diff -r 24662b614fd4 -r a6c141925a8a src/HOL/Tools/SMT/smt_monomorph.ML --- a/src/HOL/Tools/SMT/smt_monomorph.ML Thu Mar 31 11:16:51 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML Thu Mar 31 11:16:52 2011 +0200 @@ -28,8 +28,8 @@ signature SMT_MONOMORPH = sig - val monomorph: (int * thm) list -> Proof.context -> - (int * thm) list * Proof.context + val monomorph: ('a * thm) list -> Proof.context -> + ('a * thm) list * Proof.context end structure SMT_Monomorph: SMT_MONOMORPH = diff -r 24662b614fd4 -r a6c141925a8a src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Mar 31 11:16:51 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Thu Mar 31 11:16:52 2011 +0200 @@ -88,6 +88,8 @@ #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation #> fst +val unprefix_fact_number = space_implode "_" o tl o space_explode "_" + fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names = if String.isSubstring set_ClauseFormulaRelationN output then let @@ -100,7 +102,8 @@ |> map (fn s => find_index (curry (op =) s) seq + 1) fun names_for_number j = j |> AList.lookup (op =) name_map |> these - |> map_filter (try (unprefix fact_prefix)) |> map unascii_of + |> map_filter (try (unascii_of o unprefix_fact_number + o unprefix fact_prefix)) |> map (fn name => (name, name |> find_first_in_list_vector fact_names |> the) handle Option.Option => @@ -145,16 +148,19 @@ "\nTo minimize the number of lemmas, try this: " ^ Markup.markup Markup.sendback command ^ "." -val vampire_fact_prefix = "f" (* grrr... *) +val vampire_step_prefix = "f" (* grrr... *) fun resolve_fact fact_names ((_, SOME s)) = - (case strip_prefix_and_unascii fact_prefix s of - SOME s' => (case find_first_in_list_vector fact_names s' of - SOME x => [(s', x)] - | NONE => []) + (case try (unprefix fact_prefix) s of + SOME s' => + let val s' = s' |> unprefix_fact_number |> unascii_of in + case find_first_in_list_vector fact_names s' of + SOME x => [(s', x)] + | NONE => [] + end | NONE => []) | resolve_fact fact_names (num, NONE) = - case Int.fromString (perhaps (try (unprefix vampire_fact_prefix)) num) of + case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of SOME j => if j > 0 andalso j <= Vector.length fact_names then Vector.sub (fact_names, j - 1) @@ -233,7 +239,7 @@ val raw_prefix = "X" val assum_prefix = "A" -val fact_prefix = "F" +val have_prefix = "F" fun resolve_conjecture conjecture_shape (num, s_opt) = let @@ -847,7 +853,7 @@ (l, subst, next_fact) else let - val l' = (prefix_for_depth depth fact_prefix, next_fact) + val l' = (prefix_for_depth depth have_prefix, next_fact) in (l', (l, l') :: subst, next_fact + 1) end val relabel_facts = apfst (maps (the_list o AList.lookup (op =) subst)) diff -r 24662b614fd4 -r a6c141925a8a src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Mar 31 11:16:51 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Mar 31 11:16:52 2011 +0200 @@ -442,9 +442,13 @@ (atp_type_literals_for_types type_sys ctypes_sorts)) (formula_for_combformula ctxt type_sys combformula) -fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) = - Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula, - NONE) +(* Each fact is given a unique fact number to avoid name clashes (e.g., because + of monomorphization). The TPTP explicitly forbids name clashes, and some of + the remote provers might care. *) +fun problem_line_for_fact ctxt prefix type_sys + (j, formula as {name, kind, ...}) = + Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind, + formula_for_fact ctxt type_sys formula, NONE) fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, superclass, ...}) = @@ -626,7 +630,8 @@ (* Reordering these might or might not confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem = - [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) facts), + [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) + (0 upto length facts - 1 ~~ facts)), (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses), (aritiesN, map problem_line_for_arity_clause arity_clauses), (helpersN, []), @@ -638,7 +643,8 @@ val helper_lines = get_helper_facts ctxt explicit_forall type_sys (maps (map (#3 o dest_Fof) o snd) problem) - |>> map (problem_line_for_fact ctxt helper_prefix type_sys + |>> map (pair 0 + #> problem_line_for_fact ctxt helper_prefix type_sys #> repair_problem_line thy explicit_forall type_sys const_tab) |> op @ val (problem, pool) = diff -r 24662b614fd4 -r a6c141925a8a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 31 11:16:51 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 31 11:16:52 2011 +0200 @@ -79,10 +79,12 @@ ("verbose", "false"), ("overlord", "false"), ("blocking", "false"), + ("relevance_thresholds", "0.45 0.85"), + ("max_relevant", "smart"), + ("monomorphize", "false"), + ("monomorphize_limit", "4"), ("type_sys", "smart"), ("explicit_apply", "false"), - ("relevance_thresholds", "0.45 0.85"), - ("max_relevant", "smart"), ("isar_proof", "false"), ("isar_shrink_factor", "1")] @@ -95,6 +97,7 @@ ("quiet", "verbose"), ("no_overlord", "overlord"), ("non_blocking", "blocking"), + ("dont_monomorphize", "monomorphize"), ("partial_types", "full_types"), ("implicit_apply", "explicit_apply"), ("no_isar_proof", "isar_proof")] @@ -233,6 +236,10 @@ val blocking = auto orelse debug orelse lookup_bool "blocking" val provers = lookup_string "provers" |> space_explode " " |> auto ? single o hd + val relevance_thresholds = lookup_real_pair "relevance_thresholds" + val max_relevant = lookup_int_option "max_relevant" + val monomorphize = lookup_bool "monomorphize" + val monomorphize_limit = lookup_int "monomorphize_limit" val type_sys = case (lookup_string "type_sys", lookup_bool "full_types") of ("tags", full_types) => Tags full_types @@ -245,18 +252,18 @@ else error ("Unknown type system: " ^ quote type_sys ^ ".") val explicit_apply = lookup_bool "explicit_apply" - val relevance_thresholds = lookup_real_pair "relevance_thresholds" - val max_relevant = lookup_int_option "max_relevant" val isar_proof = lookup_bool "isar_proof" val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, - provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, - relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, - timeout = timeout, expect = expect} + provers = provers, relevance_thresholds = relevance_thresholds, + max_relevant = max_relevant, monomorphize = monomorphize, + monomorphize_limit = monomorphize_limit, type_sys = type_sys, + explicit_apply = explicit_apply, isar_proof = isar_proof, + isar_shrink_factor = isar_shrink_factor, timeout = timeout, + expect = expect} end fun get_params auto ctxt = extract_params auto (default_raw_params ctxt) diff -r 24662b614fd4 -r a6c141925a8a src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Mar 31 11:16:51 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Mar 31 11:16:52 2011 +0200 @@ -42,8 +42,8 @@ fun print silent f = if silent then () else Output.urgent_message (f ()) -fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof, - isar_shrink_factor, ...} : params) +fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit, + 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,6 +65,7 @@ {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 = false, monomorphize_limit = monomorphize_limit, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} val facts = diff -r 24662b614fd4 -r a6c141925a8a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Mar 31 11:16:51 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Mar 31 11:16:52 2011 +0200 @@ -21,10 +21,12 @@ overlord: bool, blocking: bool, provers: string list, + relevance_thresholds: real * real, + max_relevant: int option, + monomorphize: bool, + monomorphize_limit: int, type_sys: type_system, explicit_apply: bool, - relevance_thresholds: real * real, - max_relevant: int option, isar_proof: bool, isar_shrink_factor: int, timeout: Time.time, @@ -66,7 +68,6 @@ val smt_iter_fact_frac : real Unsynchronized.ref val smt_iter_time_frac : real Unsynchronized.ref val smt_iter_min_msecs : int Unsynchronized.ref - val smt_monomorphize_limit : int Unsynchronized.ref val das_Tool : string val select_smt_solver : string -> Proof.context -> Proof.context @@ -229,10 +230,12 @@ overlord: bool, blocking: bool, provers: string list, + relevance_thresholds: real * real, + max_relevant: int option, + monomorphize: bool, + monomorphize_limit: int, type_sys: type_system, explicit_apply: bool, - relevance_thresholds: real * real, - max_relevant: int option, isar_proof: bool, isar_shrink_factor: int, timeout: Time.time, @@ -333,13 +336,27 @@ ({exec, required_execs, arguments, has_incomplete_mode, proof_delims, known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config) - ({debug, verbose, overlord, type_sys, explicit_apply, isar_proof, - isar_shrink_factor, timeout, ...} : params) + ({debug, verbose, overlord, monomorphize, monomorphize_limit, type_sys, + explicit_apply, isar_proof, isar_shrink_factor, timeout, ...} + : params) minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = let val ctxt = Proof.context_of state val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal - val facts = facts |> map (atp_translated_fact ctxt) + fun monomorphize_facts facts = + let + val facts = facts |> map untranslated_fact + val indexed_facts = + (~1, goal) :: (0 upto length facts - 1 ~~ map snd facts) + in + ctxt |> Config.put SMT_Config.monomorph_limit monomorphize_limit + |> 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 + val facts = facts |> monomorphize ? monomorphize_facts + |> map (atp_translated_fact ctxt) val (dest_dir, problem_prefix) = if overlord then overlord_file_location_for_prover name else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix) @@ -513,9 +530,9 @@ val smt_iter_fact_frac = Unsynchronized.ref 0.5 val smt_iter_time_frac = Unsynchronized.ref 0.5 val smt_iter_min_msecs = Unsynchronized.ref 5000 -val smt_monomorphize_limit = Unsynchronized.ref 4 -fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params) +fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit, + timeout, ...} : params) state i smt_filter = let val ctxt = Proof.context_of state @@ -529,7 +546,7 @@ else I) #> Config.put SMT_Config.infer_triggers (!smt_triggers) - #> Config.put SMT_Config.monomorph_limit (!smt_monomorphize_limit) + #> Config.put SMT_Config.monomorph_limit monomorphize_limit val state = state |> Proof.map_context repair_context fun iter timeout iter_num outcome0 time_so_far facts = diff -r 24662b614fd4 -r a6c141925a8a src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Mar 31 11:16:51 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Mar 31 11:16:52 2011 +0200 @@ -164,9 +164,9 @@ (* FUDGE *) val auto_max_relevant_divisor = 2 -fun run_sledgehammer (params as {debug, blocking, provers, type_sys, - relevance_thresholds, max_relevant, timeout, - ...}) +fun run_sledgehammer (params as {debug, blocking, provers, monomorphize, + type_sys, relevance_thresholds, max_relevant, + timeout, ...}) auto i (relevance_override as {only, ...}) minimize_command state = if null provers then @@ -246,7 +246,10 @@ else launch_provers state (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps) - (ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst)) + (if monomorphize then + K (Untranslated_Fact o fst) + else + ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst)) (K (K NONE)) atps fun launch_smts accum = if null smts then