# HG changeset patch # User blanchet # Date 1292600731 -3600 # Node ID 7c05c8301d7e22c2b6479cefab2d932977ef6457 # Parent 975db7bd23e3d4dbf5b31463ec9a7d4e4b7ec313# Parent 15ba335d0ba2f7c56aa870e4325f44e9fdade16b merged diff -r 975db7bd23e3 -r 7c05c8301d7e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Dec 17 15:30:00 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Dec 17 16:45:31 2010 +0100 @@ -376,7 +376,8 @@ val problem = {state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, - facts = facts |> map Sledgehammer_Provers.Untranslated_Fact} + facts = facts |> map Sledgehammer_Provers.Untranslated_Fact, + smt_head = NONE} val time_limit = (case hard_timeout of NONE => I diff -r 975db7bd23e3 -r 7c05c8301d7e src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Fri Dec 17 15:30:00 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Fri Dec 17 16:45:31 2010 +0100 @@ -47,7 +47,8 @@ (prop_of goal)) val problem = {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - facts = map Sledgehammer_Provers.Untranslated_Fact facts} + facts = map Sledgehammer_Provers.Untranslated_Fact facts, + smt_head = NONE} in (case prover params (K "") problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME diff -r 975db7bd23e3 -r 7c05c8301d7e src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Dec 17 15:30:00 2010 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Dec 17 16:45:31 2010 +0100 @@ -243,7 +243,7 @@ val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] val remote_sine_e = remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")] - 800 (* FUDGE *) true + 600 (* FUDGE *) true val remote_snark = remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] [] 250 (* FUDGE *) true diff -r 975db7bd23e3 -r 7c05c8301d7e src/HOL/Tools/SMT/lib/scripts/z3_wrapper --- a/src/HOL/Tools/SMT/lib/scripts/z3_wrapper Fri Dec 17 15:30:00 2010 +0100 +++ b/src/HOL/Tools/SMT/lib/scripts/z3_wrapper Fri Dec 17 16:45:31 2010 +0100 @@ -29,7 +29,7 @@ print STDERR join("", @err_lines); if ($code != 0) { - foreach my $err_line (@err_lines) { + foreach my $err_line (reverse(@err_lines)) { if ($err_line =~ /[lL]ine ([0-9]+)/) { my $line_num = $1; diff -r 975db7bd23e3 -r 7c05c8301d7e src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Fri Dec 17 15:30:00 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Dec 17 16:45:31 2010 +0100 @@ -33,10 +33,12 @@ val default_max_relevant: Proof.context -> string -> int (*filter*) - val smt_filter: bool -> Time.time -> Proof.state -> - ('a * (int option * thm)) list -> int -> - {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list, - run_time_in_msecs: int option} + type 'a smt_filter_head_result = ('a list * (int option * thm) list) * + (((int * thm) list * Proof.context) * (int * (int option * thm)) list) + val smt_filter_head: Proof.state -> + ('a * (int option * thm)) list -> int -> 'a smt_filter_head_result + val smt_filter_tail: Time.time -> bool -> 'a smt_filter_head_result -> + {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list} (*tactic*) val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic @@ -212,16 +214,19 @@ int list * thm, default_max_relevant: int } -fun gen_solver name (info : solver_info) rm ctxt iwthms = +fun gen_solver_head ctxt iwthms = + SMT_Normalize.normalize ctxt iwthms + |> rpair ctxt + |-> SMT_Monomorph.monomorph + +fun gen_solver_tail (name, info : solver_info) rm (iwthms', ctxt) iwthms = let val {env_var, is_remote, options, reconstruct, ...} = info val cmd = (rm, env_var, is_remote, name) in - SMT_Normalize.normalize ctxt iwthms - |> rpair ctxt - |-> SMT_Monomorph.monomorph - |> (fn (iwthms', ctxt') => invoke name cmd options iwthms' ctxt' - |> reconstruct ctxt') + (iwthms', ctxt) + |-> invoke name cmd options + |> reconstruct ctxt |> (fn (idxs, thm) => thm |> tap (fn _ => trace_assumptions ctxt iwthms idxs) |> pair idxs) @@ -284,9 +289,8 @@ in (name, get_info ctxt name) end val solver_name_of = fst o name_and_solver_of -fun solver_of ctxt = - let val (name, raw_solver) = name_and_solver_of ctxt - in gen_solver name raw_solver end +fun solver_of ctxt rm ctxt' = + `(gen_solver_head ctxt') #-> gen_solver_tail (name_and_solver_of ctxt) rm val available_solvers_of = Symtab.keys o Solvers.get o Context.Proof @@ -306,24 +310,26 @@ | TVar (_, []) => true | _ => false)) -fun smt_solver rm ctxt iwthms = - (* without this test, we would run into problems when atomizing the rules: *) +(* without this test, we would run into problems when atomizing the rules: *) +fun check_topsort iwthms = if exists (has_topsort o Thm.prop_of o snd o snd) iwthms then raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^ "contains the universal sort {}")) - else solver_of ctxt rm ctxt iwthms + else + () val cnot = Thm.cterm_of @{theory} @{const Not} -fun mk_result outcome xrules = - { outcome = outcome, used_facts = xrules, run_time_in_msecs = NONE } +fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules } -fun smt_filter run_remote time_limit st xwrules i = +type 'a smt_filter_head_result = ('a list * (int option * thm) list) * + (((int * thm) list * Proof.context) * (int * (int option * thm)) list) + +fun smt_filter_head st xwrules i = let val ctxt = Proof.context_of st |> Config.put C.oracle false - |> Config.put C.timeout (Time.toReal time_limit) |> Config.put C.drop_bad_facts true |> Config.put C.filter_only_facts true @@ -333,20 +339,29 @@ val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl)) val (xs, wthms) = split_list xwrules + in + ((xs, wthms), + wthms + |> map_index I + |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) + |> tap check_topsort + |> `(gen_solver_head ctxt')) + end + +fun smt_filter_tail time_limit run_remote + ((xs, wthms), ((iwthms', ctxt), iwthms)) = + let + val ctxt = ctxt |> Config.put C.timeout (Time.toReal time_limit) val xrules = xs ~~ map snd wthms in - wthms - |> map_index I - |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) - |> smt_solver (SOME run_remote) ctxt' + ((iwthms', ctxt), iwthms) + |-> gen_solver_tail (name_and_solver_of ctxt) (SOME run_remote) |> distinct (op =) o fst |> map_filter (try (nth xrules)) |> (if solver_name_of ctxt = "z3" (* FIXME *) then I else K xrules) |> mk_result NONE end handle SMT_Failure.SMT fail => mk_result (SOME fail) [] - (* FIXME: measure runtime *) - (* SMT tactic *) @@ -356,7 +371,7 @@ THEN' Tactic.rtac @{thm ccontr} THEN' SUBPROOF (fn {context=ctxt', prems, ...} => let - fun solve iwthms = snd (smt_solver NONE ctxt' iwthms) + val solve = snd o solver_of ctxt' NONE ctxt' o tap check_topsort val tag = "Solver " ^ C.solver_of ctxt' ^ ": " val str_of = prefix tag o SMT_Failure.string_of_failure ctxt' fun safe_solve iwthms = diff -r 975db7bd23e3 -r 7c05c8301d7e src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Dec 17 15:30:00 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Dec 17 16:45:31 2010 +0100 @@ -64,7 +64,7 @@ val {goal, ...} = Proof.goal state val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - facts = facts} + facts = facts, smt_head = NONE} val result as {outcome, used_facts, ...} = prover params (K "") problem in print silent diff -r 975db7bd23e3 -r 7c05c8301d7e src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 17 15:30:00 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 17 16:45:31 2010 +0100 @@ -33,14 +33,16 @@ datatype prover_fact = Untranslated_Fact of (string * locality) * thm | ATP_Translated_Fact of - translated_formula option * ((string * locality) * thm) + translated_formula option * ((string * locality) * thm) | + SMT_Weighted_Fact of (string * locality) * (int option * thm) type prover_problem = {state: Proof.state, goal: thm, subgoal: int, subgoal_count: int, - facts: prover_fact list} + facts: prover_fact list, + smt_head: (string * locality) SMT_Solver.smt_filter_head_result option} type prover_result = {outcome: failure option, @@ -56,13 +58,9 @@ val smt_iter_time_frac : real Unsynchronized.ref val smt_iter_min_msecs : int Unsynchronized.ref val smt_monomorph_limit : int Unsynchronized.ref - val smt_weights : bool Unsynchronized.ref - val smt_min_weight : int Unsynchronized.ref - val smt_max_weight : int Unsynchronized.ref - val smt_max_index : int Unsynchronized.ref - val smt_weight_curve : (int -> 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_available : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool @@ -76,6 +74,8 @@ val problem_prefix : string Config.T val measure_run_time : bool Config.T val untranslated_fact : prover_fact -> (string * locality) * thm + val smt_weighted_fact : + prover_fact -> (string * locality) * (int option * thm) val available_provers : Proof.context -> unit val kill_provers : unit -> unit val running_provers : unit -> unit @@ -102,11 +102,16 @@ "Async_Manager". *) val das_Tool = "Sledgehammer" +val unremotify = perhaps (try (unprefix remote_prefix)) + +val select_smt_solver = + Context.proof_map o SMT_Config.select_solver o unremotify + fun is_smt_prover ctxt name = let val smts = SMT_Solver.available_solvers_of ctxt in case try (unprefix remote_prefix) name of - SOME suffix => member (op =) smts suffix andalso - SMT_Solver.is_remotely_available ctxt suffix + SOME base => member (op =) smts base andalso + SMT_Solver.is_remotely_available ctxt base | NONE => member (op =) smts name end @@ -133,8 +138,7 @@ fun default_max_relevant_for_prover ctxt name = let val thy = ProofContext.theory_of ctxt in if is_smt_prover ctxt name then - SMT_Solver.default_max_relevant ctxt - (perhaps (try (unprefix remote_prefix)) name) + SMT_Solver.default_max_relevant ctxt (unremotify name) else #default_max_relevant (get_atp thy name) end @@ -146,9 +150,11 @@ @{const_name conj}, @{const_name disj}, @{const_name implies}, @{const_name HOL.eq}, @{const_name If}, @{const_name Let}] -fun is_built_in_const_for_prover ctxt name (s, T) args = - if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args - else member (op =) atp_irrelevant_consts s +fun is_built_in_const_for_prover ctxt name = + if is_smt_prover ctxt name then + ctxt |> select_smt_solver name |> SMT_Builtin.is_builtin_ext + else + K o member (op =) atp_irrelevant_consts o fst (* FUDGE *) val atp_relevance_fudge = @@ -230,14 +236,17 @@ datatype prover_fact = Untranslated_Fact of (string * locality) * thm | - ATP_Translated_Fact of translated_formula option * ((string * locality) * thm) + ATP_Translated_Fact of + translated_formula option * ((string * locality) * thm) | + SMT_Weighted_Fact of (string * locality) * (int option * thm) type prover_problem = {state: Proof.state, goal: thm, subgoal: int, subgoal_count: int, - facts: prover_fact list} + facts: prover_fact list, + smt_head: (string * locality) SMT_Solver.smt_filter_head_result option} type prover_result = {outcome: failure option, @@ -272,8 +281,12 @@ fun untranslated_fact (Untranslated_Fact p) = p | untranslated_fact (ATP_Translated_Fact (_, p)) = p -fun atp_translated_fact ctxt (Untranslated_Fact p) = translate_atp_fact ctxt p - | atp_translated_fact _ (ATP_Translated_Fact q) = q + | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th) +fun atp_translated_fact _ (ATP_Translated_Fact p) = p + | atp_translated_fact ctxt fact = + translate_atp_fact ctxt (untranslated_fact fact) +fun smt_weighted_fact (SMT_Weighted_Fact p) = p + | smt_weighted_fact fact = untranslated_fact fact |> apsnd (pair NONE) fun int_opt_add (SOME m) (SOME n) = SOME (m + n) | int_opt_add _ _ = NONE @@ -442,7 +455,8 @@ (12, InternalError), (13, InternalError)] val z3_failures = - [(103, MalformedInput), + [(101, OutOfResources), + (103, MalformedInput), (110, MalformedInput)] val unix_failures = [(139, Crashed)] @@ -470,9 +484,26 @@ val smt_iter_min_msecs = Unsynchronized.ref 5000 val smt_monomorph_limit = Unsynchronized.ref 4 -fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i = +fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params) + state i smt_head = let val ctxt = Proof.context_of state + val (remote, base) = + case try (unprefix remote_prefix) name of + SOME base => (true, base) + | NONE => (false, name) + val repair_context = + select_smt_solver base + #> Config.put SMT_Config.verbose debug + #> (if overlord then + Config.put SMT_Config.debug_files + (overlord_file_location_for_prover name + |> (fn (path, base) => path ^ "/" ^ base)) + else + I) + #> Config.put SMT_Config.monomorph_limit (!smt_monomorph_limit) + val state = state |> Proof.map_context repair_context + fun iter timeout iter_num outcome0 time_so_far facts = let val timer = Timer.startRealTimer () @@ -497,8 +528,11 @@ val _ = if debug then Output.urgent_message "Invoking SMT solver..." else () val (outcome, used_facts) = - SMT_Solver.smt_filter remote iter_timeout state facts i - |> (fn {outcome, used_facts, ...} => (outcome, used_facts)) + (case (iter_num, smt_head) of + (1, SOME head) => head |> apsnd (apfst (apsnd repair_context)) + | _ => SMT_Solver.smt_filter_head state facts i) + |> SMT_Solver.smt_filter_tail iter_timeout remote + |> (fn {outcome, used_facts} => (outcome, used_facts)) handle exn => if Exn.is_interrupt exn then reraise exn else @@ -563,53 +597,14 @@ (Config.put Metis_Tactics.verbose debug #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i -val smt_weights = Unsynchronized.ref true -val smt_weight_min_facts = 20 - -(* FUDGE *) -val smt_min_weight = Unsynchronized.ref 0 -val smt_max_weight = Unsynchronized.ref 10 -val smt_max_index = Unsynchronized.ref 200 -val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x) - -fun smt_fact_weight j num_facts = - if !smt_weights andalso num_facts >= smt_weight_min_facts then - SOME (!smt_max_weight - - (!smt_max_weight - !smt_min_weight + 1) - * !smt_weight_curve (Int.max (0, !smt_max_index - j - 1)) - div !smt_weight_curve (!smt_max_index)) - else - NONE - -fun run_smt_solver auto name (params as {debug, verbose, overlord, ...}) - minimize_command - ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = +fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command + ({state, subgoal, subgoal_count, facts, smt_head, ...} + : prover_problem) = let - val (remote, suffix) = - case try (unprefix remote_prefix) name of - SOME suffix => (true, suffix) - | NONE => (false, name) - val repair_context = - Context.proof_map (SMT_Config.select_solver suffix) - #> Config.put SMT_Config.verbose debug - #> (if overlord then - Config.put SMT_Config.debug_files - (overlord_file_location_for_prover name - |> (fn (path, base) => path ^ "/" ^ base)) - else - I) - #> Config.put SMT_Config.monomorph_limit (!smt_monomorph_limit) - val state = state |> Proof.map_context repair_context - val thy = Proof.theory_of state - val num_facts = length facts - val facts = - facts ~~ (0 upto num_facts - 1) - |> map (fn (fact, j) => - fact |> untranslated_fact - |> apsnd (pair (smt_fact_weight j num_facts) - o Thm.transfer thy)) + val ctxt = Proof.context_of state + val facts = facts |> map smt_weighted_fact val {outcome, used_facts, run_time_in_msecs} = - smt_filter_loop params remote state subgoal facts + smt_filter_loop name params state subgoal smt_head facts val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) val outcome = outcome |> Option.map failure_from_smt_failure val message = @@ -620,8 +615,10 @@ if can_apply_metis debug state subgoal (map snd used_facts) then ("metis", "") else - ("smt", if suffix = SMT_Config.solver_of @{context} then "" - else "smt_solver = " ^ maybe_quote suffix) + let val base = unremotify name in + ("smt", if base = SMT_Config.solver_of ctxt then "" + else "smt_solver = " ^ maybe_quote base) + end in try_command_line (proof_banner auto) (apply_on_subgoal settings subgoal subgoal_count ^ diff -r 975db7bd23e3 -r 7c05c8301d7e src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 15:30:00 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 16:45:31 2010 +0100 @@ -43,7 +43,7 @@ fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...}) auto minimize_command only - {state, goal, subgoal, subgoal_count, facts} name = + {state, goal, subgoal, subgoal_count, facts, smt_head} name = let val ctxt = Proof.context_of state val birth_time = Time.now () @@ -56,7 +56,8 @@ val prover = get_prover ctxt auto name val problem = {state = state, goal = goal, subgoal = subgoal, - subgoal_count = subgoal_count, facts = take num_facts facts} + subgoal_count = subgoal_count, facts = take num_facts facts, + smt_head = smt_head} fun go () = let fun really_go () = @@ -115,6 +116,36 @@ (false, state)) end +val smt_weights = Unsynchronized.ref true +val smt_weight_min_facts = 20 + +(* FUDGE *) +val smt_min_weight = Unsynchronized.ref 0 +val smt_max_weight = Unsynchronized.ref 10 +val smt_max_index = Unsynchronized.ref 200 +val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x) + +fun smt_fact_weight j num_facts = + if !smt_weights andalso num_facts >= smt_weight_min_facts then + SOME (!smt_max_weight + - (!smt_max_weight - !smt_min_weight + 1) + * !smt_weight_curve (Int.max (0, !smt_max_index - j - 1)) + div !smt_weight_curve (!smt_max_index)) + else + NONE + +fun weight_smt_fact thy num_facts (fact, j) = + fact |> apsnd (pair (smt_fact_weight j num_facts) o Thm.transfer thy) + +fun class_of_smt_solver ctxt name = + ctxt |> select_smt_solver name + |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class + +(* Makes backtraces more transparent and might be more efficient as well. *) +fun smart_par_list_map _ [] = [] + | smart_par_list_map f [x] = [f x] + | smart_par_list_map f xs = Par_List.map f xs + (* FUDGE *) val auto_max_relevant_divisor = 2 @@ -129,7 +160,10 @@ | n => let val _ = Proof.assert_backward state + val state = + state |> Proof.map_context (Config.put SMT_Config.verbose debug) val ctxt = Proof.context_of state + val thy = ProofContext.theory_of ctxt 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 @@ -139,60 +173,83 @@ | NONE => () val _ = if auto then () else Output.urgent_message "Sledgehammering..." val (smts, atps) = provers |> List.partition (is_smt_prover ctxt) - fun run_provers label no_dangerous_types relevance_fudge maybe_translate - provers (res as (success, state)) = + fun run_provers get_facts translate maybe_smt_head provers + (res as (success, state)) = if success orelse null provers then res else let - val max_max_relevant = - case max_relevant of - SOME n => n - | NONE => - 0 |> fold (Integer.max o default_max_relevant_for_prover ctxt) - provers - |> auto ? (fn n => n div auto_max_relevant_divisor) - val is_built_in_const = - is_built_in_const_for_prover ctxt (hd provers) - val facts = - relevant_facts ctxt no_dangerous_types relevance_thresholds - max_max_relevant is_built_in_const relevance_fudge - relevance_override chained_ths hyp_ts concl_t - |> map maybe_translate + val facts = get_facts () + val num_facts = length facts + val facts = facts ~~ (0 upto num_facts - 1) + |> map (translate num_facts) val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - facts = facts} + facts = facts, + smt_head = maybe_smt_head (map smt_weighted_fact facts) i} val run_prover = run_prover params auto minimize_command only in - if debug then - Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^ - (if null facts then - "Found no relevant facts." - else - "Including (up to) " ^ string_of_int (length facts) ^ - " relevant fact" ^ plural_s (length facts) ^ ":\n" ^ - (facts |> map (fst o fst o untranslated_fact) - |> space_implode " ") ^ ".")) - else - (); if auto then fold (fn prover => fn (true, state) => (true, state) | (false, _) => run_prover problem prover) provers (false, state) else provers - |> (if blocking andalso length provers > 1 then Par_List.map - else map) + |> (if blocking then smart_par_list_map else map) (run_prover problem) |> exists fst |> rpair state end + fun get_facts label no_dangerous_types relevance_fudge provers = + let + val max_max_relevant = + case max_relevant of + SOME n => n + | NONE => + 0 |> fold (Integer.max o default_max_relevant_for_prover ctxt) + provers + |> auto ? (fn n => n div auto_max_relevant_divisor) + val is_built_in_const = + is_built_in_const_for_prover ctxt (hd provers) + in + relevant_facts ctxt no_dangerous_types relevance_thresholds + max_max_relevant is_built_in_const relevance_fudge + relevance_override chained_ths hyp_ts concl_t + |> tap (fn facts => + if debug then + label ^ plural_s (length provers) ^ ": " ^ + (if null facts then + "Found no relevant facts." + else + "Including (up to) " ^ string_of_int (length facts) ^ + " relevant fact" ^ plural_s (length facts) ^ ":\n" ^ + (facts |> map (fst o fst) |> space_implode " ") ^ ".") + |> Output.urgent_message + else + ()) + end val run_atps = - run_provers "ATP" no_dangerous_types atp_relevance_fudge - (ATP_Translated_Fact o translate_atp_fact ctxt) atps - val run_smts = - run_provers "SMT solver" true smt_relevance_fudge Untranslated_Fact smts + run_provers + (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps) + (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst)) + (K (K NONE)) atps + fun run_smts (accum as (success, _)) = + if success orelse null smts then + accum + else + let + val facts = get_facts "SMT solver" true smt_relevance_fudge smts + val translate = SMT_Weighted_Fact oo weight_smt_fact thy + val maybe_smt_head = try o SMT_Solver.smt_filter_head state + in + smts |> map (`(class_of_smt_solver ctxt)) + |> AList.group (op =) + |> map (fn (_, smts) => run_provers (K facts) translate + maybe_smt_head smts accum) + |> exists fst |> rpair state + end fun run_atps_and_smt_solvers () = - [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ()) + [run_atps, run_smts] + |> smart_par_list_map (fn f => f (false, state) |> K ()) handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg) in (false, state)