--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 14 15:42:58 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 14 16:18:15 2012 +0200
@@ -927,12 +927,6 @@
name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
noncommercial user. Sledgehammer has been tested with versions 3.0, 3.1, 3.2,
and 4.0.
-
-\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
-an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
-formats (FOF and TFF0). It is included for experimental purposes. Sledgehammer
-requires version 4.0 or above. To use it, set the environment variable
-\texttt{Z3\_HOME} to the directory that contains the \texttt{z3} executable.
\end{enum}
\end{sloppy}
@@ -986,9 +980,6 @@
\item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
point).
-
-\item[\labelitemi] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
-with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
\end{enum}
By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Aug 14 15:42:58 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Aug 14 16:18:15 2012 +0200
@@ -52,7 +52,7 @@
Proof.context -> (string * stature) list vector -> 'a proof
-> string list option
val unalias_type_enc : string -> string list
- val one_line_proof_text : one_line_params -> string
+ val one_line_proof_text : int -> one_line_params -> string
val make_tvar : string -> typ
val make_tfree : Proof.context -> string -> typ
val term_from_atp :
@@ -64,7 +64,7 @@
val isar_proof_text :
Proof.context -> bool -> isar_params -> one_line_params -> string
val proof_text :
- Proof.context -> bool -> isar_params -> one_line_params -> string
+ Proof.context -> bool -> isar_params -> int -> one_line_params -> string
end;
structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
@@ -250,21 +250,33 @@
fun show_time NONE = ""
| show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
+fun unusing_chained_facts _ 0 = ""
+ | unusing_chained_facts used_chaineds num_chained =
+ if length used_chaineds = num_chained then ""
+ else if null used_chaineds then "(* using no facts *) "
+ else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
+
fun apply_on_subgoal _ 1 = "by "
| apply_on_subgoal 1 _ = "apply "
| apply_on_subgoal i n =
"prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
+
fun command_call name [] =
name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
| command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+
fun try_command_line banner time command =
banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^ show_time time ^ "."
+
fun using_labels [] = ""
| using_labels ls =
"using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun reconstructor_command reconstr i n (ls, ss) =
+
+fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
+ unusing_chained_facts used_chaineds num_chained ^
using_labels ls ^ apply_on_subgoal i n ^
command_call (string_for_reconstructor reconstr) ss
+
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
@@ -276,8 +288,9 @@
facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
|> pairself (sort_distinct (string_ord o pairself fst))
-fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
- subgoal, subgoal_count) =
+fun one_line_proof_text num_chained
+ (preplay, banner, used_facts, minimize_command, subgoal,
+ subgoal_count) =
let
val (chained, extra) = split_used_facts used_facts
val (failed, reconstr, ext_time) =
@@ -292,7 +305,8 @@
| Failed_to_Play reconstr => (true, reconstr, NONE)
val try_line =
([], map fst extra)
- |> reconstructor_command reconstr subgoal subgoal_count
+ |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
+ num_chained
|> (if failed then
enclose "One-line proof reconstruction failed: "
".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
@@ -845,7 +859,7 @@
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
val reconstr = Metis (type_enc, lam_trans)
fun do_facts (ls, ss) =
- reconstructor_command reconstr 1 1
+ reconstructor_command reconstr 1 1 [] 0
(ls |> sort_distinct (prod_ord string_ord int_ord),
ss |> sort_distinct string_ord)
and do_step ind (Fix xs) =
@@ -887,7 +901,7 @@
(if isar_proof_requested then 1 else 2) * isar_shrink_factor
val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
- val one_line_proof = one_line_proof_text one_line_params
+ val one_line_proof = one_line_proof_text 0 one_line_params
val type_enc =
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
else partial_typesN
@@ -982,11 +996,11 @@
""
in one_line_proof ^ isar_proof end
-fun proof_text ctxt isar_proof isar_params
+fun proof_text ctxt isar_proof isar_params num_chained
(one_line_params as (preplay, _, _, _, _, _)) =
(if case preplay of Failed_to_Play _ => true | _ => isar_proof then
isar_proof_text ctxt isar_proof isar_params
else
- one_line_proof_text) one_line_params
+ one_line_proof_text num_chained) one_line_params
end;
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 14 15:42:58 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 14 16:18:15 2012 +0200
@@ -513,8 +513,8 @@
best_slices = fn ctxt =>
(* FUDGE *)
(if is_vampire_beyond_1_8 () then
- [(0.333, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)),
- (0.333, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN)),
+ [(0.333, ((500, vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
+ (0.333, ((150, vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
(0.334, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
else
[(0.333, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
@@ -528,7 +528,7 @@
val vampire = (vampireN, fn () => vampire_config)
-(* Z3 with TPTP syntax *)
+(* Z3 with TPTP syntax (half experimental, half legacy) *)
val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
@@ -665,9 +665,6 @@
val remote_vampire =
remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
(K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
-val remote_z3_tptp =
- remotify_atp z3_tptp "Z3" ["3.0"]
- (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
(K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
@@ -728,7 +725,7 @@
[alt_ergo, e, e_males, iprover, iprover_eq, leo2, satallax, spass, spass_poly,
vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, remote_e_tofof,
remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax,
- remote_vampire, remote_z3_tptp, remote_snark, remote_waldmeister]
+ remote_vampire, remote_snark, remote_waldmeister]
val setup = fold add_atp atps
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Aug 14 15:42:58 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Aug 14 16:18:15 2012 +0200
@@ -128,8 +128,9 @@
case test timeout (xs @ seen) of
result as {outcome = NONE, used_facts, run_time, ...}
: prover_result =>
- min (new_timeout timeout run_time) (filter_used_facts used_facts xs)
- (filter_used_facts used_facts seen, result)
+ min (new_timeout timeout run_time)
+ (filter_used_facts true used_facts xs)
+ (filter_used_facts false used_facts seen, result)
| _ => min timeout xs (x :: seen, result)
in min timeout xs ([], result) end
@@ -154,20 +155,21 @@
in
case test timeout (sup @ l0) of
result as {outcome = NONE, used_facts, ...} =>
- min depth result (filter_used_facts used_facts sup)
- (filter_used_facts used_facts l0)
+ min depth result (filter_used_facts true used_facts sup)
+ (filter_used_facts true used_facts l0)
| _ =>
case test timeout (sup @ r0) of
result as {outcome = NONE, used_facts, ...} =>
- min depth result (filter_used_facts used_facts sup)
- (filter_used_facts used_facts r0)
+ min depth result (filter_used_facts true used_facts sup)
+ (filter_used_facts true used_facts r0)
| _ =>
let
val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
val (sup, r0) =
- (sup, r0) |> pairself (filter_used_facts (map fst sup_r0))
+ (sup, r0)
+ |> pairself (filter_used_facts true (map fst sup_r0))
val (sup_l, (r, result)) = min depth result (sup @ l) r0
- val sup = sup |> filter_used_facts (map fst sup_l)
+ val sup = sup |> filter_used_facts true (map fst sup_l)
in (sup, (l @ r, result)) end
end
(*
@@ -189,14 +191,18 @@
val ctxt = Proof.context_of state
val prover =
get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
- val _ = print silent (fn () => "Sledgehammer minimizer: " ^
- quote prover_name ^ ".")
fun test timeout = test_facts params silent prover timeout i n state
+ val (chained, non_chained) = List.partition is_fact_chained facts
+ (* Push chained facts to the back, so that they are less likely to be
+ kicked out by the linear minimization algorithm. *)
+ val facts = non_chained @ chained
in
- (case test timeout facts of
+ (print silent (fn () => "Sledgehammer minimizer: " ^
+ quote prover_name ^ ".");
+ case test timeout facts of
result as {outcome = NONE, used_facts, run_time, ...} =>
let
- val facts = filter_used_facts used_facts facts
+ val facts = filter_used_facts true used_facts facts
val min =
if length facts >= Config.get ctxt binary_min_facts then
binary_minimize
@@ -207,8 +213,7 @@
in
print silent (fn () => cat_lines
["Minimized to " ^ n_facts (map fst min_facts)] ^
- (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
- |> length of
+ (case min_facts |> filter is_fact_chained |> length of
0 => ""
| n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
(if learn then do_learn prover_name (maps snd min_facts) else ());
@@ -302,7 +307,7 @@
minimize_facts do_learn minimize_name params
(mode <> Normal orelse not verbose) subgoal
subgoal_count state
- (filter_used_facts used_facts
+ (filter_used_facts true used_facts
(map (apsnd single o untranslated_fact) facts))
|>> Option.map (map fst)
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 14 15:42:58 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 14 16:18:15 2012 +0200
@@ -131,7 +131,10 @@
val kill_provers : unit -> unit
val running_provers : unit -> unit
val messages : int option -> unit
- val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
+ val is_fact_chained : (('a * stature) * 'b) -> bool
+ val filter_used_facts :
+ bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
+ ((''a * stature) * 'b) list
val get_prover : Proof.context -> mode -> string -> prover
end;
@@ -442,14 +445,18 @@
| _ => "Try this"
fun bunch_of_reconstructors needs_full_types lam_trans =
- [(false, Metis (partial_type_enc, lam_trans false)),
- (true, Metis (full_type_enc, lam_trans false)),
- (false, Metis (no_typesN, lam_trans true)),
- (true, Metis (really_full_type_enc, lam_trans true)),
- (true, SMT)]
- |> map_filter (fn (full_types, reconstr) =>
- if needs_full_types andalso not full_types then NONE
- else SOME reconstr)
+ if needs_full_types then
+ [Metis (full_type_enc, lam_trans false),
+ Metis (really_full_type_enc, lam_trans false),
+ Metis (full_type_enc, lam_trans true),
+ Metis (really_full_type_enc, lam_trans true),
+ SMT]
+ else
+ [Metis (partial_type_enc, lam_trans false),
+ Metis (full_type_enc, lam_trans false),
+ Metis (no_typesN, lam_trans true),
+ Metis (really_full_type_enc, lam_trans true),
+ SMT]
fun extract_reconstructor ({type_enc, lam_trans, ...} : params)
(Metis (type_enc', lam_trans')) =
@@ -483,7 +490,11 @@
#> (fn ctxt => tac_for_reconstructor reconstr ctxt ths))
|> timed_apply timeout
-fun filter_used_facts used = filter (member (op =) used o fst)
+fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
+
+fun filter_used_facts keep_chained used =
+ filter ((member (op =) used o fst) orf
+ (if keep_chained then is_fact_chained else K false))
fun play_one_line_proof mode debug verbose timeout pairs state i preferred
reconstrs =
@@ -862,7 +873,8 @@
fn () =>
let
val used_pairs =
- facts |> map untranslated_fact |> filter_used_facts used_facts
+ facts |> map untranslated_fact
+ |> filter_used_facts false used_facts
in
play_one_line_proof mode debug verbose preplay_timeout
used_pairs state subgoal (hd reconstrs) reconstrs
@@ -876,7 +888,11 @@
(preplay, proof_banner mode name, used_facts,
choose_minimize_command params minimize_command name preplay,
subgoal, subgoal_count)
- in proof_text ctxt isar_proof isar_params one_line_params end,
+ val num_chained = length (#facts (Proof.goal state))
+ in
+ proof_text ctxt isar_proof isar_params num_chained
+ one_line_params
+ end,
(if verbose then
"\nATP real CPU time: " ^ string_from_time run_time ^ "."
else
@@ -906,7 +922,8 @@
(103, MalformedInput),
(110, MalformedInput)]
val unix_failures =
- [(139, Crashed)]
+ [(138, Crashed),
+ (139, Crashed)]
val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
@@ -1045,15 +1062,17 @@
play_one_line_proof mode debug verbose preplay_timeout used_pairs
state subgoal SMT
(bunch_of_reconstructors false
- (fn plain =>
- if plain then metis_default_lam_trans else liftingN)),
+ (fn desperate =>
+ if desperate then liftingN
+ else metis_default_lam_trans)),
fn preplay =>
let
val one_line_params =
(preplay, proof_banner mode name, used_facts,
choose_minimize_command params minimize_command name preplay,
subgoal, subgoal_count)
- in one_line_proof_text one_line_params end,
+ val num_chained = length (#facts (Proof.goal state))
+ in one_line_proof_text num_chained one_line_params end,
if verbose then
"\nSMT solver real CPU time: " ^ string_from_time run_time ^ "."
else
@@ -1095,7 +1114,8 @@
(play, proof_banner mode name, used_facts,
minimize_command override_params name, subgoal,
subgoal_count)
- in one_line_proof_text one_line_params end,
+ val num_chained = length (#facts (Proof.goal state))
+ in one_line_proof_text num_chained one_line_params end,
message_tail = ""}
| play =>
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 14 15:42:58 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 14 16:18:15 2012 +0200
@@ -87,7 +87,7 @@
fun print_used_facts used_facts =
tag_list 1 facts
|> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
- |> filter_used_facts used_facts
+ |> filter_used_facts false used_facts
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
|> commas
|> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^