# HG changeset patch # User blanchet # Date 1387457001 -3600 # Node ID 10d48c2a3e320ede7fcc960c6d42e139aa32c0cf # Parent 4f6ec8754bf53bbc5c81fd170907bb68623bf36e made timeouts in Sledgehammer not be 'option's -- simplified lots of code diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/Doc/Nitpick/document/root.tex --- a/src/Doc/Nitpick/document/root.tex Thu Dec 19 10:15:12 2013 +0100 +++ b/src/Doc/Nitpick/document/root.tex Thu Dec 19 13:43:21 2013 +0100 @@ -1892,9 +1892,8 @@ \item[\labelitemi] \qtybf{int\_range}: An integer (e.g., 3) or a range of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\}. \item[\labelitemi] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8). -\item[\labelitemi] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number -(e.g., 0.5) expressing a number of seconds, or the keyword \textit{none} -($\infty$ seconds). +\item[\labelitemi] \qtybf{float}: An floating-point number (e.g., 0.5 or 60) +expressing a number of seconds. \item[\labelitemi] \qtybf{const\/}: The name of a HOL constant. \item[\labelitemi] \qtybf{term}: A HOL term (e.g., ``$f~x$''). \item[\labelitemi] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g., @@ -2531,7 +2530,7 @@ \label{timeouts} \begin{enum} -\opdefault{timeout}{float\_or\_none}{\upshape 30} +\opdefault{timeout}{float}{\upshape 30} Specifies the maximum number of seconds that the \textbf{nitpick} command should spend looking for a counterexample. Nitpick tries to honor this constraint as well as it can but offers no guarantees. For automatic runs, the ``Auto Time @@ -2541,7 +2540,7 @@ \nopagebreak {\small See also \textit{max\_threads} (\S\ref{optimizations}).} -\opdefault{tac\_timeout}{float\_or\_none}{\upshape 0.5} +\opdefault{tac\_timeout}{float}{\upshape 0.5} Specifies the maximum number of seconds that should be used by internal tactics---\textit{lexicographic\_order} and \textit{size\_change} when checking whether a (co)in\-duc\-tive predicate is well-founded, \textit{auto} tactic when diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Dec 19 10:15:12 2013 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Dec 19 13:43:21 2013 +0100 @@ -789,13 +789,11 @@ \item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or \textit{smart}. \item[\labelitemi] \qtybf{int\/}: An integer. -%\item[\labelitemi] \qtybf{float\/}: A floating-point number (e.g., 2.5). +\item[\labelitemi] \qtybf{float}: A floating-point number (e.g., 2.5 or 60) +expressing a number of seconds. \item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers (e.g., 0.6 0.95). \item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}. -\item[\labelitemi] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or -0.5) expressing a number of seconds, or the keyword \textit{none} ($\infty$ -seconds). \end{enum} Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options @@ -1356,11 +1354,11 @@ \label{timeouts} \begin{enum} -\opdefault{timeout}{float\_or\_none}{\upshape 30} +\opdefault{timeout}{float}{\upshape 30} Specifies the maximum number of seconds that the automatic provers should spend searching for a proof. This excludes problem preparation and is a soft limit. -\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 3} +\opdefault{preplay\_timeout}{float}{\upshape 3} Specifies the maximum number of seconds that \textit{metis} or \textit{smt} should spend trying to ``preplay'' the found proof. If this option is set to 0, no preplaying takes place, and no timing information is displayed next to the diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Thu Dec 19 13:43:21 2013 +0100 @@ -176,7 +176,7 @@ "slice" |> not slice ? prefix "dont_", "type_enc = " ^ the_default "smart" type_enc, "lam_trans = " ^ the_default "smart" lam_trans, - "timeout = " ^ ATP_Util.string_of_time (the_default one_year timeout), + "timeout = " ^ ATP_Util.string_of_time timeout, "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] val _ = print " * * *"; val _ = print ("Options: " ^ commas options); diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Dec 19 13:43:21 2013 +0100 @@ -172,7 +172,7 @@ val is_problem_trivially_false : problem -> bool val problems_equivalent : problem * problem -> bool val solve_any_problem : - bool -> bool -> Time.time option -> int -> int -> problem list -> outcome + bool -> bool -> Time.time -> int -> int -> problem list -> outcome end; structure Kodkod : KODKOD = @@ -983,10 +983,7 @@ val fudge_ms = 250 fun milliseconds_until_deadline deadline = - case deadline of - NONE => ~1 - | SOME time => - Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) - fudge_ms) + Int.max (0, Time.toMilliseconds (Time.- (deadline, Time.now ())) - fudge_ms) fun uncached_solve_any_problem overlord deadline max_threads max_solutions problems = diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Dec 19 13:43:21 2013 +0100 @@ -43,8 +43,8 @@ peephole_optim: bool, datatype_sym_break: int, kodkod_sym_break: int, - timeout: Time.time option, - tac_timeout: Time.time option, + timeout: Time.time, + tac_timeout: Time.time, max_threads: int, show_datatypes: bool, show_skolems: bool, @@ -129,8 +129,8 @@ peephole_optim: bool, datatype_sym_break: int, kodkod_sym_break: int, - timeout: Time.time option, - tac_timeout: Time.time option, + timeout: Time.time, + tac_timeout: Time.time, max_threads: int, show_datatypes: bool, show_skolems: bool, @@ -193,14 +193,10 @@ val max_unsound_delay_ms = 200 val max_unsound_delay_percent = 2 -fun unsound_delay_for_timeout NONE = max_unsound_delay_ms - | unsound_delay_for_timeout (SOME timeout) = - Int.max (0, Int.min (max_unsound_delay_ms, - Time.toMilliseconds timeout - * max_unsound_delay_percent div 100)) - -fun passed_deadline NONE = false - | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS +fun unsound_delay_for_timeout timeout = + Int.max (0, Int.min (max_unsound_delay_ms, + Time.toMilliseconds timeout + * max_unsound_delay_percent div 100)) fun none_true assigns = forall (not_equal (SOME true) o snd) assigns @@ -258,7 +254,10 @@ val print_v = pprint_v o K o plazy fun check_deadline () = - if passed_deadline deadline then raise TimeLimit.TimeOut else () + if Time.compare (Time.now (), deadline) <> LESS then + raise TimeLimit.TimeOut + else + () val (def_assm_ts, nondef_assm_ts) = if assms orelse mode <> Normal then (def_assm_ts, nondef_assm_ts) @@ -385,8 +384,8 @@ (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse is_number_type ctxt T orelse is_bit_type T fun is_type_actually_monotonic T = - time_limit tac_timeout (formulas_monotonic hol_ctxt binarize T) - (nondef_ts, def_ts) + TimeLimit.timeLimit tac_timeout (formulas_monotonic hol_ctxt binarize T) + (nondef_ts, def_ts) handle TimeLimit.TimeOut => false fun is_type_kind_of_monotonic T = case triple_lookup (type_match thy) monos T of @@ -579,8 +578,7 @@ val bit_width = if bits = 0 then 16 else bits + 1 val delay = if unsound then - Option.map (fn time => Time.- (time, Time.now ())) deadline - |> unsound_delay_for_timeout + unsound_delay_for_timeout (Time.- (deadline, Time.now ())) else 0 val settings = [("solver", commas_quote kodkod_sat_solver), @@ -1075,10 +1073,9 @@ else let val unknown_outcome = (unknownN, state) - val deadline = Option.map (curry Time.+ (Time.now ())) timeout + val deadline = Time.+ (Time.now (), timeout) val outcome as (outcome_code, _) = - time_limit (if debug orelse is_none timeout then NONE - else SOME (Time.+ (the timeout, timeout_bonus))) + TimeLimit.timeLimit (Time.+ (timeout, timeout_bonus)) (pick_them_nits_in_term deadline state params mode i n step subst def_assm_ts nondef_assm_ts) orig_t handle TOO_LARGE (_, details) => diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Dec 19 13:43:21 2013 +0100 @@ -29,7 +29,7 @@ star_linear_preds: bool, total_consts: bool option, needs: term list option, - tac_timeout: Time.time option, + tac_timeout: Time.time, evals: term list, case_names: (string * int) list, def_tables: const_table * const_table, @@ -271,7 +271,7 @@ star_linear_preds: bool, total_consts: bool option, needs: term list option, - tac_timeout: Time.time option, + tac_timeout: Time.time, evals: term list, case_names: (string * int) list, def_tables: const_table * const_table, @@ -2069,8 +2069,7 @@ #> the #> Goal.finish ctxt) goal val max_cached_wfs = 50 -val cached_timeout = - Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime) +val cached_timeout = Synchronized.var "Nitpick_HOL.cached_timeout" Time.zeroTime val cached_wf_props = Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list) diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Dec 19 13:43:21 2013 +0100 @@ -226,8 +226,8 @@ lookup_assigns read prefix "" (space_explode " ") fun lookup_time name = case lookup name of - SOME s => parse_time_option name s - | NONE => NONE + SOME s => parse_time name s + | NONE => Time.zeroTime val read_type_polymorphic = Syntax.read_typ ctxt #> Logic.mk_type #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type @@ -269,7 +269,7 @@ val peephole_optim = lookup_bool "peephole_optim" val datatype_sym_break = lookup_int "datatype_sym_break" val kodkod_sym_break = lookup_int "kodkod_sym_break" - val timeout = if mode = Auto_Try then NONE else lookup_time "timeout" + val timeout = lookup_time "timeout" val tac_timeout = lookup_time "tac_timeout" val max_threads = if mode = Normal then Int.max (0, lookup_int "max_threads") else 1 diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Dec 19 13:43:21 2013 +0100 @@ -41,7 +41,7 @@ -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> Pretty.T * bool val prove_hol_model : - scope -> Time.time option -> nut list -> nut list -> nut NameTable.table + scope -> Time.time -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> term -> bool option end; diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Dec 19 13:43:21 2013 +0100 @@ -533,9 +533,9 @@ string_for_vars ", " (sort int_ord xs)) |> space_implode "\n")) -(* The ML solver timeout should correspond more or less to the overhead of - invoking an external prover. *) -val ml_solver_timeout = SOME (seconds 0.02) +(* The ML solver timeout should correspond more or less to the overhead of invoking an external + prover. *) +val ml_solver_timeout = seconds 0.02 fun solve tac_timeout max_var (comps, clauses) = let @@ -560,11 +560,12 @@ |> List.partition (member (op =) ["dptsat", "dpll"] o fst) val res = if null nonml_solvers then - time_limit tac_timeout (snd (hd ml_solvers)) prop + TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop else - time_limit ml_solver_timeout (snd (hd ml_solvers)) prop + TimeLimit.timeLimit ml_solver_timeout (snd (hd ml_solvers)) prop handle TimeLimit.TimeOut => - time_limit tac_timeout (SatSolver.invoke_solver "auto") prop + TimeLimit.timeLimit tac_timeout + (SatSolver.invoke_solver "auto") prop in case res of SatSolver.SATISFIABLE assigns => do_assigns assigns diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Thu Dec 19 13:43:21 2013 +0100 @@ -211,11 +211,11 @@ fun run_all_tests () = let - val {debug, overlord, ...} = Nitpick_Isar.default_params @{theory} [] + val {debug, overlord, timeout, ...} = Nitpick_Isar.default_params @{theory} [] val max_threads = 1 val max_solutions = 1 in - case Kodkod.solve_any_problem debug overlord NONE max_threads max_solutions + case Kodkod.solve_any_problem debug overlord timeout max_threads max_solutions (map (problem_for_nut @{context}) tests) of Kodkod.Normal ([], _, _) => () | _ => error "Tests failed." diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Dec 19 13:43:21 2013 +0100 @@ -51,7 +51,7 @@ val serial_commas : string -> string list -> string list val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list val parse_bool_option : bool -> string -> string -> bool option - val parse_time_option : string -> string -> Time.time option + val parse_time : string -> string -> Time.time val string_of_time : Time.time -> string val nat_subscript : int -> string val flip_polarity : polarity -> polarity @@ -71,8 +71,7 @@ val monomorphic_term : Type.tyenv -> term -> term val specialize_type : theory -> string * typ -> term -> term val eta_expand : typ list -> term -> int -> term - val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b - val DETERM_TIMEOUT : Time.time option -> tactic -> tactic + val DETERM_TIMEOUT : Time.time -> tactic -> tactic val indent_size : int val pstrs : string -> Pretty.T list val unyxml : string -> string @@ -238,7 +237,7 @@ p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps val parse_bool_option = Sledgehammer_Util.parse_bool_option -val parse_time_option = Sledgehammer_Util.parse_time_option +val parse_time = Sledgehammer_Util.parse_time val string_of_time = ATP_Util.string_of_time val subscript = implode o map (prefix "\<^sub>") o Symbol.explode @@ -296,10 +295,9 @@ val monomorphic_term = ATP_Util.monomorphic_term val specialize_type = ATP_Util.specialize_type val eta_expand = ATP_Util.eta_expand -val time_limit = Sledgehammer_Util.time_limit fun DETERM_TIMEOUT delay tac st = - Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ())) + Seq.of_list (the_list (TimeLimit.timeLimit delay (fn () => SINGLE tac st) ())) val indent_size = 2 diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Dec 19 13:43:21 2013 +0100 @@ -120,8 +120,7 @@ ("dont_try0_isar", "isar_try0")] val params_not_for_minimize = - ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", - "minimize"]; + ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"]; val property_dependent_params = ["provers", "timeout"] @@ -225,40 +224,40 @@ val lookup = Option.map implode_param o AList.lookup (op =) raw_params val lookup_string = the_default "" o lookup fun general_lookup_bool option default_value name = - case lookup name of + (case lookup name of SOME s => parse_bool_option option name s - | NONE => default_value + | NONE => default_value) val lookup_bool = the o general_lookup_bool false (SOME false) fun lookup_time name = - case lookup name of - SOME s => parse_time_option name s - | NONE => NONE + (case lookup name of + SOME s => parse_time name s + | NONE => Time.zeroTime) fun lookup_int name = - case lookup name of + (case lookup name of NONE => 0 - | SOME s => case Int.fromString s of - SOME n => n - | NONE => error ("Parameter " ^ quote name ^ - " must be assigned an integer value.") + | SOME s => + (case Int.fromString s of + SOME n => n + | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value."))) fun lookup_real name = - case lookup name of + (case lookup name of NONE => 0.0 - | SOME s => case Real.fromString s of - SOME n => n - | NONE => error ("Parameter " ^ quote name ^ - " must be assigned a real value.") + | SOME s => + (case Real.fromString s of + SOME n => n + | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value."))) fun lookup_real_pair name = - case lookup name of + (case lookup name of NONE => (0.0, 0.0) - | SOME s => case s |> space_explode " " |> map Real.fromString of - [SOME r1, SOME r2] => (r1, r2) - | _ => error ("Parameter " ^ quote name ^ - " must be assigned a pair of floating-point \ - \values (e.g., \"0.6 0.95\")") + | SOME s => + (case s |> space_explode " " |> map Real.fromString of + [SOME r1, SOME r2] => (r1, r2) + | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ + \values (e.g., \"0.6 0.95\")"))) fun lookup_option lookup' name = - case lookup name of + (case lookup name of SOME "smart" => NONE - | _ => SOME (lookup' name) + | _ => SOME (lookup' name)) val debug = mode <> Auto_Try andalso lookup_bool "debug" val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" @@ -291,9 +290,8 @@ val isar_try0 = lookup_bool "isar_try0" val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" - val timeout = if mode = Auto_Try then NONE else lookup_time "timeout" - val preplay_timeout = - if mode = Auto_Try then SOME Time.zeroTime else lookup_time "preplay_timeout" + val timeout = lookup_time "timeout" + val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout" val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking, diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 19 13:43:21 2013 +0100 @@ -1070,7 +1070,7 @@ fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths = if is_mash_enabled () then - launch_thread (timeout |> the_default one_day) (fn () => + launch_thread timeout (fn () => let val thy = Proof_Context.theory_of ctxt val feats = features_of ctxt thy 0 Symtab.empty (Local, General) false [t] |> map fst @@ -1095,12 +1095,11 @@ val commit_timeout = seconds 30.0 (* The timeout is understood in a very relaxed fashion. *) -fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover - save auto_level run_prover learn_timeout facts = +fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover save auto_level + run_prover learn_timeout facts = let val timer = Timer.startRealTimer () - fun next_commit_time () = - Time.+ (Timer.checkRealTimer timer, commit_timeout) + fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout) val {access_G, ...} = peek_state ctxt overlord I val is_in_access_G = is_fact_in_graph access_G o snd val no_new_facts = forall is_in_access_G facts @@ -1182,10 +1181,7 @@ (commit false learns [] []; ([], next_commit_time ())) else (learns, next_commit) - val timed_out = - case learn_timeout of - SOME timeout => Time.> (Timer.checkRealTimer timer, timeout) - | NONE => false + val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) in (learns, (n, next_commit, timed_out)) end val n = if no_new_facts then @@ -1215,10 +1211,7 @@ ([], [], next_commit_time ())) else (relearns, flops, next_commit) - val timed_out = - case learn_timeout of - SOME timeout => Time.> (Timer.checkRealTimer timer, timeout) - | NONE => false + val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) in ((relearns, flops), (n, next_commit, timed_out)) end val n = if not run_prover then @@ -1267,15 +1260,13 @@ val num_facts = length facts val prover = hd provers fun learn auto_level run_prover = - mash_learn_facts ctxt params prover true auto_level run_prover NONE facts + mash_learn_facts ctxt params prover true auto_level run_prover one_year facts |> Output.urgent_message in if run_prover then - ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ - plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ - (case timeout of - SOME timeout => " timeout: " ^ string_of_time timeout - | NONE => "") ^ ").\n\nCollecting Isar proofs first..." + ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ + " for automatic proofs (" ^ quote prover ^ " timeout: " ^ string_of_time timeout ^ + ").\n\nCollecting Isar proofs first..." |> Output.urgent_message; learn 1 false; "Now collecting automatic proofs. This may take several hours. You can \ @@ -1305,10 +1296,8 @@ Sledgehammer and Try. *) val min_secs_for_learning = 15 -fun relevant_facts ctxt - (params as {overlord, blocking, learn, fact_filter, timeout, ...}) - prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t - facts = +fun relevant_facts ctxt (params as {overlord, blocking, learn, fact_filter, timeout, ...}) prover + max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = if not (subset (op =) (the_list fact_filter, fact_filters)) then error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") else if only then @@ -1320,16 +1309,11 @@ else let fun maybe_launch_thread () = - if not blocking andalso - not (Async_Manager.has_running_threads MaShN) andalso - (timeout = NONE orelse - Time.toSeconds (the timeout) >= min_secs_for_learning) then - let - val timeout = Option.map (time_mult learn_timeout_slack) timeout - in - launch_thread (timeout |> the_default one_day) - (fn () => (true, mash_learn_facts ctxt params prover true 2 - false timeout facts)) + if not blocking andalso not (Async_Manager.has_running_threads MaShN) andalso + Time.toSeconds timeout >= min_secs_for_learning then + let val timeout = time_mult learn_timeout_slack timeout in + launch_thread timeout + (fn () => (true, mash_learn_facts ctxt params prover true 2 false timeout facts)) end else () diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 19 13:43:21 2013 +0100 @@ -61,13 +61,8 @@ let val _ = print silent (fn () => - "Testing " ^ n_facts (map fst facts) ^ - (if verbose then - case timeout of - SOME timeout => " (timeout: " ^ string_of_time timeout ^ ")" - | _ => "" - else - "") ^ "...") + "Testing " ^ n_facts (map fst facts) ^ + (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true, @@ -103,11 +98,9 @@ part of the timeout. *) val slack_msecs = 200 -fun new_timeout NONE _ = NONE - | new_timeout (SOME timeout) run_time = - Int.min (Time.toMilliseconds timeout, - Time.toMilliseconds run_time + slack_msecs) - |> Time.fromMilliseconds |> SOME +fun new_timeout timeout run_time = + Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs) + |> Time.fromMilliseconds (* The linear algorithm usually outperforms the binary algorithm when over 60% of the facts are actually needed. The binary algorithm is much more @@ -128,14 +121,15 @@ let fun min _ [] p = p | min timeout (x :: xs) (seen, result) = - case test timeout (xs @ seen) of - result as {outcome = NONE, used_facts, run_time, ...} - : prover_result => + (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 true used_facts xs) (filter_used_facts false used_facts seen, result) - | _ => min timeout xs (x :: seen, result) - in min timeout xs ([], result) end + | _ => min timeout xs (x :: seen, result)) + in + min timeout xs ([], result) + end fun binary_minimize test timeout result xs = let @@ -188,8 +182,8 @@ | p => p end -fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent - i n state goal preplay0 facts = +fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal + preplay0 facts = let val ctxt = Proof.context_of state val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name @@ -222,24 +216,18 @@ message, message_tail)) end | {outcome = SOME TimedOut, preplay, ...} => - (NONE, - (preplay, - fn _ => - "Timeout: You can increase the time limit using the \"timeout\" \ - \option (e.g., \"timeout = " ^ - string_of_int (10 + Time.toMilliseconds - (timeout |> the_default (seconds 60.0)) div 1000) ^ - "\").", "")) + (NONE, (preplay, fn _ => + "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ + \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", "")) | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))) handle ERROR msg => (NONE, (Lazy.value (Play_Failed plain_metis), fn _ => "Error: " ^ msg, "")) end fun adjust_reconstructor_params override_params - ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, - lam_trans, uncurried_aliases, learn, fact_filter, max_facts, - fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs, - isar_compress, isar_try0, slice, minimize, timeout, preplay_timeout, - expect} : params) = + ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans, + uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters, + max_new_mono_instances, isar_proofs, isar_compress, isar_try0, slice, minimize, timeout, + preplay_timeout, expect} : params) = let fun lookup_override name default_value = case AList.lookup (op =) override_params name of @@ -284,20 +272,18 @@ (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)) + (* 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)) + 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 *) + (* 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) diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Dec 19 13:43:21 2013 +0100 @@ -9,7 +9,7 @@ signature SLEDGEHAMMER_PROOF = sig type label = string * int - type facts = label list * string list (* local & global facts *) + type facts = label list * string list (* local and global facts *) datatype isar_qualifier = Show | Then diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 13:43:21 2013 +0100 @@ -40,8 +40,8 @@ isar_try0 : bool, slice : bool, minimize : bool option, - timeout : Time.time option, - preplay_timeout : Time.time option, + timeout : Time.time, + preplay_timeout : Time.time, expect : string} type prover_problem = @@ -281,8 +281,8 @@ isar_try0 : bool, slice : bool, minimize : bool option, - timeout : Time.time option, - preplay_timeout : Time.time option, + timeout : Time.time, + preplay_timeout : Time.time, expect : string} type prover_problem = @@ -378,7 +378,9 @@ let val {context = ctxt, facts, goal} = Proof.goal state val full_tac = Method.insert_tac facts i THEN tac ctxt i - in time_limit timeout (try (Seq.pull o full_tac)) goal end + in + TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal + end fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans @@ -401,24 +403,20 @@ if member (op =) reconstrs preferred then preferred else List.last reconstrs in - if timeout = SOME Time.zeroTime then + if timeout = Time.zeroTime then Play_Timed_Out (get_preferred reconstrs, Time.zeroTime) else let val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else () val ths = pairs |> sort_wrt (fst o fst) |> map snd fun play [] [] = Play_Failed (get_preferred reconstrs) - | play timed_outs [] = - Play_Timed_Out (get_preferred timed_outs, timeout |> the_default Time.zeroTime (* wrong *)) + | play timed_outs [] = Play_Timed_Out (get_preferred timed_outs, timeout) | play timed_out (reconstr :: reconstrs) = let val _ = if verbose then - "Trying \"" ^ string_of_reconstructor reconstr ^ "\"" ^ - (case timeout of - SOME timeout => " for " ^ string_of_time timeout - | NONE => "") ^ "..." - |> Output.urgent_message + Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^ + "\" for " ^ string_of_time timeout ^ "...") else () val timer = Timer.startRealTimer () @@ -664,27 +662,20 @@ val sound = is_type_enc_sound type_enc val real_ms = Real.fromInt o Time.toMilliseconds val slice_timeout = - case time_left of - SOME time_left => - ((real_ms time_left - |> (if slice < num_actual_slices - 1 then - curry Real.min (time_frac * real_ms (the timeout)) - else - I)) - * 0.001) - |> seconds |> SOME - | NONE => NONE + (real_ms time_left + |> (if slice < num_actual_slices - 1 then + curry Real.min (time_frac * real_ms timeout) + else + I)) + * 0.001 + |> seconds val generous_slice_timeout = - if mode = MaSh then NONE - else Option.map (curry Time.+ atp_timeout_slack) slice_timeout + if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack) val _ = if debug then quote name ^ " slice #" ^ string_of_int (slice + 1) ^ " with " ^ string_of_int num_facts ^ " fact" ^ - plural_s num_facts ^ - (case slice_timeout of - SOME timeout => " for " ^ string_of_time timeout - | NONE => "") ^ "..." + plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..." |> Output.urgent_message else () @@ -715,8 +706,8 @@ val ord = effective_term_order ctxt name val full_proof = isar_proofs |> the_default (mode = Minimize) val args = - arguments ctxt full_proof extra (slice_timeout |> the_default one_day) - (File.shell_path prob_path) (ord, ord_info, sel_weights) + arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path) + (ord, ord_info, sel_weights) val command = "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")" |> enclose "TIMEFORMAT='%3R'; { time " " ; }" @@ -726,7 +717,7 @@ |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path val ((output, run_time), (atp_proof, outcome)) = - time_limit generous_slice_timeout Isabelle_System.bash_output command + TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I) |> fst |> split_time |> (fn accum as (output, _) => @@ -734,7 +725,7 @@ extract_tstplike_proof_and_outcome verbose proof_delims known_failures output |>> atp_proof_of_tstplike_proof atp_problem handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete))) - handle TimeLimit.TimeOut => (("", the slice_timeout), ([], SOME TimedOut)) + handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut)) val outcome = case outcome of NONE => @@ -759,13 +750,9 @@ fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _))) = let - val time_left = - Option.map - (fn timeout => Time.- (timeout, Timer.checkRealTimer timer)) - timeout + val time_left = Time.- (timeout, Timer.checkRealTimer timer) in - if time_left <> NONE andalso - Time.<= (the time_left, Time.zeroTime) then + if Time.<= (time_left, Time.zeroTime) then result else run_slice time_left cache slice @@ -935,24 +922,21 @@ let val timer = Timer.startRealTimer () val slice_timeout = - if slice < max_slices andalso timeout <> NONE then - let val ms = timeout |> the |> Time.toMilliseconds in + if slice < max_slices then + let val ms = Time.toMilliseconds timeout in Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs, Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms))) - |> Time.fromMilliseconds |> SOME + |> Time.fromMilliseconds end else timeout val num_facts = length weighted_facts val _ = if debug then - quote name ^ " slice " ^ string_of_int slice ^ " with " ^ - string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ - (case slice_timeout of - SOME timeout => " for " ^ string_of_time timeout - | NONE => "") ^ "..." + quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^ + " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout |> Output.urgent_message else () @@ -961,7 +945,7 @@ if debug then Output.urgent_message "Invoking SMT solver..." else () val (outcome, used_facts) = SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i - |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day) + |> SMT_Solver.smt_filter_apply slice_timeout |> (fn {outcome, used_facts} => (outcome, used_facts)) handle exn => if Exn.is_interrupt exn then reraise exn @@ -979,18 +963,13 @@ | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *) | SOME SMT_Failure.Out_Of_Memory => true | SOME (SMT_Failure.Other_Failure _) => true - val timeout = - Option.map - (fn timeout => Time.- (timeout, Timer.checkRealTimer timer)) - timeout + val timeout = Time.- (timeout, Timer.checkRealTimer timer) in - if too_many_facts_perhaps andalso slice < max_slices andalso - num_facts > 0 andalso - (timeout = NONE orelse Time.> (the timeout, Time.zeroTime)) then + if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso + Time.> (timeout, Time.zeroTime) then let val new_num_facts = - Real.ceil (Config.get ctxt smt_slice_fact_frac - * Real.fromInt num_facts) + Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts) val weighted_factss as (new_fact_filter, _) :: _ = weighted_factss |> rotate_one diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 13:43:21 2013 +0100 @@ -14,8 +14,7 @@ type one_line_params = Sledgehammer_Reconstructor.one_line_params type isar_params = - bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list * - thm + bool * bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string val proof_text : Proof.context -> bool option -> (unit -> isar_params) -> int -> @@ -190,8 +189,7 @@ end type isar_params = - bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list * - thm + bool * bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm val arith_methodss = [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method, @@ -214,7 +212,7 @@ |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes) val one_line_proof = one_line_proof_text 0 one_line_params - val do_preplay = preplay_timeout <> SOME Time.zeroTime + val do_preplay = preplay_timeout <> Time.zeroTime val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev @@ -342,9 +340,6 @@ and isar_proof outer fix assms lems infs = Proof (fix, assms, lems @ isar_steps outer NONE [] infs) - (* 60 seconds seems like a reasonable interpreation of "no timeout" *) - val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) - val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) = refute_graph (* diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Dec 19 13:43:21 2013 +0100 @@ -19,10 +19,9 @@ val timeoutN : string val unknownN : string val string_of_factss : (string * fact list) list -> string - val run_sledgehammer : - params -> mode -> (string -> unit) option -> int -> fact_override - -> ((string * string list) list -> string -> minimize_command) - -> Proof.state -> bool * (string * Proof.state) + val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> + ((string * string list) list -> string -> minimize_command) -> Proof.state -> + bool * (string * Proof.state) end; structure Sledgehammer_Run : SLEDGEHAMMER_RUN = @@ -65,13 +64,13 @@ (if blocking then "." else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) -fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) - mode output_result minimize_command only learn - {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = +fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode + output_result minimize_command only learn + {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = let val ctxt = Proof.context_of state - val hard_timeout = time_mult 3.0 (timeout |> the_default one_day) + val hard_timeout = time_mult 3.0 timeout val _ = spying spy (fn () => (state, subgoal, name, "Launched")); val birth_time = Time.now () val death_time = Time.+ (birth_time, hard_timeout) @@ -173,7 +172,7 @@ in (outcome_code, message) end in if mode = Auto_Try then - let val (outcome_code, message) = time_limit timeout go () in + let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in (outcome_code, state |> outcome_code = someN diff -r 4f6ec8754bf5 -r 10d48c2a3e32 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 19 10:15:12 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 19 13:43:21 2013 +0100 @@ -17,15 +17,13 @@ val infinite_timeout : Time.time val time_mult : real -> Time.time -> Time.time val parse_bool_option : bool -> string -> string -> bool option - val parse_time_option : string -> string -> Time.time option + val parse_time : string -> string -> Time.time val subgoal_count : Proof.state -> int val reserved_isar_keyword_table : unit -> unit Symtab.table - val thms_in_proof : - (string Symtab.table * string Symtab.table) option -> thm -> string list + val thms_in_proof : (string Symtab.table * string Symtab.table) option -> thm -> string list val thms_of_name : Proof.context -> string -> thm list val one_day : Time.time val one_year : Time.time - val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b val hackish_string_of_term : Proof.context -> term -> string val spying : bool -> (unit -> Proof.state * int * string * string) -> unit @@ -86,15 +84,14 @@ val has_junk = exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *) -fun parse_time_option _ "none" = NONE - | parse_time_option name s = - let val secs = if has_junk s then NONE else Real.fromString s in - if is_none secs orelse Real.< (the secs, 0.0) then - error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \ - \number of seconds (e.g., \"60\", \"0.5\") or \"none\".") - else - SOME (seconds (the secs)) - end +fun parse_time name s = + let val secs = if has_junk s then NONE else Real.fromString s in + if is_none secs orelse Real.< (the secs, 0.0) then + error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \ + \number of seconds (e.g., \"60\", \"0.5\") or \"none\".") + else + seconds (the secs) + end val subgoal_count = Try.subgoal_count @@ -144,9 +141,6 @@ val one_day = seconds (24.0 * 60.0 * 60.0) val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0) -fun time_limit NONE = I - | time_limit (SOME delay) = TimeLimit.timeLimit delay - fun with_vanilla_print_mode f x = Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x