169 Pretty.indent indent_size (Pretty.chunks |
169 Pretty.indent indent_size (Pretty.chunks |
170 (map2 (fn j => fn t => |
170 (map2 (fn j => fn t => |
171 Pretty.block [t |> shorten_names_in_term |
171 Pretty.block [t |> shorten_names_in_term |
172 |> Syntax.pretty_term ctxt]) |
172 |> Syntax.pretty_term ctxt]) |
173 (length ts downto 1) ts))] |
173 (length ts downto 1) ts))] |
174 |
|
175 val isabelle_wrong_message = |
|
176 "something appears to be wrong with your Isabelle installation" |
|
177 val java_not_found_message = |
|
178 "Java could not be launched -- " ^ isabelle_wrong_message |
|
179 |
174 |
180 val max_unsound_delay_ms = 200 |
175 val max_unsound_delay_ms = 200 |
181 val max_unsound_delay_percent = 2 |
176 val max_unsound_delay_percent = 2 |
182 |
177 |
183 fun unsound_delay_for_timeout timeout = |
178 fun unsound_delay_for_timeout timeout = |
709 if max_solutions <= 0 then |
704 if max_solutions <= 0 then |
710 (found_really_genuine, 0, 0, donno) |
705 (found_really_genuine, 0, 0, donno) |
711 else |
706 else |
712 case KK.solve_any_problem debug overlord deadline max_threads |
707 case KK.solve_any_problem debug overlord deadline max_threads |
713 max_solutions (map fst problems) of |
708 max_solutions (map fst problems) of |
714 KK.JavaNotFound => |
709 KK.Normal ([], unsat_js, s) => |
715 (print_nt (K java_not_found_message); |
|
716 (found_really_genuine, max_potential, max_genuine, donno + 1)) |
|
717 | KK.Normal ([], unsat_js, s) => |
|
718 (update_checked_problems problems unsat_js; show_kodkod_warning s; |
710 (update_checked_problems problems unsat_js; show_kodkod_warning s; |
719 (found_really_genuine, max_potential, max_genuine, donno)) |
711 (found_really_genuine, max_potential, max_genuine, donno)) |
720 | KK.Normal (sat_ps, unsat_js, s) => |
712 | KK.Normal (sat_ps, unsat_js, s) => |
721 let |
713 let |
722 val (lib_ps, con_ps) = |
714 val (lib_ps, con_ps) = |