903 | n => |
903 | n => |
904 scope_count (do_filter (these (!checked_problems))) |
904 scope_count (do_filter (these (!checked_problems))) |
905 scope = n |
905 scope = n |
906 ? Integer.add 1) (!generated_scopes) 0 |
906 ? Integer.add 1) (!generated_scopes) 0 |
907 in |
907 in |
908 (if mode = TPTP then "% SZS status Unknown\n" else "") ^ |
908 (if mode = TPTP then "% SZS status GaveUp\n" else "") ^ |
909 "Nitpick " ^ did_so_and_so ^ |
909 "Nitpick " ^ did_so_and_so ^ |
910 (if is_some (!checked_problems) andalso total > 0 then |
910 (if is_some (!checked_problems) andalso total > 0 then |
911 " " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope" |
911 " " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope" |
912 ^ plural_s total |
912 ^ plural_s total |
913 else |
913 else |
932 (found_really_genuine, max_potential, max_genuine, donno) = |
932 (found_really_genuine, max_potential, max_genuine, donno) = |
933 if donno > 0 andalso max_genuine > 0 then |
933 if donno > 0 andalso max_genuine > 0 then |
934 (print_nt (fn () => excipit "checked"); unknownN) |
934 (print_nt (fn () => excipit "checked"); unknownN) |
935 else if max_genuine = original_max_genuine then |
935 else if max_genuine = original_max_genuine then |
936 if max_potential = original_max_potential then |
936 if max_potential = original_max_potential then |
937 (print_t (K "% SZS status Unknown"); |
937 (print_t (K "% SZS status GaveUp"); |
938 print_nt (fn () => "Nitpick found no " ^ das_wort_model ^ "."); |
938 print_nt (fn () => "Nitpick found no " ^ das_wort_model ^ "."); |
939 if skipped > 0 then unknownN else noneN) |
939 if skipped > 0 then unknownN else noneN) |
940 else |
940 else |
941 (print_nt (fn () => |
941 (print_nt (fn () => |
942 excipit ("could not find a" ^ |
942 excipit ("could not find a" ^ |
989 val outcome as (outcome_code, _) = |
989 val outcome as (outcome_code, _) = |
990 TimeLimit.timeLimit (Time.+ (timeout, timeout_bonus)) |
990 TimeLimit.timeLimit (Time.+ (timeout, timeout_bonus)) |
991 (pick_them_nits_in_term deadline state params mode i n step subst |
991 (pick_them_nits_in_term deadline state params mode i n step subst |
992 def_assm_ts nondef_assm_ts) orig_t |
992 def_assm_ts nondef_assm_ts) orig_t |
993 handle TOO_LARGE (_, details) => |
993 handle TOO_LARGE (_, details) => |
994 (print_t "% SZS status Unknown"; |
994 (print_t "% SZS status GaveUp"; |
995 print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome) |
995 print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome) |
996 | TOO_SMALL (_, details) => |
996 | TOO_SMALL (_, details) => |
997 (print_t "% SZS status Unknown"; |
997 (print_t "% SZS status GaveUp"; |
998 print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome) |
998 print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome) |
999 | Kodkod.SYNTAX (_, details) => |
999 | Kodkod.SYNTAX (_, details) => |
1000 (print_t "% SZS status Unknown"; |
1000 (print_t "% SZS status GaveUp"; |
1001 print_nt ("Malformed Kodkodi output: " ^ details ^ "."); |
1001 print_nt ("Malformed Kodkodi output: " ^ details ^ "."); |
1002 unknown_outcome) |
1002 unknown_outcome) |
1003 | TimeLimit.TimeOut => |
1003 | TimeLimit.TimeOut => |
1004 (print_t "% SZS status TimedOut"; |
1004 (print_t "% SZS status TimedOut"; |
1005 print_nt "Nitpick ran out of time."; unknown_outcome) |
1005 print_nt "Nitpick ran out of time."; unknown_outcome) |