# HG changeset patch # User blanchet # Date 1291637846 -3600 # Node ID ef119e33dc0658bfaad4cf7407262dd5d1d830ae # Parent 8df0a190df1e0d9b80d9d55e773d25e450f92d29# Parent 07526f5466806a849ed3d4c4af17a585e2567f61 merged diff -r 8df0a190df1e -r ef119e33dc06 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r 8df0a190df1e -r ef119e33dc06 src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML --- 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 diff -r 8df0a190df1e -r ef119e33dc06 src/HOL/Tools/SMT/smt_setup_solvers.ML --- 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 *) diff -r 8df0a190df1e -r ef119e33dc06 src/HOL/Tools/SMT/smt_solver.ML --- 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} diff -r 8df0a190df1e -r ef119e33dc06 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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) ^ ": " ^ diff -r 8df0a190df1e -r ef119e33dc06 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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