# HG changeset patch # User blanchet # Date 1282812142 -7200 # Node ID 3913f58d0fcc39c84694162b071c44e660ef4470 # Parent 14c1085dec028961f6a7bb4c595be63ddbaee0e6# Parent 6628adcae4a710ae19e8619ae9e319aae1c08748 merged diff -r 14c1085dec02 -r 3913f58d0fcc doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 26 09:12:00 2010 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 26 10:42:22 2010 +0200 @@ -447,33 +447,29 @@ \label{relevance-filter} \begin{enum} -\opdefault{relevance\_threshold}{int}{40} -Specifies the threshold above which facts are considered relevant by the -relevance filter. The option ranges from 0 to 100, where 0 means that all -theorems are relevant. +\opdefault{relevance\_thresholds}{int\_pair}{45~95} +Specifies the thresholds above which facts are considered relevant by the +relevance filter. The first threshold is used for the first iteration of the +relevance filter and the second threshold is used for the last iteration (if it +is reached). The effective threshold is quadratically interpolated for the other +iterations. Each threshold ranges from 0 to 100, where 0 means that all theorems +are relevant and 100 only theorems that refer to previously seen constants. -\opdefault{relevance\_convergence}{int}{31} -Specifies the convergence factor, expressed as a percentage, used by the -relevance filter. This factor is used by the relevance filter to scale down the -relevance of facts at each iteration of the filter. - -\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}} -Specifies the maximum number of facts that may be added during one iteration of -the relevance filter. If the option is set to \textit{smart}, it is set to a -value that was empirically found to be appropriate for the ATP. A typical value -would be 50. +\opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}} +Specifies the maximum number of facts that may be returned by the relevance +filter. If the option is set to \textit{smart}, it is set to a value that was +empirically found to be appropriate for the ATP. A typical value would be 300. \opsmartx{theory\_relevant}{theory\_irrelevant} Specifies whether the theory from which a fact comes should be taken into consideration by the relevance filter. If the option is set to \textit{smart}, -it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire, -because empirical results suggest that these are the best settings. +it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs; +empirical results suggest that these are the best settings. -\opfalse{defs\_relevant}{defs\_irrelevant} -Specifies whether the definition of constants occurring in the formula to prove -should be considered particularly relevant. Enabling this option tends to lead -to larger problems and typically slows down the ATPs. - +%\opfalse{defs\_relevant}{defs\_irrelevant} +%Specifies whether the definition of constants occurring in the formula to prove +%should be considered particularly relevant. Enabling this option tends to lead +%to larger problems and typically slows down the ATPs. \end{enum} \subsection{Output Format} diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Aug 26 10:42:22 2010 +0200 @@ -290,10 +290,12 @@ | NONE => get_prover (default_atp_name ())) end +type locality = Sledgehammer_Fact_Filter.locality + local datatype sh_result = - SH_OK of int * int * (string * bool) list | + SH_OK of int * int * (string * locality) list | SH_FAIL of int * int | SH_ERROR @@ -355,8 +357,8 @@ case result of SH_OK (time_isa, time_atp, names) => let - fun get_thms (name, chained) = - ((name, chained), thms_of_name (Proof.context_of st) name) + fun get_thms (name, loc) = + ((name, loc), thms_of_name (Proof.context_of st) name) in change_data id inc_sh_success; change_data id (inc_sh_lemmas (length names)); @@ -445,7 +447,7 @@ then () else let val named_thms = - Unsynchronized.ref (NONE : ((string * bool) * thm list) list option) + Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) val minimize = AList.defined (op =) args minimizeK val metis_ft = AList.defined (op =) args metis_ftK diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 26 10:42:22 2010 +0200 @@ -19,7 +19,7 @@ has_incomplete_mode: bool, proof_delims: (string * string) list, known_failures: (failure * string) list, - default_max_relevant_per_iter: int, + default_max_relevant: int, default_theory_relevant: bool, explicit_forall: bool, use_conjecture_for_hypotheses: bool} @@ -52,7 +52,7 @@ has_incomplete_mode: bool, proof_delims: (string * string) list, known_failures: (failure * string) list, - default_max_relevant_per_iter: int, + default_max_relevant: int, default_theory_relevant: bool, explicit_forall: bool, use_conjecture_for_hypotheses: bool} @@ -125,10 +125,20 @@ priority ("Available ATPs: " ^ commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") -fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000 +fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000 (* E prover *) +(* Give older versions of E an extra second, because the "eproof" script wrongly + subtracted an entire second to account for the overhead of the script + itself, which is in fact much lower. *) +fun e_bonus () = + case getenv "E_VERSION" of + "" => 1000 + | version => + if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 1000 + else 0 + val tstp_proof_delims = ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") @@ -137,8 +147,7 @@ required_execs = [], arguments = fn _ => fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \ - \--soft-cpu-limit=" ^ - string_of_int (to_generous_secs timeout), + \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout), has_incomplete_mode = false, proof_delims = [tstp_proof_delims], known_failures = @@ -150,7 +159,7 @@ "# Cannot determine problem status within resource limit"), (OutOfResources, "SZS status: ResourceOut"), (OutOfResources, "SZS status ResourceOut")], - default_max_relevant_per_iter = 80 (* FUDGE *), + default_max_relevant = 500 (* FUDGE *), default_theory_relevant = false, explicit_forall = false, use_conjecture_for_hypotheses = true} @@ -165,7 +174,7 @@ required_execs = [("SPASS_HOME", "SPASS")], arguments = fn complete => fn timeout => ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ - \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout)) + \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout)) |> not complete ? prefix "-SOS=1 ", has_incomplete_mode = true, proof_delims = [("Here is a proof", "Formulae used in the proof")], @@ -177,7 +186,7 @@ (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), (SpassTooOld, "tptp2dfg")], - default_max_relevant_per_iter = 40 (* FUDGE *), + default_max_relevant = 350 (* FUDGE *), default_theory_relevant = true, explicit_forall = true, use_conjecture_for_hypotheses = true} @@ -190,10 +199,11 @@ val vampire_config : prover_config = {exec = ("VAMPIRE_HOME", "vampire"), required_execs = [], - arguments = fn _ => fn timeout => - "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^ - " --thanks Andrei --input_file", - has_incomplete_mode = false, + arguments = fn complete => fn timeout => + ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^ + " --thanks Andrei --input_file") + |> not complete ? prefix "--sos on ", + has_incomplete_mode = true, proof_delims = [("=========== Refutation ==========", "======= End of refutation ======="), @@ -206,7 +216,7 @@ (Unprovable, "Satisfiability detected"), (Unprovable, "Termination reason: Satisfiable"), (VampireTooOld, "not a valid option")], - default_max_relevant_per_iter = 45 (* FUDGE *), + default_max_relevant = 400 (* FUDGE *), default_theory_relevant = false, explicit_forall = false, use_conjecture_for_hypotheses = true} @@ -246,38 +256,38 @@ | SOME sys => sys fun remote_config system_name system_versions proof_delims known_failures - default_max_relevant_per_iter default_theory_relevant - use_conjecture_for_hypotheses = + default_max_relevant default_theory_relevant + use_conjecture_for_hypotheses : prover_config = {exec = ("ISABELLE_ATP", "scripts/remote_atp"), required_execs = [], arguments = fn _ => fn timeout => - " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^ + " -t " ^ string_of_int (to_secs 0 timeout) ^ " -s " ^ the_system system_name system_versions, has_incomplete_mode = false, proof_delims = insert (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_perl_failures @ [(TimedOut, "says Timeout")], - default_max_relevant_per_iter = default_max_relevant_per_iter, + default_max_relevant = default_max_relevant, default_theory_relevant = default_theory_relevant, explicit_forall = true, use_conjecture_for_hypotheses = use_conjecture_for_hypotheses} fun remotify_config system_name system_versions - ({proof_delims, known_failures, default_max_relevant_per_iter, + ({proof_delims, known_failures, default_max_relevant, default_theory_relevant, use_conjecture_for_hypotheses, ...} : prover_config) : prover_config = remote_config system_name system_versions proof_delims known_failures - default_max_relevant_per_iter default_theory_relevant + default_max_relevant default_theory_relevant use_conjecture_for_hypotheses val remotify_name = prefix "remote_" fun remote_prover name system_name system_versions proof_delims known_failures - default_max_relevant_per_iter default_theory_relevant + default_max_relevant default_theory_relevant use_conjecture_for_hypotheses = (remotify_name name, remote_config system_name system_versions proof_delims known_failures - default_max_relevant_per_iter default_theory_relevant + default_max_relevant default_theory_relevant use_conjecture_for_hypotheses) fun remotify_prover (name, config) system_name system_versions = (remotify_name name, remotify_config system_name system_versions config) @@ -285,11 +295,11 @@ val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"] val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"] val remote_sine_e = - remote_prover "sine_e" "SInE" [] [] - [(Unprovable, "says Unknown")] 150 (* FUDGE *) false true + remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")] + 1000 (* FUDGE *) false true val remote_snark = remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] [] - 50 (* FUDGE *) false true + 350 (* FUDGE *) false true (* Setup *) diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Aug 26 10:42:22 2010 +0200 @@ -38,11 +38,10 @@ val const_prefix: string val type_const_prefix: string val class_prefix: string - val union_all: ''a list list -> ''a list val invert_const: string -> string val ascii_of: string -> string - val undo_ascii_of: string -> string - val strip_prefix_and_undo_ascii: string -> string -> string option + val unascii_of: string -> string + val strip_prefix_and_unascii: string -> string -> string option val make_bound_var : string -> string val make_schematic_var : string * int -> string val make_fixed_var : string -> string @@ -121,7 +120,7 @@ Alphanumeric characters are left unchanged. The character _ goes to __ Characters in the range ASCII space to / go to _A to _P, respectively. - Other printing characters go to _nnn where nnn is the decimal ASCII code.*) + Other characters go to _nnn where nnn is the decimal ASCII code.*) val A_minus_space = Char.ord #"A" - Char.ord #" "; fun stringN_of_int 0 _ = "" @@ -132,9 +131,7 @@ else if c = #"_" then "__" else if #" " <= c andalso c <= #"/" then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) - else if Char.isPrint c - then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) - else "" + else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) val ascii_of = String.translate ascii_of_c; @@ -142,29 +139,28 @@ (*We don't raise error exceptions because this code can run inside the watcher. Also, the errors are "impossible" (hah!)*) -fun undo_ascii_aux rcs [] = String.implode(rev rcs) - | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*) +fun unascii_aux rcs [] = String.implode(rev rcs) + | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*) (*Three types of _ escapes: __, _A to _P, _nnn*) - | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs - | undo_ascii_aux rcs (#"_" :: c :: cs) = + | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs + | unascii_aux rcs (#"_" :: c :: cs) = if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) - then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs + then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs else let val digits = List.take (c::cs, 3) handle Subscript => [] in case Int.fromString (String.implode digits) of - NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*) - | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) + NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*) + | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) end - | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs; - -val undo_ascii_of = undo_ascii_aux [] o String.explode; + | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs +val unascii_of = unascii_aux [] o String.explode (* If string s has the prefix s1, return the result of deleting it, un-ASCII'd. *) -fun strip_prefix_and_undo_ascii s1 s = +fun strip_prefix_and_unascii s1 s = if String.isPrefix s1 s then - SOME (undo_ascii_of (String.extract (s, size s1, NONE))) + SOME (unascii_of (String.extract (s, size s1, NONE))) else NONE @@ -514,8 +510,8 @@ (*Type constructors used to instantiate overloaded constants are the only ones needed.*) fun add_type_consts_in_term thy = let - val const_typargs = Sign.const_typargs thy - fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x) + fun aux (Const x) = + fold (fold_type_consts set_insert) (Sign.const_typargs thy x) | aux (Abs (_, _, u)) = aux u | aux (Const (@{const_name skolem_id}, _) $ _) = I | aux (t $ u) = aux t #> aux u diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 26 10:42:22 2010 +0200 @@ -228,15 +228,15 @@ | smart_invert_const s = invert_const s fun hol_type_from_metis_term _ (Metis.Term.Var v) = - (case strip_prefix_and_undo_ascii tvar_prefix v of + (case strip_prefix_and_unascii tvar_prefix v of SOME w => make_tvar w | NONE => make_tvar v) | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) = - (case strip_prefix_and_undo_ascii type_const_prefix x of + (case strip_prefix_and_unascii type_const_prefix x of SOME tc => Term.Type (smart_invert_const tc, map (hol_type_from_metis_term ctxt) tys) | NONE => - case strip_prefix_and_undo_ascii tfree_prefix x of + case strip_prefix_and_unascii tfree_prefix x of SOME tf => mk_tfree ctxt tf | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); @@ -246,10 +246,10 @@ val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ Metis.Term.toString fol_tm) fun tm_to_tt (Metis.Term.Var v) = - (case strip_prefix_and_undo_ascii tvar_prefix v of + (case strip_prefix_and_unascii tvar_prefix v of SOME w => Type (make_tvar w) | NONE => - case strip_prefix_and_undo_ascii schematic_var_prefix v of + case strip_prefix_and_unascii schematic_var_prefix v of SOME w => Term (mk_var (w, HOLogic.typeT)) | NONE => Term (mk_var (v, HOLogic.typeT)) ) (*Var from Metis with a name like _nnn; possibly a type variable*) @@ -266,7 +266,7 @@ and applic_to_tt ("=",ts) = Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts))) | applic_to_tt (a,ts) = - case strip_prefix_and_undo_ascii const_prefix a of + case strip_prefix_and_unascii const_prefix a of SOME b => let val c = smart_invert_const b val ntypes = num_type_args thy c @@ -284,14 +284,14 @@ cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) end | NONE => (*Not a constant. Is it a type constructor?*) - case strip_prefix_and_undo_ascii type_const_prefix a of + case strip_prefix_and_unascii type_const_prefix a of SOME b => Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts))) | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case strip_prefix_and_undo_ascii tfree_prefix a of + case strip_prefix_and_unascii tfree_prefix a of SOME b => Type (mk_tfree ctxt b) | NONE => (*a fixed variable? They are Skolem functions.*) - case strip_prefix_and_undo_ascii fixed_var_prefix a of + case strip_prefix_and_unascii fixed_var_prefix a of SOME b => let val opr = Term.Free(b, HOLogic.typeT) in apply_list opr (length ts) (map tm_to_tt ts) end @@ -307,16 +307,16 @@ let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ Metis.Term.toString fol_tm) fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = - (case strip_prefix_and_undo_ascii schematic_var_prefix v of + (case strip_prefix_and_unascii schematic_var_prefix v of SOME w => mk_var(w, dummyT) | NONE => mk_var(v, dummyT)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = Const (@{const_name "op ="}, HOLogic.typeT) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = - (case strip_prefix_and_undo_ascii const_prefix x of + (case strip_prefix_and_unascii const_prefix x of SOME c => Const (smart_invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix_and_undo_ascii fixed_var_prefix x of + case strip_prefix_and_unascii fixed_var_prefix x of SOME v => Free (v, hol_type_from_metis_term ctxt ty) | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = @@ -327,10 +327,10 @@ | cvt (Metis.Term.Fn ("=", [tm1,tm2])) = list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2]) | cvt (t as Metis.Term.Fn (x, [])) = - (case strip_prefix_and_undo_ascii const_prefix x of + (case strip_prefix_and_unascii const_prefix x of SOME c => Const (smart_invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix_and_undo_ascii fixed_var_prefix x of + case strip_prefix_and_unascii fixed_var_prefix x of SOME v => Free (v, dummyT) | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); hol_term_from_metis_PT ctxt t)) @@ -410,11 +410,11 @@ " in " ^ Display.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = - case strip_prefix_and_undo_ascii schematic_var_prefix a of + case strip_prefix_and_unascii schematic_var_prefix a of SOME b => SOME (b, t) - | NONE => case strip_prefix_and_undo_ascii tvar_prefix a of + | NONE => case strip_prefix_and_unascii tvar_prefix a of SOME _ => NONE (*type instantiations are forbidden!*) - | NONE => SOME (a,t) (*internal Metis var?*) + | NONE => SOME (a,t) (*internal Metis var?*) val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst) val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 10:42:22 2010 +0200 @@ -9,6 +9,7 @@ signature SLEDGEHAMMER = sig type failure = ATP_Systems.failure + type locality = Sledgehammer_Fact_Filter.locality type relevance_override = Sledgehammer_Fact_Filter.relevance_override type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command type params = @@ -18,11 +19,9 @@ atps: string list, full_types: bool, explicit_apply: bool, - relevance_threshold: real, - relevance_convergence: real, - max_relevant_per_iter: int option, + relevance_thresholds: real * real, + max_relevant: int option, theory_relevant: bool option, - defs_relevant: bool, isar_proof: bool, isar_shrink_factor: int, timeout: Time.time} @@ -30,16 +29,16 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axioms: ((string * bool) * thm) list option} + axioms: ((string * locality) * thm) list option} type prover_result = {outcome: failure option, message: string, pool: string Symtab.table, - used_thm_names: (string * bool) list, + used_thm_names: (string * locality) list, atp_run_time_in_msecs: int, output: string, proof: string, - axiom_names: (string * bool) vector, + axiom_names: (string * locality) vector, conjecture_shape: int list list} type prover = params -> minimize_command -> problem -> prover_result @@ -87,11 +86,9 @@ atps: string list, full_types: bool, explicit_apply: bool, - relevance_threshold: real, - relevance_convergence: real, - max_relevant_per_iter: int option, + relevance_thresholds: real * real, + max_relevant: int option, theory_relevant: bool option, - defs_relevant: bool, isar_proof: bool, isar_shrink_factor: int, timeout: Time.time} @@ -100,17 +97,17 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axioms: ((string * bool) * thm) list option} + axioms: ((string * locality) * thm) list option} type prover_result = {outcome: failure option, message: string, pool: string Symtab.table, - used_thm_names: (string * bool) list, + used_thm_names: (string * locality) list, atp_run_time_in_msecs: int, output: string, proof: string, - axiom_names: (string * bool) vector, + axiom_names: (string * locality) vector, conjecture_shape: int list list} type prover = params -> minimize_command -> problem -> prover_result @@ -174,10 +171,9 @@ Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" |-- Scan.repeat parse_clause_formula_pair val extract_clause_formula_relation = - Substring.full - #> Substring.position set_ClauseFormulaRelationN - #> snd #> Substring.string #> strip_spaces #> explode - #> parse_clause_formula_relation #> fst + Substring.full #> Substring.position set_ClauseFormulaRelationN + #> snd #> Substring.string #> strip_spaces_except_between_ident_chars + #> explode #> parse_clause_formula_relation #> fst fun repair_conjecture_shape_and_theorem_names output conjecture_shape axiom_names = @@ -190,17 +186,19 @@ val seq = extract_clause_sequence output val name_map = extract_clause_formula_relation output fun renumber_conjecture j = - conjecture_prefix ^ Int.toString (j - j0) + conjecture_prefix ^ string_of_int (j - j0) |> AList.find (fn (s, ss) => member (op =) ss s) name_map |> map (fn s => find_index (curry (op =) s) seq + 1) fun name_for_number j = let val axioms = - j |> AList.lookup (op =) name_map - |> these |> map_filter (try (unprefix axiom_prefix)) - |> map undo_ascii_of - val chained = forall (is_true_for axiom_names) axioms - in (axioms |> space_implode " ", chained) end + j |> AList.lookup (op =) name_map |> these + |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of + val loc = + case axioms of + [axiom] => find_first_in_vector axiom_names axiom General + | _ => General + in (axioms |> space_implode " ", loc) end in (conjecture_shape |> map (maps renumber_conjecture), seq |> map name_for_number |> Vector.fromList) @@ -213,12 +211,11 @@ fun prover_fun atp_name {exec, required_execs, arguments, has_incomplete_mode, proof_delims, - known_failures, default_max_relevant_per_iter, default_theory_relevant, + known_failures, default_max_relevant, default_theory_relevant, explicit_forall, use_conjecture_for_hypotheses} ({debug, verbose, overlord, full_types, explicit_apply, - relevance_threshold, relevance_convergence, - max_relevant_per_iter, theory_relevant, - defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) + relevance_thresholds, max_relevant, theory_relevant, isar_proof, + isar_shrink_factor, timeout, ...} : params) minimize_command ({subgoal, goal, relevance_override, axioms} : problem) = let @@ -226,7 +223,7 @@ val thy = ProofContext.theory_of ctxt val (params, hyp_ts, concl_t) = strip_subgoal th subgoal - fun print s = (priority s; if debug then tracing s else ()) + val print = priority fun print_v f = () |> verbose ? print o f fun print_d f = () |> debug ? print o f @@ -234,15 +231,13 @@ case axioms of SOME axioms => axioms | NONE => - (relevant_facts full_types relevance_threshold relevance_convergence - defs_relevant - (the_default default_max_relevant_per_iter - max_relevant_per_iter) + (relevant_facts full_types relevance_thresholds + (the_default default_max_relevant max_relevant) (the_default default_theory_relevant theory_relevant) relevance_override goal hyp_ts concl_t |> tap ((fn n => print_v (fn () => - "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^ - " for " ^ quote atp_name ^ ".")) o length)) + "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^ + " for " ^ quote atp_name ^ ".")) o length)) (* path to unique problem file *) val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" @@ -261,6 +256,7 @@ else error ("No such directory: " ^ the_dest_dir ^ ".") end; + val measure_run_time = verbose orelse Config.get ctxt measure_runtime val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) (* write out problem file and call prover *) fun command_line complete timeout probfile = @@ -268,10 +264,8 @@ val core = File.shell_path command ^ " " ^ arguments complete timeout ^ " " ^ File.shell_path probfile in - (if Config.get ctxt measure_runtime then - "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" - else - "exec " ^ core) ^ " 2>&1" + (if measure_run_time then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" + else "exec " ^ core) ^ " 2>&1" end fun split_time s = let @@ -300,14 +294,11 @@ prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I) - |>> (if Config.get ctxt measure_runtime then split_time - else rpair 0) + |>> (if measure_run_time then split_time else rpair 0) val (proof, outcome) = extract_proof_and_outcome complete res_code proof_delims known_failures output in (output, msecs, proof, outcome) end - val _ = print_d (fn () => "Preparing problem for " ^ - quote atp_name ^ "...") val readable_names = debug andalso overlord val (problem, pool, conjecture_offset, axiom_names) = prepare_problem ctxt readable_names explicit_forall full_types @@ -358,6 +349,11 @@ proof_text isar_proof (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) (full_types, minimize_command, proof, axiom_names, th, subgoal) + |>> (fn message => + message ^ (if verbose then + "\nATP CPU time: " ^ string_of_int msecs ^ " ms." + else + "")) | SOME failure => (string_for_failure failure, []) in {outcome = outcome, message = message, pool = pool, diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 10:42:22 2010 +0200 @@ -5,19 +5,21 @@ signature SLEDGEHAMMER_FACT_FILTER = sig + datatype locality = General | Theory | Local | Chained + type relevance_override = {add: Facts.ref list, del: Facts.ref list, only: bool} val trace : bool Unsynchronized.ref - val name_thms_pair_from_ref : + val name_thm_pairs_from_ref : Proof.context -> unit Symtab.table -> thm list -> Facts.ref - -> (unit -> string * bool) * thm list + -> ((string * locality) * thm) list val relevant_facts : - bool -> real -> real -> bool -> int -> bool -> relevance_override + bool -> real * real -> int -> bool -> relevance_override -> Proof.context * (thm list * 'a) -> term list -> term - -> ((string * bool) * thm) list + -> ((string * locality) * thm) list end; structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = @@ -30,6 +32,8 @@ val respect_no_atp = true +datatype locality = General | Theory | Local | Chained + type relevance_override = {add: Facts.ref list, del: Facts.ref list, @@ -37,13 +41,22 @@ val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator -fun name_thms_pair_from_ref ctxt reserved chained_ths xref = - let val ths = ProofContext.get_fact ctxt xref in - (fn () => let - val name = Facts.string_of_ref xref - val name = name |> Symtab.defined reserved name ? quote - val chained = forall (member Thm.eq_thm chained_ths) ths - in (name, chained) end, ths) +fun repair_name reserved multi j name = + (name |> Symtab.defined reserved name ? quote) ^ + (if multi then "(" ^ Int.toString j ^ ")" else "") + +fun name_thm_pairs_from_ref ctxt reserved chained_ths xref = + let + val ths = ProofContext.get_fact ctxt xref + val name = Facts.string_of_ref xref + val multi = length ths > 1 + in + (ths, (1, [])) + |-> fold (fn th => fn (j, rest) => + (j + 1, ((repair_name reserved multi j name, + if member Thm.eq_thm chained_ths th then Chained + else General), th) :: rest)) + |> snd end (***************************************************************) @@ -53,61 +66,81 @@ (*** constants with types ***) (*An abstraction of Isabelle types*) -datatype const_typ = CTVar | CType of string * const_typ list +datatype pseudotype = PVar | PType of string * pseudotype list + +fun string_for_pseudotype PVar = "?" + | string_for_pseudotype (PType (s, Ts)) = + (case Ts of + [] => "" + | [T] => string_for_pseudotype T + | Ts => string_for_pseudotypes Ts ^ " ") ^ s +and string_for_pseudotypes Ts = + "(" ^ commas (map string_for_pseudotype Ts) ^ ")" (*Is the second type an instance of the first one?*) -fun match_type (CType(con1,args1)) (CType(con2,args2)) = - con1=con2 andalso match_types args1 args2 - | match_type CTVar _ = true - | match_type _ CTVar = false -and match_types [] [] = true - | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2; +fun match_pseudotype (PType (a, T), PType (b, U)) = + a = b andalso match_pseudotypes (T, U) + | match_pseudotype (PVar, _) = true + | match_pseudotype (_, PVar) = false +and match_pseudotypes ([], []) = true + | match_pseudotypes (T :: Ts, U :: Us) = + match_pseudotype (T, U) andalso match_pseudotypes (Ts, Us) (*Is there a unifiable constant?*) -fun const_mem const_tab (c, c_typ) = - exists (match_types c_typ) (these (Symtab.lookup const_tab c)) +fun pseudoconst_mem f const_tab (c, c_typ) = + exists (curry (match_pseudotypes o f) c_typ) + (these (Symtab.lookup const_tab c)) -(*Maps a "real" type to a const_typ*) -fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) - | const_typ_of (TFree _) = CTVar - | const_typ_of (TVar _) = CTVar +fun pseudotype_for (Type (c,typs)) = PType (c, map pseudotype_for typs) + | pseudotype_for (TFree _) = PVar + | pseudotype_for (TVar _) = PVar +(* Pairs a constant with the list of its type instantiations. *) +fun pseudoconst_for thy (c, T) = + (c, map pseudotype_for (Sign.const_typargs thy (c, T))) + handle TYPE _ => (c, []) (* Variable (locale constant): monomorphic *) -(*Pairs a constant with the list of its type instantiations (using const_typ)*) -fun const_with_typ thy (c,typ) = - let val tvars = Sign.const_typargs thy (c,typ) in - (c, map const_typ_of tvars) end - handle TYPE _ => (c, []) (*Variable (locale constant): monomorphic*) +fun string_for_pseudoconst (s, []) = s + | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts +fun string_for_super_pseudoconst (s, [[]]) = s + | string_for_super_pseudoconst (s, Tss) = + s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}" + +val abs_prefix = "Sledgehammer.abs" +val skolem_prefix = "Sledgehammer.sko" -(*Add a const/type pair to the table, but a [] entry means a standard connective, - which we ignore.*) -fun add_const_to_table (c, ctyps) = - Symtab.map_default (c, [ctyps]) - (fn [] => [] | ctypss => insert (op =) ctyps ctypss) +(* Add a pseudoconstant to the table, but a [] entry means a standard + connective, which we ignore.*) +fun add_pseudoconst_to_table also_skolem (c, ctyps) = + if also_skolem orelse not (String.isPrefix skolem_prefix c) then + Symtab.map_default (c, [ctyps]) + (fn [] => [] | ctypss => insert (op =) ctyps ctypss) + else + I fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) -val fresh_prefix = "Sledgehammer.FRESH." val flip = Option.map not (* These are typically simplified away by "Meson.presimplify". *) val boring_consts = [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}] -fun get_consts thy pos ts = +fun get_pseudoconsts thy also_skolems pos ts = let (* We include free variables, as well as constants, to handle locales. For each quantifiers that must necessarily be skolemized by the ATP, we introduce a fresh constant to simulate the effect of Skolemization. *) fun do_term t = case t of - Const x => add_const_to_table (const_with_typ thy x) - | Free (s, _) => add_const_to_table (s, []) + Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x) + | Free (s, _) => add_pseudoconst_to_table also_skolems (s, []) | t1 $ t2 => fold do_term [t1, t2] - | Abs (_, _, t') => do_term t' + | Abs (_, _, t') => + do_term t' #> add_pseudoconst_to_table true (abs_prefix, []) | _ => I fun do_quantifier will_surely_be_skolemized body_t = do_formula pos body_t - #> (if will_surely_be_skolemized then - add_const_to_table (gensym fresh_prefix, []) + #> (if also_skolems andalso will_surely_be_skolemized then + add_pseudoconst_to_table true (gensym skolem_prefix, []) else I) and do_term_or_formula T = @@ -164,31 +197,25 @@ (**** Constant / Type Frequencies ****) -(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by - constant name and second by its list of type instantiations. For the latter, we need - a linear ordering on type const_typ list.*) - -local - -fun cons_nr CTVar = 0 - | cons_nr (CType _) = 1; +(* A two-dimensional symbol table counts frequencies of constants. It's keyed + first by constant name and second by its list of type instantiations. For the + latter, we need a linear ordering on "pseudotype list". *) -in +fun pseudotype_ord p = + case p of + (PVar, PVar) => EQUAL + | (PVar, PType _) => LESS + | (PType _, PVar) => GREATER + | (PType q1, PType q2) => + prod_ord fast_string_ord (dict_ord pseudotype_ord) (q1, q2) -fun const_typ_ord TU = - case TU of - (CType (a, Ts), CType (b, Us)) => - (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord) - | (T, U) => int_ord (cons_nr T, cons_nr U); - -end; - -structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord); +structure CTtab = + Table(type key = pseudotype list val ord = dict_ord pseudotype_ord) fun count_axiom_consts theory_relevant thy (_, th) = let fun do_const (a, T) = - let val (c, cts) = const_with_typ thy (a, T) in + let val (c, cts) = pseudoconst_for thy (a, T) in (* Two-dimensional table update. Constant maps to types maps to count. *) CTtab.map_default (cts, 0) (Integer.add 1) @@ -205,8 +232,8 @@ (**** Actual Filtering Code ****) (*The frequency of a constant is the sum of those of all instances of its type.*) -fun const_frequency const_tab (c, cts) = - CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m) +fun pseudoconst_freq match const_tab (c, cts) = + CTtab.fold (fn (cts', m) => match (cts, cts') ? Integer.add m) (the (Symtab.lookup const_tab c)) 0 handle Option.Option => 0 @@ -216,183 +243,206 @@ (* "log" seems best in practice. A constant function of one ignores the constant frequencies. *) -fun rel_log (x : real) = 1.0 + 2.0 / Math.ln (x + 1.0) -fun irrel_log (x : real) = Math.ln (x + 19.0) / 6.4 +fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0) +(* TODO: experiment +fun irrel_log n = 0.5 + 1.0 / Math.ln (Real.fromInt n + 1.0) +*) +fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4 + +(* FUDGE *) +val skolem_weight = 1.0 +val abs_weight = 2.0 (* Computes a constant's weight, as determined by its frequency. *) -val rel_const_weight = rel_log o real oo const_frequency -val irrel_const_weight = irrel_log o real oo const_frequency -(* fun irrel_const_weight _ _ = 1.0 FIXME: OLD CODE *) - -fun axiom_weight const_tab relevant_consts axiom_consts = - let - val (rel, irrel) = List.partition (const_mem relevant_consts) axiom_consts - val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0 - val irrel_weight = fold (curry Real.+ o irrel_const_weight const_tab) irrel 0.0 - val res = rel_weight / (rel_weight + irrel_weight) - in if Real.isFinite res then res else 0.0 end - -(* OLD CODE: -(*Relevant constants are weighted according to frequency, - but irrelevant constants are simply counted. Otherwise, Skolem functions, - which are rare, would harm a formula's chances of being picked.*) -fun axiom_weight const_tab relevant_consts axiom_consts = - let - val rel = filter (const_mem relevant_consts) axiom_consts - val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0 - val res = rel_weight / (rel_weight + real (length axiom_consts - length rel)) - in if Real.isFinite res then res else 0.0 end +val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes +fun irrel_weight const_tab (c as (s, _)) = + if String.isPrefix skolem_prefix s then skolem_weight + else if String.isPrefix abs_prefix s then abs_weight + else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c) +(* TODO: experiment +fun irrel_weight _ _ = 1.0 *) -(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*) -fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys +(* FUDGE *) +fun locality_multiplier General = 1.0 + | locality_multiplier Theory = 1.1 + | locality_multiplier Local = 1.3 + | locality_multiplier Chained = 2.0 + +fun axiom_weight loc const_tab relevant_consts axiom_consts = + case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts) + ||> filter_out (pseudoconst_mem swap relevant_consts) of + ([], []) => 0.0 + | (_, []) => 1.0 + | (rel, irrel) => + let + val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0 + |> curry Real.* (locality_multiplier loc) + val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0 + val res = rel_weight / (rel_weight + irrel_weight) + in if Real.isFinite res then res else 0.0 end -fun consts_of_term thy t = - Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) [] +(* TODO: experiment +fun debug_axiom_weight const_tab relevant_consts axiom_consts = + case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts) + ||> filter_out (pseudoconst_mem swap relevant_consts) of + ([], []) => 0.0 + | (_, []) => 1.0 + | (rel, irrel) => + let +val _ = tracing (PolyML.makestring ("REL: ", rel)) +val _ = tracing (PolyML.makestring ("IRREL: ", irrel)) + val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0 + val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0 + val res = rel_weight / (rel_weight + irrel_weight) + in if Real.isFinite res then res else 0.0 end +*) +fun pseudoconsts_of_term thy t = + Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys) + (get_pseudoconsts thy true (SOME true) [t]) [] fun pair_consts_axiom theory_relevant thy axiom = (axiom, axiom |> snd |> theory_const_prop_of theory_relevant - |> consts_of_term thy) - -exception CONST_OR_FREE of unit - -fun dest_Const_or_Free (Const x) = x - | dest_Const_or_Free (Free x) = x - | dest_Const_or_Free _ = raise CONST_OR_FREE () - -(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*) -fun defines thy thm gctypes = - let val tm = prop_of thm - fun defs lhs rhs = - let val (rator,args) = strip_comb lhs - val ct = const_with_typ thy (dest_Const_or_Free rator) - in - forall is_Var args andalso const_mem gctypes ct andalso - subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) - end - handle CONST_OR_FREE () => false - in - case tm of - @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => - defs lhs rhs - | _ => false - end; + |> pseudoconsts_of_term thy) type annotated_thm = - ((unit -> string * bool) * thm) * (string * const_typ list) list - -(*For a reverse sort, putting the largest values first.*) -fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) + (((unit -> string) * locality) * thm) * (string * pseudotype list) list -(* Limit the number of new facts, to prevent runaway acceptance. *) -fun take_best max_new (new_pairs : (annotated_thm * real) list) = - let val nnew = length new_pairs in - if nnew <= max_new then - (map #1 new_pairs, []) - else - let - val new_pairs = sort compare_pairs new_pairs - val accepted = List.take (new_pairs, max_new) - in - trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ - ", exceeds the limit of " ^ Int.toString max_new)); - trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); - trace_msg (fn () => "Actually passed: " ^ - space_implode ", " (map (fst o (fn f => f ()) o fst o fst o fst) accepted)); - (map #1 accepted, List.drop (new_pairs, max_new)) - end - end; +fun take_most_relevant max_max_imperfect max_relevant remaining_max + (candidates : (annotated_thm * real) list) = + let + val max_imperfect = + Real.ceil (Math.pow (max_max_imperfect, + Real.fromInt remaining_max + / Real.fromInt max_relevant)) + val (perfect, imperfect) = + candidates |> List.partition (fn (_, w) => w > 0.99999) + ||> sort (Real.compare o swap o pairself snd) + val ((accepts, more_rejects), rejects) = + chop max_imperfect imperfect |>> append perfect |>> chop remaining_max + in + trace_msg (fn () => "Number of candidates: " ^ + string_of_int (length candidates)); + trace_msg (fn () => "Effective threshold: " ^ + Real.toString (#2 (hd accepts))); + trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^ + "): " ^ (accepts + |> map (fn ((((name, _), _), _), weight) => + name () ^ " [" ^ Real.toString weight ^ "]") + |> commas)); + (accepts, more_rejects @ rejects) + end +(* FUDGE *) val threshold_divisor = 2.0 val ridiculous_threshold = 0.1 +val max_max_imperfect_fudge_factor = 0.66 -fun relevance_filter ctxt relevance_threshold relevance_convergence - defs_relevant max_new theory_relevant +fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant ({add, del, ...} : relevance_override) axioms goal_ts = - if relevance_threshold > 1.0 then - [] - else if relevance_threshold < 0.0 then - axioms - else - let - val thy = ProofContext.theory_of ctxt - val const_tab = fold (count_axiom_consts theory_relevant thy) axioms - Symtab.empty - val goal_const_tab = get_consts thy (SOME false) goal_ts - val _ = - trace_msg (fn () => "Initial constants: " ^ - commas (goal_const_tab - |> Symtab.dest - |> filter (curry (op <>) [] o snd) - |> map fst)) - val add_thms = maps (ProofContext.get_fact ctxt) add - val del_thms = maps (ProofContext.get_fact ctxt) del - fun iter j threshold rel_const_tab = - let - fun relevant ([], rejects) [] = - (* Nothing was added this iteration. *) - if j = 0 andalso threshold >= ridiculous_threshold then - (* First iteration? Try again. *) - iter 0 (threshold / threshold_divisor) rel_const_tab - (map (apsnd SOME) rejects) + let + val thy = ProofContext.theory_of ctxt + val const_tab = fold (count_axiom_consts theory_relevant thy) axioms + Symtab.empty + val add_thms = maps (ProofContext.get_fact ctxt) add + val del_thms = maps (ProofContext.get_fact ctxt) del + val max_max_imperfect = + Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor) + fun iter j remaining_max threshold rel_const_tab hopeless hopeful = + let + fun game_over rejects = + (* Add "add:" facts. *) + if null add_thms then + [] + else + map_filter (fn ((p as (_, th), _), _) => + if member Thm.eq_thm add_thms th then SOME p + else NONE) rejects + fun relevant [] rejects hopeless [] = + (* Nothing has been added this iteration. *) + if j = 0 andalso threshold >= ridiculous_threshold then + (* First iteration? Try again. *) + iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab + hopeless hopeful + else + game_over (rejects @ hopeless) + | relevant candidates rejects hopeless [] = + let + val (accepts, more_rejects) = + take_most_relevant max_max_imperfect max_relevant remaining_max + candidates + val rel_const_tab' = + rel_const_tab + |> fold (add_pseudoconst_to_table false) + (maps (snd o fst) accepts) + fun is_dirty (c, _) = + Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c + val (hopeful_rejects, hopeless_rejects) = + (rejects @ hopeless, ([], [])) + |-> fold (fn (ax as (_, consts), old_weight) => + if exists is_dirty consts then + apfst (cons (ax, NONE)) + else + apsnd (cons (ax, old_weight))) + |>> append (more_rejects + |> map (fn (ax as (_, consts), old_weight) => + (ax, if exists is_dirty consts then NONE + else SOME old_weight))) + val threshold = + threshold + (1.0 - threshold) + * Math.pow (decay, Real.fromInt (length accepts)) + val remaining_max = remaining_max - length accepts + in + trace_msg (fn () => "New or updated constants: " ^ + commas (rel_const_tab' |> Symtab.dest + |> subtract (op =) (Symtab.dest rel_const_tab) + |> map string_for_super_pseudoconst)); + map (fst o fst) accepts @ + (if remaining_max = 0 then + game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects) + else + iter (j + 1) remaining_max threshold rel_const_tab' + hopeless_rejects hopeful_rejects) + end + | relevant candidates rejects hopeless + (((ax as (((_, loc), th), axiom_consts)), cached_weight) + :: hopeful) = + let + val weight = + case cached_weight of + SOME w => w + | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts +(* TODO: experiment +val name = fst (fst (fst ax)) () +val _ = if String.isPrefix "lift.simps(3" name then +tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts)) +else +() +*) + in + if weight >= threshold then + relevant ((ax, weight) :: candidates) rejects hopeless hopeful else - (* Add "add:" facts. *) - if null add_thms then - [] - else - map_filter (fn ((p as (_, th), _), _) => - if member Thm.eq_thm add_thms th then SOME p - else NONE) rejects - | relevant (new_pairs, rejects) [] = - let - val (new_rels, more_rejects) = take_best max_new new_pairs - val rel_const_tab' = - rel_const_tab |> fold add_const_to_table (maps snd new_rels) - fun is_dirty c = - const_mem rel_const_tab' c andalso - not (const_mem rel_const_tab c) - val rejects = - more_rejects @ rejects - |> map (fn (ax as (_, consts), old_weight) => - (ax, if exists is_dirty consts then NONE - else SOME old_weight)) - val threshold = - threshold + (1.0 - threshold) * relevance_convergence - in - trace_msg (fn () => "relevant this iteration: " ^ - Int.toString (length new_rels)); - map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects - end - | relevant (new_rels, rejects) - (((ax as ((name, th), axiom_consts)), cached_weight) - :: rest) = - let - val weight = - case cached_weight of - SOME w => w - | NONE => axiom_weight const_tab rel_const_tab axiom_consts - in - if weight >= threshold orelse - (defs_relevant andalso defines thy th rel_const_tab) then - (trace_msg (fn () => - fst (name ()) ^ " passes: " ^ Real.toString weight - ^ " consts: " ^ commas (map fst axiom_consts)); - relevant ((ax, weight) :: new_rels, rejects) rest) - else - relevant (new_rels, (ax, weight) :: rejects) rest - end - in - trace_msg (fn () => "relevant_facts, current threshold: " ^ - Real.toString threshold); - relevant ([], []) - end - in - axioms |> filter_out (member Thm.eq_thm del_thms o snd) - |> map (rpair NONE o pair_consts_axiom theory_relevant thy) - |> iter 0 relevance_threshold goal_const_tab - |> tap (fn res => trace_msg (fn () => + relevant candidates ((ax, weight) :: rejects) hopeless hopeful + end + in + trace_msg (fn () => + "ITERATION " ^ string_of_int j ^ ": current threshold: " ^ + Real.toString threshold ^ ", constants: " ^ + commas (rel_const_tab |> Symtab.dest + |> filter (curry (op <>) [] o snd) + |> map string_for_super_pseudoconst)); + relevant [] [] hopeless hopeful + end + in + axioms |> filter_out (member Thm.eq_thm del_thms o snd) + |> map (rpair NONE o pair_consts_axiom theory_relevant thy) + |> iter 0 max_relevant threshold0 + (get_pseudoconsts thy false (SOME false) goal_ts) [] + |> tap (fn res => trace_msg (fn () => "Total relevant: " ^ Int.toString (length res))) - end + end + (***************************************************************) (* Retrieving and filtering lemmas *) @@ -533,22 +583,24 @@ fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths = let - val is_chained = member Thm.eq_thm chained_ths - val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt) + val thy = ProofContext.theory_of ctxt + val thy_prefix = Context.theory_name thy ^ Long_Name.separator + val global_facts = PureThy.facts_of thy val local_facts = ProofContext.facts_of ctxt val named_locals = local_facts |> Facts.dest_static [] + val is_chained = member Thm.eq_thm chained_ths (* Unnamed, not chained formulas with schematic variables are omitted, because they are rejected by the backticks (`...`) parser for some reason. *) - fun is_bad_unnamed_local th = - exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse - (exists_subterm is_Var (prop_of th) andalso not (is_chained th)) + fun is_good_unnamed_local th = + forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals + andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) val unnamed_locals = - local_facts |> Facts.props |> filter_out is_bad_unnamed_local + local_facts |> Facts.props |> filter is_good_unnamed_local |> map (pair "" o single) val full_space = - Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts); - fun add_valid_facts foldx facts = + Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) + fun add_facts global foldx facts = foldx (fn (name0, ths) => if name0 <> "" andalso forall (not o member Thm.eq_thm add_thms) ths andalso @@ -559,10 +611,16 @@ I else let + val base_loc = + if not global then Local + else if String.isPrefix thy_prefix name0 then Theory + else General val multi = length ths > 1 fun backquotify th = "`" ^ Print_Mode.setmp [Print_Mode.input] (Syntax.string_of_term ctxt) (prop_of th) ^ "`" + |> String.translate (fn c => if Char.isPrint c then str c else "") + |> simplify_spaces fun check_thms a = case try (ProofContext.get_thms ctxt) a of NONE => false @@ -575,54 +633,48 @@ not (member Thm.eq_thm add_thms th) then rest else - (fn () => - (if name0 = "" then - th |> backquotify - else - let - val name1 = Facts.extern facts name0 - val name2 = Name_Space.extern full_space name0 - in - case find_first check_thms [name1, name2, name0] of - SOME name => - let - val name = - name |> Symtab.defined reserved name ? quote - in - if multi then name ^ "(" ^ Int.toString j ^ ")" - else name - end - | NONE => "" - end, is_chained th), (multi, th)) :: rest)) ths + (((fn () => + if name0 = "" then + th |> backquotify + else + let + val name1 = Facts.extern facts name0 + val name2 = Name_Space.extern full_space name0 + in + case find_first check_thms [name1, name2, name0] of + SOME name => repair_name reserved multi j name + | NONE => "" + end), if is_chained th then Chained else base_loc), + (multi, th)) :: rest)) ths #> snd end) in - [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals) - |> add_valid_facts Facts.fold_static global_facts global_facts + [] |> add_facts false fold local_facts (unnamed_locals @ named_locals) + |> add_facts true Facts.fold_static global_facts global_facts end (* The single-name theorems go after the multiple-name ones, so that single names are preferred when both are available. *) fun name_thm_pairs ctxt respect_no_atp = - List.partition (fst o snd) #> op @ - #> map (apsnd snd) + List.partition (fst o snd) #> op @ #> map (apsnd snd) #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) (***************************************************************) (* ATP invocation methods setup *) (***************************************************************) -fun relevant_facts full_types relevance_threshold relevance_convergence - defs_relevant max_new theory_relevant - (relevance_override as {add, del, only}) +fun relevant_facts full_types (threshold0, threshold1) max_relevant + theory_relevant (relevance_override as {add, del, only}) (ctxt, (chained_ths, _)) hyp_ts concl_t = let + val decay = 1.0 - Math.pow ((1.0 - threshold1) / (1.0 - threshold0), + 1.0 / Real.fromInt (max_relevant + 1)) val add_thms = maps (ProofContext.get_fact ctxt) add val reserved = reserved_isar_keyword_table () val axioms = (if only then - maps ((fn (n, ths) => map (pair n o pair false) ths) - o name_thms_pair_from_ref ctxt reserved chained_ths) add + maps (map (fn ((name, loc), th) => ((K name, loc), (true, th))) + o name_thm_pairs_from_ref ctxt reserved chained_ths) add else all_name_thms_pairs ctxt reserved full_types add_thms chained_ths) |> name_thm_pairs ctxt (respect_no_atp andalso not only) @@ -630,11 +682,14 @@ in trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^ " theorems"); - relevance_filter ctxt relevance_threshold relevance_convergence - defs_relevant max_new theory_relevant relevance_override - axioms (concl_t :: hyp_ts) - |> map (apfst (fn f => f ())) - |> sort_wrt (fst o fst) + (if threshold0 > 1.0 orelse threshold0 > threshold1 then + [] + else if threshold0 < 0.0 then + axioms + else + relevance_filter ctxt threshold0 decay max_relevant theory_relevant + relevance_override axioms (concl_t :: hyp_ts)) + |> map (apfst (apfst (fn f => f ()))) |> sort_wrt (fst o fst) end end; diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Thu Aug 26 10:42:22 2010 +0200 @@ -7,11 +7,12 @@ signature SLEDGEHAMMER_FACT_MINIMIZE = sig + type locality = Sledgehammer_Fact_Filter.locality type params = Sledgehammer.params val minimize_theorems : - params -> int -> int -> Proof.state -> ((string * bool) * thm list) list - -> ((string * bool) * thm list) list option * string + params -> int -> int -> Proof.state -> ((string * locality) * thm list) list + -> ((string * locality) * thm list) list option * string val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit end; @@ -40,24 +41,20 @@ "") end -fun test_theorems ({debug, verbose, overlord, atps, full_types, - relevance_threshold, relevance_convergence, - defs_relevant, isar_proof, isar_shrink_factor, ...} - : params) +fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof, + isar_shrink_factor, ...} : params) (prover : prover) explicit_apply timeout subgoal state - name_thms_pairs = + axioms = let val _ = - priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...") + priority ("Testing " ^ n_theorems (map fst axioms) ^ "...") val params = {debug = debug, verbose = verbose, overlord = overlord, atps = atps, full_types = full_types, explicit_apply = explicit_apply, - relevance_threshold = relevance_threshold, - relevance_convergence = relevance_convergence, - max_relevant_per_iter = NONE, theory_relevant = NONE, - defs_relevant = defs_relevant, isar_proof = isar_proof, + relevance_thresholds = (1.01, 1.01), max_relevant = NONE, + theory_relevant = NONE, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout} - val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs + val axioms = maps (fn (n, ths) => map (pair n) ths) axioms val {context = ctxt, facts, goal} = Proof.goal state val problem = {subgoal = subgoal, goal = (ctxt, (facts, goal)), @@ -67,7 +64,7 @@ in priority (case outcome of NONE => - if length used_thm_names = length name_thms_pairs then + if length used_thm_names = length axioms then "Found proof." else "Found proof with " ^ n_theorems used_thm_names ^ "." @@ -93,10 +90,9 @@ val fudge_msecs = 1000 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." - | minimize_theorems - (params as {debug, atps = atp :: _, full_types, isar_proof, - isar_shrink_factor, timeout, ...}) - i n state name_thms_pairs = + | minimize_theorems (params as {debug, atps = atp :: _, full_types, + isar_proof, isar_shrink_factor, timeout, ...}) + i n state axioms = let val thy = Proof.theory_of state val prover = get_prover_fun thy atp @@ -106,13 +102,12 @@ val (_, hyp_ts, concl_t) = strip_subgoal goal i val explicit_apply = not (forall (Meson.is_fol_term thy) - (concl_t :: hyp_ts @ - maps (map prop_of o snd) name_thms_pairs)) + (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms)) fun do_test timeout = test_theorems params prover explicit_apply timeout i state val timer = Timer.startRealTimer () in - (case do_test timeout name_thms_pairs of + (case do_test timeout axioms of result as {outcome = NONE, pool, used_thm_names, conjecture_shape, ...} => let @@ -122,11 +117,11 @@ |> Time.fromMilliseconds val (min_thms, {proof, axiom_names, ...}) = sublinear_minimize (do_test new_timeout) - (filter_used_facts used_thm_names name_thms_pairs) ([], result) + (filter_used_facts used_thm_names axioms) ([], result) val n = length min_thms val _ = priority (cat_lines ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ - (case length (filter (snd o fst) min_thms) of + (case length (filter (curry (op =) Chained o snd o fst) min_thms) of 0 => "" | n => " (including " ^ Int.toString n ^ " chained)") ^ ".") in @@ -154,15 +149,14 @@ val ctxt = Proof.context_of state val reserved = reserved_isar_keyword_table () val chained_ths = #facts (Proof.goal state) - val name_thms_pairs = - map (apfst (fn f => f ()) - o name_thms_pair_from_ref ctxt reserved chained_ths) refs + val axioms = + maps (map (apsnd single) + o name_thm_pairs_from_ref ctxt reserved chained_ths) refs in case subgoal_count state of 0 => priority "No subgoal!" | n => - (kill_atps (); - priority (#2 (minimize_theorems params i n state name_thms_pairs))) + (kill_atps (); priority (#2 (minimize_theorems params i n state axioms))) end end; diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 26 10:42:22 2010 +0200 @@ -67,11 +67,9 @@ ("verbose", "false"), ("overlord", "false"), ("explicit_apply", "false"), - ("relevance_threshold", "40"), - ("relevance_convergence", "31"), - ("max_relevant_per_iter", "smart"), + ("relevance_thresholds", "45 95"), + ("max_relevant", "smart"), ("theory_relevant", "smart"), - ("defs_relevant", "false"), ("isar_proof", "false"), ("isar_shrink_factor", "1")] @@ -84,7 +82,6 @@ ("partial_types", "full_types"), ("implicit_apply", "explicit_apply"), ("theory_irrelevant", "theory_relevant"), - ("defs_irrelevant", "defs_relevant"), ("no_isar_proof", "isar_proof")] val params_for_minimize = @@ -158,6 +155,14 @@ SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value.") + fun lookup_int_pair name = + case lookup name of + NONE => (0, 0) + | SOME s => case s |> space_explode " " |> map Int.fromString of + [SOME n1, SOME n2] => (n1, n2) + | _ => error ("Parameter " ^ quote name ^ + "must be assigned a pair of integer values \ + \(e.g., \"60 95\")") fun lookup_int_option name = case lookup name of SOME "smart" => NONE @@ -168,25 +173,20 @@ val atps = lookup_string "atps" |> space_explode " " val full_types = lookup_bool "full_types" val explicit_apply = lookup_bool "explicit_apply" - val relevance_threshold = - 0.01 * Real.fromInt (lookup_int "relevance_threshold") - val relevance_convergence = - 0.01 * Real.fromInt (lookup_int "relevance_convergence") - val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter" + val relevance_thresholds = + lookup_int_pair "relevance_thresholds" + |> pairself (fn n => 0.01 * Real.fromInt n) + val max_relevant = lookup_int_option "max_relevant" val theory_relevant = lookup_bool_option "theory_relevant" - val defs_relevant = lookup_bool "defs_relevant" val isar_proof = lookup_bool "isar_proof" val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") val timeout = lookup_time "timeout" in {debug = debug, verbose = verbose, overlord = overlord, atps = atps, full_types = full_types, explicit_apply = explicit_apply, - relevance_threshold = relevance_threshold, - relevance_convergence = relevance_convergence, - max_relevant_per_iter = max_relevant_per_iter, - theory_relevant = theory_relevant, defs_relevant = defs_relevant, - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, - timeout = timeout} + relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, + theory_relevant = theory_relevant, isar_proof = isar_proof, + isar_shrink_factor = isar_shrink_factor, timeout = timeout} end fun get_params thy = extract_params (default_raw_params thy) diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 10:42:22 2010 +0200 @@ -8,19 +8,20 @@ signature SLEDGEHAMMER_PROOF_RECONSTRUCT = sig + type locality = Sledgehammer_Fact_Filter.locality type minimize_command = string list -> string val metis_proof_text: - bool * minimize_command * string * (string * bool) vector * thm * int - -> string * (string * bool) list + bool * minimize_command * string * (string * locality) vector * thm * int + -> string * (string * locality) list val isar_proof_text: string Symtab.table * bool * int * Proof.context * int list list - -> bool * minimize_command * string * (string * bool) vector * thm * int - -> string * (string * bool) list + -> bool * minimize_command * string * (string * locality) vector * thm * int + -> string * (string * locality) list val proof_text: bool -> string Symtab.table * bool * int * Proof.context * int list list - -> bool * minimize_command * string * (string * bool) vector * thm * int - -> string * (string * bool) list + -> bool * minimize_command * string * (string * locality) vector * thm * int + -> string * (string * locality) list end; structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = @@ -234,7 +235,7 @@ fst o Scan.finite Symbol.stopper (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output") (parse_lines pool))) - o explode o strip_spaces + o explode o strip_spaces_except_between_ident_chars (**** INTERPRETATION OF TSTP SYNTAX TREES ****) @@ -246,18 +247,18 @@ constrained by information from type literals, or by type inference. *) fun type_from_fo_term tfrees (u as ATerm (a, us)) = let val Ts = map (type_from_fo_term tfrees) us in - case strip_prefix_and_undo_ascii type_const_prefix a of + case strip_prefix_and_unascii type_const_prefix a of SOME b => Type (invert_const b, Ts) | NONE => if not (null us) then raise FO_TERM [u] (* only "tconst"s have type arguments *) - else case strip_prefix_and_undo_ascii tfree_prefix a of + else case strip_prefix_and_unascii tfree_prefix a of SOME b => let val s = "'" ^ b in TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS) end | NONE => - case strip_prefix_and_undo_ascii tvar_prefix a of + case strip_prefix_and_unascii tvar_prefix a of SOME b => TVar (("'" ^ b, 0), HOLogic.typeS) | NONE => (* Variable from the ATP, say "X1" *) @@ -267,7 +268,7 @@ (* Type class literal applied to a type. Returns triple of polarity, class, type. *) fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) = - case (strip_prefix_and_undo_ascii class_prefix a, + case (strip_prefix_and_unascii class_prefix a, map (type_from_fo_term tfrees) us) of (SOME b, [T]) => (pos, b, T) | _ => raise FO_TERM [u] @@ -309,7 +310,7 @@ [typ_u, term_u] => aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u | _ => raise FO_TERM us - else case strip_prefix_and_undo_ascii const_prefix a of + else case strip_prefix_and_unascii const_prefix a of SOME "equal" => list_comb (Const (@{const_name "op ="}, HOLogic.typeT), map (aux NONE []) us) @@ -341,10 +342,10 @@ val ts = map (aux NONE []) (us @ extra_us) val T = map fastype_of ts ---> HOLogic.typeT val t = - case strip_prefix_and_undo_ascii fixed_var_prefix a of + case strip_prefix_and_unascii fixed_var_prefix a of SOME b => Free (b, T) | NONE => - case strip_prefix_and_undo_ascii schematic_var_prefix a of + case strip_prefix_and_unascii schematic_var_prefix a of SOME b => Var ((b, 0), T) | NONE => if is_tptp_variable a then @@ -575,10 +576,10 @@ String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_") fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) = if tag = "cnf" orelse tag = "fof" then - (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of + (case strip_prefix_and_unascii axiom_prefix (List.last rest) of SOME name => if member (op =) rest "file" then - SOME (name, is_true_for axiom_names name) + SOME (name, find_first_in_vector axiom_names name General) else axiom_name_at_index num | NONE => axiom_name_at_index num) @@ -624,8 +625,8 @@ fun used_facts axiom_names = used_facts_in_atp_proof axiom_names - #> List.partition snd - #> pairself (sort_distinct (string_ord) o map fst) + #> List.partition (curry (op =) Chained o snd) + #> pairself (sort_distinct (string_ord o pairself fst)) fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names, goal, i) = @@ -633,9 +634,9 @@ val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof val n = Logic.count_prems (prop_of goal) in - (metis_line full_types i n other_lemmas ^ - minimize_line minimize_command (other_lemmas @ chained_lemmas), - map (rpair false) other_lemmas @ map (rpair true) chained_lemmas) + (metis_line full_types i n (map fst other_lemmas) ^ + minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), + other_lemmas @ chained_lemmas) end (** Isar proof construction and manipulation **) diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 10:42:22 2010 +0200 @@ -18,8 +18,8 @@ val tfrees_name : string val prepare_problem : Proof.context -> bool -> bool -> bool -> bool -> term list -> term - -> ((string * bool) * thm) list - -> string problem * string Symtab.table * int * (string * bool) vector + -> ((string * 'a) * thm) list + -> string problem * string Symtab.table * int * (string * 'a) vector end; structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE = @@ -39,11 +39,11 @@ (* Freshness almost guaranteed! *) val sledgehammer_weak_prefix = "Sledgehammer:" -datatype fol_formula = - FOLFormula of {name: string, - kind: kind, - combformula: (name, combterm) formula, - ctypes_sorts: typ list} +type fol_formula = + {name: string, + kind: kind, + combformula: (name, combterm) formula, + ctypes_sorts: typ list} fun mk_anot phi = AConn (ANot, [phi]) fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) @@ -190,15 +190,14 @@ |> kind <> Axiom ? freeze_term val (combformula, ctypes_sorts) = combformula_for_prop thy t [] in - FOLFormula {name = name, combformula = combformula, kind = kind, - ctypes_sorts = ctypes_sorts} + {name = name, combformula = combformula, kind = kind, + ctypes_sorts = ctypes_sorts} end -fun make_axiom ctxt presimp ((name, chained), th) = +fun make_axiom ctxt presimp ((name, loc), th) = case make_formula ctxt presimp name Axiom (prop_of th) of - FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => - NONE - | formula => SOME ((name, chained), formula) + {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE + | formula => SOME ((name, loc), formula) fun make_conjecture ctxt ts = let val last = length ts - 1 in map2 (fn j => make_formula ctxt true (Int.toString j) @@ -215,7 +214,7 @@ fun count_combformula (AQuant (_, _, phi)) = count_combformula phi | count_combformula (AConn (_, phis)) = fold count_combformula phis | count_combformula (AAtom tm) = count_combterm tm -fun count_fol_formula (FOLFormula {combformula, ...}) = +fun count_fol_formula ({combformula, ...} : fol_formula) = count_combformula combformula val optional_helpers = @@ -326,13 +325,13 @@ | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm) in aux end -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = +fun formula_for_axiom full_types + ({combformula, ctypes_sorts, ...} : fol_formula) = mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) (type_literals_for_types ctypes_sorts)) (formula_for_combformula full_types combformula) -fun problem_line_for_fact prefix full_types - (formula as FOLFormula {name, kind, ...}) = +fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) = Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula) fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, @@ -357,11 +356,11 @@ (fo_literal_for_arity_literal conclLit))) fun problem_line_for_conjecture full_types - (FOLFormula {name, kind, combformula, ...}) = + ({name, kind, combformula, ...} : fol_formula) = Fof (conjecture_prefix ^ name, kind, formula_for_combformula full_types combformula) -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = +fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) = map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) fun problem_line_for_free_type lit = @@ -407,7 +406,7 @@ 16383 (* large number *) else if full_types then 0 - else case strip_prefix_and_undo_ascii const_prefix s of + else case strip_prefix_and_unascii const_prefix s of SOME s' => num_type_args thy (invert_const s') | NONE => 0) | min_arity_of _ _ (SOME the_const_tab) s = diff -r 14c1085dec02 -r 3913f58d0fcc src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 26 09:12:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 26 10:42:22 2010 +0200 @@ -6,10 +6,11 @@ signature SLEDGEHAMMER_UTIL = sig - val is_true_for : (string * bool) vector -> string -> bool + val find_first_in_vector : (''a * 'b) vector -> ''a -> 'b -> 'b val plural_s : int -> string val serial_commas : string -> string list -> string list - val strip_spaces : string -> string + val simplify_spaces : string -> string + val strip_spaces_except_between_ident_chars : string -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option val scan_integer : string list -> int * string list @@ -28,8 +29,9 @@ structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = struct -fun is_true_for v s = - Vector.foldl (fn ((s', b'), b) => if s' = s then b' else b) false v +fun find_first_in_vector vec key default = + Vector.foldl (fn ((key', value'), value) => + if key' = key then value' else value) default vec fun plural_s n = if n = 1 then "" else "s" @@ -39,24 +41,27 @@ | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" - -fun strip_spaces_in_list [] = "" - | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1 - | strip_spaces_in_list [c1, c2] = - strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2] - | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) = +fun strip_spaces_in_list _ [] = "" + | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then "" else str c1 + | strip_spaces_in_list is_evil [c1, c2] = + strip_spaces_in_list is_evil [c1] ^ strip_spaces_in_list is_evil [c2] + | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) = if Char.isSpace c1 then - strip_spaces_in_list (c2 :: c3 :: cs) + strip_spaces_in_list is_evil (c2 :: c3 :: cs) else if Char.isSpace c2 then if Char.isSpace c3 then - strip_spaces_in_list (c1 :: c3 :: cs) + strip_spaces_in_list is_evil (c1 :: c3 :: cs) else - str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^ - strip_spaces_in_list (c3 :: cs) + str c1 ^ (if forall is_evil [c1, c3] then " " else "") ^ + strip_spaces_in_list is_evil (c3 :: cs) else - str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs) -val strip_spaces = strip_spaces_in_list o String.explode + str c1 ^ strip_spaces_in_list is_evil (c2 :: c3 :: cs) +fun strip_spaces is_evil = strip_spaces_in_list is_evil o String.explode + +val simplify_spaces = strip_spaces (K true) + +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" +val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char fun parse_bool_option option name s = (case s of