--- a/Admin/components/components.sha1 Thu Jan 17 14:11:26 2013 +0100
+++ b/Admin/components/components.sha1 Thu Jan 17 14:12:35 2013 +0100
@@ -6,6 +6,8 @@
cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz
+2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
+e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz
8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz
e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz
--- a/Admin/components/main Thu Jan 17 14:11:26 2013 +0100
+++ b/Admin/components/main Thu Jan 17 14:12:35 2013 +0100
@@ -1,6 +1,6 @@
#main components for everyday use, without big impact on overall build time
cvc3-2.4.1
-e-1.6
+e-1.6-2
exec_process-1.0.3
Haskabelle-2013
jdk-7u11
--- a/src/Doc/Sledgehammer/document/root.tex Thu Jan 17 14:11:26 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Jan 17 14:12:35 2013 +0100
@@ -12,7 +12,7 @@
%\usepackage[scaled=.85]{beramono}
\usepackage{isabelle,iman,pdfsetup}
-\newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}}
+\newcommand\download{\url{http://isabelle.in.tum.de/components/}}
\def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}
@@ -865,6 +865,12 @@
that contains the \texttt{emales.py} script. Sledgehammer has been tested with
version 1.1.
+\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is a metaprover developed
+by Josef Urban that implements strategy scheduling on top of E. To use
+E-Par, set the environment variable \texttt{E\_HOME} to the directory
+that contains the \texttt{runepar.pl} script and the \texttt{eprover} and
+\texttt{epclextract} executables, or use the prebuilt E package from \download.
+
\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the
--- a/src/HOL/Sledgehammer.thy Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/Sledgehammer.thy Thu Jan 17 14:12:35 2013 +0100
@@ -16,6 +16,7 @@
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
ML_file "Tools/Sledgehammer/sledgehammer_shrink.ML"
ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
--- a/src/HOL/TPTP/MaSh_Eval.thy Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy Thu Jan 17 14:12:35 2013 +0100
@@ -12,9 +12,9 @@
sledgehammer_params
[provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
- lam_trans = combs_and_lifting, timeout = 15, dont_preplay, minimize]
+ lam_trans = lifting, timeout = 15, dont_preplay, minimize]
-declare [[sledgehammer_instantiate_inducts]]
+declare [[sledgehammer_instantiate_inducts = false]]
ML {*
!Multithreading.max_threads
--- a/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jan 17 14:12:35 2013 +0100
@@ -12,9 +12,9 @@
sledgehammer_params
[provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
- lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize]
+ lam_trans = lifting, timeout = 2, dont_preplay, minimize]
-declare [[sledgehammer_instantiate_inducts]]
+declare [[sledgehammer_instantiate_inducts = false]]
ML {*
!Multithreading.max_threads
@@ -29,7 +29,7 @@
val thys = [@{theory List}]
val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
val prover = hd provers
-val max_suggestions = 1024
+val max_suggestions = 1536
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
*}
--- a/src/HOL/TPTP/atp_theory_export.ML Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Jan 17 14:12:35 2013 +0100
@@ -68,9 +68,9 @@
|> File.write_list prob_file
val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
- File.shell_path (Path.explode path) ^
- " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^
- File.shell_path prob_file
+ File.shell_path (Path.explode path) ^ " " ^
+ arguments ctxt false "" (seconds 1.0) (File.shell_path prob_file)
+ (ord, K [], K [])
in
TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command
|> fst
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Jan 17 14:12:35 2013 +0100
@@ -16,7 +16,7 @@
type atp_config =
{exec : string list * string list,
arguments :
- Proof.context -> bool -> string -> Time.time
+ Proof.context -> bool -> string -> Time.time -> string
-> term_order * (unit -> (string * int) list)
* (unit -> (string * real) list) -> string,
proof_delims : (string * string) list,
@@ -45,6 +45,7 @@
val dummy_thfN : string
val eN : string
val e_malesN : string
+ val e_parN : string
val e_sineN : string
val e_tofofN : string
val iproverN : string
@@ -88,7 +89,7 @@
type atp_config =
{exec : string list * string list,
arguments :
- Proof.context -> bool -> string -> Time.time
+ Proof.context -> bool -> string -> Time.time -> string
-> term_order * (unit -> (string * int) list)
* (unit -> (string * real) list) -> string,
proof_delims : (string * string) list,
@@ -140,6 +141,7 @@
val dummy_thfN = "dummy_thf" (* for experiments *)
val eN = "e"
val e_malesN = "e_males"
+val e_parN = "e_par"
val e_sineN = "e_sine"
val e_tofofN = "e_tofof"
val iproverN = "iprover"
@@ -189,9 +191,9 @@
val alt_ergo_config : atp_config =
{exec = (["WHY3_HOME"], ["why3"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
"--format tff1 --prover alt-ergo --timelimit " ^
- string_of_int (to_secs 1 timeout),
+ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
proof_delims = [],
known_failures =
[(ProofMissing, ": Valid"),
@@ -301,13 +303,14 @@
val e_config : atp_config =
{exec = (["E_HOME"], ["eproof_ram", "eproof"]),
arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout =>
+ fn file_name =>
fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
"--tstp-in --tstp-out --output-level=5 --silent " ^
e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
"--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
"--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
- e_shell_level_argument full_proof,
+ e_shell_level_argument full_proof ^ " " ^ file_name,
proof_delims = tstp_proof_delims,
known_failures =
[(TimedOut, "Failure: Resource limit exceeded (time)"),
@@ -334,27 +337,45 @@
val e_males_config : atp_config =
{exec = (["E_MALES_HOME"], ["emales.py"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
- "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p",
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+ "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name,
proof_delims = tstp_proof_delims,
known_failures = #known_failures e_config,
prem_role = Conjecture,
best_slices =
(* FUDGE *)
- K [(1.0, ((1000, FOF, "mono_tags??", combsN, false), ""))],
+ K [(0.5, ((1000, FOF, "mono_tags??", combsN, false), "")),
+ (0.5, ((1000, FOF, "mono_guards??", combsN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
val e_males = (e_malesN, fn () => e_males_config)
+(* E-Par *)
+
+val e_par_config : atp_config =
+ {exec = (["E_HOME"], ["runepar.pl"]),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+ string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^
+ " 2" (* proofs *),
+ proof_delims = tstp_proof_delims,
+ known_failures = #known_failures e_config,
+ prem_role = Conjecture,
+ best_slices = #best_slices e_males_config,
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = default_max_new_mono_instances}
+
+val e_par = (e_parN, fn () => e_par_config)
+
+
(* iProver *)
val iprover_config : atp_config =
{exec = (["IPROVER_HOME"], ["iprover"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
"--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^
- string_of_real (Time.toReal timeout),
+ string_of_real (Time.toReal timeout) ^ " " ^ file_name,
proof_delims = tstp_proof_delims,
known_failures =
[(ProofIncomplete, "% SZS output start CNFRefutation")] @
@@ -393,10 +414,11 @@
val leo2_config : atp_config =
{exec = (["LEO2_HOME"], ["leo"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
"--foatp e --atp e=\"$E_HOME\"/eprover \
\--atp epclextract=\"$E_HOME\"/epclextract \
- \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
+ \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
+ file_name,
proof_delims = tstp_proof_delims,
known_failures =
[(TimedOut, "CPU time limit exceeded, terminating"),
@@ -419,8 +441,8 @@
val satallax_config : atp_config =
{exec = (["SATALLAX_HOME"], ["satallax"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
- "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+ "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
proof_delims =
[("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
known_failures = known_szs_status_failures,
@@ -446,9 +468,11 @@
(* FIXME: Make "SPASS_NEW_HOME" legacy. *)
val spass_config : atp_config =
{exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
- arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
- ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
- |> extra_options <> "" ? prefix (extra_options ^ " "),
+ arguments =
+ fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ =>
+ "-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^
+ file_name
+ |> extra_options <> "" ? prefix (extra_options ^ " "),
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
[(OldSPASS, "Unrecognized option Isabelle"),
@@ -489,14 +513,14 @@
val vampire_config : atp_config =
{exec = (["VAMPIRE_HOME"], ["vampire"]),
- arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
+ arguments = fn _ => fn _ => fn sos => fn timeout => fn file_name => fn _ =>
"--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"
else
"") ^
- " --thanks \"Andrei and Krystof\" --input_file"
+ " --thanks \"Andrei and Krystof\" --input_file " ^ file_name
|> sos = sosN ? prefix "--sos on ",
proof_delims =
[("=========== Refutation ==========",
@@ -535,9 +559,9 @@
val z3_tptp_config : atp_config =
{exec = (["Z3_HOME"], ["z3"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
"MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
- string_of_int (to_secs 1 timeout),
+ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
proof_delims = [("\ncore(", ").")],
known_failures = known_szs_status_failures,
prem_role = Hypothesis,
@@ -557,7 +581,7 @@
fun dummy_config format type_enc : atp_config =
{exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
- arguments = K (K (K (K (K "")))),
+ arguments = K (K (K (K (K (K ""))))),
proof_delims = [],
known_failures = known_szs_status_failures,
prem_role = Hypothesis,
@@ -623,10 +647,12 @@
fun remote_config system_name system_versions proof_delims known_failures
prem_role best_slice : atp_config =
{exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
- arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
- (if command <> "" then "-c " ^ quote command ^ " " else "") ^
- "-s " ^ the_remote_system system_name system_versions ^ " " ^
- "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
+ arguments =
+ fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
+ (if command <> "" then "-c " ^ quote command ^ " " else "") ^
+ "-s " ^ the_remote_system system_name system_versions ^ " " ^
+ "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
+ " " ^ file_name,
proof_delims = union (op =) tstp_proof_delims proof_delims,
known_failures = known_failures @ known_perl_failures @ known_says_failures,
prem_role = prem_role,
@@ -726,10 +752,10 @@
end
val atps=
- [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_snark, remote_waldmeister]
+ [alt_ergo, e, e_males, e_par, 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_snark, remote_waldmeister]
val setup = fold add_atp atps
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jan 17 14:12:35 2013 +0100
@@ -0,0 +1,112 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Preplaying of isar proofs.
+*)
+
+signature SLEDGEHAMMER_PREPLAY =
+sig
+ type isar_step = Sledgehammer_Proof.isar_step
+ eqtype preplay_time
+ val zero_preplay_time : preplay_time
+ val some_preplay_time : preplay_time
+ val add_preplay_time : preplay_time -> preplay_time -> preplay_time
+ val string_of_preplay_time : preplay_time -> string
+ val try_metis : bool -> string -> string -> Proof.context ->
+ Time.time -> (isar_step option * isar_step) -> unit -> preplay_time
+ val try_metis_quietly : bool -> string -> string -> Proof.context ->
+ Time.time -> (isar_step option * isar_step) -> unit -> preplay_time
+end
+
+structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Proof
+
+(* The boolean flag encodes whether the time is exact (false) or an lower bound
+ (true) *)
+type preplay_time = bool * Time.time
+
+val zero_preplay_time = (false, Time.zeroTime)
+val some_preplay_time = (true, Time.zeroTime)
+
+fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
+
+val string_of_preplay_time = ATP_Util.string_from_ext_time
+
+(* timing *)
+fun take_time timeout tac arg =
+ let
+ val timing = Timing.start ()
+ in
+ (TimeLimit.timeLimit timeout tac arg;
+ Timing.result timing |> #cpu |> pair false)
+ handle TimeLimit.TimeOut => (true, timeout)
+ end
+
+(* lookup facts in context *)
+fun resolve_fact_names ctxt names =
+ names
+ |>> map string_for_label
+ |> op @
+ |> maps (thms_of_name ctxt)
+
+exception ZEROTIME
+fun try_metis debug type_enc lam_trans ctxt timeout (succedent, step) =
+ let
+ val (t, byline, obtain) =
+ (case step of
+ Prove (_, _, t, byline) => (t, byline, false)
+ | Obtain (_, xs, _, t, byline) =>
+ (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
+ (see ~~/src/Pure/Isar/obtain.ML) *)
+ let
+ val thesis = Term.Free ("thesis", HOLogic.boolT)
+ val thesis_prop = thesis |> HOLogic.mk_Trueprop
+ val frees = map Term.Free xs
+
+ (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
+ val inner_prop =
+ fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
+
+ (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
+ val prop =
+ Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
+ in
+ (prop, byline, true)
+ end
+ | _ => raise ZEROTIME)
+ val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+ val facts =
+ (case byline of
+ By_Metis fact_names => resolve_fact_names ctxt fact_names
+ | Case_Split (cases, fact_names) =>
+ resolve_fact_names ctxt fact_names
+ @ (case the succedent of
+ Assume (_, t) => make_thm t
+ | Obtain (_, _, _, t, _) => make_thm t
+ | Prove (_, _, t, _) => make_thm t
+ | _ => error "preplay error: unexpected succedent of case split")
+ :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
+ | _ => error "preplay error: malformed case split")
+ #> make_thm)
+ cases)
+ val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
+ |> obtain ? Config.put Metis_Tactic.new_skolem true
+ val goal =
+ Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
+ fun tac {context = ctxt, prems = _} =
+ Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
+ in
+ take_time timeout
+ (fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg))
+ end
+ handle ZEROTIME => K zero_preplay_time
+
+(* this version treats exceptions like timeouts *)
+fun try_metis_quietly debug type_enc lam_trans ctxt timeout =
+ the_default (true, timeout) oo try o try_metis debug type_enc lam_trans ctxt timeout
+
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 17 14:12:35 2013 +0100
@@ -786,12 +786,12 @@
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 args = arguments ctxt full_proof extra
- (slice_timeout |> the_default one_day)
- (ord, ord_info, sel_weights)
+ val args =
+ arguments ctxt full_proof extra
+ (slice_timeout |> the_default one_day)
+ (File.shell_path prob_path) (ord, ord_info, sel_weights)
val command =
- "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
- File.shell_path prob_path ^ ")"
+ "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
|> enclose "TIMEFORMAT='%3R'; { time " " ; }"
val _ =
atp_problem
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 17 14:12:35 2013 +0100
@@ -741,7 +741,7 @@
and do_case outer (c, infs) =
Assume (label_of_clause c, prop_of_clause c) ::
map (isar_step_of_direct_inf outer) infs
- val (isar_proof, (preplay_fail, ext_time)) =
+ val (isar_proof, (preplay_fail, preplay_time)) =
ref_graph
|> redirect_graph axioms tainted
|> map (isar_step_of_direct_inf true)
@@ -771,8 +771,8 @@
let
val msg =
(if preplay then
- [if preplay_fail then "may fail"
- else string_from_ext_time ext_time]
+ [(if preplay_fail then "may fail, " else "") ^
+ Sledgehammer_Preplay.string_of_preplay_time preplay_time]
else
[]) @
(if verbose then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Thu Jan 17 14:12:35 2013 +0100
@@ -2,15 +2,16 @@
Author: Jasmin Blanchette, TU Muenchen
Author: Steffen Juilf Smolka, TU Muenchen
-Shrinking and preplaying of reconstructed isar proofs.
+Shrinking of reconstructed isar proofs.
*)
signature SLEDGEHAMMER_SHRINK =
sig
type isar_step = Sledgehammer_Proof.isar_step
+ type preplay_time = Sledgehammer_Preplay.preplay_time
val shrink_proof :
bool -> Proof.context -> string -> string -> bool -> Time.time option
- -> real -> isar_step list -> isar_step list * (bool * (bool * Time.time))
+ -> real -> isar_step list -> isar_step list * (bool * preplay_time)
end
structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK =
@@ -18,6 +19,7 @@
open Sledgehammer_Util
open Sledgehammer_Proof
+open Sledgehammer_Preplay
(* Parameters *)
val merge_timeout_slack = 1.2
@@ -44,17 +46,6 @@
fun pop_max tab = pop tab (the (Inttab.max_key tab))
fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
-(* Timing *)
-fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
-val no_time = (false, Time.zeroTime)
-fun take_time timeout tac arg =
- let val timing = Timing.start () in
- (TimeLimit.timeLimit timeout tac arg;
- Timing.result timing |> #cpu |> SOME)
- handle TimeLimit.TimeOut => NONE
- end
-
-
(* Main function for shrinking proofs *)
fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
isar_shrink proof =
@@ -70,9 +61,11 @@
fun handle_metis_fail try_metis () =
try_metis () handle exn =>
(if Exn.is_interrupt exn orelse debug then reraise exn
- else metis_fail := true; SOME Time.zeroTime)
+ else metis_fail := true; some_preplay_time)
fun get_time lazy_time =
- if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
+ if !metis_fail andalso not (Lazy.is_finished lazy_time)
+ then some_preplay_time
+ else Lazy.force lazy_time
val metis_fail = fn () => !metis_fail
end
@@ -118,116 +111,60 @@
v_fold_index (add_if_cand proof_vect) refed_by_vect []
|> Inttab.make_list
- (* Metis Preplaying *)
- fun resolve_fact_names names =
- names
- |>> map string_for_label
- |> op @
- |> maps (thms_of_name ctxt)
-
- (* TODO: add "Obtain" case *)
- exception ZEROTIME
- fun try_metis timeout (succedent, step) =
- (if not preplay then K (SOME Time.zeroTime) else
- let
- val (t, byline, obtain) =
- (case step of
- Prove (_, _, t, byline) => (t, byline, false)
- | Obtain (_, xs, _, t, byline) =>
- (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
- (see ~~/src/Pure/Isar/obtain.ML) *)
- let
- val thesis = Term.Free ("thesis", HOLogic.boolT)
- val thesis_prop = thesis |> HOLogic.mk_Trueprop
- val frees = map Term.Free xs
-
- (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
- val inner_prop =
- fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
-
- (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
- val prop =
- Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
- in
- (prop, byline, true)
- end
- | _ => raise ZEROTIME)
- val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
- val facts =
- (case byline of
- By_Metis fact_names => resolve_fact_names fact_names
- | Case_Split (cases, fact_names) =>
- resolve_fact_names fact_names
- @ (case the succedent of
- Assume (_, t) => make_thm t
- | Obtain (_, _, _, t, _) => make_thm t
- | Prove (_, _, t, _) => make_thm t
- | _ => error "Internal error: unexpected succedent of case split")
- :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
- | _ => error "Internal error: malformed case split")
- #> make_thm)
- cases)
- val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
- |> obtain ? Config.put Metis_Tactic.new_skolem true
- val goal =
- Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
- fun tac {context = ctxt, prems = _} =
- Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
- in
- take_time timeout (fn () => goal tac)
- end)
- handle ZEROTIME => K (SOME Time.zeroTime)
-
- val try_metis_quietly = the_default NONE oo try oo try_metis
-
(* cache metis preplay times in lazy time vector *)
val metis_time =
v_map_index
- (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout
- o apfst (fn i => try (the o get (i-1)) proof_vect) o apsnd the)
+ (if not preplay then K (zero_preplay_time) #> Lazy.value
+ else
+ apsnd the (* step *)
+ #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *)
+ #> try_metis debug type_enc lam_trans ctxt preplay_timeout
+ #> handle_metis_fail
+ #> Lazy.lazy)
proof_vect
+
fun sum_up_time lazy_time_vector =
Vector.foldl
- ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts))
- | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout)))
- o apfst get_time)
- no_time lazy_time_vector
+ (apfst get_time #> uncurry add_preplay_time)
+ zero_preplay_time lazy_time_vector
(* Merging *)
- (* TODO: consider adding "Obtain" cases *)
fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 =
let
val (step_constructor, lfs2, gfs2) =
(case step2 of
(Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
(fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
- | (Obtain(qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
+ | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
(fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
- | _ => error "Internal error: unmergeable Isar steps" )
+ | _ => error "sledgehammer_shrink: unmergeable Isar steps" )
val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
val gfs = union (op =) gfs1 gfs2
in step_constructor (By_Metis (lfs, gfs)) end
- | merge _ _ = error "Internal error: unmergeable Isar steps"
+ | merge _ _ = error "sledgehammer_shrink: unmergeable Isar steps"
fun try_merge metis_time (s1, i) (s2, j) =
- (case get i metis_time |> Lazy.force of
- NONE => (NONE, metis_time)
- | SOME t1 =>
- (case get j metis_time |> Lazy.force of
- NONE => (NONE, metis_time)
- | SOME t2 =>
- let
- val s12 = merge s1 s2
- val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
- in
- case try_metis_quietly timeout (NONE, s12) () of
- NONE => (NONE, metis_time)
- | some_t12 =>
- (SOME s12, metis_time
- |> replace (Time.zeroTime |> SOME |> Lazy.value) i
- |> replace (Lazy.value some_t12) j)
+ if not preplay then (merge s1 s2 |> SOME, metis_time)
+ else
+ (case get i metis_time |> Lazy.force of
+ (true, _) => (NONE, metis_time)
+ | (_, t1) =>
+ (case get j metis_time |> Lazy.force of
+ (true, _) => (NONE, metis_time)
+ | (_, t2) =>
+ let
+ val s12 = merge s1 s2
+ val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
+ in
+ case try_metis_quietly debug type_enc lam_trans ctxt timeout
+ (NONE, s12) () of
+ (true, _) => (NONE, metis_time)
+ | exact_time =>
+ (SOME s12, metis_time
+ |> replace (zero_preplay_time |> Lazy.value) i
+ |> replace (Lazy.value exact_time) j)
- end))
+ end))
fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
if Inttab.is_empty cand_tab
@@ -286,20 +223,20 @@
proof |> do_case_splits rich_ctxt
|>> shrink_top_level on_top_level rich_ctxt
in
- (proof, ext_time_add lower_level_time top_level_time)
+ (proof, add_preplay_time lower_level_time top_level_time)
end
and do_case_splits ctxt proof =
let
fun shrink_each_and_collect_time shrink candidates =
- let fun f_m cand time = shrink cand ||> ext_time_add time
- in fold_map f_m candidates no_time end
+ let fun f_m cand time = shrink cand ||> add_preplay_time time
+ in fold_map f_m candidates zero_preplay_time end
val shrink_case_split =
shrink_each_and_collect_time (do_proof false ctxt)
fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) =
let val (cases, time) = shrink_case_split cases
in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
- | shrink step = (step, no_time)
+ | shrink step = (step, zero_preplay_time)
in
shrink_each_and_collect_time shrink proof
end