# HG changeset patch # User blanchet # Date 1303403962 -7200 # Node ID 724e612ba2481d24a263eafb56b0ffcff4fc3619 # Parent 036142bd030239d6c9ebd99c314d19aef492069d implemented general slicing for ATPs, especially E 1.2w and above diff -r 036142bd0302 -r 724e612ba248 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Thu Apr 21 18:39:22 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Apr 21 18:39:22 2011 +0200 @@ -356,7 +356,8 @@ General. For automatic runs, only the first prover set using \textit{provers} (\S\ref{mode-of-operation}) is considered, \textit{verbose} (\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled, -fewer facts are passed to the prover, and \textit{timeout} +fewer facts are passed to the prover, \textit{slicing} +(\S\ref{mode-of-operation}) is disabled, and \textit{timeout} (\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in Proof General's ``Isabelle'' menu. Sledgehammer's output is also more concise. @@ -508,6 +509,21 @@ the putative theorem manually while Sledgehammer looks for a proof, but it can also be more confusing. +\optrue{slicing}{no\_slicing} +Specifies whether the time allocated to a prover should be sliced into several +segments, each of which has its own set of possibly prover-dependent options. +For SPASS and Vampire, the first slice tries the fast-but-incomplete +set-of-support (SOS) strategy, whereas the second slice runs without it. For E, +up to three slices are defined, with different weighted search strategies and +number of facts. For SMT solvers, several slices are tried with the same options +but fewer and fewer facts. According to benchmarks with a timeout of 30 seconds, +slicing is a valuable optimization, and you should probably leave it enabled +unless you are conducting experiments. However, this option is implicitly +disabled for (short) automatic runs. + +\nopagebreak +{\small See also \textit{verbose} (\S\ref{output-format}).} + \opfalse{overlord}{no\_overlord} Specifies whether Sledgehammer should put its temporary files in \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for diff -r 036142bd0302 -r 724e612ba248 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 18:39:22 2011 +0200 @@ -317,13 +317,13 @@ fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) -fun get_prover ctxt args = +fun get_prover ctxt slicing args = let fun default_prover_name () = hd (#provers (Sledgehammer_Isar.default_params ctxt [])) handle Empty => error "No ATP available." fun get_prover name = - (name, Sledgehammer_Run.get_minimizing_prover ctxt false name) + (name, Sledgehammer_Run.get_minimizing_prover ctxt false slicing name) in (case AList.lookup (op =) args proverK of SOME name => get_prover name @@ -362,14 +362,15 @@ st |> Proof.map_context (change_dir dir #> Config.put Sledgehammer_Provers.measure_run_time true) - val params as {type_sys, relevance_thresholds, max_relevant, ...} = + val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} = Sledgehammer_Isar.default_params ctxt [("verbose", "true"), ("type_sys", type_sys), ("max_relevant", max_relevant), ("timeout", string_of_int timeout)] val default_max_relevant = - Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name + Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing + prover_name val is_built_in_const = Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name val relevance_fudge = @@ -428,7 +429,7 @@ val triv_str = if trivial then "[T] " else "" val _ = change_data id inc_sh_calls val _ = if trivial then () else change_data id inc_sh_nontriv_calls - val (prover_name, prover) = get_prover (Proof.context_of st) args + val (prover_name, prover) = get_prover (Proof.context_of st) true args val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart" val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart" val dir = AList.lookup (op =) args keepK @@ -472,7 +473,7 @@ let val ctxt = Proof.context_of st val n0 = length (these (!named_thms)) - val (prover_name, _) = get_prover ctxt args + val (prover_name, _) = get_prover ctxt false args val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart" val timeout = AList.lookup (op =) args minimize_timeoutK diff -r 036142bd0302 -r 724e612ba248 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Apr 21 18:39:22 2011 +0200 @@ -112,16 +112,17 @@ val {context = ctxt, facts, goal} = Proof.goal pre val prover = AList.lookup (op =) args "prover" |> the_default default_prover + val {relevance_thresholds, type_sys, max_relevant, slicing, ...} = + Sledgehammer_Isar.default_params ctxt args val default_max_relevant = - Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover + Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing + prover val is_built_in_const = Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover val relevance_fudge = extract_relevance_fudge args (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover) val relevance_override = {add = [], del = [], only = false} - val {relevance_thresholds, type_sys, max_relevant, ...} = - Sledgehammer_Isar.default_params ctxt args val subgoal = 1 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal val no_dangerous_types = diff -r 036142bd0302 -r 724e612ba248 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Apr 21 18:39:22 2011 +0200 @@ -12,15 +12,15 @@ type atp_config = {exec: string * string, required_execs: (string * string) list, - arguments: bool -> Time.time -> (unit -> (string * real) list) -> string, - has_incomplete_mode: bool, + arguments: int -> Time.time -> (unit -> (string * real) list) -> string, + slices: unit -> (real * (bool * int)) list, proof_delims: (string * string) list, known_failures: (failure * string) list, - default_max_relevant: int, explicit_forall: bool, use_conjecture_for_hypotheses: bool} - datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight + datatype e_weight_method = + E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight (* for experimentation purposes -- do not use in production code *) val e_weight_method : e_weight_method Unsynchronized.ref @@ -40,7 +40,7 @@ val remote_prefix : string val remote_atp : string -> string -> string list -> (string * string) list - -> (failure * string) list -> int -> bool -> string * atp_config + -> (failure * string) list -> (unit -> int) -> bool -> string * atp_config val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config val supported_atps : theory -> string list @@ -59,11 +59,10 @@ type atp_config = {exec: string * string, required_execs: (string * string) list, - arguments: bool -> Time.time -> (unit -> (string * real) list) -> string, - has_incomplete_mode: bool, + arguments: int -> Time.time -> (unit -> (string * real) list) -> string, + slices: unit -> (real * (bool * int)) list, proof_delims: (string * string) list, known_failures: (failure * string) list, - default_max_relevant: int, explicit_forall: bool, use_conjecture_for_hypotheses: bool} @@ -106,9 +105,10 @@ val tstp_proof_delims = ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") -datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight +datatype e_weight_method = + E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight -val e_weight_method = Unsynchronized.ref E_Fun_Weight +val e_weight_method = Unsynchronized.ref E_Slices (* FUDGE *) val e_default_fun_weight = Unsynchronized.ref 20.0 val e_fun_weight_base = Unsynchronized.ref 0.0 @@ -117,44 +117,67 @@ val e_sym_offs_weight_base = Unsynchronized.ref ~20.0 val e_sym_offs_weight_span = Unsynchronized.ref 60.0 -fun e_weight_method_case fw sow = - case !e_weight_method of +fun e_weight_method_case method fw sow = + case method of E_Auto => raise Fail "Unexpected \"E_Auto\"" | E_Fun_Weight => fw | E_Sym_Offset_Weight => sow -fun scaled_e_weight w = - e_weight_method_case (!e_fun_weight_base) (!e_sym_offs_weight_base) - + w * e_weight_method_case (!e_fun_weight_span) (!e_sym_offs_weight_span) +fun scaled_e_weight method w = + w * e_weight_method_case method (!e_fun_weight_span) (!e_sym_offs_weight_span) + + e_weight_method_case method (!e_fun_weight_base) (!e_sym_offs_weight_base) |> Real.ceil |> signed_string_of_int -fun e_weight_arguments weights = - if !e_weight_method = E_Auto orelse - string_ord (getenv "E_VERSION", "1.2w") = LESS then +fun e_weight_arguments method weights = + if method = E_Auto then "-xAutoDev" else "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ \--destructive-er-aggressive --destructive-er --presat-simplify \ \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ - \-H'(4*" ^ e_weight_method_case "FunWeight" "SymOffsetWeight" ^ + \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^ "(SimulateSOS, " ^ - (e_weight_method_case (!e_default_fun_weight) (!e_default_sym_offs_weight) + (e_weight_method_case method (!e_default_fun_weight) + (!e_default_sym_offs_weight) |> Real.ceil |> signed_string_of_int) ^ ",20,1.5,1.5,1" ^ - (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight w) + (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight method w) |> implode) ^ "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ \FIFOWeight(PreferProcessed))'" +fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS) + +fun effective_e_weight_method () = + if is_old_e_version () then E_Auto else !e_weight_method + +(* The order here must correspond to the order in "e_config" below. *) +fun method_for_slice slice = + case effective_e_weight_method () of + E_Slices => (case slice of + 0 => E_Sym_Offset_Weight + | 1 => E_Auto + | 2 => E_Fun_Weight + | _ => raise Fail "no such slice") + | method => method + val e_config : atp_config = {exec = ("E_HOME", "eproof"), required_execs = [], - arguments = fn _ => fn timeout => fn weights => - "--tstp-in --tstp-out -l5 " ^ e_weight_arguments weights ^ " -tAutoDev \ - \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout), - has_incomplete_mode = false, + arguments = fn slice => fn timeout => fn weights => + "--tstp-in --tstp-out -l5 " ^ + e_weight_arguments (method_for_slice slice) weights ^ + " -tAutoDev --silent --cpu-limit=" ^ + string_of_int (to_secs (e_bonus ()) timeout), + slices = fn () => + if effective_e_weight_method () = E_Slices then + [(0.33333, (true, 100 (* FUDGE *))) (* E_Sym_Offset_Weight *), + (0.33333, (true, 1000 (* FUDGE *))) (* E_Auto *), + (0.33334, (true, 200 (* FUDGE *))) (* E_Fun_Weight *)] + else + [(1.0, (true, 250 (* FUDGE *)))], proof_delims = [tstp_proof_delims], known_failures = [(Unprovable, "SZS status: CounterSatisfiable"), @@ -165,7 +188,6 @@ "# Cannot determine problem status within resource limit"), (OutOfResources, "SZS status: ResourceOut"), (OutOfResources, "SZS status ResourceOut")], - default_max_relevant = 250 (* FUDGE *), explicit_forall = false, use_conjecture_for_hypotheses = true} @@ -179,11 +201,12 @@ val spass_config : atp_config = {exec = ("ISABELLE_ATP", "scripts/spass"), required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], - arguments = fn complete => fn timeout => fn _ => + arguments = fn slice => fn timeout => fn _ => ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout)) - |> not complete ? prefix "-SOS=1 ", - has_incomplete_mode = true, + |> slice = 0 ? prefix "-SOS=1 ", + slices = K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *), + (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)], proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = known_perl_failures @ @@ -194,7 +217,6 @@ (MalformedInput, "Free Variable"), (SpassTooOld, "tptp2dfg"), (InternalError, "Please report this error")], - default_max_relevant = 150 (* FUDGE *), explicit_forall = true, use_conjecture_for_hypotheses = true} @@ -206,12 +228,13 @@ val vampire_config : atp_config = {exec = ("VAMPIRE_HOME", "vampire"), required_execs = [], - arguments = fn complete => fn timeout => fn _ => + arguments = fn slice => fn timeout => fn _ => (* This would work too but it's less tested: "--proof tptp " ^ *) "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^ " --thanks \"Andrei and Krystof\" --input_file" - |> not complete ? prefix "--sos on ", - has_incomplete_mode = true, + |> slice = 0 ? prefix "--sos on ", + slices = K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *), + (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)], proof_delims = [("=========== Refutation ==========", "======= End of refutation ======="), @@ -227,7 +250,6 @@ (Unprovable, "Termination reason: Satisfiable"), (VampireTooOld, "not a valid option"), (Interrupted, "Aborted by signal SIGINT")], - default_max_relevant = 450 (* FUDGE *), explicit_forall = false, use_conjecture_for_hypotheses = true} @@ -241,13 +263,14 @@ required_execs = [], arguments = fn _ => fn timeout => fn _ => "MBQI=true -p -t:" ^ string_of_int (to_secs 0 timeout), - has_incomplete_mode = false, + slices = K [(1.0, (false, 250 (* FUDGE *)))], proof_delims = [], known_failures = [(Unprovable, "\nsat"), (IncompleteUnprovable, "\nunknown"), - (ProofMissing, "\nunsat")], - default_max_relevant = 225 (* FUDGE *), + (IncompleteUnprovable, "SZS status Satisfiable"), + (ProofMissing, "\nunsat"), + (ProofMissing, "SZS status Unsatisfiable")], explicit_forall = true, use_conjecture_for_hypotheses = false} @@ -293,20 +316,21 @@ arguments = fn _ => fn timeout => fn _ => " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout))) ^ " -s " ^ the_system system_name system_versions, - has_incomplete_mode = false, + slices = fn () => [(1.0, (false, default_max_relevant ()))], proof_delims = insert (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_perl_failures @ [(TimedOut, "says Timeout")], - default_max_relevant = default_max_relevant, explicit_forall = true, use_conjecture_for_hypotheses = use_conjecture_for_hypotheses} +fun int_average f xs = fold (Integer.add o f) xs 0 div length xs + fun remotify_config system_name system_versions - ({proof_delims, known_failures, default_max_relevant, - use_conjecture_for_hypotheses, ...} : atp_config) : atp_config = + ({proof_delims, slices, known_failures, use_conjecture_for_hypotheses, + ...} : atp_config) : atp_config = remote_config system_name system_versions proof_delims known_failures - default_max_relevant use_conjecture_for_hypotheses + (int_average (snd o snd) o slices) use_conjecture_for_hypotheses fun remote_atp name system_name system_versions proof_delims known_failures default_max_relevant use_conjecture_for_hypotheses = @@ -318,17 +342,13 @@ val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] -val remote_z3_atp = - remote_atp z3_atpN "Z3---" ["2.18"] [] - [(IncompleteUnprovable, "SZS status Satisfiable"), - (ProofMissing, "SZS status Unsatisfiable")] - 225 (* FUDGE *) false +val remote_z3_atp = remotify_atp z3_atp "Z3---" ["2.18"] val remote_sine_e = remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")] - 500 (* FUDGE *) true + (K 500 (* FUDGE *)) true val remote_snark = remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] [] - 250 (* FUDGE *) true + (K 250 (* FUDGE *)) true (* Setup *) diff -r 036142bd0302 -r 724e612ba248 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Apr 21 18:39:22 2011 +0200 @@ -86,7 +86,8 @@ ("type_sys", "smart"), ("explicit_apply", "false"), ("isar_proof", "false"), - ("isar_shrink_factor", "1")] + ("isar_shrink_factor", "1"), + ("slicing", "true")] val alias_params = [("prover", "provers"), @@ -100,7 +101,8 @@ ("dont_monomorphize", "monomorphize"), ("partial_types", "full_types"), ("implicit_apply", "explicit_apply"), - ("no_isar_proof", "isar_proof")] + ("no_isar_proof", "isar_proof"), + ("no_slicing", "slicing")] val params_for_minimize = ["debug", "verbose", "overlord", "type_sys", "full_types", "isar_proof", @@ -252,6 +254,7 @@ val explicit_apply = lookup_bool "explicit_apply" val isar_proof = lookup_bool "isar_proof" val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") + val slicing = lookup_bool "slicing" val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout val expect = lookup_string "expect" in @@ -260,8 +263,8 @@ max_relevant = max_relevant, monomorphize = monomorphize, monomorphize_limit = monomorphize_limit, type_sys = type_sys, explicit_apply = explicit_apply, isar_proof = isar_proof, - isar_shrink_factor = isar_shrink_factor, timeout = timeout, - expect = expect} + isar_shrink_factor = isar_shrink_factor, slicing = slicing, + timeout = timeout, expect = expect} end fun get_params auto ctxt = extract_params auto (default_raw_params ctxt) @@ -300,7 +303,7 @@ in if subcommand = runN then let val i = the_default 1 opt_i in - run_sledgehammer (get_params false ctxt override_params) false i + run_sledgehammer (get_params false ctxt override_params) false true i relevance_override (minimize_command override_params i) state |> K () @@ -373,8 +376,8 @@ fun auto_sledgehammer state = let val ctxt = Proof.context_of state in - run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override - (minimize_command [] 1) state + run_sledgehammer (get_params true ctxt []) true false 1 + no_relevance_override (minimize_command [] 1) state end val setup = Auto_Tools.register_tool (auto, auto_sledgehammer) diff -r 036142bd0302 -r 724e612ba248 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Apr 21 18:39:22 2011 +0200 @@ -67,7 +67,7 @@ relevance_thresholds = (1.01, 1.01), max_relevant = NONE, monomorphize = false, monomorphize_limit = monomorphize_limit, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, - timeout = timeout, expect = ""} + slicing = false, timeout = timeout, expect = ""} val facts = facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) val problem = @@ -147,7 +147,7 @@ silent i n state facts = let val ctxt = Proof.context_of state - val prover = get_prover ctxt false prover_name + val prover = get_prover ctxt false false prover_name val msecs = Time.toMilliseconds timeout val _ = print silent (fn () => "Sledgehammer minimize: " ^ quote prover_name ^ ".") diff -r 036142bd0302 -r 724e612ba248 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 18:39:22 2011 +0200 @@ -29,6 +29,7 @@ explicit_apply: bool, isar_proof: bool, isar_shrink_factor: int, + slicing: bool, timeout: Time.time, expect: string} @@ -55,8 +56,6 @@ type prover = params -> minimize_command -> prover_problem -> prover_result (* for experimentation purposes -- do not use in production code *) - val atp_run_twice_threshold : int Unsynchronized.ref - val atp_first_iter_time_frac : real Unsynchronized.ref val smt_triggers : bool Unsynchronized.ref val smt_weights : bool Unsynchronized.ref val smt_weight_min_facts : int Unsynchronized.ref @@ -64,17 +63,17 @@ val smt_max_weight : int Unsynchronized.ref val smt_max_weight_index : int Unsynchronized.ref val smt_weight_curve : (int -> int) Unsynchronized.ref - val smt_max_iters : int Unsynchronized.ref - val smt_iter_fact_frac : real Unsynchronized.ref - val smt_iter_time_frac : real Unsynchronized.ref - val smt_iter_min_msecs : int Unsynchronized.ref + val smt_max_slices : int Unsynchronized.ref + val smt_slice_fact_frac : real Unsynchronized.ref + val smt_slice_time_frac : real Unsynchronized.ref + val smt_slice_min_secs : int Unsynchronized.ref val das_Tool : string val select_smt_solver : string -> Proof.context -> Proof.context val is_smt_prover : Proof.context -> string -> bool val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool - val default_max_relevant_for_prover : Proof.context -> string -> int + val default_max_relevant_for_prover : Proof.context -> bool -> string -> int val is_built_in_const_for_prover : Proof.context -> string -> string * typ -> term list -> bool * term list val atp_relevance_fudge : relevance_fudge @@ -94,7 +93,7 @@ val kill_provers : unit -> unit val running_provers : unit -> unit val messages : int option -> unit - val get_prover : Proof.context -> bool -> string -> prover + val get_prover : Proof.context -> bool -> bool -> string -> prover val setup : theory -> theory end; @@ -130,12 +129,17 @@ fun is_prover_installed ctxt = is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) -fun default_max_relevant_for_prover ctxt name = +fun get_slices slicing slices = + (0 upto length slices - 1) ~~ slices + |> not slicing ? (List.last #> single) + +fun default_max_relevant_for_prover ctxt slicing name = let val thy = Proof_Context.theory_of ctxt in if is_smt_prover ctxt name then SMT_Solver.default_max_relevant ctxt name else - #default_max_relevant (get_atp thy name) + fold (Integer.max o snd o snd o snd) + (get_slices slicing (#slices (get_atp thy name) ())) 0 end (* These are either simplified away by "Meson.presimplify" (most of the time) or @@ -238,6 +242,7 @@ explicit_apply: bool, isar_proof: bool, isar_shrink_factor: int, + slicing: bool, timeout: Time.time, expect: string} @@ -325,25 +330,22 @@ fun int_opt_add (SOME m) (SOME n) = SOME (m + n) | int_opt_add _ _ = NONE -val atp_run_twice_threshold = Unsynchronized.ref 50 -val atp_first_iter_time_frac = Unsynchronized.ref 0.67 - (* Important messages are important but not so important that users want to see them each time. *) -val important_message_keep_factor = 0.1 +val atp_important_message_keep_factor = 0.1 -fun run_atp auto name - ({exec, required_execs, arguments, has_incomplete_mode, proof_delims, - known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} - : atp_config) - ({debug, verbose, overlord, monomorphize, monomorphize_limit, type_sys, - explicit_apply, isar_proof, isar_shrink_factor, timeout, ...} - : params) +fun run_atp auto may_slice name + ({exec, required_execs, arguments, slices, proof_delims, known_failures, + explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config) + ({debug, verbose, overlord, max_relevant, monomorphize, + monomorphize_limit, type_sys, explicit_apply, isar_proof, + isar_shrink_factor, slicing, timeout, ...} : params) minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal + val slicing = may_slice andalso slicing fun monomorphize_facts facts = let val repair_context = @@ -400,27 +402,55 @@ if File.exists command then let val readable_names = debug andalso overlord - val (atp_problem, pool, conjecture_offset, fact_names) = - prepare_atp_problem ctxt readable_names explicit_forall type_sys - explicit_apply hyp_ts concl_t facts - val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses - atp_problem - val _ = File.write_list prob_file ss - val conjecture_shape = - conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 - |> map single - fun run complete timeout = + (* If slicing is disabled, we expand the last slice to fill the + entire time available. *) + val actual_slices = get_slices slicing (slices ()) + val num_actual_slices = length actual_slices + fun run_slice (slice, (time_frac, (complete, default_max_relevant))) + time_left = let + val num_facts = + length facts |> is_none max_relevant + ? Integer.min default_max_relevant + val real_ms = Real.fromInt o Time.toMilliseconds + val slice_timeout = + ((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 _ = + if verbose then + "ATP slice " ^ string_of_int (slice + 1) ^ " with " ^ + string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ + " for " ^ string_from_time slice_timeout ^ "..." + |> Output.urgent_message + else + () + val (atp_problem, pool, conjecture_offset, fact_names) = + prepare_atp_problem ctxt readable_names explicit_forall + type_sys explicit_apply hyp_ts concl_t + (facts |> take num_facts) fun weights () = atp_problem_weights atp_problem val core = File.shell_path command ^ " " ^ - arguments complete timeout weights ^ " " ^ + arguments slice slice_timeout weights ^ " " ^ File.shell_path prob_file val command = (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }" else "exec " ^ core) ^ " 2>&1" + val _ = + atp_problem + |> tptp_strings_for_atp_problem use_conjecture_for_hypotheses + |> cons ("% " ^ command ^ "\n") + |> File.write_list prob_file + val conjecture_shape = + conjecture_offset + 1 + upto conjecture_offset + length hyp_ts + 1 + |> map single val ((output, msecs), res_code) = bash_output command |>> (if overlord then @@ -431,26 +461,22 @@ val (tstplike_proof, outcome) = extract_tstplike_proof_and_outcome debug verbose complete res_code proof_delims known_failures output - in (output, msecs, tstplike_proof, outcome) end - val run_twice = - has_incomplete_mode andalso not auto andalso - length facts >= !atp_run_twice_threshold + in + ((pool, conjecture_shape, fact_names), + (output, msecs, tstplike_proof, outcome)) + end val timer = Timer.startRealTimer () - val result = - run (not run_twice) - (if run_twice then - seconds (0.001 * !atp_first_iter_time_frac - * Real.fromInt (Time.toMilliseconds timeout)) - else - timeout) - |> run_twice - ? (fn (_, msecs0, _, SOME _) => - run true (Time.- (timeout, Timer.checkRealTimer timer)) - |> (fn (output, msecs, tstplike_proof, outcome) => - (output, int_opt_add msecs0 msecs, tstplike_proof, - outcome)) - | result => result) - in ((pool, conjecture_shape, fact_names), result) end + fun maybe_run_slice slice (_, (_, msecs0, _, SOME _)) = + run_slice slice (Time.- (timeout, Timer.checkRealTimer timer)) + |> (fn (stuff, (output, msecs, tstplike_proof, outcome)) => + (stuff, (output, int_opt_add msecs0 msecs, + tstplike_proof, outcome))) + | maybe_run_slice _ result = result + in + ((Symtab.empty, [], Vector.fromList []), + ("", SOME 0, "", SOME InternalError)) + |> fold maybe_run_slice actual_slices + end else error ("Bad executable: " ^ Path.print command ^ ".") @@ -469,7 +495,7 @@ val (conjecture_shape, fact_names) = repair_conjecture_shape_and_fact_names output conjecture_shape fact_names val important_message = - if not auto andalso random () <= important_message_keep_factor then + if not auto andalso random () <= atp_important_message_keep_factor then extract_important_message output else "" @@ -535,16 +561,19 @@ UnknownError msg (* FUDGE *) -val smt_max_iters = Unsynchronized.ref 8 -val smt_iter_fact_frac = Unsynchronized.ref 0.5 -val smt_iter_time_frac = Unsynchronized.ref 0.5 -val smt_iter_min_msecs = Unsynchronized.ref 5000 +val smt_max_slices = Unsynchronized.ref 8 +val smt_slice_fact_frac = Unsynchronized.ref 0.5 +val smt_slice_time_frac = Unsynchronized.ref 0.5 +val smt_slice_min_secs = Unsynchronized.ref 5 -fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit, - timeout, ...} : params) +fun smt_filter_loop may_slice name + ({debug, verbose, overlord, monomorphize_limit, timeout, + slicing, ...} : params) state i smt_filter = let val ctxt = Proof.context_of state + val slicing = may_slice andalso slicing + val max_slices = if slicing then !smt_max_slices else 1 val repair_context = select_smt_solver name #> Config.put SMT_Config.verbose debug @@ -559,23 +588,24 @@ #> Config.put SMT_Config.monomorph_limit monomorphize_limit val state = state |> Proof.map_context repair_context - fun iter timeout iter_num outcome0 time_so_far facts = + fun do_slice timeout slice outcome0 time_so_far facts = let val timer = Timer.startRealTimer () val ms = timeout |> Time.toMilliseconds - val iter_timeout = - if iter_num < !smt_max_iters then + val slice_timeout = + if slice < max_slices then Int.min (ms, - Int.max (!smt_iter_min_msecs, - Real.ceil (!smt_iter_time_frac * Real.fromInt ms))) + Int.max (1000 * !smt_slice_min_secs, + Real.ceil (!smt_slice_time_frac * Real.fromInt ms))) |> Time.fromMilliseconds else timeout val num_facts = length facts val _ = if verbose then - "SMT iteration with " ^ string_of_int num_facts ^ " fact" ^ - plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..." + "SMT slice with " ^ string_of_int num_facts ^ " fact" ^ + plural_s num_facts ^ " for " ^ string_from_time slice_timeout ^ + "..." |> Output.urgent_message else () @@ -583,10 +613,10 @@ val _ = if debug then Output.urgent_message "Invoking SMT solver..." else () val (outcome, used_facts) = - (case (iter_num, smt_filter) of + (case (slice, smt_filter) of (1, SOME head) => head |> apsnd (apsnd repair_context) | _ => SMT_Solver.smt_filter_preprocess state facts i) - |> SMT_Solver.smt_filter_apply iter_timeout + |> SMT_Solver.smt_filter_apply slice_timeout |> (fn {outcome, used_facts} => (outcome, used_facts)) handle exn => if Exn.is_interrupt exn then reraise exn @@ -608,7 +638,7 @@ case outcome of NONE => false | SOME (SMT_Failure.Counterexample _) => false - | SOME SMT_Failure.Time_Out => iter_timeout <> timeout + | SOME SMT_Failure.Time_Out => slice_timeout <> timeout | SOME (SMT_Failure.Abnormal_Termination code) => (if verbose then "The SMT solver invoked with " ^ string_of_int num_facts ^ @@ -622,17 +652,19 @@ | SOME (SMT_Failure.Other_Failure _) => true val timeout = Time.- (timeout, Timer.checkRealTimer timer) in - if too_many_facts_perhaps andalso iter_num < !smt_max_iters andalso + if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then let - val n = Real.ceil (!smt_iter_fact_frac * Real.fromInt num_facts) - in iter timeout (iter_num + 1) outcome0 time_so_far (take n facts) end + val n = Real.ceil (!smt_slice_fact_frac * Real.fromInt num_facts) + in + do_slice timeout (slice + 1) outcome0 time_so_far (take n facts) + end else {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts, run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)} end - in iter timeout 1 NONE Time.zeroTime end + in do_slice timeout 1 NONE Time.zeroTime end (* taken from "Mirabelle" and generalized *) fun can_apply timeout tac state i = @@ -652,9 +684,10 @@ (Config.put Metis_Tactics.verbose debug #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i -fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command - ({state, subgoal, subgoal_count, facts, smt_filter, ...} - : prover_problem) = +fun run_smt_solver auto may_slice name (params as {debug, verbose, ...}) + minimize_command + ({state, subgoal, subgoal_count, facts, smt_filter, ...} + : prover_problem) = let val ctxt = Proof.context_of state val thy = Proof.theory_of state @@ -662,7 +695,7 @@ val facts = facts ~~ (0 upto num_facts - 1) |> map (smt_weighted_fact thy num_facts) val {outcome, used_facts, run_time_in_msecs} = - smt_filter_loop name params state subgoal smt_filter facts + smt_filter_loop may_slice name params state subgoal smt_filter facts val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) val outcome = outcome |> Option.map failure_from_smt_failure val message = @@ -694,12 +727,12 @@ run_time_in_msecs = run_time_in_msecs, message = message} end -fun get_prover ctxt auto name = +fun get_prover ctxt auto may_slice name = let val thy = Proof_Context.theory_of ctxt in if is_smt_prover ctxt name then - run_smt_solver auto name + run_smt_solver auto may_slice name else if member (op =) (supported_atps thy) name then - run_atp auto name (get_atp thy name) + run_atp auto may_slice name (get_atp thy name) else error ("No such prover: " ^ name ^ ".") end diff -r 036142bd0302 -r 724e612ba248 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Apr 21 18:39:22 2011 +0200 @@ -14,10 +14,10 @@ type prover = Sledgehammer_Provers.prover val auto_minimize_min_facts : int Unsynchronized.ref - val get_minimizing_prover : Proof.context -> bool -> string -> prover + val get_minimizing_prover : Proof.context -> bool -> bool -> string -> prover val run_sledgehammer : - params -> bool -> int -> relevance_override -> (string -> minimize_command) - -> Proof.state -> bool * Proof.state + params -> bool -> bool -> int -> relevance_override + -> (string -> minimize_command) -> Proof.state -> bool * Proof.state end; structure Sledgehammer_Run : SLEDGEHAMMER_RUN = @@ -44,10 +44,10 @@ val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts) -fun get_minimizing_prover ctxt auto name +fun get_minimizing_prover ctxt auto may_slice name (params as {debug, verbose, explicit_apply, ...}) minimize_command (problem as {state, subgoal, subgoal_count, facts, ...}) = - get_prover ctxt auto name params minimize_command problem + get_prover ctxt auto may_slice name params minimize_command problem |> (fn result as {outcome, used_facts, run_time_in_msecs, message} => if is_some outcome then result @@ -83,16 +83,18 @@ | NONE => result end) -fun launch_prover - (params as {debug, blocking, max_relevant, timeout, expect, ...}) - auto minimize_command only +fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout, + expect, ...}) + auto may_slice minimize_command only {state, goal, subgoal, subgoal_count, facts, smt_filter} name = let val ctxt = Proof.context_of state + val slicing = may_slice andalso slicing val birth_time = Time.now () val death_time = Time.+ (birth_time, timeout) val max_relevant = - the_default (default_max_relevant_for_prover ctxt name) max_relevant + max_relevant + |> the_default (default_max_relevant_for_prover ctxt slicing name) val num_facts = length facts |> not only ? Integer.min max_relevant val desc = prover_description ctxt params name num_facts subgoal subgoal_count goal @@ -102,7 +104,8 @@ smt_filter = smt_filter} fun really_go () = problem - |> get_minimizing_prover ctxt auto name params (minimize_command name) + |> get_minimizing_prover ctxt auto may_slice name params + (minimize_command name) |> (fn {outcome, message, ...} => (if is_some outcome then "none" else "some" (* sic *), message)) fun go () = @@ -166,9 +169,9 @@ fun run_sledgehammer (params as {debug, blocking, provers, monomorphize, type_sys, relevance_thresholds, max_relevant, - timeout, ...}) - auto i (relevance_override as {only, ...}) minimize_command - state = + slicing, timeout, ...}) + auto may_slice i (relevance_override as {only, ...}) + minimize_command state = if null provers then error "No prover is set." else case subgoal_count state of @@ -181,6 +184,7 @@ state |> Proof.map_context (Config.put SMT_Config.verbose debug) val ctxt = Proof.context_of state val thy = Proof_Context.theory_of ctxt + val slicing = may_slice andalso slicing val {facts = chained_ths, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i val no_dangerous_types = types_dangerous_types type_sys @@ -201,7 +205,7 @@ facts = facts, smt_filter = maybe_smt_filter (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} - val launch = launch_prover params auto minimize_command only + val launch = launch_prover params auto may_slice minimize_command only in if auto then fold (fn prover => fn (true, state) => (true, state) @@ -218,7 +222,8 @@ case max_relevant of SOME n => n | NONE => - 0 |> fold (Integer.max o default_max_relevant_for_prover ctxt) + 0 |> fold (Integer.max + o default_max_relevant_for_prover ctxt slicing) provers |> auto ? (fn n => n div auto_max_relevant_divisor) val is_built_in_const = diff -r 036142bd0302 -r 724e612ba248 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 21 18:39:22 2011 +0200 @@ -18,14 +18,14 @@ fun run_atp force_full_types timeout i n ctxt goal name = let val chained_ths = [] (* a tactic has no chained ths *) - val params as {type_sys, relevance_thresholds, max_relevant, ...} = + val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} = ((if force_full_types then [("full_types", "true")] else []) @ [("timeout", string_of_int (Time.toSeconds timeout))]) (* @ [("overlord", "true")] *) |> Sledgehammer_Isar.default_params ctxt - val prover = Sledgehammer_Provers.get_prover ctxt false name + val prover = Sledgehammer_Provers.get_prover ctxt false true name val default_max_relevant = - Sledgehammer_Provers.default_max_relevant_for_prover ctxt name + Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name val is_built_in_const = Sledgehammer_Provers.is_built_in_const_for_prover ctxt name val relevance_fudge =