--- a/.hgtags Thu Feb 21 10:52:14 2013 +0100
+++ b/.hgtags Thu Feb 21 16:00:48 2013 +0100
@@ -5,7 +5,6 @@
23ceb1dc9755a8ad6f0230697d0cc52f54102bf4 Isabelle94-5
2cf13a72e1704d0094d21e7dc68e7271a282ed31 Isabelle2008
33b9b5da3e6faee6ca6969d17e79634d49e5b46a Isabelle94-1
-35fba71ec6ef550178e5f5e44d95d96c6f36eae6 nominal_01
3e47692e3a3e4c695f6345b3534ed0c36817fd40 Isabelle99-2
50be659d4222b68f95e9c966097e59091f26acf3 Isabelle99-1
67692db44c7099ad8789f088003213aeb095e914 Isabelle94-2
@@ -16,11 +15,8 @@
831a9a7ab9f352c65b0f449630b428304c89362b Isabelle93
836950047d8508e3c200edc1e07a46c2c5e09cd7 Isabelle94-6
8d42a7bccf0b0880dff8e46c71c4811be8b2e7ec Isabelle94-7
-a23af144eb47f12354dff090813c796f278e2eb8 nominal_03
be6b5edbca9ffeb3bace5f4bac5c6478bf8cbdb2 Isabelle98
-cd41a57221d07441647284e239b8d8d77d498ef5 isa94
ce180e5b7fa056003791fff19cc5cefba193b135 Isabelle2002
-dde117622dace696123b023d1f06cf8d8ef9eb46 nominal_02
f9eb0f819642b2ad77119dbf8935bf13248f205d Isabelle94
fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009
--- a/src/Doc/Sledgehammer/document/root.tex Thu Feb 21 10:52:14 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Feb 21 16:00:48 2013 +0100
@@ -223,7 +223,7 @@
for Alt-Ergo, set the
environment variable \texttt{WHY3\_HOME} to the directory that contains the
\texttt{why3} executable.
-Sledgehammer has been tested with Alt-Ergo 0.93 and 0.94, CVC3 2.2 and 2.4.1,
+Sledgehammer has been tested with Alt-Ergo 0.95, CVC3 2.2 and 2.4.1,
Yices 1.0.28 and 1.0.33, and Z3 3.0 to 4.0. Since the SMT solvers' output
formats are somewhat unstable, other versions of the solvers might not work well
with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION},
@@ -308,7 +308,7 @@
\textit{smt} method call. Rough timings are shown in parentheses, indicating how
fast the call is. You can click the proof to insert it into the theory text.
-In addition, you can ask Sledgehammer for an Isar text proof by passing the
+In addition, you can ask Sledgehammer for an Isar text proof by enabling the
\textit{isar\_proofs} option (\S\ref{output-format}):
\prew
@@ -367,7 +367,7 @@
if that helps.
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
-that Isar proofs should be generated, instead of one-liner \textit{metis} or
+that Isar proofs should be generated, in addition to one-liner \textit{metis} or
\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
\textit{isar\_compress} (\S\ref{output-format}).
@@ -501,15 +501,15 @@
using \textit{type\_enc} (\S\ref{problem-encoding}), this is a bug, and you are
strongly encouraged to report this to the author at \authoremail.
-\point{Why are the generated Isar proofs so ugly/broken?}
-
-The current implementation of the Isar proof feature,
-enabled by the \textit{isar\_proofs} option (\S\ref{output-format}),
-is highly experimental. Work on a new implementation has begun. There is a large body of
-research into transforming resolution proofs into natural deduction proofs (such
-as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
-set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger
-value or to try several provers and keep the nicest-looking proof.
+%\point{Why are the generated Isar proofs so ugly/broken?}
+%
+%The current implementation of the Isar proof feature,
+%enabled by the \textit{isar\_proofs} option (\S\ref{output-format}),
+%is experimental. Work on a new implementation has begun. There is a large body of
+%research into transforming resolution proofs into natural deduction proofs (such
+%as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
+%set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger
+%value or to try several provers and keep the nicest-looking proof.
\point{How can I tell whether a suggested proof is sound?}
@@ -843,7 +843,7 @@
It supports the TPTP polymorphic typed first-order format (TFF1) via Why3
\cite{why3}. It is included for experimental purposes. To use Alt-Ergo, set the
environment variable \texttt{WHY3\_HOME} to the directory that contains the
-\texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.93 and an
+\texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.95 and an
unidentified development version of Why3.
\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
@@ -1296,16 +1296,22 @@
\nopagebreak
{\small See also \textit{overlord} (\S\ref{mode-of-operation}).}
-\opfalse{isar\_proofs}{no\_isar\_proofs}
+\opsmart{isar\_proofs}{no\_isar\_proofs}
Specifies whether Isar proofs should be output in addition to one-liner
-\textit{metis} proofs. Isar proof construction is still experimental and often
-fails; however, they are usually faster and sometimes more robust than
-\textit{metis} proofs.
+\textit{metis} proofs. The construction of Isar proof is still experimental and
+may sometimes fail; however, when they succeed they are usually faster and more
+intelligible than \textit{metis} proofs. If the option is set to \textit{smart}
+(the default), Isar proofs are only generated when no working one-liner
+\textit{metis} proof is available.
\opdefault{isar\_compress}{int}{\upshape 10}
Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
-is enabled. A value of $n$ indicates that each Isar proof step should correspond
-to a group of up to $n$ consecutive proof steps in the ATP proof.
+is explicitly enabled. A value of $n$ indicates that each Isar proof step should
+correspond to a group of up to $n$ consecutive proof steps in the ATP proof.
+
+\optrueonly{dont\_compress\_isar}
+Alias for ``\textit{isar\_compress} = 0''.
+
\end{enum}
\subsection{Authentication}
--- a/src/HOL/Int.thy Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Int.thy Thu Feb 21 16:00:48 2013 +0100
@@ -1656,7 +1656,7 @@
int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer
plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer
int_transfer less_eq_int.transfer less_int.transfer of_int.transfer
- nat.transfer
+ nat.transfer int.right_unique int.right_total int.bi_total
declare Quotient_int [quot_del]
--- a/src/HOL/Library/Cardinality.thy Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Library/Cardinality.thy Thu Feb 21 16:00:48 2013 +0100
@@ -234,8 +234,6 @@
dest!: finite_imageD intro: inj_onI)
end
-declare [[show_consts]]
-
instantiation integer :: card_UNIV begin
definition "finite_UNIV = Phantom(integer) False"
definition "card_UNIV = Phantom(integer) 0"
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Feb 21 16:00:48 2013 +0100
@@ -50,7 +50,7 @@
(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*)
(*defaults used in this Mirabelle action*)
-val preplay_timeout_default = "4"
+val preplay_timeout_default = "3"
val lam_trans_default = "smart"
val uncurried_aliases_default = "smart"
val fact_filter_default = "smart"
@@ -377,18 +377,22 @@
fun learn prover =
Sledgehammer_MaSh.mash_learn_proof ctxt params prover (prop_of goal) all_facts
in
- Sledgehammer_Minimize.get_minimizing_isar_prover ctxt Sledgehammer_Provers.Normal
+ Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Provers.Normal
learn name
end
type stature = ATP_Problem_Generate.stature
-(* hack *)
+(* Fragile hack *)
fun reconstructor_from_msg args msg =
(case AList.lookup (op =) args reconstructorK of
SOME name => name
| NONE =>
- if String.isSubstring "metis (" msg then
+ if (String.isSubstring " ms)" msg orelse String.isSubstring " s)" msg)
+ andalso not (String.isSubstring "(> " msg)
+ andalso not (String.isSubstring ", > " msg) then
+ "none" (* trust the preplayed proof *)
+ else if String.isSubstring "metis (" msg then
msg |> Substring.full
|> Substring.position "metis ("
|> snd |> Substring.position ")"
@@ -605,7 +609,7 @@
true 1 (Sledgehammer_Util.subgoal_count st)
val _ = log separator
val (used_facts, (preplay, message, message_tail)) =
- minimize st (these (!named_thms))
+ minimize st NONE (these (!named_thms))
val msg = message (Lazy.force preplay) ^ message_tail
in
case used_facts of
--- a/src/HOL/Rat.thy Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Rat.thy Thu Feb 21 16:00:48 2013 +0100
@@ -1129,7 +1129,7 @@
rat.All_transfer rat.Ex_transfer rat.rel_eq_transfer forall_rat_transfer
Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer
uminus_rat.transfer times_rat.transfer inverse_rat.transfer
- positive.transfer of_rat.transfer
+ positive.transfer of_rat.transfer rat.right_unique rat.right_total
text {* De-register @{text "rat"} as a quotient type: *}
--- a/src/HOL/RealDef.thy Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/RealDef.thy Thu Feb 21 16:00:48 2013 +0100
@@ -933,7 +933,8 @@
lemmas [transfer_rule del] =
real.All_transfer real.Ex_transfer real.rel_eq_transfer forall_real_transfer
zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
- times_real.transfer inverse_real.transfer positive.transfer
+ times_real.transfer inverse_real.transfer positive.transfer real.right_unique
+ real.right_total
subsection{*More Lemmas*}
--- a/src/HOL/TPTP/MaSh_Eval.thy Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy Thu Feb 21 16:00:48 2013 +0100
@@ -28,6 +28,7 @@
val do_it = false (* switch to "true" to generate the files *)
val params = Sledgehammer_Isar.default_params @{context} []
val range = (1, NONE)
+val linearize = false
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
val prob_dir = prefix ^ "mash_problems"
@@ -42,7 +43,7 @@
ML {*
if do_it then
- evaluate_mash_suggestions @{context} params range
+ evaluate_mash_suggestions @{context} params range linearize
[MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
(SOME prob_dir)
(prefix ^ "mepo_suggestions")
--- a/src/HOL/TPTP/MaSh_Export.thy Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Thu Feb 21 16:00:48 2013 +0100
@@ -33,6 +33,7 @@
val prover = hd provers
val range = (1, NONE)
val step = 1
+val linearize = false
val max_suggestions = 1024
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
@@ -47,21 +48,22 @@
ML {*
if do_it then
- generate_accessibility @{context} thys false (prefix ^ "mash_accessibility")
+ generate_accessibility @{context} thys linearize
+ (prefix ^ "mash_accessibility")
else
()
*}
ML {*
if do_it then
- generate_features @{context} prover thys false (prefix ^ "mash_features")
+ generate_features @{context} prover thys (prefix ^ "mash_features")
else
()
*}
ML {*
if do_it then
- generate_isar_dependencies @{context} thys false
+ generate_isar_dependencies @{context} thys linearize
(prefix ^ "mash_dependencies")
else
()
@@ -70,7 +72,7 @@
ML {*
if do_it then
generate_isar_commands @{context} prover (range, step) thys
- (prefix ^ "mash_commands")
+ linearize (prefix ^ "mash_commands")
else
()
*}
@@ -78,7 +80,7 @@
ML {*
if do_it then
generate_mepo_suggestions @{context} params (range, step) thys
- max_suggestions (prefix ^ "mepo_suggestions")
+ linearize max_suggestions (prefix ^ "mepo_suggestions")
else
()
*}
@@ -93,7 +95,7 @@
ML {*
if do_it then
- generate_prover_dependencies @{context} params range thys false
+ generate_prover_dependencies @{context} params range thys linearize
(prefix ^ "mash_prover_dependencies")
else
()
@@ -102,7 +104,7 @@
ML {*
if do_it then
generate_prover_commands @{context} params (range, step) thys
- (prefix ^ "mash_prover_commands")
+ linearize (prefix ^ "mash_prover_commands")
else
()
*}
--- a/src/HOL/TPTP/mash_eval.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Thu Feb 21 16:00:48 2013 +0100
@@ -16,8 +16,9 @@
val MeSh_ProverN : string
val IsarN : string
val evaluate_mash_suggestions :
- Proof.context -> params -> int * int option -> string list -> string option
- -> string -> string -> string -> string -> string -> string -> unit
+ Proof.context -> params -> int * int option -> bool -> string list
+ -> string option -> string -> string -> string -> string -> string -> string
+ -> unit
end;
structure MaSh_Eval : MASH_EVAL =
@@ -39,7 +40,7 @@
fun in_range (from, to) j =
j >= from andalso (to = NONE orelse j <= the to)
-fun evaluate_mash_suggestions ctxt params range methods prob_dir_name
+fun evaluate_mash_suggestions ctxt params range linearize methods prob_dir_name
mepo_file_name mash_isar_file_name mash_prover_file_name
mesh_isar_file_name mesh_prover_file_name report_file_name =
let
@@ -111,7 +112,10 @@
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val isar_deps = isar_dependencies_of name_tabs th
val facts =
- facts |> filter (fn (_, th') => crude_thm_ord (th', th) = LESS)
+ facts
+ |> filter (fn (_, th') =>
+ if linearize then crude_thm_ord (th', th) = LESS
+ else thm_less (th', th))
val find_suggs =
find_suggested_facts ctxt facts #> map fact_of_raw_fact
fun get_facts [] compute = compute facts
--- a/src/HOL/TPTP/mash_export.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML Thu Feb 21 16:00:48 2013 +0100
@@ -12,21 +12,21 @@
val generate_accessibility :
Proof.context -> theory list -> bool -> string -> unit
val generate_features :
- Proof.context -> string -> theory list -> bool -> string -> unit
+ Proof.context -> string -> theory list -> string -> unit
val generate_isar_dependencies :
Proof.context -> theory list -> bool -> string -> unit
val generate_prover_dependencies :
Proof.context -> params -> int * int option -> theory list -> bool -> string
-> unit
val generate_isar_commands :
- Proof.context -> string -> (int * int option) * int -> theory list -> string
- -> unit
+ Proof.context -> string -> (int * int option) * int -> theory list -> bool
+ -> string -> unit
val generate_prover_commands :
- Proof.context -> params -> (int * int option) * int -> theory list -> string
- -> unit
+ Proof.context -> params -> (int * int option) * int -> theory list -> bool
+ -> string -> unit
val generate_mepo_suggestions :
- Proof.context -> params -> (int * int option) * int -> theory list -> int
- -> string -> unit
+ Proof.context -> params -> (int * int option) * int -> theory list -> bool
+ -> int -> string -> unit
val generate_mesh_suggestions : int -> string -> string -> string -> unit
end;
@@ -51,28 +51,30 @@
|> sort (crude_thm_ord o pairself snd)
end
-fun generate_accessibility ctxt thys include_thys file_name =
+fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th))
+
+fun generate_accessibility ctxt thys linearize file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
- fun do_fact fact prevs =
+ fun do_fact (parents, fact) prevs =
let
- val s = encode_str fact ^ ": " ^ encode_strs prevs ^ "\n"
+ val parents = if linearize then prevs else parents
+ val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n"
val _ = File.append path s
in [fact] end
val facts =
all_facts ctxt
- |> not include_thys ? filter_out (has_thys thys o snd)
- |> map (snd #> nickname_of_thm)
+ |> filter_out (has_thys thys o snd)
+ |> attach_parents_to_facts []
+ |> map (apsnd (nickname_of_thm o snd))
in fold do_fact facts []; () end
-fun generate_features ctxt prover thys include_thys file_name =
+fun generate_features ctxt prover thys file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
- val facts =
- all_facts ctxt
- |> not include_thys ? filter_out (has_thys thys o snd)
+ val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
fun do_fact ((_, stature), th) =
let
val name = nickname_of_thm th
@@ -109,20 +111,22 @@
| NONE => (omitted_marker, [])
end
-fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
+fun generate_isar_or_prover_dependencies ctxt params_opt range thys linearize
file_name =
let
val path = file_name |> Path.explode
- val facts =
- all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
+ val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
val name_tabs = build_name_tables nickname_of_thm facts
fun do_fact (j, (_, th)) =
if in_range range j then
let
val name = nickname_of_thm th
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
+ val access_facts =
+ if linearize then take (j - 1) facts
+ else facts |> filter_accessible_from th
val (marker, deps) =
- smart_dependencies_of ctxt params_opt facts name_tabs th NONE
+ smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE
in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end
else
""
@@ -142,25 +146,29 @@
is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
- file_name =
+ linearize file_name =
let
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val path = file_name |> Path.explode
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
val name_tabs = build_name_tables nickname_of_thm facts
- fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
+ fun do_fact (j, ((name, (parents, ((_, stature), th))), prevs)) =
if in_range range j then
let
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val feats =
features_of ctxt prover (theory_of_thm th) stature [prop_of th]
val isar_deps = isar_dependencies_of name_tabs th
+ val access_facts =
+ (if linearize then take (j - 1) new_facts
+ else new_facts |> filter_accessible_from th) @ old_facts
val (marker, deps) =
- smart_dependencies_of ctxt params_opt facts name_tabs th
+ smart_dependencies_of ctxt params_opt access_facts name_tabs th
(SOME isar_deps)
+ val parents = if linearize then prevs else parents
val core =
- encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^
+ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
encode_features (sort_wrt fst feats)
val query =
if is_bad_query ctxt ho_atp step j th isar_deps then ""
@@ -170,10 +178,12 @@
in query ^ update end
else
""
- val parents =
+ val new_facts =
+ new_facts |> attach_parents_to_facts old_facts
+ |> map (`(nickname_of_thm o snd o snd))
+ val hd_prevs =
map (nickname_of_thm o snd) (the_list (try List.last old_facts))
- val new_facts = new_facts |> map (`(nickname_of_thm o snd))
- val prevss = fst (split_last (parents :: map (single o fst) new_facts))
+ val prevss = fst (split_last (hd_prevs :: map (single o fst) new_facts))
val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss))
in File.write_list path lines end
@@ -184,7 +194,7 @@
generate_isar_or_prover_commands ctxt prover (SOME params)
fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...})
- (range, step) thys max_suggs file_name =
+ (range, step) thys linearize max_suggs file_name =
let
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val path = file_name |> Path.explode
@@ -206,6 +216,7 @@
let
val suggs =
old_facts
+ |> linearize ? filter_accessible_from th
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
max_suggs NONE hyp_ts concl_t
|> map (nickname_of_thm o snd)
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Feb 21 16:00:48 2013 +0100
@@ -36,10 +36,7 @@
UnknownError of string
type step_name = string * string list
-
- datatype 'a step =
- Definition_Step of step_name * 'a * 'a |
- Inference_Step of step_name * formula_role * 'a * string * step_name list
+ type 'a step = step_name * formula_role * 'a * string * step_name list
type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
@@ -210,15 +207,10 @@
| (SOME i, SOME j) => int_ord (i, j)
end
-datatype 'a step =
- Definition_Step of step_name * 'a * 'a |
- Inference_Step of step_name * formula_role * 'a * string * step_name list
+type 'a step = step_name * formula_role * 'a * string * step_name list
type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
-fun step_name (Definition_Step (name, _, _)) = name
- | step_name (Inference_Step (name, _, _, _, _)) = name
-
(**** PARSING OF TSTP FORMAT ****)
(* Strings enclosed in single quotes (e.g., file names) *)
@@ -421,18 +413,14 @@
phi), "", [])
| Inference_Source (rule, deps) => (((num, []), phi), rule, deps)
fun mk_step () =
- Inference_Step (name, role_of_tptp_string role, phi, rule,
- map (rpair []) deps)
+ (name, role_of_tptp_string role, phi, rule, map (rpair []) deps)
in
case role_of_tptp_string role of
Definition =>
(case phi of
- AConn (AIff, [phi1 as AAtom _, phi2]) =>
- Definition_Step (name, phi1, phi2)
- | AAtom (ATerm (("equal", []), _)) =>
+ AAtom (ATerm (("equal", []), _)) =>
(* Vampire's equality proxy axiom *)
- Inference_Step (name, Definition, phi, rule,
- map (rpair []) deps)
+ (name, Definition, phi, rule, map (rpair []) deps)
| _ => mk_step ())
| _ => mk_step ()
end)
@@ -472,14 +460,14 @@
(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
derived from formulae <ident>* *)
fun parse_spass_line x =
- (parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
- -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]"
+ (parse_spass_debug |-- scan_general_id --| $$ "[" --|
+ Scan.many1 Symbol.is_digit --| $$ ":" -- Symbol.scan_ascii_id
+ -- parse_spass_annotations --| $$ "]"
-- parse_horn_clause --| $$ "."
-- Scan.option (Scan.this_string "derived from formulae "
|-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
>> (fn ((((num, rule), deps), u), names) =>
- Inference_Step ((num, these names), Unknown, u, rule,
- map (rpair []) deps))) x
+ ((num, these names), Unknown, u, rule, map (rpair []) deps))) x
val satallax_coreN = "__satallax_core" (* arbitrary *)
val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *)
@@ -488,14 +476,12 @@
fun parse_z3_tptp_line x =
(scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
>> (fn (name, names) =>
- Inference_Step (("", name :: names), Unknown, dummy_phi,
- z3_tptp_coreN, []))) x
+ (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x
(* Syntax: <name> *)
fun parse_satallax_line x =
(scan_general_id --| Scan.option ($$ " ")
- >> (fn s => Inference_Step ((s, [s]), Unknown, dummy_phi, satallax_coreN,
- []))) x
+ >> (fn s => ((s, [s]), Unknown, dummy_phi, satallax_coreN, []))) x
fun parse_line problem =
parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
@@ -512,16 +498,12 @@
| atp_proof_from_tstplike_proof problem tstp =
tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof problem
- |> sort (step_name_ord o pairself step_name)
+ |> sort (step_name_ord o pairself #1)
fun clean_up_dependencies _ [] = []
- | clean_up_dependencies seen
- ((step as Definition_Step (name, _, _)) :: steps) =
- step :: clean_up_dependencies (name :: seen) steps
- | clean_up_dependencies seen
- (Inference_Step (name, role, u, rule, deps) :: steps) =
- Inference_Step (name, role, u, rule,
- map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
+ | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
+ (name, role, u, rule,
+ map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
clean_up_dependencies (name :: seen) steps
fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
@@ -533,10 +515,8 @@
AQuant (q, map (apfst f) xs, do_formula phi)
| do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
| do_formula (AAtom t) = AAtom (do_term t)
- fun do_step (Definition_Step (name, phi1, phi2)) =
- Definition_Step (name, do_formula phi1, do_formula phi2)
- | do_step (Inference_Step (name, role, phi, rule, deps)) =
- Inference_Step (name, role, do_formula phi, rule, deps)
+ fun do_step (name, role, phi, rule, deps) =
+ (name, role, do_formula phi, rule, deps)
in map do_step end
fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Feb 21 16:00:48 2013 +0100
@@ -158,6 +158,10 @@
fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
+(* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)
+fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
+ | loose_aconv (t, t') = t aconv t'
+
val vampire_skolem_prefix = "sK"
(* First-order translation. No types are known for variables. "HOLogic.typeT"
@@ -178,8 +182,7 @@
else if s = tptp_equal then
let val ts = map (do_term [] NONE) us in
if textual andalso length ts = 2 andalso
- hd ts aconv List.last ts then
- (* Vampire is keen on producing these. *)
+ loose_aconv (hd ts, List.last ts) then
@{const True}
else
list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Thu Feb 21 16:00:48 2013 +0100
@@ -32,7 +32,7 @@
type direct_proof = direct_inference list
- val make_refute_graph : (atom list * atom) list -> refute_graph
+ val make_refute_graph : atom -> (atom list * atom) list -> refute_graph
val axioms_of_refute_graph : refute_graph -> atom list -> atom list
val tainted_atoms_of_refute_graph : refute_graph -> atom list -> atom list
val sequents_of_refute_graph : refute_graph -> ref_sequent list
@@ -67,19 +67,22 @@
type direct_proof = direct_inference list
-fun atom_eq p = (Atom.ord p = EQUAL)
-fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d))
-fun direct_sequent_eq ((gamma, c), (delta, d)) =
- clause_eq (gamma, delta) andalso clause_eq (c, d)
+val atom_eq = is_equal o Atom.ord
+val clause_ord = dict_ord Atom.ord
+val clause_eq = is_equal o clause_ord
+val direct_sequent_ord = prod_ord clause_ord clause_ord
+val direct_sequent_eq = is_equal o direct_sequent_ord
-fun make_refute_graph infers =
+fun make_refute_graph bot infers =
let
fun add_edge to from =
Atom_Graph.default_node (from, ())
#> Atom_Graph.default_node (to, ())
#> Atom_Graph.add_edge_acyclic (from, to)
fun add_infer (froms, to) = fold (add_edge to) froms
- in Atom_Graph.empty |> fold add_infer infers end
+ val graph = fold add_infer infers Atom_Graph.empty
+ val reachable = Atom_Graph.all_preds graph [bot]
+ in graph |> Atom_Graph.restrict (member (is_equal o Atom.ord) reachable) end
fun axioms_of_refute_graph refute_graph conjs =
subtract atom_eq conjs (Atom_Graph.minimals refute_graph)
@@ -165,7 +168,10 @@
val provable =
filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
- val seq as (gamma, c) = hd (horn_provable @ provable)
+ val seq as (gamma, c) =
+ case horn_provable @ provable of
+ [] => raise Fail "ill-formed refutation graph"
+ | next :: _ => next
in
Have (map single gamma, c) ::
redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 21 16:00:48 2013 +0100
@@ -207,7 +207,7 @@
val alt_ergo_config : atp_config =
{exec = (["WHY3_HOME"], ["why3"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- "--format tff1 --prover alt-ergo --timelimit " ^
+ "--format tptp --prover 'Alt-Ergo,0.95,' --timelimit " ^
string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
proof_delims = [],
known_failures =
@@ -339,9 +339,9 @@
[(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
(0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)),
(0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)),
- (0.15, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN)),
(0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)),
- (0.25, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN))]
+ (0.15, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN)),
+ (0.25, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN))]
else
[(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))]
end,
@@ -543,7 +543,10 @@
"--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
" --proof tptp --output_axiom_names on" ^
(if is_vampire_at_least_1_8 () then
- " --forced_options propositional_to_bdd=off"
+ (* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
+ " --forced_options propositional_to_bdd=off:splitting=off:\
+ \equality_proxy=off:general_splitting=off:inequality_splitting=0:\
+ \naming=0"
else
"") ^
" --thanks \"Andrei and Krystof\" --input_file " ^ file_name
--- a/src/HOL/Tools/ATP/atp_util.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Thu Feb 21 16:00:48 2013 +0100
@@ -287,15 +287,23 @@
| s_not t = @{const Not} $ t
fun s_conj (@{const True}, t2) = t2
| s_conj (t1, @{const True}) = t1
- | s_conj p = HOLogic.mk_conj p
+ | s_conj (@{const False}, _) = @{const False}
+ | s_conj (_, @{const False}) = @{const False}
+ | s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2)
fun s_disj (@{const False}, t2) = t2
| s_disj (t1, @{const False}) = t1
- | s_disj p = HOLogic.mk_disj p
+ | s_disj (@{const True}, _) = @{const True}
+ | s_disj (_, @{const True}) = @{const True}
+ | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2)
fun s_imp (@{const True}, t2) = t2
| s_imp (t1, @{const False}) = s_not t1
+ | s_imp (@{const False}, _) = @{const True}
+ | s_imp (_, @{const True}) = @{const True}
| s_imp p = HOLogic.mk_imp p
fun s_iff (@{const True}, t2) = t2
| s_iff (t1, @{const True}) = t1
+ | s_iff (@{const False}, t2) = s_not t2
+ | s_iff (t1, @{const False}) = s_not t1
| s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
(* cf. "close_form" in "refute.ML" *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 21 16:00:48 2013 +0100
@@ -94,7 +94,7 @@
("fact_thresholds", "0.45 0.85"),
("max_mono_iters", "smart"),
("max_new_mono_instances", "smart"),
- ("isar_proofs", "false"),
+ ("isar_proofs", "smart"),
("isar_compress", "10"),
("slice", "true"),
("minimize", "smart"),
@@ -102,7 +102,8 @@
val alias_params =
[("prover", ("provers", [])), (* undocumented *)
- ("dont_preplay", ("preplay_timeout", ["0"]))]
+ ("dont_preplay", ("preplay_timeout", ["0"])),
+ ("dont_compress_isar", ("isar_compress", ["0"]))]
val negated_alias_params =
[("no_debug", "debug"),
("quiet", "verbose"),
@@ -188,20 +189,6 @@
fun merge data : T = AList.merge (op =) (K true) data
)
-fun remotify_prover_if_supported_and_not_already_remote ctxt name =
- if String.isPrefix remote_prefix name then
- SOME name
- else
- let val remote_name = remote_prefix ^ name in
- if is_prover_supported ctxt remote_name then SOME remote_name else NONE
- end
-
-fun remotify_prover_if_not_installed ctxt name =
- if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
- SOME name
- else
- remotify_prover_if_supported_and_not_already_remote ctxt name
-
fun avoid_too_many_threads _ _ [] = []
| avoid_too_many_threads _ (0, 0) _ = []
| avoid_too_many_threads ctxt (0, max_remote) provers =
@@ -312,7 +299,7 @@
val max_mono_iters = lookup_option lookup_int "max_mono_iters"
val max_new_mono_instances =
lookup_option lookup_int "max_new_mono_instances"
- val isar_proofs = lookup_bool "isar_proofs"
+ val isar_proofs = lookup_option lookup_bool "isar_proofs"
val isar_compress = Real.max (1.0, lookup_real "isar_compress")
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Feb 21 16:00:48 2013 +0100
@@ -56,6 +56,7 @@
('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
-> 'a list
val crude_thm_ord : thm * thm -> order
+ val thm_less : thm * thm -> bool
val goal_of_thm : theory -> thm -> thm
val run_prover_for_mash :
Proof.context -> params -> string -> fact list -> thm -> prover_result
@@ -80,6 +81,8 @@
val mash_learn_proof :
Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
-> unit
+ val attach_parents_to_facts :
+ ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list
val mash_learn :
Proof.context -> params -> fact_override -> thm list -> bool -> unit
val is_mash_enabled : unit -> bool
@@ -555,8 +558,8 @@
{state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
factss = [("", facts)]}
in
- get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
- problem
+ get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
+ problem
end
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
@@ -902,6 +905,8 @@
(true, "")
end)
+(* In the following functions, chunks are risers w.r.t. "thm_less_eq". *)
+
fun chunks_and_parents_for chunks th =
let
fun insert_parent new parents =
@@ -925,27 +930,30 @@
in
fold_rev do_chunk chunks ([], [])
|>> cons []
+ ||> map nickname_of_thm
end
-fun attach_parents_to_facts facts =
- let
- fun do_facts _ _ [] = []
- | do_facts _ parents [fact] = [(parents, fact)]
- | do_facts chunks parents ((fact as (_, th)) :: (facts as (_, th') :: _)) =
- let
- val chunks = app_hd (cons th) chunks
- val (chunks', parents') =
- (if thm_less_eq (th, th') andalso
- thy_name_of_thm th = thy_name_of_thm th' then
- (chunks, [th])
- else
- chunks_and_parents_for chunks th')
- ||> map nickname_of_thm
- in (parents, fact) :: do_facts chunks' parents' facts end
- in
- facts |> sort (crude_thm_ord o pairself snd)
- |> do_facts [[]] []
- end
+fun attach_parents_to_facts _ [] = []
+ | attach_parents_to_facts old_facts (facts as (_, th) :: _) =
+ let
+ fun do_facts _ [] = []
+ | do_facts (_, parents) [fact] = [(parents, fact)]
+ | do_facts (chunks, parents)
+ ((fact as (_, th)) :: (facts as (_, th') :: _)) =
+ let
+ val chunks = app_hd (cons th) chunks
+ val chunks_and_parents' =
+ if thm_less_eq (th, th') andalso
+ thy_name_of_thm th = thy_name_of_thm th' then
+ (chunks, [nickname_of_thm th])
+ else
+ chunks_and_parents_for chunks th'
+ in (parents, fact) :: do_facts chunks_and_parents' facts end
+ in
+ old_facts @ facts
+ |> do_facts (chunks_and_parents_for [[]] th)
+ |> drop (length old_facts)
+ end
fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
@@ -1046,12 +1054,13 @@
0
else
let
- val facts =
- facts |> attach_parents_to_facts
+ val new_facts =
+ facts |> sort (crude_thm_ord o pairself snd)
+ |> attach_parents_to_facts []
|> filter_out (is_in_access_G o snd)
val (learns, (n, _, _)) =
([], (0, next_commit_time (), false))
- |> fold learn_new_fact facts
+ |> fold learn_new_fact new_facts
in commit true learns [] []; n end
fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
| relearn_old_fact ((_, (_, status)), th)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 21 16:00:48 2013 +0100
@@ -18,10 +18,11 @@
val auto_minimize_max_time : real Config.T
val minimize_facts :
(string -> thm list -> unit) -> string -> params -> bool -> int -> int
- -> Proof.state -> ((string * stature) * thm list) list
+ -> Proof.state -> play Lazy.lazy option
+ -> ((string * stature) * thm list) list
-> ((string * stature) * thm list) list option
* (play Lazy.lazy * (play -> string) * string)
- val get_minimizing_isar_prover :
+ val get_minimizing_prover :
Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover
val run_minimize :
params -> (string -> thm list -> unit) -> int
@@ -34,6 +35,7 @@
open ATP_Util
open ATP_Proof
open ATP_Problem_Generate
+open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Fact
open Sledgehammer_Reconstruct
@@ -190,7 +192,7 @@
end
fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
- i n state facts =
+ i n state preplay0 facts =
let
val ctxt = Proof.context_of state
val prover =
@@ -221,7 +223,12 @@
0 => ""
| n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
(if learn then do_learn prover_name (maps snd min_facts) else ());
- (SOME min_facts, (preplay, message, message_tail))
+ (SOME min_facts,
+ (if is_some preplay0 andalso length min_facts = length facts then
+ the preplay0
+ else
+ preplay,
+ message, message_tail))
end
| {outcome = SOME TimedOut, preplay, ...} =>
(NONE,
@@ -287,20 +294,26 @@
<= Config.get ctxt auto_minimize_max_time
fun prover_fast_enough () = can_min_fast_enough run_time
in
- if isar_proofs then
- ((prover_fast_enough (), (name, params)), preplay)
- else
- (case Lazy.force preplay of
- Played (reconstr, timeout) =>
- if can_min_fast_enough timeout then
- (true, extract_reconstructor params reconstr
- ||> (fn override_params =>
- adjust_reconstructor_params
- override_params params))
- else
- (prover_fast_enough (), (name, params))
- | _ => (prover_fast_enough (), (name, params)),
- preplay)
+ (case Lazy.force preplay of
+ Played (reconstr as Metis _, timeout) =>
+ if isar_proofs = SOME true then
+ (* Cheat: Assume the selected ATP is as fast as "metis" for
+ the goal it proved itself. *)
+ (can_min_fast_enough timeout,
+ (isar_proof_reconstructor ctxt name, params))
+ else if can_min_fast_enough timeout then
+ (true, extract_reconstructor params reconstr
+ ||> (fn override_params =>
+ adjust_reconstructor_params override_params
+ params))
+ else
+ (prover_fast_enough (), (name, params))
+ | Played (SMT, timeout) =>
+ (* Cheat: Assume the original prover is as fast as "smt" for
+ the goal it proved itself *)
+ (can_min_fast_enough timeout, (name, params))
+ | _ => (prover_fast_enough (), (name, params)),
+ preplay)
end
else
((false, (name, params)), preplay)
@@ -309,6 +322,7 @@
if minimize then
minimize_facts do_learn minimize_name params
(mode <> Normal orelse not verbose) subgoal subgoal_count state
+ (SOME preplay)
(filter_used_facts true used_facts (map (apsnd single) used_from))
|>> Option.map (map fst)
else
@@ -322,14 +336,10 @@
| NONE => result
end
-(* TODO: implement *)
-fun maybe_regenerate_isar_proof result = result
-
-fun get_minimizing_isar_prover ctxt mode do_learn name params minimize_command
- problem =
+fun get_minimizing_prover ctxt mode do_learn name params minimize_command
+ problem =
get_prover ctxt mode name params minimize_command problem
|> maybe_minimize ctxt mode do_learn name params problem
- |> maybe_regenerate_isar_proof
fun run_minimize (params as {provers, ...}) do_learn i refs state =
let
@@ -347,7 +357,7 @@
[] => error "No prover is set."
| prover :: _ =>
(kill_provers ();
- minimize_facts do_learn prover params false i n state facts
+ minimize_facts do_learn prover params false i n state NONE facts
|> (fn (_, (preplay, message, message_tail)) =>
message (Lazy.force preplay) ^ message_tail
|> Output.urgent_message))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 21 16:00:48 2013 +0100
@@ -34,7 +34,7 @@
fact_thresholds : real * real,
max_mono_iters : int option,
max_new_mono_instances : int option,
- isar_proofs : bool,
+ isar_proofs : bool option,
isar_compress : real,
slice : bool,
minimize : bool option,
@@ -110,6 +110,10 @@
val is_unit_equational_atp : Proof.context -> string -> bool
val is_prover_supported : Proof.context -> string -> bool
val is_prover_installed : Proof.context -> string -> bool
+ val remotify_prover_if_supported_and_not_already_remote :
+ Proof.context -> string -> string option
+ val remotify_prover_if_not_installed :
+ Proof.context -> string -> string option
val default_max_facts_for_prover : Proof.context -> bool -> string -> int
val is_unit_equality : term -> bool
val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
@@ -129,6 +133,7 @@
val filter_used_facts :
bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
((''a * stature) * 'b) list
+ val isar_proof_reconstructor : Proof.context -> string -> string
val get_prover : Proof.context -> mode -> string -> prover
end;
@@ -186,17 +191,33 @@
is_reconstructor orf is_smt_prover ctxt orf
is_atp_installed (Proof_Context.theory_of ctxt)
+fun remotify_prover_if_supported_and_not_already_remote ctxt name =
+ if String.isPrefix remote_prefix name then
+ SOME name
+ else
+ let val remote_name = remote_prefix ^ name in
+ if is_prover_supported ctxt remote_name then SOME remote_name else NONE
+ end
+
+fun remotify_prover_if_not_installed ctxt name =
+ if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
+ SOME name
+ else
+ remotify_prover_if_supported_and_not_already_remote ctxt name
+
fun get_slices slice slices =
(0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
val reconstructor_default_max_facts = 20
+fun slice_max_facts (_, (_, ( ((max_facts, _), _, _, _, _), _))) = max_facts
+
fun default_max_facts_for_prover ctxt slice name =
let val thy = Proof_Context.theory_of ctxt in
if is_reconstructor name then
reconstructor_default_max_facts
else if is_atp thy name then
- fold (Integer.max o fst o #1 o fst o snd o snd)
+ fold (Integer.max o slice_max_facts)
(get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0
else (* is_smt_prover ctxt name *)
SMT_Solver.default_max_relevant ctxt name
@@ -321,7 +342,7 @@
fact_thresholds : real * real,
max_mono_iters : int option,
max_new_mono_instances : int option,
- isar_proofs : bool,
+ isar_proofs : bool option,
isar_compress : real,
slice : bool,
minimize : bool option,
@@ -596,19 +617,26 @@
#> type_enc_from_string soundness
#> adjust_type_enc format
-val metis_minimize_max_time = seconds 2.0
+fun isar_proof_reconstructor ctxt name =
+ let val thy = Proof_Context.theory_of ctxt in
+ if is_atp thy name then name
+ else remotify_prover_if_not_installed ctxt eN |> the_default name
+ end
-fun choose_minimize_command params minimize_command name preplay =
+(* See the analogous logic in the function "maybe_minimize" in
+ "sledgehammer_minimize.ML". *)
+fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command
+ name preplay =
let
- val (name, override_params) =
+ val maybe_isar_name =
+ name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
+ val (min_name, override_params) =
case preplay of
- Played (reconstr, time) =>
- if Time.<= (time, metis_minimize_max_time) then
- extract_reconstructor params reconstr
- else
- (name, [])
- | _ => (name, [])
- in minimize_command override_params name end
+ Played (reconstr, _) =>
+ if isar_proofs = SOME true then (maybe_isar_name, [])
+ else extract_reconstructor params reconstr
+ | _ => (maybe_isar_name, [])
+ in minimize_command override_params min_name end
fun repair_monomorph_context max_iters best_max_iters max_new_instances
best_max_new_instances =
@@ -630,6 +658,10 @@
val mono_max_privileged_facts = 10
+(* For low values of "max_facts", this fudge value ensures that most slices are
+ invoked with a nontrivial amount of facts. *)
+val max_fact_factor_fudge = 5
+
fun run_atp mode name
({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
@@ -692,6 +724,13 @@
time available. *)
val actual_slices = get_slices slice (best_slices ctxt)
val num_actual_slices = length actual_slices
+ val max_fact_factor =
+ case max_facts of
+ NONE => 1.0
+ | SOME max =>
+ Real.fromInt max
+ / Real.fromInt (fold (Integer.max o slice_max_facts)
+ actual_slices 0)
fun monomorphize_facts facts =
let
val ctxt =
@@ -724,7 +763,9 @@
fact_filter |> the_default best_fact_filter
val facts = get_facts_for_filter effective_fact_filter factss
val num_facts =
- length facts |> is_none max_facts ? Integer.min best_max_facts
+ Real.ceil (max_fact_factor * Real.fromInt best_max_facts) +
+ max_fact_factor_fudge
+ |> Integer.min (length facts)
val soundness = if strict then Strict else Non_Strict
val type_enc =
type_enc |> choose_type_enc soundness best_type_enc format
@@ -780,7 +821,8 @@
fun sel_weights () = atp_problem_selection_weights atp_problem
fun ord_info () = atp_problem_term_order_info atp_problem
val ord = effective_term_order ctxt name
- val full_proof = debug orelse isar_proofs
+ val full_proof =
+ debug orelse (isar_proofs |> the_default (mode = Minimize))
val args =
arguments ctxt full_proof extra
(slice_timeout |> the_default one_day)
@@ -894,7 +936,7 @@
let
val _ =
if verbose then
- Output.urgent_message "Generating proof text..."
+ Output.urgent_message "Generating structured proof..."
else
()
val isar_params =
@@ -902,7 +944,8 @@
pool, fact_names, sym_tab, atp_proof, goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,
- choose_minimize_command params minimize_command name preplay,
+ choose_minimize_command ctxt params minimize_command name
+ preplay,
subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
@@ -1022,10 +1065,8 @@
val birth = Timer.checkRealTimer timer
val _ =
if debug then Output.urgent_message "Invoking SMT solver..." else ()
- val state_facts = these (try (#facts o Proof.goal) state)
val (outcome, used_facts) =
- SMT_Solver.smt_filter_preprocess ctxt state_facts goal weighted_facts
- i
+ SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
|> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
|> (fn {outcome, used_facts} => (outcome, used_facts))
handle exn => if Exn.is_interrupt exn then
@@ -1112,7 +1153,8 @@
let
val one_line_params =
(preplay, proof_banner mode name, used_facts,
- choose_minimize_command params minimize_command name preplay,
+ choose_minimize_command ctxt params minimize_command name
+ preplay,
subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in one_line_proof_text num_chained one_line_params end,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 21 16:00:48 2013 +0100
@@ -38,9 +38,10 @@
string list option
val one_line_proof_text : int -> one_line_params -> string
val isar_proof_text :
- Proof.context -> bool -> isar_params -> one_line_params -> string
+ Proof.context -> bool option -> isar_params -> one_line_params -> string
val proof_text :
- Proof.context -> bool -> isar_params -> int -> one_line_params -> string
+ Proof.context -> bool option -> isar_params -> int -> one_line_params
+ -> string
end;
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -118,8 +119,7 @@
val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
fun is_axiom_used_in_proof pred =
- exists (fn Inference_Step ((_, ss), _, _, _, []) => exists pred ss
- | _ => false)
+ exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
fun lam_trans_from_atp_proof atp_proof default =
case (is_axiom_used_in_proof is_combinator_def atp_proof,
@@ -154,24 +154,23 @@
val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
val leo2_unfold_def_rule = "unfold_def"
-fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, _, rule, deps)) =
- (if rule = leo2_extcnf_equal_neg_rule then
- insert (op =) (ext_name ctxt, (Global, General))
- else if rule = leo2_unfold_def_rule then
- (* LEO 1.3.3 does not record definitions properly, leading to missing
- dependencies in the TSTP proof. Remove the next line once this is
- fixed. *)
- add_non_rec_defs fact_names
- else if rule = satallax_coreN then
- (fn [] =>
- (* Satallax doesn't include definitions in its unsatisfiable cores,
- so we assume the worst and include them all here. *)
- [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
- | facts => facts)
- else
- I)
- #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
- | add_fact _ _ _ = I
+fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) =
+ (if rule = leo2_extcnf_equal_neg_rule then
+ insert (op =) (ext_name ctxt, (Global, General))
+ else if rule = leo2_unfold_def_rule then
+ (* LEO 1.3.3 does not record definitions properly, leading to missing
+ dependencies in the TSTP proof. Remove the next line once this is
+ fixed. *)
+ add_non_rec_defs fact_names
+ else if rule = satallax_coreN then
+ (fn [] =>
+ (* Satallax doesn't include definitions in its unsatisfiable cores, so
+ we assume the worst and include them all here. *)
+ [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
+ | facts => facts)
+ else
+ I)
+ #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
fun used_facts_in_atp_proof ctxt fact_names atp_proof =
if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
@@ -298,9 +297,6 @@
else
s
-fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
- | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
-
fun infer_formula_types ctxt =
Type.constraint HOLogic.boolT
#> Syntax.check_term
@@ -325,41 +321,22 @@
| aux t = t
in aux end
-fun decode_line sym_tab (Definition_Step (name, phi1, phi2)) ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
- val t1 = prop_from_atp ctxt true sym_tab phi1
- val vars = snd (strip_comb t1)
- val frees = map unvarify_term vars
- val unvarify_args = subst_atomic (vars ~~ frees)
- val t2 = prop_from_atp ctxt true sym_tab phi2
- val (t1, t2) =
- HOLogic.eq_const HOLogic.typeT $ t1 $ t2
- |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt
- |> HOLogic.dest_eq
- in
- (Definition_Step (name, t1, t2),
- fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
- end
- | decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
- val t = u |> prop_from_atp ctxt true sym_tab
- |> uncombine_term thy |> infer_formula_types ctxt
- in
- (Inference_Step (name, role, t, rule, deps),
- fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
- end
+fun decode_line sym_tab (name, role, u, rule, deps) ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val t = u |> prop_from_atp ctxt true sym_tab
+ |> uncombine_term thy |> infer_formula_types ctxt
+ in
+ ((name, role, t, rule, deps),
+ fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
+ end
fun decode_lines ctxt sym_tab lines =
fst (fold_map (decode_line sym_tab) lines ctxt)
fun replace_one_dependency (old, new) dep =
if is_same_atp_step dep old then new else [dep]
-fun replace_dependencies_in_line _ (line as Definition_Step _) = line
- | replace_dependencies_in_line p
- (Inference_Step (name, role, t, rule, deps)) =
- Inference_Step (name, role, t, rule,
- fold (union (op =) o replace_one_dependency p) deps [])
+fun replace_dependencies_in_line p (name, role, t, rule, deps) =
+ (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps [])
(* No "real" literals means only type information (tfree_tcs, clsrel, or
clsarity). *)
@@ -367,19 +344,16 @@
fun s_maybe_not role = role <> Conjecture ? s_not
-fun is_same_inference _ (Definition_Step _) = false
- | is_same_inference (role, t) (Inference_Step (_, role', t', _, _)) =
- s_maybe_not role t aconv s_maybe_not role' t'
+fun is_same_inference (role, t) (_, role', t', _, _) =
+ s_maybe_not role t aconv s_maybe_not role' t'
(* Discard facts; consolidate adjacent lines that prove the same formula, since
they differ only in type information.*)
-fun add_line _ (line as Definition_Step _) lines = line :: lines
- | add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, []))
- lines =
+fun add_line fact_names (name as (_, ss), role, t, rule, []) lines =
(* No dependencies: fact, conjecture, or (for Vampire) internal facts or
definitions. *)
if is_conjecture ss then
- Inference_Step (name, role, t, rule, []) :: lines
+ (name, role, t, rule, []) :: lines
else if is_fact fact_names ss then
(* Facts are not proof lines. *)
if is_only_type_information t then
@@ -388,35 +362,30 @@
lines
else
map (replace_dependencies_in_line (name, [])) lines
- | add_line _ (line as Inference_Step (name, role, t, rule, deps)) lines =
+ | add_line _ (line as (name, role, t, _, _)) lines =
(* Type information will be deleted later; skip repetition test. *)
if is_only_type_information t then
line :: lines
(* Is there a repetition? If so, replace later line by earlier one. *)
else case take_prefix (not o is_same_inference (role, t)) lines of
- (* FIXME: Doesn't this code risk conflating proofs involving different
- types? *)
(_, []) => line :: lines
- | (pre, Inference_Step (name', _, _, _, _) :: post) =>
+ | (pre, (name', _, _, _, _) :: post) =>
line :: pre @ map (replace_dependencies_in_line (name', [name])) post
- | _ => raise Fail "unexpected inference"
val waldmeister_conjecture_num = "1.0.0.0"
val repair_waldmeister_endgame =
let
- fun do_tail (Inference_Step (name, _, t, rule, deps)) =
- Inference_Step (name, Negated_Conjecture, s_not t, rule, deps)
- | do_tail line = line
+ fun do_tail (name, _, t, rule, deps) =
+ (name, Negated_Conjecture, s_not t, rule, deps)
fun do_body [] = []
- | do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) =
+ | do_body ((line as ((num, _), _, _, _, _)) :: lines) =
if num = waldmeister_conjecture_num then map do_tail (line :: lines)
else line :: do_body lines
- | do_body (line :: lines) = line :: do_body lines
in do_body end
(* Recursively delete empty lines (type information) from the proof. *)
-fun add_nontrivial_line (line as Inference_Step (name, _, t, _, [])) lines =
+fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
if is_only_type_information t then delete_dependency name lines
else line :: lines
| add_nontrivial_line line lines = line :: lines
@@ -435,25 +404,23 @@
val is_skolemize_rule =
member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
-fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) =
- (j, line :: map (replace_dependencies_in_line (name, [])) lines)
- | add_desired_line fact_names frees
- (Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) =
- (j + 1,
- if is_fact fact_names ss orelse
- is_conjecture ss orelse
- is_skolemize_rule rule orelse
- (* the last line must be kept *)
- j = 0 orelse
- (not (is_only_type_information t) andalso
- null (Term.add_tvars t []) andalso
- not (exists_subterm (is_bad_free frees) t) andalso
- length deps >= 2 andalso
- (* kill next to last line, which usually results in a trivial step *)
- j <> 1) then
- Inference_Step (name, role, t, rule, deps) :: lines (* keep line *)
- else
- map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
+fun add_desired_line fact_names frees (name as (_, ss), role, t, rule, deps)
+ (j, lines) =
+ (j + 1,
+ if is_fact fact_names ss orelse
+ is_conjecture ss orelse
+ is_skolemize_rule rule orelse
+ (* the last line must be kept *)
+ j = 0 orelse
+ (not (is_only_type_information t) andalso
+ null (Term.add_tvars t []) andalso
+ not (exists_subterm (is_bad_free frees) t) andalso
+ length deps >= 2 andalso
+ (* kill next to last line, which usually results in a trivial step *)
+ j <> 1) then
+ (name, role, t, rule, deps) :: lines (* keep line *)
+ else
+ map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
val indent_size = 2
@@ -537,18 +504,20 @@
add_step_pre ind qs subproofs
#> add_suffix (of_prove qs (length subproofs) ^ " ")
#> add_step_post ind l t facts ""
- | add_step ind (Obtain (qs, Fix xs, l, t,
- By_Metis (subproofs, facts))) =
+ | add_step ind (Obtain (qs, Fix xs, l, t, By_Metis (subproofs, facts))) =
add_step_pre ind qs subproofs
#> add_suffix (of_obtain qs (length subproofs) ^ " ")
#> add_frees xs
#> add_suffix " where "
(* The new skolemizer puts the arguments in the same order as the ATPs
- (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
- Vampire). *)
- #> add_step_post ind l t facts "using [[metis_new_skolem]] "
- and add_steps ind steps =
- fold (add_step ind) steps
+ (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
+ Vampire). *)
+ #> add_step_post ind l t facts
+ (if exists (fn (_, T) => length (binder_types T) > 1) xs then
+ "using [[metis_new_skolem]] "
+ else
+ "")
+ and add_steps ind = fold (add_step ind)
and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
("", ctxt)
|> add_fix ind xs
@@ -566,12 +535,11 @@
end
fun add_labels_of_step step =
- (case byline_of_step step of
- NONE => I
- | SOME (By_Metis (subproofs, (ls, _))) =>
- union (op =) (add_labels_of_proofs subproofs ls))
+ case byline_of_step step of
+ NONE => I
+ | SOME (By_Metis (subproofs, (ls, _))) =>
+ union (op =) ls #> fold add_labels_of_proof subproofs
and add_labels_of_proof proof = fold add_labels_of_step (steps_of_proof proof)
-and add_labels_of_proofs proofs = fold add_labels_of_proof proofs
fun kill_useless_labels_in_proof proof =
let
@@ -617,17 +585,13 @@
val (l, subst, next) =
(l, subst, next) |> fresh_label depth have_prefix
val by = by |> do_byline subst depth
- in
- Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps
- end
+ in Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps end
| do_steps subst depth next (Prove (qs, l, t, by) :: steps) =
let
val (l, subst, next) =
(l, subst, next) |> fresh_label depth have_prefix
val by = by |> do_byline subst depth
- in
- Prove (qs, l, t, by) :: do_steps subst depth next steps
- end
+ in Prove (qs, l, t, by) :: do_steps subst depth next steps end
| do_steps subst depth next (step :: steps) =
step :: do_steps subst depth next steps
and do_proof subst depth (Proof (fix, assms, steps)) =
@@ -646,7 +610,7 @@
if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0)
else ([], lfs)
fun chain_step lbl (Obtain (qs, xs, l, t,
- By_Metis (subproofs, (lfs, gfs)))) =
+ By_Metis (subproofs, (lfs, gfs)))) =
let val (qs', lfs) = do_qs_lfs lbl lfs in
Obtain (qs' @ qs, xs, l, t,
By_Metis (chain_proofs subproofs, (lfs, gfs)))
@@ -701,31 +665,30 @@
val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
val conjs =
atp_proof |> map_filter
- (fn Inference_Step (name as (_, ss), _, _, _, []) =>
+ (fn (name as (_, ss), _, _, _, []) =>
if member (op =) ss conj_name then SOME name else NONE
| _ => NONE)
val assms =
atp_proof |> map_filter
- (fn Inference_Step (name as (_, ss), _, _, _, []) =>
+ (fn (name as (_, ss), _, _, _, []) =>
(case resolve_conjecture ss of
[j] =>
if j = length hyp_ts then NONE
else SOME (raw_label_for_name name, nth hyp_ts j)
| _ => NONE)
| _ => NONE)
- fun dep_of_step (Definition_Step _) = NONE
- | dep_of_step (Inference_Step (name, _, _, _, from)) =
- SOME (from, name)
+ val bot = atp_proof |> List.last |> #1
val refute_graph =
- atp_proof |> map_filter dep_of_step |> make_refute_graph
+ atp_proof
+ |> map (fn (name, _, _, _, from) => (from, name))
+ |> make_refute_graph bot
+ |> fold (Atom_Graph.default_node o rpair ()) conjs
val axioms = axioms_of_refute_graph refute_graph conjs
val tainted = tainted_atoms_of_refute_graph refute_graph conjs
val is_clause_tainted = exists (member (op =) tainted)
- val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
val steps =
Symtab.empty
- |> fold (fn Definition_Step _ => I (* FIXME *)
- | Inference_Step (name as (s, _), role, t, rule, _) =>
+ |> fold (fn (name as (s, _), role, t, rule, _) =>
Symtab.update_new (s, (rule,
t |> (if is_clause_tainted [name] then
s_maybe_not role
@@ -750,9 +713,8 @@
in
case List.partition (can HOLogic.dest_not) lits of
(negs as _ :: _, pos as _ :: _) =>
- HOLogic.mk_imp
- (Library.foldr1 s_conj (map HOLogic.dest_not negs),
- Library.foldr1 s_disj pos)
+ s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs),
+ Library.foldr1 s_disj pos)
| _ => fold (curry s_disj) lits @{term False}
end
|> HOLogic.mk_Trueprop |> close_form
@@ -831,7 +793,7 @@
else
compress_proof debug ctxt type_enc lam_trans preplay
preplay_timeout
- (if isar_proofs then isar_compress else 1000.0))
+ (if isar_proofs = SOME true then isar_compress else 1000.0))
|>> cleanup_labels_in_proof
val isar_text =
string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
@@ -839,25 +801,23 @@
in
case isar_text of
"" =>
- if isar_proofs then
+ if isar_proofs = SOME true then
"\nNo structured proof available (proof too simple)."
else
""
| _ =>
let
val msg =
+ (if verbose then
+ let
+ val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
+ in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end
+ else
+ []) @
(if preplay then
[(if preplay_fail then "may fail, " else "") ^
Sledgehammer_Preplay.string_of_preplay_time preplay_time]
else
- []) @
- (if verbose then
- let
- val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
- in
- [string_of_int num_steps ^ " step" ^ plural_s num_steps]
- end
- else
[])
in
"\n\nStructured proof "
@@ -870,15 +830,22 @@
isar_proof_of ()
else case try isar_proof_of () of
SOME s => s
- | NONE => if isar_proofs then
+ | NONE => if isar_proofs = SOME true then
"\nWarning: The Isar proof construction failed."
else
""
in one_line_proof ^ isar_proof end
+fun isar_proof_would_be_a_good_idea preplay =
+ case preplay of
+ Played (reconstr, _) => reconstr = SMT
+ | Trust_Playable _ => true
+ | Failed_to_Play _ => true
+
fun proof_text ctxt isar_proofs isar_params num_chained
(one_line_params as (preplay, _, _, _, _, _)) =
- (if case preplay of Failed_to_Play _ => true | _ => isar_proofs then
+ (if isar_proofs = SOME true orelse
+ (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
isar_proof_text ctxt isar_proofs isar_params
else
one_line_proof_text num_chained) one_line_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Feb 21 10:52:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Feb 21 16:00:48 2013 +0100
@@ -98,7 +98,7 @@
|> Output.urgent_message
fun really_go () =
problem
- |> get_minimizing_isar_prover ctxt mode learn name params minimize_command
+ |> get_minimizing_prover ctxt mode learn name params minimize_command
|> verbose
? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
print_used_facts used_facts used_from