1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 18:46:22 2010 +0200
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 26 09:03:18 2010 +0200
1.3 @@ -447,33 +447,29 @@
1.4 \label{relevance-filter}
1.5
1.6 \begin{enum}
1.7 -\opdefault{relevance\_threshold}{int}{40}
1.8 -Specifies the threshold above which facts are considered relevant by the
1.9 -relevance filter. The option ranges from 0 to 100, where 0 means that all
1.10 -theorems are relevant.
1.11 +\opdefault{relevance\_thresholds}{int\_pair}{45~95}
1.12 +Specifies the thresholds above which facts are considered relevant by the
1.13 +relevance filter. The first threshold is used for the first iteration of the
1.14 +relevance filter and the second threshold is used for the last iteration (if it
1.15 +is reached). The effective threshold is quadratically interpolated for the other
1.16 +iterations. Each threshold ranges from 0 to 100, where 0 means that all theorems
1.17 +are relevant and 100 only theorems that refer to previously seen constants.
1.18
1.19 -\opdefault{relevance\_convergence}{int}{31}
1.20 -Specifies the convergence factor, expressed as a percentage, used by the
1.21 -relevance filter. This factor is used by the relevance filter to scale down the
1.22 -relevance of facts at each iteration of the filter.
1.23 -
1.24 -\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
1.25 -Specifies the maximum number of facts that may be added during one iteration of
1.26 -the relevance filter. If the option is set to \textit{smart}, it is set to a
1.27 -value that was empirically found to be appropriate for the ATP. A typical value
1.28 -would be 50.
1.29 +\opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}}
1.30 +Specifies the maximum number of facts that may be returned by the relevance
1.31 +filter. If the option is set to \textit{smart}, it is set to a value that was
1.32 +empirically found to be appropriate for the ATP. A typical value would be 300.
1.33
1.34 \opsmartx{theory\_relevant}{theory\_irrelevant}
1.35 Specifies whether the theory from which a fact comes should be taken into
1.36 consideration by the relevance filter. If the option is set to \textit{smart},
1.37 -it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
1.38 -because empirical results suggest that these are the best settings.
1.39 +it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
1.40 +empirical results suggest that these are the best settings.
1.41
1.42 -\opfalse{defs\_relevant}{defs\_irrelevant}
1.43 -Specifies whether the definition of constants occurring in the formula to prove
1.44 -should be considered particularly relevant. Enabling this option tends to lead
1.45 -to larger problems and typically slows down the ATPs.
1.46 -
1.47 +%\opfalse{defs\_relevant}{defs\_irrelevant}
1.48 +%Specifies whether the definition of constants occurring in the formula to prove
1.49 +%should be considered particularly relevant. Enabling this option tends to lead
1.50 +%to larger problems and typically slows down the ATPs.
1.51 \end{enum}
1.52
1.53 \subsection{Output Format}
2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 25 18:46:22 2010 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 26 09:03:18 2010 +0200
2.3 @@ -19,7 +19,7 @@
2.4 has_incomplete_mode: bool,
2.5 proof_delims: (string * string) list,
2.6 known_failures: (failure * string) list,
2.7 - default_max_relevant_per_iter: int,
2.8 + default_max_relevant: int,
2.9 default_theory_relevant: bool,
2.10 explicit_forall: bool,
2.11 use_conjecture_for_hypotheses: bool}
2.12 @@ -52,7 +52,7 @@
2.13 has_incomplete_mode: bool,
2.14 proof_delims: (string * string) list,
2.15 known_failures: (failure * string) list,
2.16 - default_max_relevant_per_iter: int,
2.17 + default_max_relevant: int,
2.18 default_theory_relevant: bool,
2.19 explicit_forall: bool,
2.20 use_conjecture_for_hypotheses: bool}
2.21 @@ -125,10 +125,20 @@
2.22 priority ("Available ATPs: " ^
2.23 commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
2.24
2.25 -fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
2.26 +fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
2.27
2.28 (* E prover *)
2.29
2.30 +(* Give older versions of E an extra second, because the "eproof" script wrongly
2.31 + subtracted an entire second to account for the overhead of the script
2.32 + itself, which is in fact much lower. *)
2.33 +fun e_bonus () =
2.34 + case getenv "E_VERSION" of
2.35 + "" => 1000
2.36 + | version =>
2.37 + if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 1000
2.38 + else 0
2.39 +
2.40 val tstp_proof_delims =
2.41 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
2.42
2.43 @@ -137,8 +147,7 @@
2.44 required_execs = [],
2.45 arguments = fn _ => fn timeout =>
2.46 "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
2.47 - \--soft-cpu-limit=" ^
2.48 - string_of_int (to_generous_secs timeout),
2.49 + \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
2.50 has_incomplete_mode = false,
2.51 proof_delims = [tstp_proof_delims],
2.52 known_failures =
2.53 @@ -150,7 +159,7 @@
2.54 "# Cannot determine problem status within resource limit"),
2.55 (OutOfResources, "SZS status: ResourceOut"),
2.56 (OutOfResources, "SZS status ResourceOut")],
2.57 - default_max_relevant_per_iter = 80 (* FUDGE *),
2.58 + default_max_relevant = 500 (* FUDGE *),
2.59 default_theory_relevant = false,
2.60 explicit_forall = false,
2.61 use_conjecture_for_hypotheses = true}
2.62 @@ -165,7 +174,7 @@
2.63 required_execs = [("SPASS_HOME", "SPASS")],
2.64 arguments = fn complete => fn timeout =>
2.65 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
2.66 - \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
2.67 + \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
2.68 |> not complete ? prefix "-SOS=1 ",
2.69 has_incomplete_mode = true,
2.70 proof_delims = [("Here is a proof", "Formulae used in the proof")],
2.71 @@ -177,7 +186,7 @@
2.72 (MalformedInput, "Undefined symbol"),
2.73 (MalformedInput, "Free Variable"),
2.74 (SpassTooOld, "tptp2dfg")],
2.75 - default_max_relevant_per_iter = 40 (* FUDGE *),
2.76 + default_max_relevant = 350 (* FUDGE *),
2.77 default_theory_relevant = true,
2.78 explicit_forall = true,
2.79 use_conjecture_for_hypotheses = true}
2.80 @@ -190,10 +199,11 @@
2.81 val vampire_config : prover_config =
2.82 {exec = ("VAMPIRE_HOME", "vampire"),
2.83 required_execs = [],
2.84 - arguments = fn _ => fn timeout =>
2.85 - "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
2.86 - " --thanks Andrei --input_file",
2.87 - has_incomplete_mode = false,
2.88 + arguments = fn complete => fn timeout =>
2.89 + ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
2.90 + " --thanks Andrei --input_file")
2.91 + |> not complete ? prefix "--sos on ",
2.92 + has_incomplete_mode = true,
2.93 proof_delims =
2.94 [("=========== Refutation ==========",
2.95 "======= End of refutation ======="),
2.96 @@ -206,7 +216,7 @@
2.97 (Unprovable, "Satisfiability detected"),
2.98 (Unprovable, "Termination reason: Satisfiable"),
2.99 (VampireTooOld, "not a valid option")],
2.100 - default_max_relevant_per_iter = 45 (* FUDGE *),
2.101 + default_max_relevant = 400 (* FUDGE *),
2.102 default_theory_relevant = false,
2.103 explicit_forall = false,
2.104 use_conjecture_for_hypotheses = true}
2.105 @@ -246,38 +256,38 @@
2.106 | SOME sys => sys
2.107
2.108 fun remote_config system_name system_versions proof_delims known_failures
2.109 - default_max_relevant_per_iter default_theory_relevant
2.110 - use_conjecture_for_hypotheses =
2.111 + default_max_relevant default_theory_relevant
2.112 + use_conjecture_for_hypotheses : prover_config =
2.113 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
2.114 required_execs = [],
2.115 arguments = fn _ => fn timeout =>
2.116 - " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
2.117 + " -t " ^ string_of_int (to_secs 0 timeout) ^ " -s " ^
2.118 the_system system_name system_versions,
2.119 has_incomplete_mode = false,
2.120 proof_delims = insert (op =) tstp_proof_delims proof_delims,
2.121 known_failures =
2.122 known_failures @ known_perl_failures @
2.123 [(TimedOut, "says Timeout")],
2.124 - default_max_relevant_per_iter = default_max_relevant_per_iter,
2.125 + default_max_relevant = default_max_relevant,
2.126 default_theory_relevant = default_theory_relevant,
2.127 explicit_forall = true,
2.128 use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
2.129
2.130 fun remotify_config system_name system_versions
2.131 - ({proof_delims, known_failures, default_max_relevant_per_iter,
2.132 + ({proof_delims, known_failures, default_max_relevant,
2.133 default_theory_relevant, use_conjecture_for_hypotheses, ...}
2.134 : prover_config) : prover_config =
2.135 remote_config system_name system_versions proof_delims known_failures
2.136 - default_max_relevant_per_iter default_theory_relevant
2.137 + default_max_relevant default_theory_relevant
2.138 use_conjecture_for_hypotheses
2.139
2.140 val remotify_name = prefix "remote_"
2.141 fun remote_prover name system_name system_versions proof_delims known_failures
2.142 - default_max_relevant_per_iter default_theory_relevant
2.143 + default_max_relevant default_theory_relevant
2.144 use_conjecture_for_hypotheses =
2.145 (remotify_name name,
2.146 remote_config system_name system_versions proof_delims known_failures
2.147 - default_max_relevant_per_iter default_theory_relevant
2.148 + default_max_relevant default_theory_relevant
2.149 use_conjecture_for_hypotheses)
2.150 fun remotify_prover (name, config) system_name system_versions =
2.151 (remotify_name name, remotify_config system_name system_versions config)
2.152 @@ -285,11 +295,11 @@
2.153 val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
2.154 val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"]
2.155 val remote_sine_e =
2.156 - remote_prover "sine_e" "SInE" [] []
2.157 - [(Unprovable, "says Unknown")] 150 (* FUDGE *) false true
2.158 + remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
2.159 + 1000 (* FUDGE *) false true
2.160 val remote_snark =
2.161 remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
2.162 - 50 (* FUDGE *) false true
2.163 + 350 (* FUDGE *) false true
2.164
2.165 (* Setup *)
2.166
3.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Wed Aug 25 18:46:22 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Aug 26 09:03:18 2010 +0200
3.3 @@ -38,11 +38,10 @@
3.4 val const_prefix: string
3.5 val type_const_prefix: string
3.6 val class_prefix: string
3.7 - val union_all: ''a list list -> ''a list
3.8 val invert_const: string -> string
3.9 val ascii_of: string -> string
3.10 - val undo_ascii_of: string -> string
3.11 - val strip_prefix_and_undo_ascii: string -> string -> string option
3.12 + val unascii_of: string -> string
3.13 + val strip_prefix_and_unascii: string -> string -> string option
3.14 val make_bound_var : string -> string
3.15 val make_schematic_var : string * int -> string
3.16 val make_fixed_var : string -> string
3.17 @@ -121,7 +120,7 @@
3.18 Alphanumeric characters are left unchanged.
3.19 The character _ goes to __
3.20 Characters in the range ASCII space to / go to _A to _P, respectively.
3.21 - Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
3.22 + Other characters go to _nnn where nnn is the decimal ASCII code.*)
3.23 val A_minus_space = Char.ord #"A" - Char.ord #" ";
3.24
3.25 fun stringN_of_int 0 _ = ""
3.26 @@ -132,9 +131,7 @@
3.27 else if c = #"_" then "__"
3.28 else if #" " <= c andalso c <= #"/"
3.29 then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
3.30 - else if Char.isPrint c
3.31 - then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
3.32 - else ""
3.33 + else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
3.34
3.35 val ascii_of = String.translate ascii_of_c;
3.36
3.37 @@ -142,29 +139,28 @@
3.38
3.39 (*We don't raise error exceptions because this code can run inside the watcher.
3.40 Also, the errors are "impossible" (hah!)*)
3.41 -fun undo_ascii_aux rcs [] = String.implode(rev rcs)
3.42 - | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) [] (*ERROR*)
3.43 +fun unascii_aux rcs [] = String.implode(rev rcs)
3.44 + | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*)
3.45 (*Three types of _ escapes: __, _A to _P, _nnn*)
3.46 - | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
3.47 - | undo_ascii_aux rcs (#"_" :: c :: cs) =
3.48 + | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs
3.49 + | unascii_aux rcs (#"_" :: c :: cs) =
3.50 if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*)
3.51 - then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
3.52 + then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
3.53 else
3.54 let val digits = List.take (c::cs, 3) handle Subscript => []
3.55 in
3.56 case Int.fromString (String.implode digits) of
3.57 - NONE => undo_ascii_aux (c:: #"_"::rcs) cs (*ERROR*)
3.58 - | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
3.59 + NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*)
3.60 + | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
3.61 end
3.62 - | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
3.63 -
3.64 -val undo_ascii_of = undo_ascii_aux [] o String.explode;
3.65 + | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs
3.66 +val unascii_of = unascii_aux [] o String.explode
3.67
3.68 (* If string s has the prefix s1, return the result of deleting it,
3.69 un-ASCII'd. *)
3.70 -fun strip_prefix_and_undo_ascii s1 s =
3.71 +fun strip_prefix_and_unascii s1 s =
3.72 if String.isPrefix s1 s then
3.73 - SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
3.74 + SOME (unascii_of (String.extract (s, size s1, NONE)))
3.75 else
3.76 NONE
3.77
3.78 @@ -514,8 +510,8 @@
3.79 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
3.80 fun add_type_consts_in_term thy =
3.81 let
3.82 - val const_typargs = Sign.const_typargs thy
3.83 - fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
3.84 + fun aux (Const x) =
3.85 + fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
3.86 | aux (Abs (_, _, u)) = aux u
3.87 | aux (Const (@{const_name skolem_id}, _) $ _) = I
3.88 | aux (t $ u) = aux t #> aux u
4.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Aug 25 18:46:22 2010 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 26 09:03:18 2010 +0200
4.3 @@ -228,15 +228,15 @@
4.4 | smart_invert_const s = invert_const s
4.5
4.6 fun hol_type_from_metis_term _ (Metis.Term.Var v) =
4.7 - (case strip_prefix_and_undo_ascii tvar_prefix v of
4.8 + (case strip_prefix_and_unascii tvar_prefix v of
4.9 SOME w => make_tvar w
4.10 | NONE => make_tvar v)
4.11 | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
4.12 - (case strip_prefix_and_undo_ascii type_const_prefix x of
4.13 + (case strip_prefix_and_unascii type_const_prefix x of
4.14 SOME tc => Term.Type (smart_invert_const tc,
4.15 map (hol_type_from_metis_term ctxt) tys)
4.16 | NONE =>
4.17 - case strip_prefix_and_undo_ascii tfree_prefix x of
4.18 + case strip_prefix_and_unascii tfree_prefix x of
4.19 SOME tf => mk_tfree ctxt tf
4.20 | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
4.21
4.22 @@ -246,10 +246,10 @@
4.23 val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
4.24 Metis.Term.toString fol_tm)
4.25 fun tm_to_tt (Metis.Term.Var v) =
4.26 - (case strip_prefix_and_undo_ascii tvar_prefix v of
4.27 + (case strip_prefix_and_unascii tvar_prefix v of
4.28 SOME w => Type (make_tvar w)
4.29 | NONE =>
4.30 - case strip_prefix_and_undo_ascii schematic_var_prefix v of
4.31 + case strip_prefix_and_unascii schematic_var_prefix v of
4.32 SOME w => Term (mk_var (w, HOLogic.typeT))
4.33 | NONE => Term (mk_var (v, HOLogic.typeT)) )
4.34 (*Var from Metis with a name like _nnn; possibly a type variable*)
4.35 @@ -266,7 +266,7 @@
4.36 and applic_to_tt ("=",ts) =
4.37 Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
4.38 | applic_to_tt (a,ts) =
4.39 - case strip_prefix_and_undo_ascii const_prefix a of
4.40 + case strip_prefix_and_unascii const_prefix a of
4.41 SOME b =>
4.42 let val c = smart_invert_const b
4.43 val ntypes = num_type_args thy c
4.44 @@ -284,14 +284,14 @@
4.45 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
4.46 end
4.47 | NONE => (*Not a constant. Is it a type constructor?*)
4.48 - case strip_prefix_and_undo_ascii type_const_prefix a of
4.49 + case strip_prefix_and_unascii type_const_prefix a of
4.50 SOME b =>
4.51 Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
4.52 | NONE => (*Maybe a TFree. Should then check that ts=[].*)
4.53 - case strip_prefix_and_undo_ascii tfree_prefix a of
4.54 + case strip_prefix_and_unascii tfree_prefix a of
4.55 SOME b => Type (mk_tfree ctxt b)
4.56 | NONE => (*a fixed variable? They are Skolem functions.*)
4.57 - case strip_prefix_and_undo_ascii fixed_var_prefix a of
4.58 + case strip_prefix_and_unascii fixed_var_prefix a of
4.59 SOME b =>
4.60 let val opr = Term.Free(b, HOLogic.typeT)
4.61 in apply_list opr (length ts) (map tm_to_tt ts) end
4.62 @@ -307,16 +307,16 @@
4.63 let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
4.64 Metis.Term.toString fol_tm)
4.65 fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
4.66 - (case strip_prefix_and_undo_ascii schematic_var_prefix v of
4.67 + (case strip_prefix_and_unascii schematic_var_prefix v of
4.68 SOME w => mk_var(w, dummyT)
4.69 | NONE => mk_var(v, dummyT))
4.70 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
4.71 Const (@{const_name "op ="}, HOLogic.typeT)
4.72 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
4.73 - (case strip_prefix_and_undo_ascii const_prefix x of
4.74 + (case strip_prefix_and_unascii const_prefix x of
4.75 SOME c => Const (smart_invert_const c, dummyT)
4.76 | NONE => (*Not a constant. Is it a fixed variable??*)
4.77 - case strip_prefix_and_undo_ascii fixed_var_prefix x of
4.78 + case strip_prefix_and_unascii fixed_var_prefix x of
4.79 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
4.80 | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
4.81 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
4.82 @@ -327,10 +327,10 @@
4.83 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
4.84 list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
4.85 | cvt (t as Metis.Term.Fn (x, [])) =
4.86 - (case strip_prefix_and_undo_ascii const_prefix x of
4.87 + (case strip_prefix_and_unascii const_prefix x of
4.88 SOME c => Const (smart_invert_const c, dummyT)
4.89 | NONE => (*Not a constant. Is it a fixed variable??*)
4.90 - case strip_prefix_and_undo_ascii fixed_var_prefix x of
4.91 + case strip_prefix_and_unascii fixed_var_prefix x of
4.92 SOME v => Free (v, dummyT)
4.93 | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
4.94 hol_term_from_metis_PT ctxt t))
4.95 @@ -410,11 +410,11 @@
4.96 " in " ^ Display.string_of_thm ctxt i_th);
4.97 NONE)
4.98 fun remove_typeinst (a, t) =
4.99 - case strip_prefix_and_undo_ascii schematic_var_prefix a of
4.100 + case strip_prefix_and_unascii schematic_var_prefix a of
4.101 SOME b => SOME (b, t)
4.102 - | NONE => case strip_prefix_and_undo_ascii tvar_prefix a of
4.103 + | NONE => case strip_prefix_and_unascii tvar_prefix a of
4.104 SOME _ => NONE (*type instantiations are forbidden!*)
4.105 - | NONE => SOME (a,t) (*internal Metis var?*)
4.106 + | NONE => SOME (a,t) (*internal Metis var?*)
4.107 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
4.108 val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
4.109 val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 18:46:22 2010 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 09:03:18 2010 +0200
5.3 @@ -18,11 +18,9 @@
5.4 atps: string list,
5.5 full_types: bool,
5.6 explicit_apply: bool,
5.7 - relevance_threshold: real,
5.8 - relevance_convergence: real,
5.9 - max_relevant_per_iter: int option,
5.10 + relevance_thresholds: real * real,
5.11 + max_relevant: int option,
5.12 theory_relevant: bool option,
5.13 - defs_relevant: bool,
5.14 isar_proof: bool,
5.15 isar_shrink_factor: int,
5.16 timeout: Time.time}
5.17 @@ -87,11 +85,9 @@
5.18 atps: string list,
5.19 full_types: bool,
5.20 explicit_apply: bool,
5.21 - relevance_threshold: real,
5.22 - relevance_convergence: real,
5.23 - max_relevant_per_iter: int option,
5.24 + relevance_thresholds: real * real,
5.25 + max_relevant: int option,
5.26 theory_relevant: bool option,
5.27 - defs_relevant: bool,
5.28 isar_proof: bool,
5.29 isar_shrink_factor: int,
5.30 timeout: Time.time}
5.31 @@ -174,10 +170,9 @@
5.32 Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
5.33 |-- Scan.repeat parse_clause_formula_pair
5.34 val extract_clause_formula_relation =
5.35 - Substring.full
5.36 - #> Substring.position set_ClauseFormulaRelationN
5.37 - #> snd #> Substring.string #> strip_spaces #> explode
5.38 - #> parse_clause_formula_relation #> fst
5.39 + Substring.full #> Substring.position set_ClauseFormulaRelationN
5.40 + #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
5.41 + #> explode #> parse_clause_formula_relation #> fst
5.42
5.43 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
5.44 axiom_names =
5.45 @@ -190,15 +185,14 @@
5.46 val seq = extract_clause_sequence output
5.47 val name_map = extract_clause_formula_relation output
5.48 fun renumber_conjecture j =
5.49 - conjecture_prefix ^ Int.toString (j - j0)
5.50 + conjecture_prefix ^ string_of_int (j - j0)
5.51 |> AList.find (fn (s, ss) => member (op =) ss s) name_map
5.52 |> map (fn s => find_index (curry (op =) s) seq + 1)
5.53 fun name_for_number j =
5.54 let
5.55 val axioms =
5.56 - j |> AList.lookup (op =) name_map
5.57 - |> these |> map_filter (try (unprefix axiom_prefix))
5.58 - |> map undo_ascii_of
5.59 + j |> AList.lookup (op =) name_map |> these
5.60 + |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
5.61 val chained = forall (is_true_for axiom_names) axioms
5.62 in (axioms |> space_implode " ", chained) end
5.63 in
5.64 @@ -213,12 +207,11 @@
5.65
5.66 fun prover_fun atp_name
5.67 {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
5.68 - known_failures, default_max_relevant_per_iter, default_theory_relevant,
5.69 + known_failures, default_max_relevant, default_theory_relevant,
5.70 explicit_forall, use_conjecture_for_hypotheses}
5.71 ({debug, verbose, overlord, full_types, explicit_apply,
5.72 - relevance_threshold, relevance_convergence,
5.73 - max_relevant_per_iter, theory_relevant,
5.74 - defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
5.75 + relevance_thresholds, max_relevant, theory_relevant, isar_proof,
5.76 + isar_shrink_factor, timeout, ...} : params)
5.77 minimize_command
5.78 ({subgoal, goal, relevance_override, axioms} : problem) =
5.79 let
5.80 @@ -226,7 +219,7 @@
5.81 val thy = ProofContext.theory_of ctxt
5.82 val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
5.83
5.84 - fun print s = (priority s; if debug then tracing s else ())
5.85 + val print = priority
5.86 fun print_v f = () |> verbose ? print o f
5.87 fun print_d f = () |> debug ? print o f
5.88
5.89 @@ -234,15 +227,13 @@
5.90 case axioms of
5.91 SOME axioms => axioms
5.92 | NONE =>
5.93 - (relevant_facts full_types relevance_threshold relevance_convergence
5.94 - defs_relevant
5.95 - (the_default default_max_relevant_per_iter
5.96 - max_relevant_per_iter)
5.97 + (relevant_facts full_types relevance_thresholds
5.98 + (the_default default_max_relevant max_relevant)
5.99 (the_default default_theory_relevant theory_relevant)
5.100 relevance_override goal hyp_ts concl_t
5.101 |> tap ((fn n => print_v (fn () =>
5.102 - "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
5.103 - " for " ^ quote atp_name ^ ".")) o length))
5.104 + "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
5.105 + " for " ^ quote atp_name ^ ".")) o length))
5.106
5.107 (* path to unique problem file *)
5.108 val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
5.109 @@ -261,6 +252,7 @@
5.110 else error ("No such directory: " ^ the_dest_dir ^ ".")
5.111 end;
5.112
5.113 + val measure_run_time = verbose orelse Config.get ctxt measure_runtime
5.114 val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
5.115 (* write out problem file and call prover *)
5.116 fun command_line complete timeout probfile =
5.117 @@ -268,10 +260,8 @@
5.118 val core = File.shell_path command ^ " " ^ arguments complete timeout ^
5.119 " " ^ File.shell_path probfile
5.120 in
5.121 - (if Config.get ctxt measure_runtime then
5.122 - "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
5.123 - else
5.124 - "exec " ^ core) ^ " 2>&1"
5.125 + (if measure_run_time then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
5.126 + else "exec " ^ core) ^ " 2>&1"
5.127 end
5.128 fun split_time s =
5.129 let
5.130 @@ -300,14 +290,11 @@
5.131 prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
5.132 else
5.133 I)
5.134 - |>> (if Config.get ctxt measure_runtime then split_time
5.135 - else rpair 0)
5.136 + |>> (if measure_run_time then split_time else rpair 0)
5.137 val (proof, outcome) =
5.138 extract_proof_and_outcome complete res_code proof_delims
5.139 known_failures output
5.140 in (output, msecs, proof, outcome) end
5.141 - val _ = print_d (fn () => "Preparing problem for " ^
5.142 - quote atp_name ^ "...")
5.143 val readable_names = debug andalso overlord
5.144 val (problem, pool, conjecture_offset, axiom_names) =
5.145 prepare_problem ctxt readable_names explicit_forall full_types
5.146 @@ -358,6 +345,11 @@
5.147 proof_text isar_proof
5.148 (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
5.149 (full_types, minimize_command, proof, axiom_names, th, subgoal)
5.150 + |>> (fn message =>
5.151 + message ^ (if verbose then
5.152 + "\nATP CPU time: " ^ string_of_int msecs ^ " ms."
5.153 + else
5.154 + ""))
5.155 | SOME failure => (string_for_failure failure, [])
5.156 in
5.157 {outcome = outcome, message = message, pool = pool,
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 18:46:22 2010 +0200
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 09:03:18 2010 +0200
6.3 @@ -11,11 +11,11 @@
6.4 only: bool}
6.5
6.6 val trace : bool Unsynchronized.ref
6.7 - val name_thms_pair_from_ref :
6.8 + val name_thm_pairs_from_ref :
6.9 Proof.context -> unit Symtab.table -> thm list -> Facts.ref
6.10 - -> (unit -> string * bool) * thm list
6.11 + -> ((unit -> string * bool) * (bool * thm)) list
6.12 val relevant_facts :
6.13 - bool -> real -> real -> bool -> int -> bool -> relevance_override
6.14 + bool -> real * real -> int -> bool -> relevance_override
6.15 -> Proof.context * (thm list * 'a) -> term list -> term
6.16 -> ((string * bool) * thm) list
6.17 end;
6.18 @@ -37,13 +37,22 @@
6.19
6.20 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
6.21
6.22 -fun name_thms_pair_from_ref ctxt reserved chained_ths xref =
6.23 - let val ths = ProofContext.get_fact ctxt xref in
6.24 - (fn () => let
6.25 - val name = Facts.string_of_ref xref
6.26 - val name = name |> Symtab.defined reserved name ? quote
6.27 - val chained = forall (member Thm.eq_thm chained_ths) ths
6.28 - in (name, chained) end, ths)
6.29 +fun repair_name reserved multi j name =
6.30 + (name |> Symtab.defined reserved name ? quote) ^
6.31 + (if multi then "(" ^ Int.toString j ^ ")" else "")
6.32 +
6.33 +fun name_thm_pairs_from_ref ctxt reserved chained_ths xref =
6.34 + let
6.35 + val ths = ProofContext.get_fact ctxt xref
6.36 + val name = Facts.string_of_ref xref
6.37 + val multi = length ths > 1
6.38 + in
6.39 + fold (fn th => fn (j, rest) =>
6.40 + (j + 1, (fn () => (repair_name reserved multi j name,
6.41 + member Thm.eq_thm chained_ths th),
6.42 + (multi, th)) :: rest))
6.43 + ths (1, [])
6.44 + |> snd
6.45 end
6.46
6.47 (***************************************************************)
6.48 @@ -53,61 +62,81 @@
6.49 (*** constants with types ***)
6.50
6.51 (*An abstraction of Isabelle types*)
6.52 -datatype const_typ = CTVar | CType of string * const_typ list
6.53 +datatype pseudotype = PVar | PType of string * pseudotype list
6.54 +
6.55 +fun string_for_pseudotype PVar = "?"
6.56 + | string_for_pseudotype (PType (s, Ts)) =
6.57 + (case Ts of
6.58 + [] => ""
6.59 + | [T] => string_for_pseudotype T
6.60 + | Ts => string_for_pseudotypes Ts ^ " ") ^ s
6.61 +and string_for_pseudotypes Ts =
6.62 + "(" ^ commas (map string_for_pseudotype Ts) ^ ")"
6.63
6.64 (*Is the second type an instance of the first one?*)
6.65 -fun match_type (CType(con1,args1)) (CType(con2,args2)) =
6.66 - con1=con2 andalso match_types args1 args2
6.67 - | match_type CTVar _ = true
6.68 - | match_type _ CTVar = false
6.69 -and match_types [] [] = true
6.70 - | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
6.71 +fun match_pseudotype (PType (a, T), PType (b, U)) =
6.72 + a = b andalso match_pseudotypes (T, U)
6.73 + | match_pseudotype (PVar, _) = true
6.74 + | match_pseudotype (_, PVar) = false
6.75 +and match_pseudotypes ([], []) = true
6.76 + | match_pseudotypes (T :: Ts, U :: Us) =
6.77 + match_pseudotype (T, U) andalso match_pseudotypes (Ts, Us)
6.78
6.79 (*Is there a unifiable constant?*)
6.80 -fun const_mem const_tab (c, c_typ) =
6.81 - exists (match_types c_typ) (these (Symtab.lookup const_tab c))
6.82 +fun pseudoconst_mem f const_tab (c, c_typ) =
6.83 + exists (curry (match_pseudotypes o f) c_typ)
6.84 + (these (Symtab.lookup const_tab c))
6.85
6.86 -(*Maps a "real" type to a const_typ*)
6.87 -fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
6.88 - | const_typ_of (TFree _) = CTVar
6.89 - | const_typ_of (TVar _) = CTVar
6.90 +fun pseudotype_for (Type (c,typs)) = PType (c, map pseudotype_for typs)
6.91 + | pseudotype_for (TFree _) = PVar
6.92 + | pseudotype_for (TVar _) = PVar
6.93 +(* Pairs a constant with the list of its type instantiations. *)
6.94 +fun pseudoconst_for thy (c, T) =
6.95 + (c, map pseudotype_for (Sign.const_typargs thy (c, T)))
6.96 + handle TYPE _ => (c, []) (* Variable (locale constant): monomorphic *)
6.97
6.98 -(*Pairs a constant with the list of its type instantiations (using const_typ)*)
6.99 -fun const_with_typ thy (c,typ) =
6.100 - let val tvars = Sign.const_typargs thy (c,typ) in
6.101 - (c, map const_typ_of tvars) end
6.102 - handle TYPE _ => (c, []) (*Variable (locale constant): monomorphic*)
6.103 +fun string_for_pseudoconst (s, []) = s
6.104 + | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts
6.105 +fun string_for_super_pseudoconst (s, [[]]) = s
6.106 + | string_for_super_pseudoconst (s, Tss) =
6.107 + s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
6.108
6.109 -(*Add a const/type pair to the table, but a [] entry means a standard connective,
6.110 - which we ignore.*)
6.111 -fun add_const_to_table (c, ctyps) =
6.112 - Symtab.map_default (c, [ctyps])
6.113 - (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
6.114 +val abs_prefix = "Sledgehammer.abs"
6.115 +val skolem_prefix = "Sledgehammer.sko"
6.116 +
6.117 +(* Add a pseudoconstant to the table, but a [] entry means a standard
6.118 + connective, which we ignore.*)
6.119 +fun add_pseudoconst_to_table also_skolem (c, ctyps) =
6.120 + if also_skolem orelse not (String.isPrefix skolem_prefix c) then
6.121 + Symtab.map_default (c, [ctyps])
6.122 + (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
6.123 + else
6.124 + I
6.125
6.126 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
6.127
6.128 -val fresh_prefix = "Sledgehammer.FRESH."
6.129 val flip = Option.map not
6.130 (* These are typically simplified away by "Meson.presimplify". *)
6.131 val boring_consts =
6.132 [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
6.133
6.134 -fun get_consts thy pos ts =
6.135 +fun get_pseudoconsts thy also_skolems pos ts =
6.136 let
6.137 (* We include free variables, as well as constants, to handle locales. For
6.138 each quantifiers that must necessarily be skolemized by the ATP, we
6.139 introduce a fresh constant to simulate the effect of Skolemization. *)
6.140 fun do_term t =
6.141 case t of
6.142 - Const x => add_const_to_table (const_with_typ thy x)
6.143 - | Free (s, _) => add_const_to_table (s, [])
6.144 + Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x)
6.145 + | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
6.146 | t1 $ t2 => fold do_term [t1, t2]
6.147 - | Abs (_, _, t') => do_term t'
6.148 + | Abs (_, _, t') =>
6.149 + do_term t' #> add_pseudoconst_to_table true (abs_prefix, [])
6.150 | _ => I
6.151 fun do_quantifier will_surely_be_skolemized body_t =
6.152 do_formula pos body_t
6.153 - #> (if will_surely_be_skolemized then
6.154 - add_const_to_table (gensym fresh_prefix, [])
6.155 + #> (if also_skolems andalso will_surely_be_skolemized then
6.156 + add_pseudoconst_to_table true (gensym skolem_prefix, [])
6.157 else
6.158 I)
6.159 and do_term_or_formula T =
6.160 @@ -164,31 +193,25 @@
6.161
6.162 (**** Constant / Type Frequencies ****)
6.163
6.164 -(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
6.165 - constant name and second by its list of type instantiations. For the latter, we need
6.166 - a linear ordering on type const_typ list.*)
6.167 +(* A two-dimensional symbol table counts frequencies of constants. It's keyed
6.168 + first by constant name and second by its list of type instantiations. For the
6.169 + latter, we need a linear ordering on "pseudotype list". *)
6.170
6.171 -local
6.172 +fun pseudotype_ord p =
6.173 + case p of
6.174 + (PVar, PVar) => EQUAL
6.175 + | (PVar, PType _) => LESS
6.176 + | (PType _, PVar) => GREATER
6.177 + | (PType q1, PType q2) =>
6.178 + prod_ord fast_string_ord (dict_ord pseudotype_ord) (q1, q2)
6.179
6.180 -fun cons_nr CTVar = 0
6.181 - | cons_nr (CType _) = 1;
6.182 -
6.183 -in
6.184 -
6.185 -fun const_typ_ord TU =
6.186 - case TU of
6.187 - (CType (a, Ts), CType (b, Us)) =>
6.188 - (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
6.189 - | (T, U) => int_ord (cons_nr T, cons_nr U);
6.190 -
6.191 -end;
6.192 -
6.193 -structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
6.194 +structure CTtab =
6.195 + Table(type key = pseudotype list val ord = dict_ord pseudotype_ord)
6.196
6.197 fun count_axiom_consts theory_relevant thy (_, th) =
6.198 let
6.199 fun do_const (a, T) =
6.200 - let val (c, cts) = const_with_typ thy (a, T) in
6.201 + let val (c, cts) = pseudoconst_for thy (a, T) in
6.202 (* Two-dimensional table update. Constant maps to types maps to
6.203 count. *)
6.204 CTtab.map_default (cts, 0) (Integer.add 1)
6.205 @@ -205,8 +228,8 @@
6.206 (**** Actual Filtering Code ****)
6.207
6.208 (*The frequency of a constant is the sum of those of all instances of its type.*)
6.209 -fun const_frequency const_tab (c, cts) =
6.210 - CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
6.211 +fun pseudoconst_freq match const_tab (c, cts) =
6.212 + CTtab.fold (fn (cts', m) => match (cts, cts') ? Integer.add m)
6.213 (the (Symtab.lookup const_tab c)) 0
6.214 handle Option.Option => 0
6.215
6.216 @@ -216,183 +239,193 @@
6.217
6.218 (* "log" seems best in practice. A constant function of one ignores the constant
6.219 frequencies. *)
6.220 -fun rel_log (x : real) = 1.0 + 2.0 / Math.ln (x + 1.0)
6.221 -fun irrel_log (x : real) = Math.ln (x + 19.0) / 6.4
6.222 +fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0)
6.223 +(* TODO: experiment
6.224 +fun irrel_log n = 0.5 + 1.0 / Math.ln (Real.fromInt n + 1.0)
6.225 +*)
6.226 +fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
6.227
6.228 (* Computes a constant's weight, as determined by its frequency. *)
6.229 -val rel_const_weight = rel_log o real oo const_frequency
6.230 -val irrel_const_weight = irrel_log o real oo const_frequency
6.231 -(* fun irrel_const_weight _ _ = 1.0 FIXME: OLD CODE *)
6.232 +val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
6.233 +fun irrel_weight const_tab (c as (s, _)) =
6.234 + if String.isPrefix skolem_prefix s then 1.0
6.235 + else if String.isPrefix abs_prefix s then 2.0
6.236 + else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
6.237 +(* TODO: experiment
6.238 +fun irrel_weight _ _ = 1.0
6.239 +*)
6.240
6.241 fun axiom_weight const_tab relevant_consts axiom_consts =
6.242 - let
6.243 - val (rel, irrel) = List.partition (const_mem relevant_consts) axiom_consts
6.244 - val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
6.245 - val irrel_weight = fold (curry Real.+ o irrel_const_weight const_tab) irrel 0.0
6.246 - val res = rel_weight / (rel_weight + irrel_weight)
6.247 - in if Real.isFinite res then res else 0.0 end
6.248 + case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
6.249 + ||> filter_out (pseudoconst_mem swap relevant_consts) of
6.250 + ([], []) => 0.0
6.251 + | (_, []) => 1.0
6.252 + | (rel, irrel) =>
6.253 + let
6.254 + val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
6.255 + val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
6.256 + val res = rel_weight / (rel_weight + irrel_weight)
6.257 + in if Real.isFinite res then res else 0.0 end
6.258
6.259 -(* OLD CODE:
6.260 -(*Relevant constants are weighted according to frequency,
6.261 - but irrelevant constants are simply counted. Otherwise, Skolem functions,
6.262 - which are rare, would harm a formula's chances of being picked.*)
6.263 -fun axiom_weight const_tab relevant_consts axiom_consts =
6.264 - let
6.265 - val rel = filter (const_mem relevant_consts) axiom_consts
6.266 - val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
6.267 - val res = rel_weight / (rel_weight + real (length axiom_consts - length rel))
6.268 - in if Real.isFinite res then res else 0.0 end
6.269 +(* TODO: experiment
6.270 +fun debug_axiom_weight const_tab relevant_consts axiom_consts =
6.271 + case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
6.272 + ||> filter_out (pseudoconst_mem swap relevant_consts) of
6.273 + ([], []) => 0.0
6.274 + | (_, []) => 1.0
6.275 + | (rel, irrel) =>
6.276 + let
6.277 +val _ = tracing (PolyML.makestring ("REL: ", rel))
6.278 +val _ = tracing (PolyML.makestring ("IRREL: ", irrel))
6.279 + val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
6.280 + val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
6.281 + val res = rel_weight / (rel_weight + irrel_weight)
6.282 + in if Real.isFinite res then res else 0.0 end
6.283 *)
6.284
6.285 -(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
6.286 -fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys
6.287 -
6.288 -fun consts_of_term thy t =
6.289 - Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) []
6.290 -
6.291 +fun pseudoconsts_of_term thy t =
6.292 + Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
6.293 + (get_pseudoconsts thy true (SOME true) [t]) []
6.294 fun pair_consts_axiom theory_relevant thy axiom =
6.295 (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
6.296 - |> consts_of_term thy)
6.297 -
6.298 -exception CONST_OR_FREE of unit
6.299 -
6.300 -fun dest_Const_or_Free (Const x) = x
6.301 - | dest_Const_or_Free (Free x) = x
6.302 - | dest_Const_or_Free _ = raise CONST_OR_FREE ()
6.303 -
6.304 -(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
6.305 -fun defines thy thm gctypes =
6.306 - let val tm = prop_of thm
6.307 - fun defs lhs rhs =
6.308 - let val (rator,args) = strip_comb lhs
6.309 - val ct = const_with_typ thy (dest_Const_or_Free rator)
6.310 - in
6.311 - forall is_Var args andalso const_mem gctypes ct andalso
6.312 - subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
6.313 - end
6.314 - handle CONST_OR_FREE () => false
6.315 - in
6.316 - case tm of
6.317 - @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
6.318 - defs lhs rhs
6.319 - | _ => false
6.320 - end;
6.321 + |> pseudoconsts_of_term thy)
6.322
6.323 type annotated_thm =
6.324 - ((unit -> string * bool) * thm) * (string * const_typ list) list
6.325 + ((unit -> string * bool) * thm) * (string * pseudotype list) list
6.326
6.327 -(*For a reverse sort, putting the largest values first.*)
6.328 -fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
6.329 -
6.330 -(* Limit the number of new facts, to prevent runaway acceptance. *)
6.331 -fun take_best max_new (new_pairs : (annotated_thm * real) list) =
6.332 - let val nnew = length new_pairs in
6.333 - if nnew <= max_new then
6.334 - (map #1 new_pairs, [])
6.335 - else
6.336 - let
6.337 - val new_pairs = sort compare_pairs new_pairs
6.338 - val accepted = List.take (new_pairs, max_new)
6.339 - in
6.340 - trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
6.341 - ", exceeds the limit of " ^ Int.toString max_new));
6.342 - trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
6.343 - trace_msg (fn () => "Actually passed: " ^
6.344 - space_implode ", " (map (fst o (fn f => f ()) o fst o fst o fst) accepted));
6.345 - (map #1 accepted, List.drop (new_pairs, max_new))
6.346 - end
6.347 - end;
6.348 +fun take_most_relevant max_max_imperfect max_relevant remaining_max
6.349 + (candidates : (annotated_thm * real) list) =
6.350 + let
6.351 + val max_imperfect =
6.352 + Real.ceil (Math.pow (max_max_imperfect,
6.353 + Real.fromInt remaining_max
6.354 + / Real.fromInt max_relevant))
6.355 + val (perfect, imperfect) =
6.356 + candidates |> List.partition (fn (_, w) => w > 0.99999)
6.357 + ||> sort (Real.compare o swap o pairself snd)
6.358 + val ((accepts, more_rejects), rejects) =
6.359 + chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
6.360 + in
6.361 + trace_msg (fn () => "Number of candidates: " ^
6.362 + string_of_int (length candidates));
6.363 + trace_msg (fn () => "Effective threshold: " ^
6.364 + Real.toString (#2 (hd accepts)));
6.365 + trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
6.366 + "): " ^ (accepts
6.367 + |> map (fn (((name, _), _), weight) =>
6.368 + fst (name ()) ^ " [" ^ Real.toString weight ^ "]")
6.369 + |> commas));
6.370 + (accepts, more_rejects @ rejects)
6.371 + end
6.372
6.373 val threshold_divisor = 2.0
6.374 val ridiculous_threshold = 0.1
6.375 +val max_max_imperfect_fudge_factor = 0.66
6.376
6.377 -fun relevance_filter ctxt relevance_threshold relevance_convergence
6.378 - defs_relevant max_new theory_relevant
6.379 +fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
6.380 ({add, del, ...} : relevance_override) axioms goal_ts =
6.381 - if relevance_threshold > 1.0 then
6.382 - []
6.383 - else if relevance_threshold < 0.0 then
6.384 - axioms
6.385 - else
6.386 - let
6.387 - val thy = ProofContext.theory_of ctxt
6.388 - val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
6.389 - Symtab.empty
6.390 - val goal_const_tab = get_consts thy (SOME false) goal_ts
6.391 - val _ =
6.392 - trace_msg (fn () => "Initial constants: " ^
6.393 - commas (goal_const_tab
6.394 - |> Symtab.dest
6.395 - |> filter (curry (op <>) [] o snd)
6.396 - |> map fst))
6.397 - val add_thms = maps (ProofContext.get_fact ctxt) add
6.398 - val del_thms = maps (ProofContext.get_fact ctxt) del
6.399 - fun iter j threshold rel_const_tab =
6.400 - let
6.401 - fun relevant ([], rejects) [] =
6.402 - (* Nothing was added this iteration. *)
6.403 - if j = 0 andalso threshold >= ridiculous_threshold then
6.404 - (* First iteration? Try again. *)
6.405 - iter 0 (threshold / threshold_divisor) rel_const_tab
6.406 - (map (apsnd SOME) rejects)
6.407 + let
6.408 + val thy = ProofContext.theory_of ctxt
6.409 + val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
6.410 + Symtab.empty
6.411 + val add_thms = maps (ProofContext.get_fact ctxt) add
6.412 + val del_thms = maps (ProofContext.get_fact ctxt) del
6.413 + val max_max_imperfect =
6.414 + Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor)
6.415 + fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
6.416 + let
6.417 + fun game_over rejects =
6.418 + (* Add "add:" facts. *)
6.419 + if null add_thms then
6.420 + []
6.421 + else
6.422 + map_filter (fn ((p as (_, th), _), _) =>
6.423 + if member Thm.eq_thm add_thms th then SOME p
6.424 + else NONE) rejects
6.425 + fun relevant [] rejects hopeless [] =
6.426 + (* Nothing has been added this iteration. *)
6.427 + if j = 0 andalso threshold >= ridiculous_threshold then
6.428 + (* First iteration? Try again. *)
6.429 + iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
6.430 + hopeless hopeful
6.431 + else
6.432 + game_over (rejects @ hopeless)
6.433 + | relevant candidates rejects hopeless [] =
6.434 + let
6.435 + val (accepts, more_rejects) =
6.436 + take_most_relevant max_max_imperfect max_relevant remaining_max
6.437 + candidates
6.438 + val rel_const_tab' =
6.439 + rel_const_tab
6.440 + |> fold (add_pseudoconst_to_table false)
6.441 + (maps (snd o fst) accepts)
6.442 + fun is_dirty (c, _) =
6.443 + Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
6.444 + val (hopeful_rejects, hopeless_rejects) =
6.445 + (rejects @ hopeless, ([], []))
6.446 + |-> fold (fn (ax as (_, consts), old_weight) =>
6.447 + if exists is_dirty consts then
6.448 + apfst (cons (ax, NONE))
6.449 + else
6.450 + apsnd (cons (ax, old_weight)))
6.451 + |>> append (more_rejects
6.452 + |> map (fn (ax as (_, consts), old_weight) =>
6.453 + (ax, if exists is_dirty consts then NONE
6.454 + else SOME old_weight)))
6.455 + val threshold =
6.456 + threshold + (1.0 - threshold)
6.457 + * Math.pow (decay, Real.fromInt (length accepts))
6.458 + val remaining_max = remaining_max - length accepts
6.459 + in
6.460 + trace_msg (fn () => "New or updated constants: " ^
6.461 + commas (rel_const_tab' |> Symtab.dest
6.462 + |> subtract (op =) (Symtab.dest rel_const_tab)
6.463 + |> map string_for_super_pseudoconst));
6.464 + map (fst o fst) accepts @
6.465 + (if remaining_max = 0 then
6.466 + game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
6.467 + else
6.468 + iter (j + 1) remaining_max threshold rel_const_tab'
6.469 + hopeless_rejects hopeful_rejects)
6.470 + end
6.471 + | relevant candidates rejects hopeless
6.472 + (((ax as ((name, th), axiom_consts)), cached_weight)
6.473 + :: hopeful) =
6.474 + let
6.475 + val weight =
6.476 + case cached_weight of
6.477 + SOME w => w
6.478 + | NONE => axiom_weight const_tab rel_const_tab axiom_consts
6.479 +(* TODO: experiment
6.480 +val _ = if String.isPrefix "lift.simps(3" (fst (name ())) then
6.481 +tracing ("*** " ^ (fst (name ())) ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
6.482 +else
6.483 +()
6.484 +*)
6.485 + in
6.486 + if weight >= threshold then
6.487 + relevant ((ax, weight) :: candidates) rejects hopeless hopeful
6.488 else
6.489 - (* Add "add:" facts. *)
6.490 - if null add_thms then
6.491 - []
6.492 - else
6.493 - map_filter (fn ((p as (_, th), _), _) =>
6.494 - if member Thm.eq_thm add_thms th then SOME p
6.495 - else NONE) rejects
6.496 - | relevant (new_pairs, rejects) [] =
6.497 - let
6.498 - val (new_rels, more_rejects) = take_best max_new new_pairs
6.499 - val rel_const_tab' =
6.500 - rel_const_tab |> fold add_const_to_table (maps snd new_rels)
6.501 - fun is_dirty c =
6.502 - const_mem rel_const_tab' c andalso
6.503 - not (const_mem rel_const_tab c)
6.504 - val rejects =
6.505 - more_rejects @ rejects
6.506 - |> map (fn (ax as (_, consts), old_weight) =>
6.507 - (ax, if exists is_dirty consts then NONE
6.508 - else SOME old_weight))
6.509 - val threshold =
6.510 - threshold + (1.0 - threshold) * relevance_convergence
6.511 - in
6.512 - trace_msg (fn () => "relevant this iteration: " ^
6.513 - Int.toString (length new_rels));
6.514 - map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects
6.515 - end
6.516 - | relevant (new_rels, rejects)
6.517 - (((ax as ((name, th), axiom_consts)), cached_weight)
6.518 - :: rest) =
6.519 - let
6.520 - val weight =
6.521 - case cached_weight of
6.522 - SOME w => w
6.523 - | NONE => axiom_weight const_tab rel_const_tab axiom_consts
6.524 - in
6.525 - if weight >= threshold orelse
6.526 - (defs_relevant andalso defines thy th rel_const_tab) then
6.527 - (trace_msg (fn () =>
6.528 - fst (name ()) ^ " passes: " ^ Real.toString weight
6.529 - ^ " consts: " ^ commas (map fst axiom_consts));
6.530 - relevant ((ax, weight) :: new_rels, rejects) rest)
6.531 - else
6.532 - relevant (new_rels, (ax, weight) :: rejects) rest
6.533 - end
6.534 - in
6.535 - trace_msg (fn () => "relevant_facts, current threshold: " ^
6.536 - Real.toString threshold);
6.537 - relevant ([], [])
6.538 - end
6.539 - in
6.540 - axioms |> filter_out (member Thm.eq_thm del_thms o snd)
6.541 - |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
6.542 - |> iter 0 relevance_threshold goal_const_tab
6.543 - |> tap (fn res => trace_msg (fn () =>
6.544 + relevant candidates ((ax, weight) :: rejects) hopeless hopeful
6.545 + end
6.546 + in
6.547 + trace_msg (fn () =>
6.548 + "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
6.549 + Real.toString threshold ^ ", constants: " ^
6.550 + commas (rel_const_tab |> Symtab.dest
6.551 + |> filter (curry (op <>) [] o snd)
6.552 + |> map string_for_super_pseudoconst));
6.553 + relevant [] [] hopeless hopeful
6.554 + end
6.555 + in
6.556 + axioms |> filter_out (member Thm.eq_thm del_thms o snd)
6.557 + |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
6.558 + |> iter 0 max_relevant threshold0
6.559 + (get_pseudoconsts thy false (SOME false) goal_ts) []
6.560 + |> tap (fn res => trace_msg (fn () =>
6.561 "Total relevant: " ^ Int.toString (length res)))
6.562 - end
6.563 + end
6.564 +
6.565
6.566 (***************************************************************)
6.567 (* Retrieving and filtering lemmas *)
6.568 @@ -540,14 +573,14 @@
6.569 (* Unnamed, not chained formulas with schematic variables are omitted,
6.570 because they are rejected by the backticks (`...`) parser for some
6.571 reason. *)
6.572 - fun is_bad_unnamed_local th =
6.573 - exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
6.574 - (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
6.575 + fun is_good_unnamed_local th =
6.576 + forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
6.577 + andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
6.578 val unnamed_locals =
6.579 - local_facts |> Facts.props |> filter_out is_bad_unnamed_local
6.580 + local_facts |> Facts.props |> filter is_good_unnamed_local
6.581 |> map (pair "" o single)
6.582 val full_space =
6.583 - Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
6.584 + Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
6.585 fun add_valid_facts foldx facts =
6.586 foldx (fn (name0, ths) =>
6.587 if name0 <> "" andalso
6.588 @@ -563,6 +596,8 @@
6.589 fun backquotify th =
6.590 "`" ^ Print_Mode.setmp [Print_Mode.input]
6.591 (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
6.592 + |> String.translate (fn c => if Char.isPrint c then str c else "")
6.593 + |> simplify_spaces
6.594 fun check_thms a =
6.595 case try (ProofContext.get_thms ctxt) a of
6.596 NONE => false
6.597 @@ -584,14 +619,7 @@
6.598 val name2 = Name_Space.extern full_space name0
6.599 in
6.600 case find_first check_thms [name1, name2, name0] of
6.601 - SOME name =>
6.602 - let
6.603 - val name =
6.604 - name |> Symtab.defined reserved name ? quote
6.605 - in
6.606 - if multi then name ^ "(" ^ Int.toString j ^ ")"
6.607 - else name
6.608 - end
6.609 + SOME name => repair_name reserved multi j name
6.610 | NONE => ""
6.611 end, is_chained th), (multi, th)) :: rest)) ths
6.612 #> snd
6.613 @@ -604,25 +632,24 @@
6.614 (* The single-name theorems go after the multiple-name ones, so that single
6.615 names are preferred when both are available. *)
6.616 fun name_thm_pairs ctxt respect_no_atp =
6.617 - List.partition (fst o snd) #> op @
6.618 - #> map (apsnd snd)
6.619 + List.partition (fst o snd) #> op @ #> map (apsnd snd)
6.620 #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
6.621
6.622 (***************************************************************)
6.623 (* ATP invocation methods setup *)
6.624 (***************************************************************)
6.625
6.626 -fun relevant_facts full_types relevance_threshold relevance_convergence
6.627 - defs_relevant max_new theory_relevant
6.628 - (relevance_override as {add, del, only})
6.629 +fun relevant_facts full_types (threshold0, threshold1) max_relevant
6.630 + theory_relevant (relevance_override as {add, del, only})
6.631 (ctxt, (chained_ths, _)) hyp_ts concl_t =
6.632 let
6.633 + val decay = 1.0 - Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
6.634 + 1.0 / Real.fromInt (max_relevant + 1))
6.635 val add_thms = maps (ProofContext.get_fact ctxt) add
6.636 val reserved = reserved_isar_keyword_table ()
6.637 val axioms =
6.638 (if only then
6.639 - maps ((fn (n, ths) => map (pair n o pair false) ths)
6.640 - o name_thms_pair_from_ref ctxt reserved chained_ths) add
6.641 + maps (name_thm_pairs_from_ref ctxt reserved chained_ths) add
6.642 else
6.643 all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
6.644 |> name_thm_pairs ctxt (respect_no_atp andalso not only)
6.645 @@ -630,11 +657,14 @@
6.646 in
6.647 trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
6.648 " theorems");
6.649 - relevance_filter ctxt relevance_threshold relevance_convergence
6.650 - defs_relevant max_new theory_relevant relevance_override
6.651 - axioms (concl_t :: hyp_ts)
6.652 - |> map (apfst (fn f => f ()))
6.653 - |> sort_wrt (fst o fst)
6.654 + (if threshold0 > 1.0 orelse threshold0 > threshold1 then
6.655 + []
6.656 + else if threshold0 < 0.0 then
6.657 + axioms
6.658 + else
6.659 + relevance_filter ctxt threshold0 decay max_relevant theory_relevant
6.660 + relevance_override axioms (concl_t :: hyp_ts))
6.661 + |> map (apfst (fn f => f ())) |> sort_wrt (fst o fst)
6.662 end
6.663
6.664 end;
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 18:46:22 2010 +0200
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Thu Aug 26 09:03:18 2010 +0200
7.3 @@ -40,24 +40,20 @@
7.4 "")
7.5 end
7.6
7.7 -fun test_theorems ({debug, verbose, overlord, atps, full_types,
7.8 - relevance_threshold, relevance_convergence,
7.9 - defs_relevant, isar_proof, isar_shrink_factor, ...}
7.10 - : params)
7.11 +fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof,
7.12 + isar_shrink_factor, ...} : params)
7.13 (prover : prover) explicit_apply timeout subgoal state
7.14 - name_thms_pairs =
7.15 + axioms =
7.16 let
7.17 val _ =
7.18 - priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
7.19 + priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
7.20 val params =
7.21 {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
7.22 full_types = full_types, explicit_apply = explicit_apply,
7.23 - relevance_threshold = relevance_threshold,
7.24 - relevance_convergence = relevance_convergence,
7.25 - max_relevant_per_iter = NONE, theory_relevant = NONE,
7.26 - defs_relevant = defs_relevant, isar_proof = isar_proof,
7.27 + relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
7.28 + theory_relevant = NONE, isar_proof = isar_proof,
7.29 isar_shrink_factor = isar_shrink_factor, timeout = timeout}
7.30 - val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
7.31 + val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
7.32 val {context = ctxt, facts, goal} = Proof.goal state
7.33 val problem =
7.34 {subgoal = subgoal, goal = (ctxt, (facts, goal)),
7.35 @@ -67,7 +63,7 @@
7.36 in
7.37 priority (case outcome of
7.38 NONE =>
7.39 - if length used_thm_names = length name_thms_pairs then
7.40 + if length used_thm_names = length axioms then
7.41 "Found proof."
7.42 else
7.43 "Found proof with " ^ n_theorems used_thm_names ^ "."
7.44 @@ -93,10 +89,9 @@
7.45 val fudge_msecs = 1000
7.46
7.47 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
7.48 - | minimize_theorems
7.49 - (params as {debug, atps = atp :: _, full_types, isar_proof,
7.50 - isar_shrink_factor, timeout, ...})
7.51 - i n state name_thms_pairs =
7.52 + | minimize_theorems (params as {debug, atps = atp :: _, full_types,
7.53 + isar_proof, isar_shrink_factor, timeout, ...})
7.54 + i n state axioms =
7.55 let
7.56 val thy = Proof.theory_of state
7.57 val prover = get_prover_fun thy atp
7.58 @@ -106,13 +101,12 @@
7.59 val (_, hyp_ts, concl_t) = strip_subgoal goal i
7.60 val explicit_apply =
7.61 not (forall (Meson.is_fol_term thy)
7.62 - (concl_t :: hyp_ts @
7.63 - maps (map prop_of o snd) name_thms_pairs))
7.64 + (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
7.65 fun do_test timeout =
7.66 test_theorems params prover explicit_apply timeout i state
7.67 val timer = Timer.startRealTimer ()
7.68 in
7.69 - (case do_test timeout name_thms_pairs of
7.70 + (case do_test timeout axioms of
7.71 result as {outcome = NONE, pool, used_thm_names,
7.72 conjecture_shape, ...} =>
7.73 let
7.74 @@ -122,7 +116,7 @@
7.75 |> Time.fromMilliseconds
7.76 val (min_thms, {proof, axiom_names, ...}) =
7.77 sublinear_minimize (do_test new_timeout)
7.78 - (filter_used_facts used_thm_names name_thms_pairs) ([], result)
7.79 + (filter_used_facts used_thm_names axioms) ([], result)
7.80 val n = length min_thms
7.81 val _ = priority (cat_lines
7.82 ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
7.83 @@ -154,15 +148,14 @@
7.84 val ctxt = Proof.context_of state
7.85 val reserved = reserved_isar_keyword_table ()
7.86 val chained_ths = #facts (Proof.goal state)
7.87 - val name_thms_pairs =
7.88 - map (apfst (fn f => f ())
7.89 - o name_thms_pair_from_ref ctxt reserved chained_ths) refs
7.90 + val axioms =
7.91 + maps (map (fn (name, (_, th)) => (name (), [th]))
7.92 + o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
7.93 in
7.94 case subgoal_count state of
7.95 0 => priority "No subgoal!"
7.96 | n =>
7.97 - (kill_atps ();
7.98 - priority (#2 (minimize_theorems params i n state name_thms_pairs)))
7.99 + (kill_atps (); priority (#2 (minimize_theorems params i n state axioms)))
7.100 end
7.101
7.102 end;
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 18:46:22 2010 +0200
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 26 09:03:18 2010 +0200
8.3 @@ -67,11 +67,9 @@
8.4 ("verbose", "false"),
8.5 ("overlord", "false"),
8.6 ("explicit_apply", "false"),
8.7 - ("relevance_threshold", "40"),
8.8 - ("relevance_convergence", "31"),
8.9 - ("max_relevant_per_iter", "smart"),
8.10 + ("relevance_thresholds", "45 95"),
8.11 + ("max_relevant", "smart"),
8.12 ("theory_relevant", "smart"),
8.13 - ("defs_relevant", "false"),
8.14 ("isar_proof", "false"),
8.15 ("isar_shrink_factor", "1")]
8.16
8.17 @@ -84,7 +82,6 @@
8.18 ("partial_types", "full_types"),
8.19 ("implicit_apply", "explicit_apply"),
8.20 ("theory_irrelevant", "theory_relevant"),
8.21 - ("defs_irrelevant", "defs_relevant"),
8.22 ("no_isar_proof", "isar_proof")]
8.23
8.24 val params_for_minimize =
8.25 @@ -158,6 +155,14 @@
8.26 SOME n => n
8.27 | NONE => error ("Parameter " ^ quote name ^
8.28 " must be assigned an integer value.")
8.29 + fun lookup_int_pair name =
8.30 + case lookup name of
8.31 + NONE => (0, 0)
8.32 + | SOME s => case s |> space_explode " " |> map Int.fromString of
8.33 + [SOME n1, SOME n2] => (n1, n2)
8.34 + | _ => error ("Parameter " ^ quote name ^
8.35 + "must be assigned a pair of integer values \
8.36 + \(e.g., \"60 95\")")
8.37 fun lookup_int_option name =
8.38 case lookup name of
8.39 SOME "smart" => NONE
8.40 @@ -168,25 +173,20 @@
8.41 val atps = lookup_string "atps" |> space_explode " "
8.42 val full_types = lookup_bool "full_types"
8.43 val explicit_apply = lookup_bool "explicit_apply"
8.44 - val relevance_threshold =
8.45 - 0.01 * Real.fromInt (lookup_int "relevance_threshold")
8.46 - val relevance_convergence =
8.47 - 0.01 * Real.fromInt (lookup_int "relevance_convergence")
8.48 - val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
8.49 + val relevance_thresholds =
8.50 + lookup_int_pair "relevance_thresholds"
8.51 + |> pairself (fn n => 0.01 * Real.fromInt n)
8.52 + val max_relevant = lookup_int_option "max_relevant"
8.53 val theory_relevant = lookup_bool_option "theory_relevant"
8.54 - val defs_relevant = lookup_bool "defs_relevant"
8.55 val isar_proof = lookup_bool "isar_proof"
8.56 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
8.57 val timeout = lookup_time "timeout"
8.58 in
8.59 {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
8.60 full_types = full_types, explicit_apply = explicit_apply,
8.61 - relevance_threshold = relevance_threshold,
8.62 - relevance_convergence = relevance_convergence,
8.63 - max_relevant_per_iter = max_relevant_per_iter,
8.64 - theory_relevant = theory_relevant, defs_relevant = defs_relevant,
8.65 - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
8.66 - timeout = timeout}
8.67 + relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
8.68 + theory_relevant = theory_relevant, isar_proof = isar_proof,
8.69 + isar_shrink_factor = isar_shrink_factor, timeout = timeout}
8.70 end
8.71
8.72 fun get_params thy = extract_params (default_raw_params thy)
9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Aug 25 18:46:22 2010 +0200
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 09:03:18 2010 +0200
9.3 @@ -234,7 +234,7 @@
9.4 fst o Scan.finite Symbol.stopper
9.5 (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
9.6 (parse_lines pool)))
9.7 - o explode o strip_spaces
9.8 + o explode o strip_spaces_except_between_ident_chars
9.9
9.10 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
9.11
9.12 @@ -246,18 +246,18 @@
9.13 constrained by information from type literals, or by type inference. *)
9.14 fun type_from_fo_term tfrees (u as ATerm (a, us)) =
9.15 let val Ts = map (type_from_fo_term tfrees) us in
9.16 - case strip_prefix_and_undo_ascii type_const_prefix a of
9.17 + case strip_prefix_and_unascii type_const_prefix a of
9.18 SOME b => Type (invert_const b, Ts)
9.19 | NONE =>
9.20 if not (null us) then
9.21 raise FO_TERM [u] (* only "tconst"s have type arguments *)
9.22 - else case strip_prefix_and_undo_ascii tfree_prefix a of
9.23 + else case strip_prefix_and_unascii tfree_prefix a of
9.24 SOME b =>
9.25 let val s = "'" ^ b in
9.26 TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
9.27 end
9.28 | NONE =>
9.29 - case strip_prefix_and_undo_ascii tvar_prefix a of
9.30 + case strip_prefix_and_unascii tvar_prefix a of
9.31 SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
9.32 | NONE =>
9.33 (* Variable from the ATP, say "X1" *)
9.34 @@ -267,7 +267,7 @@
9.35 (* Type class literal applied to a type. Returns triple of polarity, class,
9.36 type. *)
9.37 fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
9.38 - case (strip_prefix_and_undo_ascii class_prefix a,
9.39 + case (strip_prefix_and_unascii class_prefix a,
9.40 map (type_from_fo_term tfrees) us) of
9.41 (SOME b, [T]) => (pos, b, T)
9.42 | _ => raise FO_TERM [u]
9.43 @@ -309,7 +309,7 @@
9.44 [typ_u, term_u] =>
9.45 aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
9.46 | _ => raise FO_TERM us
9.47 - else case strip_prefix_and_undo_ascii const_prefix a of
9.48 + else case strip_prefix_and_unascii const_prefix a of
9.49 SOME "equal" =>
9.50 list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
9.51 map (aux NONE []) us)
9.52 @@ -341,10 +341,10 @@
9.53 val ts = map (aux NONE []) (us @ extra_us)
9.54 val T = map fastype_of ts ---> HOLogic.typeT
9.55 val t =
9.56 - case strip_prefix_and_undo_ascii fixed_var_prefix a of
9.57 + case strip_prefix_and_unascii fixed_var_prefix a of
9.58 SOME b => Free (b, T)
9.59 | NONE =>
9.60 - case strip_prefix_and_undo_ascii schematic_var_prefix a of
9.61 + case strip_prefix_and_unascii schematic_var_prefix a of
9.62 SOME b => Var ((b, 0), T)
9.63 | NONE =>
9.64 if is_tptp_variable a then
9.65 @@ -575,7 +575,7 @@
9.66 String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
9.67 fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
9.68 if tag = "cnf" orelse tag = "fof" then
9.69 - (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
9.70 + (case strip_prefix_and_unascii axiom_prefix (List.last rest) of
9.71 SOME name =>
9.72 if member (op =) rest "file" then
9.73 SOME (name, is_true_for axiom_names name)
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 25 18:46:22 2010 +0200
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 09:03:18 2010 +0200
10.3 @@ -407,7 +407,7 @@
10.4 16383 (* large number *)
10.5 else if full_types then
10.6 0
10.7 - else case strip_prefix_and_undo_ascii const_prefix s of
10.8 + else case strip_prefix_and_unascii const_prefix s of
10.9 SOME s' => num_type_args thy (invert_const s')
10.10 | NONE => 0)
10.11 | min_arity_of _ _ (SOME the_const_tab) s =
11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Aug 25 18:46:22 2010 +0200
11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 26 09:03:18 2010 +0200
11.3 @@ -9,7 +9,8 @@
11.4 val is_true_for : (string * bool) vector -> string -> bool
11.5 val plural_s : int -> string
11.6 val serial_commas : string -> string list -> string list
11.7 - val strip_spaces : string -> string
11.8 + val simplify_spaces : string -> string
11.9 + val strip_spaces_except_between_ident_chars : string -> string
11.10 val parse_bool_option : bool -> string -> string -> bool option
11.11 val parse_time_option : string -> string -> Time.time option
11.12 val scan_integer : string list -> int * string list
11.13 @@ -39,24 +40,27 @@
11.14 | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
11.15 | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
11.16
11.17 -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
11.18 -
11.19 -fun strip_spaces_in_list [] = ""
11.20 - | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
11.21 - | strip_spaces_in_list [c1, c2] =
11.22 - strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
11.23 - | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
11.24 +fun strip_spaces_in_list _ [] = ""
11.25 + | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then "" else str c1
11.26 + | strip_spaces_in_list is_evil [c1, c2] =
11.27 + strip_spaces_in_list is_evil [c1] ^ strip_spaces_in_list is_evil [c2]
11.28 + | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
11.29 if Char.isSpace c1 then
11.30 - strip_spaces_in_list (c2 :: c3 :: cs)
11.31 + strip_spaces_in_list is_evil (c2 :: c3 :: cs)
11.32 else if Char.isSpace c2 then
11.33 if Char.isSpace c3 then
11.34 - strip_spaces_in_list (c1 :: c3 :: cs)
11.35 + strip_spaces_in_list is_evil (c1 :: c3 :: cs)
11.36 else
11.37 - str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
11.38 - strip_spaces_in_list (c3 :: cs)
11.39 + str c1 ^ (if forall is_evil [c1, c3] then " " else "") ^
11.40 + strip_spaces_in_list is_evil (c3 :: cs)
11.41 else
11.42 - str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
11.43 -val strip_spaces = strip_spaces_in_list o String.explode
11.44 + str c1 ^ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
11.45 +fun strip_spaces is_evil = strip_spaces_in_list is_evil o String.explode
11.46 +
11.47 +val simplify_spaces = strip_spaces (K true)
11.48 +
11.49 +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
11.50 +val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
11.51
11.52 fun parse_bool_option option name s =
11.53 (case s of