equal
deleted
inserted
replaced
231 *) |
231 *) |
232 val print_m = pprint_m o K o plazy |
232 val print_m = pprint_m o K o plazy |
233 val print_v = pprint_v o K o plazy |
233 val print_v = pprint_v o K o plazy |
234 |
234 |
235 fun check_deadline () = |
235 fun check_deadline () = |
236 if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut |
236 if passed_deadline deadline then raise TimeLimit.TimeOut else () |
237 else () |
|
238 |
237 |
239 val assm_ts = if assms orelse auto then assm_ts else [] |
238 val assm_ts = if assms orelse auto then assm_ts else [] |
240 val _ = |
239 val _ = |
241 if step = 0 then |
240 if step = 0 then |
242 print_m (fn () => "Nitpicking formula...") |
241 print_m (fn () => "Nitpicking formula...") |
979 val _ = print_v (fn () => |
978 val _ = print_v (fn () => |
980 "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^ |
979 "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^ |
981 ".") |
980 ".") |
982 in (outcome_code, !state_ref) end |
981 in (outcome_code, !state_ref) end |
983 |
982 |
|
983 (* Give the inner timeout a chance. *) |
|
984 val timeout_bonus = seconds 0.25 |
|
985 |
984 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n |
986 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n |
985 step subst assm_ts orig_t = |
987 step subst assm_ts orig_t = |
986 let val warning_m = if auto then K () else warning in |
988 let val warning_m = if auto then K () else warning in |
987 if getenv "KODKODI" = "" then |
989 if getenv "KODKODI" = "" then |
988 (* The "expect" argument is deliberately ignored if Kodkodi is missing so |
990 (* The "expect" argument is deliberately ignored if Kodkodi is missing so |
992 else |
994 else |
993 let |
995 let |
994 val unknown_outcome = ("unknown", state) |
996 val unknown_outcome = ("unknown", state) |
995 val deadline = Option.map (curry Time.+ (Time.now ())) timeout |
997 val deadline = Option.map (curry Time.+ (Time.now ())) timeout |
996 val outcome as (outcome_code, _) = |
998 val outcome as (outcome_code, _) = |
997 time_limit (if debug then NONE else timeout) |
999 time_limit (if debug orelse is_none timeout then NONE |
|
1000 else SOME (Time.+ (the timeout, timeout_bonus))) |
998 (pick_them_nits_in_term deadline state params auto i n step subst |
1001 (pick_them_nits_in_term deadline state params auto i n step subst |
999 assm_ts) orig_t |
1002 assm_ts) orig_t |
1000 handle TOO_LARGE (_, details) => |
1003 handle TOO_LARGE (_, details) => |
1001 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome) |
1004 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome) |
1002 | TOO_SMALL (_, details) => |
1005 | TOO_SMALL (_, details) => |