--- 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."
--- 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 =>
--- 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