--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Dec 06 10:52:48 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Dec 06 13:17:26 2010 +0100
@@ -369,7 +369,7 @@
val problem =
{state = st', goal = goal, subgoal = i,
subgoal_count = Sledgehammer_Util.subgoal_count st,
- facts = facts |> map Sledgehammer.Untranslated, only = true}
+ facts = facts |> map Sledgehammer.Untranslated}
val time_limit =
(case hard_timeout of
NONE => I
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Mon Dec 06 10:52:48 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Mon Dec 06 13:17:26 2010 +0100
@@ -43,8 +43,7 @@
(prop_of goal))
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = i,
- facts = map Sledgehammer.Untranslated facts,
- only = true, subgoal_count = n}
+ subgoal_count = n, facts = map Sledgehammer.Untranslated facts}
in
(case prover params (K "") problem of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Mon Dec 06 10:52:48 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Mon Dec 06 13:17:26 2010 +0100
@@ -19,7 +19,7 @@
else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^
quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
"configuration option " ^ quote SMT_Config.traceN ^ " and " ^
- " see the trace for details."))
+ "see the trace for details."))
fun on_first_line test_outcome solver_name lines =
let
@@ -40,7 +40,8 @@
outcome =
on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
cex_parser = NONE,
- reconstruct = NONE }
+ reconstruct = NONE,
+ default_max_relevant = 250 }
(* Yices *)
@@ -53,7 +54,8 @@
interface = SMTLIB_Interface.interface,
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
cex_parser = NONE,
- reconstruct = NONE }
+ reconstruct = NONE,
+ default_max_relevant = 275 }
(* Z3 *)
@@ -85,7 +87,8 @@
interface = Z3_Interface.interface,
outcome = z3_on_last_line,
cex_parser = SOME Z3_Model.parse_counterex,
- reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
+ reconstruct = SOME Z3_Proof_Reconstruction.reconstruct,
+ default_max_relevant = 225 }
(* overall setup *)
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon Dec 06 10:52:48 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Dec 06 13:17:26 2010 +0100
@@ -21,7 +21,8 @@
cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
term list * term list) option,
reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
- (int list * thm) * Proof.context) option }
+ (int list * thm) * Proof.context) option,
+ default_max_relevant: int }
(*registry*)
type solver = bool option -> Proof.context -> (int * thm) list ->
@@ -32,6 +33,7 @@
val available_solvers_of: Proof.context -> string list
val is_locally_installed: Proof.context -> string -> bool
val is_remotely_available: Proof.context -> string -> bool
+ val default_max_relevant: Proof.context -> string -> int
(*filter*)
val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
@@ -70,7 +72,8 @@
cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
term list * term list) option,
reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
- (int list * thm) * Proof.context) option }
+ (int list * thm) * Proof.context) option,
+ default_max_relevant: int }
(* interface to external solvers *)
@@ -215,7 +218,7 @@
fun gen_solver name info rm ctxt irules =
let
- val {env_var, is_remote, options, interface, reconstruct} = info
+ val {env_var, is_remote, options, interface, reconstruct, ...} = info
val {extra_norm, translate} = interface
val (with_datatypes, translate') =
set_has_datatypes (Config.get ctxt C.datatypes) translate
@@ -244,7 +247,8 @@
options: Proof.context -> string list,
interface: interface,
reconstruct: string list * SMT_Translate.recon -> Proof.context ->
- (int list * thm) * Proof.context }
+ (int list * thm) * Proof.context,
+ default_max_relevant: int }
structure Solvers = Generic_Data
(
@@ -279,13 +283,14 @@
fun add_solver cfg =
let
val {name, env_var, is_remote, options, interface, outcome, cex_parser,
- reconstruct} = cfg
+ reconstruct, default_max_relevant} = cfg
fun core_oracle () = cfalse
fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
interface=interface,
- reconstruct=finish (outcome name) cex_parser reconstruct ocl }
+ reconstruct=finish (outcome name) cex_parser reconstruct ocl,
+ default_max_relevant=default_max_relevant }
in
Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
@@ -294,9 +299,12 @@
end
+fun get_info ctxt name =
+ the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
+
fun name_and_solver_of ctxt =
let val name = C.solver_of ctxt
- in (name, the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)) end
+ in (name, get_info ctxt name) end
val solver_name_of = fst o name_and_solver_of
fun solver_of ctxt =
@@ -306,11 +314,12 @@
val available_solvers_of = Symtab.keys o Solvers.get o Context.Proof
fun is_locally_installed ctxt name =
- let val {env_var, ...} = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
+ let val {env_var, ...} = get_info ctxt name
in is_some (get_local_solver env_var) end
-fun is_remotely_available ctxt name =
- #is_remote (the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name))
+val is_remotely_available = #is_remote oo get_info
+
+val default_max_relevant = #default_max_relevant oo get_info
(* filter *)
@@ -347,7 +356,8 @@
(xrules, map snd xrules)
||> distinct (op =) o fst o smt_solver rm ctxt' o append irs o map_index I
|-> map_filter o try o nth
- |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
+ |> (fn xs => {outcome=NONE, used_facts=if solver_name_of ctxt = "z3" (* FIXME *) then xs
+ else xrules, run_time_in_msecs=NONE})
end
handle SMT_Failure.SMT fail => {outcome=SOME fail, used_facts=[],
run_time_in_msecs=NONE}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Dec 06 10:52:48 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Dec 06 13:17:26 2010 +0100
@@ -39,8 +39,7 @@
goal: thm,
subgoal: int,
subgoal_count: int,
- facts: fact list,
- only: bool}
+ facts: fact list}
type prover_result =
{outcome: failure option,
@@ -118,13 +117,15 @@
end
(* FUDGE *)
-val smt_default_max_relevant = 225
val auto_max_relevant_divisor = 2
fun default_max_relevant_for_prover ctxt name =
let val thy = ProofContext.theory_of ctxt in
- if is_smt_prover ctxt name then smt_default_max_relevant
- else #default_max_relevant (get_atp thy name)
+ if is_smt_prover ctxt name then
+ SMT_Solver.default_max_relevant ctxt
+ (perhaps (try (unprefix remote_prefix)) name)
+ else
+ #default_max_relevant (get_atp thy name)
end
(* These are typically simplified away by "Meson.presimplify". Equality is
@@ -222,8 +223,7 @@
goal: thm,
subgoal: int,
subgoal_count: int,
- facts: fact list,
- only: bool}
+ facts: fact list}
type prover_result =
{outcome: failure option,
@@ -285,18 +285,15 @@
fun run_atp auto atp_name
{exec, required_execs, arguments, has_incomplete_mode, proof_delims,
- known_failures, default_max_relevant, explicit_forall,
- use_conjecture_for_hypotheses}
- ({debug, verbose, overlord, full_types, explicit_apply,
- max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
- minimize_command
- ({state, goal, subgoal, facts, only, ...} : prover_problem) =
+ known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
+ ({debug, verbose, overlord, full_types, explicit_apply, isar_proof,
+ isar_shrink_factor, timeout, ...} : params)
+ minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
let
val ctxt = Proof.context_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
val facts =
- facts |> not only ? take (the_default default_max_relevant max_relevant)
- |> map (translated_fact ctxt)
+ facts |> map (translated_fact ctxt)
val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
else Config.get ctxt dest_dir
val problem_prefix = Config.get ctxt problem_prefix
@@ -480,11 +477,7 @@
else
()
val {outcome, used_facts, run_time_in_msecs} =
- TimeLimit.timeLimit iter_timeout
- (SMT_Solver.smt_filter remote iter_timeout state facts) i
- handle TimeLimit.TimeOut =>
- {outcome = SOME SMT_Failure.Time_Out, used_facts = [],
- run_time_in_msecs = NONE}
+ SMT_Solver.smt_filter remote iter_timeout state facts i
val _ =
if verbose andalso is_some outcome then
"SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
@@ -553,9 +546,10 @@
#> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
val state = state |> Proof.map_context repair_context
val thy = Proof.theory_of state
- val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
+ val get_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
+ val facts = facts |> map_filter get_fact
val {outcome, used_facts, run_time_in_msecs} =
- smt_filter_loop params remote state subgoal (map_filter smt_fact facts)
+ smt_filter_loop params remote state subgoal facts
val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
val outcome = outcome |> Option.map failure_from_smt_failure
val message =
@@ -591,19 +585,21 @@
end
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
- auto minimize_command
- (problem as {state, goal, subgoal, subgoal_count, facts, ...})
- name =
+ auto minimize_command only
+ {state, goal, subgoal, subgoal_count, facts} name =
let
val ctxt = Proof.context_of state
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
- val num_facts = Int.min (length facts, max_relevant)
+ val num_facts = length facts |> not only ? Integer.min max_relevant
val desc =
prover_description ctxt params name num_facts subgoal subgoal_count goal
val prover = get_prover ctxt auto name
+ val problem =
+ {state = state, goal = goal, subgoal = subgoal,
+ subgoal_count = subgoal_count, facts = take num_facts facts}
fun go () =
let
fun really_go () =
@@ -616,8 +612,12 @@
else
(really_go ()
handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
- | exn => ("unknown", "Internal error:\n" ^
- ML_Compiler.exn_message exn ^ "\n"))
+ | exn =>
+ if Exn.is_interrupt exn then
+ reraise exn
+ else
+ ("unknown", "Internal error:\n" ^
+ ML_Compiler.exn_message exn ^ "\n"))
val _ =
if expect = "" orelse outcome_code = expect then
()
@@ -686,8 +686,8 @@
|> map maybe_translate
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts, only = only}
- val run_prover = run_prover params auto minimize_command
+ facts = facts}
+ val run_prover = run_prover params auto minimize_command only
in
if debug then
Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Dec 06 10:52:48 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Dec 06 13:17:26 2010 +0100
@@ -2,7 +2,7 @@
Author: Philipp Meyer, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
-Minimization of fact list for Metis using ATPs.
+Minimization of fact list for Metis using external provers.
*)
signature SLEDGEHAMMER_MINIMIZE =
@@ -59,19 +59,27 @@
val {goal, ...} = Proof.goal state
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts, only = true}
+ facts = facts}
val result as {outcome, used_facts, ...} = prover params (K "") problem
in
- Output.urgent_message (case outcome of
- SOME failure => string_for_failure failure
- | NONE =>
- if length used_facts = length facts then "Found proof."
- else "Found proof with " ^ n_facts used_facts ^ ".");
+ Output.urgent_message
+ (case outcome of
+ SOME failure => string_for_failure failure
+ | NONE =>
+ if length used_facts = length facts then "Found proof."
+ else "Found proof with " ^ n_facts used_facts ^ ".");
result
end
(* minimalization of facts *)
+(* The sublinear algorithm works well in almost all situations, except when the
+ external prover cannot return the list of used facts and hence returns all
+ facts as used. In that case, the binary algorithm is much more
+ appropriate. We can usually detect that situation just by looking at the
+ number of used facts reported by the prover. *)
+val binary_threshold = 50
+
fun filter_used_facts used = filter (member (op =) used o fst)
fun sublinear_minimize _ [] p = p
@@ -82,9 +90,35 @@
(filter_used_facts used_facts seen, result)
| _ => sublinear_minimize test xs (x :: seen, result)
-(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
- preprocessing time is included in the estimate below but isn't part of the
- timeout. *)
+fun binary_minimize test xs =
+ let
+ fun p xs = #outcome (test xs : prover_result) = NONE
+ fun split [] p = p
+ | split [h] (l, r) = (h :: l, r)
+ | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
+ fun min _ [] = raise Empty
+ | min _ [s0] = [s0]
+ | min sup xs =
+ let val (l0, r0) = split xs ([], []) in
+ if p (sup @ l0) then
+ min sup l0
+ else if p (sup @ r0) then
+ min sup r0
+ else
+ let
+ val l = min (sup @ r0) l0
+ val r = min (sup @ l) r0
+ in l @ r end
+ end
+ val xs =
+ case min [] xs of
+ [x] => if p [] then [] else [x]
+ | xs => xs
+ in (xs, test xs) end
+
+(* Give the external prover some slack. The ATP gets further slack because the
+ Sledgehammer preprocessing time is included in the estimate below but isn't
+ part of the timeout. *)
val fudge_msecs = 1000
fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set."
@@ -95,7 +129,8 @@
val ctxt = Proof.context_of state
val prover = get_prover ctxt false prover_name
val msecs = Time.toMilliseconds timeout
- val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
+ val _ = Output.urgent_message ("Sledgehammer minimize: " ^
+ quote prover_name ^ ".")
val {goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val explicit_apply =
@@ -112,9 +147,12 @@
val new_timeout =
Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
|> Time.fromMilliseconds
+ val facts = filter_used_facts used_facts facts
val (min_thms, {message, ...}) =
- sublinear_minimize (do_test new_timeout)
- (filter_used_facts used_facts facts) ([], result)
+ if length facts >= binary_threshold then
+ binary_minimize (do_test new_timeout) facts
+ else
+ sublinear_minimize (do_test new_timeout) facts ([], result)
val n = length min_thms
val _ = Output.urgent_message (cat_lines
["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
@@ -132,7 +170,7 @@
\can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
string_of_int (10 + msecs div 1000) ^ "\").")
- | {message, ...} => (NONE, "ATP error: " ^ message))
+ | {message, ...} => (NONE, "Prover error: " ^ message))
handle ERROR msg => (NONE, "Error: " ^ msg)
end