--- 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
--- 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
--- 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 =
--- 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 *)
--- 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)
--- 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 ^ ".")
--- 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
--- 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 =
--- 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 =