# HG changeset patch # User blanchet # Date 1289843789 -3600 # Node ID 1264c91723386c23980e22d7b30a2e9e7f4231a7 # Parent 4d48ec261d018cf1120f24241ea3de98e170abc1 pick up SMT solver crashes and report them to the user/Mirabelle if desired diff -r 4d48ec261d01 -r 1264c9172338 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Mon Nov 15 18:04:04 2010 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Nov 15 18:56:29 2010 +0100 @@ -14,7 +14,7 @@ datatype failure = Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | - MalformedInput | MalformedOutput | Interrupted | InternalError | + MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError | UnknownError type step_name = string * string option @@ -48,7 +48,7 @@ datatype failure = Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput | - MalformedOutput | Interrupted | InternalError | UnknownError + MalformedOutput | Interrupted | Crashed | InternalError | UnknownError fun strip_spaces_in_list _ [] = [] | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1] @@ -102,6 +102,7 @@ \developers." | string_for_failure MalformedOutput = "The ATP output is malformed." | string_for_failure Interrupted = "The ATP was interrupted." + | string_for_failure Crashed = "The ATP crashed." | string_for_failure InternalError = "An internal ATP error occurred." | string_for_failure UnknownError = "An unknown ATP error occurred." diff -r 4d48ec261d01 -r 1264c9172338 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 15 18:04:04 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 15 18:56:29 2010 +0100 @@ -411,57 +411,83 @@ fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut + | failure_from_smt_failure (SMT_Failure.Solver_Crashed _) = Crashed | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources | failure_from_smt_failure _ = UnknownError -val smt_max_iter = 5 +val smt_max_iter = 8 val smt_iter_fact_divisor = 2 val smt_iter_min_msecs = 5000 val smt_iter_timeout_divisor = 2 val smt_monomorph_limit = 4 -fun smt_filter_loop iter outcome0 msecs_so_far remote timeout state facts i = +fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i = let - val timer = Timer.startRealTimer () - val ms = timeout |> Time.toMilliseconds - val iter_timeout = - if iter < smt_max_iter then - Int.min (ms, Int.max (smt_iter_min_msecs, - ms div smt_iter_timeout_divisor)) - |> Time.fromMilliseconds - else - timeout - 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} - val outcome0 = if is_none outcome0 then SOME outcome else outcome0 - val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far - val too_many_facts_perhaps = - case outcome of - NONE => false - | SOME (SMT_Failure.Counterexample _) => false - | SOME SMT_Failure.Time_Out => iter_timeout <> timeout - | SOME SMT_Failure.Out_Of_Memory => true - | SOME _ => true - val timeout = Time.- (timeout, Timer.checkRealTimer timer) - in - if too_many_facts_perhaps andalso iter < smt_max_iter andalso - not (null facts) andalso Time.> (timeout, Time.zeroTime) then - let val facts = take (length facts div smt_iter_fact_divisor) facts in - smt_filter_loop (iter + 1) outcome0 msecs_so_far remote timeout state - facts i + val ctxt = Proof.context_of state + fun iter timeout iter_num outcome0 msecs_so_far facts = + let + val timer = Timer.startRealTimer () + val ms = timeout |> Time.toMilliseconds + val iter_timeout = + if iter_num < smt_max_iter then + Int.min (ms, Int.max (smt_iter_min_msecs, + ms div smt_iter_timeout_divisor)) + |> 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 ^ + "..." + |> Output.urgent_message + 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} + val _ = + if verbose andalso is_some outcome then + "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome) + |> Output.urgent_message + else + () + val outcome0 = if is_none outcome0 then SOME outcome else outcome0 + val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far + val too_many_facts_perhaps = + case outcome of + NONE => false + | SOME (SMT_Failure.Counterexample _) => false + | SOME SMT_Failure.Time_Out => iter_timeout <> timeout + | SOME (SMT_Failure.Solver_Crashed _) => + (if verbose then + "The SMT solver crashed with " ^ string_of_int num_facts ^ + " fact" ^ plural_s num_facts ^ "." + |> (if debug then error else warning) + else + (); + true (* kind of *)) + | SOME SMT_Failure.Out_Of_Memory => true + | SOME _ => true + val timeout = Time.- (timeout, Timer.checkRealTimer timer) + in + if too_many_facts_perhaps andalso iter_num < smt_max_iter andalso + num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then + let val facts = take (num_facts div smt_iter_fact_divisor) facts in + iter timeout (iter_num + 1) outcome0 msecs_so_far facts + end + else + {outcome = if is_none outcome then NONE else the outcome0, + used_facts = used_facts, run_time_in_msecs = msecs_so_far} end - else - {outcome = if is_none outcome then NONE else the outcome0, - used_facts = used_facts, run_time_in_msecs = msecs_so_far} - end + in iter timeout 1 NONE (SOME 0) end -fun run_smt_solver auto remote ({debug, timeout, ...} : params) minimize_command - ({state, subgoal, subgoal_count, facts, ...} - : prover_problem) = +fun run_smt_solver auto remote (params as {debug, ...}) minimize_command + ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = let val repair_context = Config.put SMT_Config.verbose debug @@ -469,8 +495,8 @@ val state = state |> Proof.map_context repair_context val ctxt = Proof.context_of state val {outcome, used_facts, run_time_in_msecs} = - smt_filter_loop 1 NONE (SOME 0) remote timeout state - (map_filter (try dest_Untranslated) facts) subgoal + smt_filter_loop params remote state subgoal + (map_filter (try dest_Untranslated) facts) val message = case outcome of NONE => diff -r 4d48ec261d01 -r 1264c9172338 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Nov 15 18:04:04 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Nov 15 18:56:29 2010 +0100 @@ -27,10 +27,10 @@ (* wrapper for calling external prover *) -fun string_for_failure Unprovable = "Unprovable." - | string_for_failure TimedOut = "Timed out." - | string_for_failure Interrupted = "Interrupted." - | string_for_failure _ = "Unknown error." +fun string_for_failure ATP_Proof.Unprovable = "Unprovable." + | string_for_failure ATP_Proof.TimedOut = "Timed out." + | string_for_failure ATP_Proof.Interrupted = "Interrupted." + | string_for_failure _ = "Error." fun n_facts names = let val n = length names in